include, omit

[digama0]

include h
omit h

These lean 3 commands can be used to change inclusion behavior of variables, and there is currently no lean 4 analogue.

[dwrensha]

Do you have an example where include is actually needed? The example from Theorem Proving in Lean seems to do fine without it:

-- Lean 3
section
variables (x y z : ℕ)
variables (h₁ : x = y) (h₂ : y = z)

include h₁ h₂
theorem foo : x = z :=
begin
  rw [h₁, h₂]
end
omit h₁ h₂

theorem bar : x = z :=
eq.trans h₁ h₂

theorem baz : x = x := rfl

#check @foo
#check @bar
#check @baz
end

-- Lean 4
section
variable (x y z : Nat)
variable (h₁ : x = y) (h₂ : y = z)

theorem foo : x = z :=
by rw [h₁, h₂]

theorem bar : x = z :=
Eq.trans h₁ h₂

theorem baz : x = x := rfl

#check @foo
#check @bar
#check @baz
end

(I'm on leanprover/lean4:nightly-2021-07-11.)

[digama0]

That speaks well for the porting strategy that just deletes them. It does still have an effect, e.g. if you include a variable that is not used in the theorem deliberately, but the main reason it is used in lean 3 is to get variables to be visible in tactics, and as you say that's not a problem anymore.

[dselsam]

Here is an infrequent but recurring situation where include would be nice to have. It is currently hard to make unsafe def fooUnsafe and @[implementedBy] constant foo have the same type when there are a lot of variables, because the instances used in the body of fooUnsafe won't be added to the type of foo.