how to access the proof variable when using cases tactics

Stream: new members

[Praveen Kumar]

case intro
P Q : Prop
left✝ : Q ∧ ((Q ∧ P) ∧ Q) ∧ Q ∧ Q ∧ Q
right✝ : (Q ∧ Q) ∧ Q
⊢ P

when i did cases in lean4 I get these variables in my proof window how to access them ? How to tell lean to rename them so i can access ?

[Kyle Miller]

Could you share a #mwe ?

There are many ways to deal with this, but the advice depends on how you got there.

[Praveen Kumar]

example (P Q : Prop)(h1: (Q ∧ (((Q ∧ P) ∧ Q) ∧ Q ∧ Q ∧ Q)) ∧ (Q ∧ Q) ∧ Q) : P := by
  cases h1

[Praveen Kumar]

Its a proof from the lean game server in logic i can do this nicely there but in my local machine it give me these variables that are not accessible.

[Aaron Liu]

You want

  cases h1 with
  | intro a b =>
    sorry

[Aaron Liu]

the tactic obtain also works for this and I think it's better in this case since you don't have to indent

[Praveen Kumar]

How do I use obtain ? I am still new to this so do mind me asking basic questions

[Praveen Kumar]

In the lean game server tutorial it works very nicely with all this , this seems deceiving since if it works for the game server it should work in my ide

[Robin Arnez]

The lean game server uses unhygienic so names are always accessible. This is fine for teaching but can get really confusing in real proofs. Still, even in the lean game server, all tactics allow specifying names: cases h1 with a b on the lean game server, cases h1 with | _ a b or obtain ⟨a, b⟩ := h1 in actual Lean.

[Praveen Kumar]

Thanks obtain looks clean but in logic part i failed to see it, was it mentioned there ?

[Robin Arnez]

It's not mentioned in the lean game server

[Robin Arnez]

obtain is basically a nicer syntax for rcases which is a recursive version of cases, i.e. you can have recursive patterns like:

example (P Q : Prop) (h1 : (Q ∧ (((Q ∧ P) ∧ Q) ∧ Q ∧ Q ∧ Q)) ∧ (Q ∧ Q) ∧ Q) : P := by
  rcases h1 with ⟨⟨h₁, ⟨⟨⟨h₂, h₃⟩, h₄⟩, ⟨h₅, h₆, h₇⟩⟩⟩, ⟨⟨h₈, h₉⟩, h₁₀⟩⟩

[Praveen Kumar]

can i do cases with the same rcases syntax ?

[Robin Arnez]

Every cases can be converted into an rcases, e.g.

cases h with | _ a b
cases h with | intro a b
cases h with | intro a b => ?_
rcases h with ⟨a, b⟩
obtain ⟨a, b⟩ := h

all do the same thing

[Kyle Miller]

Now that all the structured ways to do it have been mentioned, there's also rename_i a b to rename the last two inaccessible variables to a and b. That's mostly a last resort, or for exploration.