Theorem: conf_trans_clos (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ confluent (refl_trans_clos R) ↔ confluent R
Tactic:
simp [confluent, joins, wedge]
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (y z x : A),
      refl_trans_clos (refl_trans_clos R) x y →
        refl_trans_clos (refl_trans_clos R) x z →
          ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1) ↔
    ∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (y z x : A),
      refl_trans_clos (refl_trans_clos R) x y →
        refl_trans_clos (refl_trans_clos R) x z →
          ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1) ↔
    ∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
Tactic:
constructor
State after:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (y z x : A),
      refl_trans_clos (refl_trans_clos R) x y →
        refl_trans_clos (refl_trans_clos R) x z →
          ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1) →
    ∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1

case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1) →
    ∀ (y z x : A),
      refl_trans_clos (refl_trans_clos R) x y →
        refl_trans_clos (refl_trans_clos R) x z →
          ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1

State before:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (y z x : A),
      refl_trans_clos (refl_trans_clos R) x y →
        refl_trans_clos (refl_trans_clos R) x z →
          ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1) →
    ∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1

case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1) →
    ∀ (y z x : A),
      refl_trans_clos (refl_trans_clos R) x y →
        refl_trans_clos (refl_trans_clos R) x z →
          ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
Tactic:
. intros h y z x red_x_y red_x_z
  have h1 : refl_trans_clos (refl_trans_clos R) x y :=
    by
      apply (trans_clos_idempotent _ _ _).2; trivial
  have h2 : refl_trans_clos (refl_trans_clos R) x z :=
    by
      apply (trans_clos_idempotent _ _ _).2; trivial
  cases' (h _ _ _ h1 h2) with w h
  cases' h with h1 h2
  exists w; constructor <;> apply (trans_clos_idempotent _ _ _).1 <;> trivial
State after:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1) →
    ∀ (y z x : A),
      refl_trans_clos (refl_trans_clos R) x y →
        refl_trans_clos (refl_trans_clos R) x z →
          ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1

State before:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1) →
    ∀ (y z x : A),
      refl_trans_clos (refl_trans_clos R) x y →
        refl_trans_clos (refl_trans_clos R) x z →
          ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
Tactic:
. intros h y z x red_x_y red_x_z
  have h1 : refl_trans_clos R x y :=
    by
      apply (trans_clos_idempotent _ _ _).1; trivial
  have h2 : refl_trans_clos R x z :=
    by
      apply (trans_clos_idempotent _ _ _).1; trivial
  cases' (h _ _ _ h1 h2) with w h
  cases' h with h1 h2
  exists w; constructor <;> apply (trans_clos_idempotent _ _ _).2 <;> trivial
State after:
no goals

State before:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (y z x : A),
      refl_trans_clos (refl_trans_clos R) x y →
        refl_trans_clos (refl_trans_clos R) x z →
          ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1) →
    ∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
Tactic:
intros h y z x red_x_y red_x_z
State after:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1

State before:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
Tactic:
have h1 : refl_trans_clos (refl_trans_clos R) x y :=
  by
    apply (trans_clos_idempotent _ _ _).2; trivial
State after:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1 : refl_trans_clos (refl_trans_clos R) x y
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1

State before:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1 : refl_trans_clos (refl_trans_clos R) x y
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
Tactic:
have h2 : refl_trans_clos (refl_trans_clos R) x z :=
  by
    apply (trans_clos_idempotent _ _ _).2; trivial
State after:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1 : refl_trans_clos (refl_trans_clos R) x y
h2 : refl_trans_clos (refl_trans_clos R) x z
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1

State before:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1 : refl_trans_clos (refl_trans_clos R) x y
h2 : refl_trans_clos (refl_trans_clos R) x z
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
Tactic:
cases' (h _ _ _ h1 h2) with w h
State after:
case mp.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h✝ :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1 : refl_trans_clos (refl_trans_clos R) x y
h2 : refl_trans_clos (refl_trans_clos R) x z
w : A
h : refl_trans_clos (refl_trans_clos R) y w ∧ refl_trans_clos (refl_trans_clos R) z w
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1

State before:
case mp.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h✝ :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1 : refl_trans_clos (refl_trans_clos R) x y
h2 : refl_trans_clos (refl_trans_clos R) x z
w : A
h : refl_trans_clos (refl_trans_clos R) y w ∧ refl_trans_clos (refl_trans_clos R) z w
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
Tactic:
cases' h with h1 h2
State after:
case mp.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1✝ : refl_trans_clos (refl_trans_clos R) x y
h2✝ : refl_trans_clos (refl_trans_clos R) x z
w : A
h1 : refl_trans_clos (refl_trans_clos R) y w
h2 : refl_trans_clos (refl_trans_clos R) z w
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1

State before:
case mp.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1✝ : refl_trans_clos (refl_trans_clos R) x y
h2✝ : refl_trans_clos (refl_trans_clos R) x z
w : A
h1 : refl_trans_clos (refl_trans_clos R) y w
h2 : refl_trans_clos (refl_trans_clos R) z w
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
Tactic:
exists w
State after:
case mp.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1✝ : refl_trans_clos (refl_trans_clos R) x y
h2✝ : refl_trans_clos (refl_trans_clos R) x z
w : A
h1 : refl_trans_clos (refl_trans_clos R) y w
h2 : refl_trans_clos (refl_trans_clos R) z w
⊢ refl_trans_clos R y w ∧ refl_trans_clos R z w

