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

State before:
P Q : Prop
⊢ P ∧ Q → Q ∧ P
Tactic:
intro h
State after:
P Q : Prop
h : P ∧ Q
⊢ Q ∧ P

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