Theorem: MyNat.iff_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:
constructor
State after:
case mp
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ P → R

case mpr
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ R → P

State before:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ P → R
Tactic:
case mp =>
  intro hp
  exact hqr.mp (hpq.mp hp)
State after:
no goals

State before:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
⊢ R → P
Tactic:
case mpr =>
  intro hr
  cases hqr with
  | intro hqr_mp hqr_mpr =>
    cases hpq with
    | intro hpq_mp hpq_mpr =>
      apply hpq_mpr
      apply hqr_mpr
      exact hr
State after:
no goals

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

State before:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
hp : P
⊢ R
Tactic:
exact hqr.mp (hpq.mp hp)
State after:
no goals

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

State before:
P Q R : Prop
hpq : P ↔ Q
hqr : Q ↔ R
hr : R
⊢ P
Tactic:
cases hqr with
| intro hqr_mp hqr_mpr =>
  cases hpq with
  | intro hpq_mp hpq_mpr =>
    apply hpq_mpr
    apply hqr_mpr
    exact hr
State after:
no goals

State before:
case intro
P Q R : Prop
hpq : P ↔ Q
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
⊢ P
Tactic:
cases hpq with
| intro hpq_mp hpq_mpr =>
  apply hpq_mpr
  apply hqr_mpr
  exact hr
State after:
no goals

State before:
case intro.intro
P Q R : Prop
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
hpq_mp : P → Q
hpq_mpr : Q → P
⊢ P
Tactic:
apply hpq_mpr
State after:
case intro.intro
P Q R : Prop
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
hpq_mp : P → Q
hpq_mpr : Q → P
⊢ Q

State before:
case intro.intro
P Q R : Prop
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
hpq_mp : P → Q
hpq_mpr : Q → P
⊢ Q
Tactic:
apply hqr_mpr
State after:
case intro.intro
P Q R : Prop
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
hpq_mp : P → Q
hpq_mpr : Q → P
⊢ R

State before:
case intro.intro
P Q R : Prop
hr : R
hqr_mp : Q → R
hqr_mpr : R → Q
hpq_mp : P → Q
hpq_mpr : Q → P
⊢ R
Tactic:
exact hr
State after:
no goals