State before:
case mp.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1✝ : refl_trans_clos (refl_trans_clos R) x y
h2✝ : refl_trans_clos (refl_trans_clos R) x z
w : A
h1 : refl_trans_clos (refl_trans_clos R) y w
h2 : refl_trans_clos (refl_trans_clos R) z w
⊢ refl_trans_clos R y w ∧ refl_trans_clos R z w
Tactic:
constructor <;> apply (trans_clos_idempotent _ _ _).1 <;> trivial
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
⊢ refl_trans_clos (refl_trans_clos R) x y
Tactic:
apply (trans_clos_idempotent _ _ _).2
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
⊢ refl_trans_clos R x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
⊢ refl_trans_clos R x y
Tactic:
trivial
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1 : refl_trans_clos (refl_trans_clos R) x y
⊢ refl_trans_clos (refl_trans_clos R) x z
Tactic:
apply (trans_clos_idempotent _ _ _).2
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1 : refl_trans_clos (refl_trans_clos R) x y
⊢ refl_trans_clos R x z

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1 : refl_trans_clos (refl_trans_clos R) x y
⊢ refl_trans_clos R x z
Tactic:
trivial
State after:
no goals

State before:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1) →
    ∀ (y z x : A),
      refl_trans_clos (refl_trans_clos R) x y →
        refl_trans_clos (refl_trans_clos R) x z →
          ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
Tactic:
intros h y z x red_x_y red_x_z
State after:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
⊢ ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1

State before:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
⊢ ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
Tactic:
have h1 : refl_trans_clos R x y :=
  by
    apply (trans_clos_idempotent _ _ _).1; trivial
State after:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1 : refl_trans_clos R x y
⊢ ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1

State before:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1 : refl_trans_clos R x y
⊢ ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
Tactic:
have h2 : refl_trans_clos R x z :=
  by
    apply (trans_clos_idempotent _ _ _).1; trivial
State after:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1 : refl_trans_clos R x y
h2 : refl_trans_clos R x z
⊢ ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1

State before:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1 : refl_trans_clos R x y
h2 : refl_trans_clos R x z
⊢ ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
Tactic:
cases' (h _ _ _ h1 h2) with w h
State after:
case mpr.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h✝ :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1 : refl_trans_clos R x y
h2 : refl_trans_clos R x z
w : A
h : refl_trans_clos R y w ∧ refl_trans_clos R z w
⊢ ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1

State before:
case mpr.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h✝ :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1 : refl_trans_clos R x y
h2 : refl_trans_clos R x z
w : A
h : refl_trans_clos R y w ∧ refl_trans_clos R z w
⊢ ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
Tactic:
cases' h with h1 h2
State after:
case mpr.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1✝ : refl_trans_clos R x y
h2✝ : refl_trans_clos R x z
w : A
h1 : refl_trans_clos R y w
h2 : refl_trans_clos R z w
⊢ ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1

State before:
case mpr.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1✝ : refl_trans_clos R x y
h2✝ : refl_trans_clos R x z
w : A
h1 : refl_trans_clos R y w
h2 : refl_trans_clos R z w
⊢ ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
Tactic:
exists w
State after:
case mpr.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1✝ : refl_trans_clos R x y
h2✝ : refl_trans_clos R x z
w : A
h1 : refl_trans_clos R y w
h2 : refl_trans_clos R z w
⊢ refl_trans_clos (refl_trans_clos R) y w ∧ refl_trans_clos (refl_trans_clos R) z w

State before:
case mpr.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1✝ : refl_trans_clos R x y
h2✝ : refl_trans_clos R x z
w : A
h1 : refl_trans_clos R y w
h2 : refl_trans_clos R z w
⊢ refl_trans_clos (refl_trans_clos R) y w ∧ refl_trans_clos (refl_trans_clos R) z w
Tactic:
constructor <;> apply (trans_clos_idempotent _ _ _).2 <;> trivial
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
⊢ refl_trans_clos R x y
Tactic:
apply (trans_clos_idempotent _ _ _).1
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
⊢ refl_trans_clos (refl_trans_clos R) x y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
⊢ refl_trans_clos (refl_trans_clos R) x y
Tactic:
trivial
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1 : refl_trans_clos R x y
⊢ refl_trans_clos R x z
Tactic:
apply (trans_clos_idempotent _ _ _).1
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1 : refl_trans_clos R x y
⊢ refl_trans_clos (refl_trans_clos R) x z

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
y z x : A
red_x_y : refl_trans_clos (refl_trans_clos R) x y
red_x_z : refl_trans_clos (refl_trans_clos R) x z
h1 : refl_trans_clos R x y
⊢ refl_trans_clos (refl_trans_clos R) x z
Tactic:
trivial
State after:
no goals