Theorem: red_joins (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
⊢ 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 : 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 : R x y
joins_y_z : joins R y z
⊢ joins R x z
Tactic:
cases' joins_y_z with w h
State after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
h : refl_trans_clos R y w ∧ refl_trans_clos R z w
⊢ joins R x z

State before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
h : refl_trans_clos R y w ∧ refl_trans_clos R z w
⊢ joins R x z
Tactic:
cases h
State after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ joins R x z

State before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ joins R x z
Tactic:
exists w
State after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w

State before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
left✝ : refl_trans_clos R y w
right✝ : refl_trans_clos R z w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w
Tactic:
aesop
State after:
no goals