Can you retain orignal when introducing variables?

Stream: general

[Assar Lannerborn]

When introducing variables, is there a way to keep the orignal without loosing it? I vaguely recall someone addressing this. when i consult Gemini it hallucinates up something using the @ symbol, the following:

example {A B C : Prop} : A ∧ B → C := by
  -- Retain 'h' as the whole proof of (A ∧ B),
  -- and break it into 'ha' and 'hb'
  rintro h@⟨ha, hb⟩

  -- Context now has:
  -- h : A ∧ B
  -- ha : A
  -- hb : B
  exact (fun _ => C) -- (dummy proof to finish)

However it doesn't work with error:

Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

A B C : Prop
h : A ∧ B
⊢ CLean 4

Is there a way to do this? Any help would be appreciated :smiley:

[Jakub Nowak]

example {A B C : Prop} : A ∧ B → C := by
  intro h
  have ⟨ha, hb⟩ := h

[Jakub Nowak]

The syntax with @ is from Haskell iirc, maybe that's where it hallucinated it from.

[Jakub Nowak]

Ah, no, we have that syntax with match too. So this works too:

example {A B C : Prop} : A ∧ B → C
| h@⟨ha, hb⟩ => by
  sorry

[Assar Lannerborn]

Ahh thank you. Yes Gemini seemed very sure that it was a thing but nothing showed up when i googled. :grinning: