internlm/Lean-Github huggingface dataset:
Theorem: inc_refl_trans_eq
Proof state before:
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos S x y
⊢ refl_trans_clos R x y
Tactic:
induction steps
Proof state after:
case mp.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos R a✝ a✝

case mp.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² c✝
Theorem: inc_refl_trans_eq
Proof state before:
case mp.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos R a✝ a✝

case mp.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² c✝
Tactic:
. constructor
Proof state after:
case mp.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² c✝
Theorem: inc_refl_trans_eq
Proof state before:
case mp.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² c✝
Tactic:
. apply refl_trans_clos_transitive
  . apply s_sub_r_star; trivial
  . trivial
Proof state after:
no goals
Theorem: inc_refl_trans_eq
Proof state before:
case mp.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos R a✝ a✝
Tactic:
constructor
Proof state after:
no goals
Theorem: inc_refl_trans_eq
Proof state before:
case mp.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² c✝
Tactic:
apply refl_trans_clos_transitive
Proof state after:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² ?mp.step.y

case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R ?mp.step.y c✝

case mp.step.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ A
Theorem: inc_refl_trans_eq
Proof state before:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² ?mp.step.y

case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R ?mp.step.y c✝

case mp.step.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ A
Tactic:
. apply s_sub_r_star; trivial
Proof state after:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R b✝ c✝
Theorem: inc_refl_trans_eq
Proof state before:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R b✝ c✝
Tactic:
. trivial
Proof state after:
no goals
Theorem: inc_refl_trans_eq
Proof state before:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² ?mp.step.y
Tactic:
apply s_sub_r_star
Proof state after:
case mp.step.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ S a✝² ?mp.step.y
Theorem: inc_refl_trans_eq
Proof state before:
case mp.step.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ S a✝² ?mp.step.y
Tactic:
trivial
Proof state after:
no goals
Theorem: inc_refl_trans_eq
Proof state before:
case mp.step.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R b✝ c✝
Tactic:
trivial
Proof state after:
no goals
Theorem: inc_refl_trans_eq
Proof state before:
case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos R x y
⊢ refl_trans_clos S x y
Tactic:
induction steps
Proof state after:
case mpr.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos S a✝ a✝

case mpr.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_clos S b✝ c✝
⊢ refl_trans_clos S a✝² c✝
Theorem: inc_refl_trans_eq
Proof state before:
case mpr.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos S a✝ a✝

case mpr.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_clos S b✝ c✝
⊢ refl_trans_clos S a✝² c✝
Tactic:
. constructor
Proof state after:
case mpr.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_clos S b✝ c✝
⊢ refl_trans_clos S a✝² c✝
Theorem: inc_refl_trans_eq
Proof state before:
case mpr.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_clos S b✝ c✝
⊢ refl_trans_clos S a✝² c✝
Tactic:
. aesop
Proof state after:
no goals
Theorem: inc_refl_trans_eq
Proof state before:
case mpr.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos S a✝ a✝
Tactic:
constructor
Proof state after:
no goals
Theorem: inc_refl_trans_eq
Proof state before:
case mpr.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_clos S b✝ c✝
⊢ refl_trans_clos S a✝² c✝
Tactic:
aesop
Proof state after:
no goals
Theorem: equiv_conf
Proof 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
Proof 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
Theorem: equiv_conf
Proof 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
Proof 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
Theorem: equiv_conf
Proof 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]
Proof 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
Theorem: equiv_conf
Proof 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
Proof 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
Theorem: equiv_conf
Proof 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
Proof 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
Theorem: equiv_conf
Proof 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
Proof 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
Theorem: equiv_conf
Proof 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
Proof 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
Theorem: equiv_conf
Proof 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
Proof 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
Theorem: equiv_conf
Proof 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
Proof 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
Theorem: equiv_conf
Proof 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
Proof 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
Theorem: equiv_conf
Proof 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
Proof state after:
no goals
Theorem: equiv_conf
Proof 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
Proof 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
Theorem: equiv_conf
Proof 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 _ _
Proof 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