Theorem: equiv_conf (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (fun R R' => ∀ (x y : A), R x y ↔ R' x y) S R → confluent S → confluent R
Tactic:
simp
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (x y : A), S x y ↔ R x y) → confluent S → confluent R

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (x y : A), S x y ↔ R x y) → confluent S → confluent R
Tactic:
intros equiv
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
⊢ confluent S → confluent R

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
⊢ confluent S → confluent R
Tactic:
simp [confluent, wedge, joins]
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
⊢ (∀ (y z x : A),
      refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S 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
equiv : ∀ (x y : A), S x y ↔ R x y
⊢ (∀ (y z x : A),
      refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S 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_y_z
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_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:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_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 S x y := by
  apply refl_trans_clos_monotone
  intros _ _; apply (equiv _ _).2
  trivial
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ ∃ 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
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
Tactic:
have h2 : refl_trans_clos S x z := by
  apply refl_trans_clos_monotone
  intros _ _; apply (equiv _ _).2
  trivial
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
h2 : refl_trans_clos S 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
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
h2 : refl_trans_clos S x z
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
Tactic:
cases' (h y z x h1 h2) with w h
State after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h✝ :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
h2 : refl_trans_clos S x z
w : A
h : refl_trans_clos S y w ∧ refl_trans_clos S z w
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1

State before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h✝ :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
h2 : refl_trans_clos S x z
w : A
h : refl_trans_clos S y w ∧ refl_trans_clos S 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 intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1

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

State before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos R y w ∧ refl_trans_clos R z w
Tactic:
constructor <;> apply refl_trans_clos_monotone
State after:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.left.R x y → R x y

case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos ?intro.intro.left.R y w

case intro.intro.left.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ A → A → Prop

case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.right.R x y → R x y

case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos ?intro.intro.right.R z w

case intro.intro.right.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ A → A → Prop

State before:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.left.R x y → R x y

case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos ?intro.intro.left.R y w

case intro.intro.left.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ A → A → Prop

case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.right.R x y → R x y

case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos ?intro.intro.right.R z w

case intro.intro.right.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ A → A → Prop
Tactic:
. intros x y; apply (equiv _ _).1
State after:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos (fun x y => S x y) y w

case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.right.R x y → R x y

case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos ?intro.intro.right.R z w

case intro.intro.right.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ A → A → Prop

State before:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos (fun x y => S x y) y w

case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.right.R x y → R x y

case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos ?intro.intro.right.R z w

case intro.intro.right.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ A → A → Prop
Tactic:
. trivial
State after:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.right.R x y → R x y

case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos ?intro.intro.right.R z w

case intro.intro.right.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ A → A → Prop

State before:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.right.R x y → R x y

case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos ?intro.intro.right.R z w

case intro.intro.right.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ A → A → Prop
Tactic:
. intros x y; apply (equiv _ _).1
State after:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos (fun x y => S x y) z w

State before:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos (fun x y => S x y) z w
Tactic:
. trivial
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ refl_trans_clos S x y
Tactic:
apply refl_trans_clos_monotone
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ ∀ (x y : A), ?R x y → S x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ refl_trans_clos ?R x y

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ A → A → Prop

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ ∀ (x y : A), ?R x y → S x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ refl_trans_clos ?R x y

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ A → A → Prop
Tactic:
intros _ _
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
x✝ y✝ : A
⊢ ?R x✝ y✝ → S x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ refl_trans_clos ?R x y

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ A → A → Prop

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
x✝ y✝ : A
⊢ ?R x✝ y✝ → S x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ refl_trans_clos ?R x y

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ A → A → Prop
Tactic:
apply (equiv _ _).2
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ refl_trans_clos (fun x y => R x y) x y

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ refl_trans_clos (fun x y => R x y) x y
Tactic:
trivial
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos S x z
Tactic:
apply refl_trans_clos_monotone
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ ∀ (x y : A), ?R x y → S x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos ?R x z

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ A → A → Prop

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ ∀ (x y : A), ?R x y → S x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos ?R x z

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ A → A → Prop
Tactic:
intros _ _
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
x✝ y✝ : A
⊢ ?R x✝ y✝ → S x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos ?R x z

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ A → A → Prop

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
x✝ y✝ : A
⊢ ?R x✝ y✝ → S x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos ?R x z

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ A → A → Prop
Tactic:
apply (equiv _ _).2
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos (fun x y => R x y) x z

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos (fun x y => R x y) x z
Tactic:
trivial
State after:
no goals

State before:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.left.R x y → R x y
Tactic:
intros x y
State after:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y✝ z x✝ : A
red_x_y : refl_trans_clos R x✝ y✝
red_y_z : refl_trans_clos R x✝ z
h1✝ : refl_trans_clos S x✝ y✝
h2✝ : refl_trans_clos S x✝ z
w : A
h1 : refl_trans_clos S y✝ w
h2 : refl_trans_clos S z w
x y : A
⊢ ?intro.intro.left.R x y → R x y

State before:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y✝ z x✝ : A
red_x_y : refl_trans_clos R x✝ y✝
red_y_z : refl_trans_clos R x✝ z
h1✝ : refl_trans_clos S x✝ y✝
h2✝ : refl_trans_clos S x✝ z
w : A
h1 : refl_trans_clos S y✝ w
h2 : refl_trans_clos S z w
x y : A
⊢ ?intro.intro.left.R x y → R x y
Tactic:
apply (equiv _ _).1
State after:
no goals

State before:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos (fun x y => S x y) y w
Tactic:
trivial
State after:
no goals

State before:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.right.R x y → R x y
Tactic:
intros x y
State after:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y✝ z x✝ : A
red_x_y : refl_trans_clos R x✝ y✝
red_y_z : refl_trans_clos R x✝ z
h1✝ : refl_trans_clos S x✝ y✝
h2✝ : refl_trans_clos S x✝ z
w : A
h1 : refl_trans_clos S y✝ w
h2 : refl_trans_clos S z w
x y : A
⊢ ?intro.intro.right.R x y → R x y

State before:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y✝ z x✝ : A
red_x_y : refl_trans_clos R x✝ y✝
red_y_z : refl_trans_clos R x✝ z
h1✝ : refl_trans_clos S x✝ y✝
h2✝ : refl_trans_clos S x✝ z
w : A
h1 : refl_trans_clos S y✝ w
h2 : refl_trans_clos S z w
x y : A
⊢ ?intro.intro.right.R x y → R x y
Tactic:
apply (equiv _ _).1
State after:
no goals

State before:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos (fun x y => S x y) z w
Tactic:
trivial
State after:
no goals