Theorem: MyNat.and_trans (TheoremProvingLean/inductive_types.lean)

State before:
P Q R : Prop
⊢ P ∧ Q → Q ∧ R → P ∧ R
Tactic:
intro hpq hqr
State after:
P Q R : Prop
hpq : P ∧ Q
hqr : Q ∧ R
⊢ P ∧ R

State before:
P Q R : Prop
hpq : P ∧ Q
hqr : Q ∧ R
⊢ P ∧ R
Tactic:
exact ⟨hpq.left, hqr.right⟩
State after:
no goals