Theorem: swap_joins (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
⊢ joins R x y → joins R y x
Tactic:
intros joins
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
joins : _root_.joins R x y
⊢ _root_.joins R y x

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
joins : _root_.joins R x y
⊢ _root_.joins R y x
Tactic:
cases' joins with z h
State after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
h : refl_trans_clos R x z ∧ refl_trans_clos R y z
⊢ joins R y x

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

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