Theorem: semi_confluent_implies_confluent (Traat/chapter1.lean)

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

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

State before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y w : A
h : refl_trans_clos R w x ∧ refl_trans_clos R w y
⊢ joins R x y
Tactic:
cases' h with h1 h2
State after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ joins R x y

State before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ joins R x y
Tactic:
revert h2 y
State after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w : A
h1 : refl_trans_clos R w x
⊢ ∀ (y : A), refl_trans_clos R w y → joins R x y

State before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w : A
h1 : refl_trans_clos R w x
⊢ ∀ (y : A), refl_trans_clos R w y → joins R x y
Tactic:
induction' h1 with z x y y' red_x_y _red_y_y' ih <;> intros z red_x_z
State after:
case intro.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w z✝ z : A
red_x_z : refl_trans_clos R z✝ z
⊢ joins R z✝ z

case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
⊢ joins R y' z

State before:
case intro.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w z✝ z : A
red_x_z : refl_trans_clos R z✝ z
⊢ joins R z✝ z

case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
⊢ joins R y' z
Tactic:
. exists z; aesop
State after:
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
⊢ joins R y' z

State before:
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
⊢ joins R y' z
Tactic:
. have h := semi x y z red_x_y red_x_z
  cases' h with z' h
  cases' h with h1 h2
  have ih := ih z' h1
  apply reds_joins_right <;> trivial
State after:
no goals

State before:
case intro.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w z✝ z : A
red_x_z : refl_trans_clos R z✝ z
⊢ joins R z✝ z
Tactic:
exists z
State after:
case intro.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w z✝ z : A
red_x_z : refl_trans_clos R z✝ z
⊢ refl_trans_clos R z✝ z ∧ refl_trans_clos R z z

State before:
case intro.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x w z✝ z : A
red_x_z : refl_trans_clos R z✝ z
⊢ refl_trans_clos R z✝ z ∧ refl_trans_clos R z z
Tactic:
aesop
State after:
no goals

State before:
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
⊢ joins R y' z
Tactic:
have h := semi x y z red_x_y red_x_z
State after:
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
h : joins R y z
⊢ joins R y' z

State before:
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
h : joins R y z
⊢ joins R y' z
Tactic:
cases' h with z' h
State after:
case intro.intro.step.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h : refl_trans_clos R y z' ∧ refl_trans_clos R z z'
⊢ joins R y' z

State before:
case intro.intro.step.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h : refl_trans_clos R y z' ∧ refl_trans_clos R z z'
⊢ joins R y' z
Tactic:
cases' h with h1 h2
State after:
case intro.intro.step.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h1 : refl_trans_clos R y z'
h2 : refl_trans_clos R z z'
⊢ joins R y' z

State before:
case intro.intro.step.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h1 : refl_trans_clos R y z'
h2 : refl_trans_clos R z z'
⊢ joins R y' z
Tactic:
have ih := ih z' h1
State after:
case intro.intro.step.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih✝ : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h1 : refl_trans_clos R y z'
h2 : refl_trans_clos R z z'
ih : joins R y' z'
⊢ joins R y' z

State before:
case intro.intro.step.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih✝ : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
z' : A
h1 : refl_trans_clos R y z'
h2 : refl_trans_clos R z z'
ih : joins R y' z'
⊢ joins R y' z
Tactic:
apply reds_joins_right <;> trivial
State after:
no goals