Theorem: confluent'_implies_confluent (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ confluent' R → confluent R
Tactic:
intros conf'
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
⊢ confluent R

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
⊢ confluent R
Tactic:
apply semi_confluent_implies_confluent
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
⊢ semi_confluent R

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
⊢ semi_confluent R
Tactic:
intros x y z red_x_y red_x_z
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
⊢ joins R y z

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
⊢ joins R y z
Tactic:
have h := refl_trans_is_trans_or_eq _ red_x_z
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h : x = z ∨ trans_clos R x z
⊢ joins R y z

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h : x = z ∨ trans_clos R x z
⊢ joins R y z
Tactic:
cases h
State after:
case a.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h✝ : x = z
⊢ joins R y z

case a.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h✝ : trans_clos R x z
⊢ joins R y z

State before:
case a.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h✝ : x = z
⊢ joins R y z

case a.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h✝ : trans_clos R x z
⊢ joins R y z
Tactic:
. case a.inl h =>
  simp [← h]
  exists y; aesop
State after:
case a.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h✝ : trans_clos R x z
⊢ joins R y z

State before:
case a.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h✝ : trans_clos R x z
⊢ joins R y z
Tactic:
. apply conf' <;> aesop
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h : x = z
⊢ joins R y z
Tactic:
case a.inl h =>
simp [← h]
exists y; aesop
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h : x = z
⊢ joins R y z
Tactic:
simp [← h]
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h : x = z
⊢ joins R y x

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h : x = z
⊢ joins R y x
Tactic:
exists y
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h : x = z
⊢ refl_trans_clos R y y ∧ refl_trans_clos R x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h : x = z
⊢ refl_trans_clos R y y ∧ refl_trans_clos R x y
Tactic:
aesop
State after:
no goals

State before:
case a.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h✝ : trans_clos R x z
⊢ joins R y z
Tactic:
apply conf' <;> aesop
State after:
no goals