Override hypothesis

Stream: lean4

[Marcus Rossel]

Is there a canonical way of overriding/shadowing a hypothesis in tactic mode?
That is, if I have a hypothesis h and want to create a new hypothesis which is also called h, how can I make the original h disappear?

[Sebastien Gouezel]

replace h : ...

[Sebastien Gouezel]

oops, sorry, this is Lean 3.

[Henrik Böving]

Lean 4 automatically ensures this behavior, if we have a proof like this:

theorem test : 3 = 3 := by
  have h : 1 = 1 := by rfl
  have h : 2 = 2 := by rfl
  have h : 3 = 3 := by rfl
  exact h

and check the proof state before the exact h

Goals (1)
h¹ : 1 = 1
h : 2 = 2
h : 3 = 3
⊢ 3 = 3

The upper two h's are greyed out (in my emacs that is) and only the last one left accessible as indicated by different highlighting (blue in my case). If you now refer to h further down the line this will always refer to the only h that is left, it is in fact impossible for you to explicitly refer to the first two h's. This is for example also how the intros tactic works, in this proof:

theorem test2 (A B : Prop) : A → B → A ∧ B := by
  intros
  apply And.intro
  assumption
  assumption

intros does introduce two greyed out hypothesis like this:

A B : Prop
a¹ : A
a : B
⊢ A ∧ B

you cannot refer to these names yourself, if you try to for example exact a the first goal the apply And.intro creates, Lean will complain that the identifier does not exist. However the assumption tactic (and tactics in general) do still have access to these anonymous or shadowed hypothesis as shown.

[Marcus Rossel]

Yeah, my problem is just that the inaccessible hypotheses are cluttering up my goal view. So I'd like to not see them at all.

[Gabriel Ebner]

In Lean 3, we had tactic state filters where you could e.g. hide all type class instances. We still need to add them back to the Lean 4 extension: https://github.com/leanprover/vscode-lean4/issues/76