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

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

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

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