Theorem: confluent_implies_weakly_confluent (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ confluent R → weakly_confluent R
Tactic:
intros confl x y z red_x_y red_x_z
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ joins R y z

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ joins R y z
Tactic:
apply confl
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ wedge R y z

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ wedge R y z
Tactic:
exists x
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ refl_trans_clos R x y ∧ refl_trans_clos R x z

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ refl_trans_clos R x y ∧ refl_trans_clos R x z
Tactic:
constructor <;> apply refl_trans_clos.step <;> try constructor
State after:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x y

case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x z

State before:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x y

case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x z
Tactic:
. trivial
State after:
case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x z

State before:
case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x z
Tactic:
. trivial
State after:
no goals

State before:
case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ refl_trans_clos R ?a.right.b✝ z
Tactic:
constructor
State after:
no goals

State before:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x y
Tactic:
trivial
State after:
no goals

State before:
case a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ R x z
Tactic:
trivial
State after:
no goals