Theorem: reds_joins_right (Traat/chapter1.lean)

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

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

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_y : refl_trans_clos R x z
joins_y_z : joins R y z
⊢ joins R x y
Tactic:
have joins_z_y := swap_joins _ joins_y_z
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_y : refl_trans_clos R x z
joins_y_z : joins R y z
joins_z_y : joins R z y
⊢ joins R x y

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x z y : A
red_x_y : refl_trans_clos R x z
joins_y_z : joins R y z
joins_z_y : joins R z y
⊢ joins R x y
Tactic:
apply (reds_joins_left _) <;> trivial
State after:
no goals