Theorem: Lean4Axiomatic.Logic.and_mapL (Lean4Axiomatic/Logic.lean)

State before:
p₁ p₂ q : Prop
f : p₁ → p₂
⊢ p₁ ∧ q → p₂ ∧ q
Tactic:
intro (And.intro (_ : p₁) (_ : q))
State after:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : p₁
right✝ : q
⊢ p₂ ∧ q

State before:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : p₁
right✝ : q
⊢ p₂ ∧ q
Tactic:
have : p₂ := f ‹p₁›
State after:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : p₁
right✝ : q
this : p₂
⊢ p₂ ∧ q

State before:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : p₁
right✝ : q
this : p₂
⊢ p₂ ∧ q
Tactic:
exact And.intro ‹p₂› ‹q›
State after:
no goals