Theorem: reds_joins_left (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
⊢ refl_trans_clos R x y → joins R y z → joins R x z
Tactic:
intros red_x_y joins_y_z
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : refl_trans_clos R x y
joins_y_z : joins R y z
⊢ joins R x z

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : refl_trans_clos R x y
joins_y_z : joins R y z
⊢ joins R x z
Tactic:
induction' red_x_y with _ _ _ _ _ _ ih
State after:
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝ : A
joins_y_z : joins R a✝ z
⊢ joins R a✝ z

case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R a✝² z

State before:
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝ : A
joins_y_z : joins R a✝ z
⊢ joins R a✝ z

case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R a✝² z
Tactic:
. trivial
State after:
case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R a✝² z

State before:
case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R a✝² z
Tactic:
. apply red_joins
  . trivial
  . have h' := ih joins_y_z
    trivial
State after:
no goals

State before:
case refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝ : A
joins_y_z : joins R a✝ z
⊢ joins R a✝ z
Tactic:
trivial
State after:
no goals

State before:
case step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R a✝² z
Tactic:
apply red_joins
State after:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ R a✝² ?step.y

case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R ?step.y z

case step.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ A

State before:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ R a✝² ?step.y

case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R ?step.y z

case step.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ A
Tactic:
. trivial
State after:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R b✝ z

State before:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R b✝ z
Tactic:
. have h' := ih joins_y_z
  trivial
State after:
no goals

State before:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ R a✝² ?step.y
Tactic:
trivial
State after:
no goals

State before:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
⊢ joins R b✝ z
Tactic:
have h' := ih joins_y_z
State after:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
h' : joins R b✝ z
⊢ joins R b✝ z

State before:
case step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
joins_y_z✝ : joins R y z
a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
ih : joins R c✝ z → joins R b✝ z
joins_y_z : joins R c✝ z
h' : joins R b✝ z
⊢ joins R b✝ z
Tactic:
trivial
State after:
no goals