internlm/Lean-Github huggingface dataset:
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ (∃ y, Positive y ∧ x ≃ -y) → Negative x
Tactic:
intro (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y)))
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
⊢ Negative x
Tactic:
have : sgn y ≃ 1 := Rational.sgn_positive.mp ‹Positive y›
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this : sgn y ≃ 1
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this : sgn y ≃ 1
⊢ Negative x
Tactic:
have : sgn x ≃ -1 := calc
  sgn x      ≃ _ := Rational.sgn_subst ‹x ≃ -y›
  sgn (-y)   ≃ _ := Rational.sgn_compat_neg
  (-(sgn y)) ≃ _ := AA.subst₁ ‹sgn y ≃ 1›
  (-1)       ≃ _ := Rel.refl
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this✝ : sgn y ≃ 1
this : sgn x ≃ -1
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this✝ : sgn y ≃ 1
this : sgn x ≃ -1
⊢ Negative x
Tactic:
have : Negative x := Rational.sgn_negative.mpr this
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this✝¹ : sgn y ≃ 1
this✝ : sgn x ≃ -1
this : Negative x
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
this✝¹ : sgn y ≃ 1
this✝ : sgn x ≃ -1
this : Negative x
⊢ Negative x
Tactic:
exact this
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x ↔ AltNegative x
Tactic:
apply Iff.intro
Proof state after:
case mp
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → AltNegative x

case mpr
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltNegative x → Negative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → AltNegative x
Tactic:
case mp =>
  intro (_ : Negative x)
  show AltNegative x
  have (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y))) :=
    negative_iff_neg_positive.mp ‹Negative x›
  have
    (AltPositive.intro
      (a : ℤ) (b : ℤ)
      (_ : AP (Positive a)) (_ : AP (Positive b)) y_eqv_a_over_b)
    := alt_positive.mp ‹Positive y›
  have : y ≃ a / b := y_eqv_a_over_b
  have : x ≃ (-a) / b := calc
    x                ≃ _ := ‹x ≃ -y›
    (-y)             ≃ _ := Rational.neg_subst ‹y ≃ a / b›
    (-((a : ℚ) / b)) ≃ _ := Rational.neg_scompatL_div
    (-a : ℚ) / b     ≃ _ := Rational.eqv_refl
  exact AltNegative.mk this
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltNegative x → Negative x
Tactic:
case mpr =>
  intro (_ : AltNegative x)
  show Negative x
  have
    (AltNegative.intro
      (a : ℤ) (b : ℤ)
      (_ : AP (Positive a)) (_ : AP (Positive b)) x_eqv_neg_a_over_b)
    := ‹AltNegative x›
  have : x ≃ (-a) / b := x_eqv_neg_a_over_b
  have : AltPositive ((a : ℚ) / b) := AltPositive.mk Rational.eqv_refl
  have : Positive ((a : ℚ) / b) := alt_positive.mpr this
  have : x ≃ -((a : ℚ) / b) := calc
    x                ≃ _ := ‹x ≃ (-a) / b›
    (-a : ℚ) / b     ≃ _ := Rational.eqv_symm Rational.neg_scompatL_div
    (-((a : ℚ) / b)) ≃ _ := Rational.eqv_refl
  have : ∃ (y : ℚ), Positive y ∧ x ≃ -y :=
    Exists.intro ((a : ℚ) / b) (And.intro ‹Positive ((a : ℚ) / b)› this)
  have : Negative x := negative_iff_neg_positive.mpr this
  exact this
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → AltNegative x
Tactic:
intro (_ : Negative x)
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
⊢ AltNegative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
⊢ AltNegative x
Tactic:
have (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y))) :=
  negative_iff_neg_positive.mp ‹Negative x›
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
⊢ AltNegative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
⊢ AltNegative x
Tactic:
have
  (AltPositive.intro
    (a : ℤ) (b : ℤ)
    (_ : AP (Positive a)) (_ : AP (Positive b)) y_eqv_a_over_b)
  := alt_positive.mp ‹Positive y›
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b : y ≃ Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b : y ≃ Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x
Tactic:
have : y ≃ a / b := y_eqv_a_over_b
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b this : y ≃ Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b this : y ≃ Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x
Tactic:
have : x ≃ (-a) / b := calc
  x                ≃ _ := ‹x ≃ -y›
  (-y)             ≃ _ := Rational.neg_subst ‹y ≃ a / b›
  (-((a : ℚ) / b)) ≃ _ := Rational.neg_scompatL_div
  (-a : ℚ) / b     ≃ _ := Rational.eqv_refl
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b this✝ : y ≃ Rational.from_integer a / Rational.from_integer b
this : x ≃ -Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
y : ℚ
left✝ : Positive y
right✝ : x ≃ -y
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
y_eqv_a_over_b this✝ : y ≃ Rational.from_integer a / Rational.from_integer b
this : x ≃ -Rational.from_integer a / Rational.from_integer b
⊢ AltNegative x
Tactic:
exact AltNegative.mk this
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltNegative x → Negative x
Tactic:
intro (_ : AltNegative x)
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
⊢ Negative x
Tactic:
have
  (AltNegative.intro
    (a : ℤ) (b : ℤ)
    (_ : AP (Positive a)) (_ : AP (Positive b)) x_eqv_neg_a_over_b)
  := ‹AltNegative x›
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b : x ≃ -Rational.from_integer a / Rational.from_integer b
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b : x ≃ -Rational.from_integer a / Rational.from_integer b
⊢ Negative x
Tactic:
have : x ≃ (-a) / b := x_eqv_neg_a_over_b
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this : x ≃ -Rational.from_integer a / Rational.from_integer b
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this : x ≃ -Rational.from_integer a / Rational.from_integer b
⊢ Negative x
Tactic:
have : AltPositive ((a : ℚ) / b) := AltPositive.mk Rational.eqv_refl
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝ : x ≃ -Rational.from_integer a / Rational.from_integer b
this : AltPositive (Rational.from_integer a / Rational.from_integer b)
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝ : x ≃ -Rational.from_integer a / Rational.from_integer b
this : AltPositive (Rational.from_integer a / Rational.from_integer b)
⊢ Negative x
Tactic:
have : Positive ((a : ℚ) / b) := alt_positive.mpr this
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝¹ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this : Positive (Rational.from_integer a / Rational.from_integer b)
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝¹ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this : Positive (Rational.from_integer a / Rational.from_integer b)
⊢ Negative x
Tactic:
have : x ≃ -((a : ℚ) / b) := calc
  x                ≃ _ := ‹x ≃ (-a) / b›
  (-a : ℚ) / b     ≃ _ := Rational.eqv_symm Rational.neg_scompatL_div
  (-((a : ℚ) / b)) ≃ _ := Rational.eqv_refl
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝² : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝¹ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝ : Positive (Rational.from_integer a / Rational.from_integer b)
this : x ≃ -(Rational.from_integer a / Rational.from_integer b)
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝² : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝¹ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝ : Positive (Rational.from_integer a / Rational.from_integer b)
this : x ≃ -(Rational.from_integer a / Rational.from_integer b)
⊢ Negative x
Tactic:
have : ∃ (y : ℚ), Positive y ∧ x ≃ -y :=
  Exists.intro ((a : ℚ) / b) (And.intro ‹Positive ((a : ℚ) / b)› this)
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝³ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝² : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝¹ : Positive (Rational.from_integer a / Rational.from_integer b)
this✝ : x ≃ -(Rational.from_integer a / Rational.from_integer b)
this : ∃ y, Positive y ∧ x ≃ -y
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝³ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝² : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝¹ : Positive (Rational.from_integer a / Rational.from_integer b)
this✝ : x ≃ -(Rational.from_integer a / Rational.from_integer b)
this : ∃ y, Positive y ∧ x ≃ -y
⊢ Negative x
Tactic:
have : Negative x := negative_iff_neg_positive.mpr this
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝⁴ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝³ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝² : Positive (Rational.from_integer a / Rational.from_integer b)
this✝¹ : x ≃ -(Rational.from_integer a / Rational.from_integer b)
this✝ : ∃ y, Positive y ∧ x ≃ -y
this : Negative x
⊢ Negative x
Theorem: AnalysisI.Ch4.Sec2.alt_negative
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltNegative x
a b : ℤ
a_pos✝ : AP (Positive a)
b_pos✝ : AP (Positive b)
x_eqv_neg_a_over_b this✝⁴ : x ≃ -Rational.from_integer a / Rational.from_integer b
this✝³ : AltPositive (Rational.from_integer a / Rational.from_integer b)
this✝² : Positive (Rational.from_integer a / Rational.from_integer b)
this✝¹ : x ≃ -(Rational.from_integer a / Rational.from_integer b)
this✝ : ∃ y, Positive y ∧ x ≃ -y
this : Negative x
⊢ Negative x
Tactic:
exact this
Proof state after:
no goals
Theorem: both_inclusions
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) R R' →
    (fun R R' => ∀ (x y : A), R x y → R' x y) R' R → (fun R R' => ∀ (x y : A), R x y ↔ R' x y) R R'
Tactic:
aesop
Proof state after:
no goals
Theorem: equiv_left
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
⊢ (fun R R' => ∀ (x y : A), R x y ↔ R' x y) R R' → (fun R R' => ∀ (x y : A), R x y → R' x y) R R'
Tactic:
aesop
Proof state after:
no goals
Theorem: equiv_right
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
⊢ (fun R R' => ∀ (x y : A), R x y ↔ R' x y) R R' → (fun R R' => ∀ (x y : A), R x y → R' x y) R' R
Tactic:
aesop
Proof state after:
no goals
Theorem: trans_clos_monotone
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) R R' →
    (fun R R' => ∀ (x y : A), R x y → R' x y) (trans_clos R) (trans_clos R')
Tactic:
intros le x y tr
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
le : ∀ (x y : A), R x y → R' x y
x y : A
tr : trans_clos R x y
⊢ trans_clos R' x y
Theorem: trans_clos_monotone
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
le : ∀ (x y : A), R x y → R' x y
x y : A
tr : trans_clos R x y
⊢ trans_clos R' x y
Tactic:
induction tr <;> aesop
Proof state after:
no goals
Theorem: sym_clos_monotone
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) R R' → (fun R R' => ∀ (x y : A), R x y → R' x y) (sym_clos R) (sym_clos R')
Tactic:
intros le x y sym
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
le : ∀ (x y : A), R x y → R' x y
x y : A
sym : sym_clos R x y
⊢ sym_clos R' x y
Theorem: sym_clos_monotone
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
le : ∀ (x y : A), R x y → R' x y
x y : A
sym : sym_clos R x y
⊢ sym_clos R' x y
Tactic:
induction sym <;> aesop
Proof state after:
no goals
Theorem: refl_clos_monotone
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) R R' →
    (fun R R' => ∀ (x y : A), R x y → R' x y) (refl_clos R) (refl_clos R')
Tactic:
intros le x y refl
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
le : ∀ (x y : A), R x y → R' x y
x y : A
refl : refl_clos R x y
⊢ refl_clos R' x y
Theorem: refl_clos_monotone
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
le : ∀ (x y : A), R x y → R' x y
x y : A
refl : refl_clos R x y
⊢ refl_clos R' x y
Tactic:
induction refl <;> aesop
Proof state after:
no goals
Theorem: trans_clos_transitive
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
⊢ trans_clos R x y → trans_clos R y z → trans_clos R x z
Tactic:
intros tr_x_y
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
tr_x_y : trans_clos R x y
⊢ trans_clos R y z → trans_clos R x z
Theorem: trans_clos_transitive
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
tr_x_y : trans_clos R x y
⊢ trans_clos R y z → trans_clos R x z
Tactic:
induction tr_x_y <;> aesop
Proof state after:
no goals
Theorem: refl_trans_clos_transitive
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
⊢ refl_trans_clos R x y → refl_trans_clos R y z → refl_trans_clos R x z
Tactic:
intros tr_x_y
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
tr_x_y : refl_trans_clos R x y
⊢ refl_trans_clos R y z → refl_trans_clos R x z
Theorem: refl_trans_clos_transitive
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
tr_x_y : refl_trans_clos R x y
⊢ refl_trans_clos R y z → refl_trans_clos R x z
Tactic:
induction tr_x_y <;> aesop
Proof state after:
no goals
Theorem: refl_trans_is_trans_refl
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ (fun R R' => ∀ (x y : A), R x y ↔ R' x y) (refl_clos (trans_clos R)) (trans_clos (refl_clos R))
Tactic:
apply both_inclusions <;> intros x y hyp
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : refl_clos (trans_clos R) x y
⊢ trans_clos (refl_clos R) x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : trans_clos (refl_clos R) x y
⊢ refl_clos (trans_clos R) x y
Theorem: refl_trans_is_trans_refl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : refl_clos (trans_clos R) x y
⊢ trans_clos (refl_clos R) x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : trans_clos (refl_clos R) x y
⊢ refl_clos (trans_clos R) x y
Tactic:
. cases hyp
  . aesop
  . apply trans_clos_monotone R <;> aesop
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : trans_clos (refl_clos R) x y
⊢ refl_clos (trans_clos R) x y
Theorem: refl_trans_is_trans_refl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : trans_clos (refl_clos R) x y
⊢ refl_clos (trans_clos R) x y
Tactic:
. induction' hyp with _ _ rc _ _ _ rc step ih
  . cases rc <;> aesop
  . cases rc; trivial
    apply refl_clos.base; aesop
Proof state after:
no goals
Theorem: refl_trans_is_trans_refl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : refl_clos (trans_clos R) x y
⊢ trans_clos (refl_clos R) x y
Tactic:
cases hyp
Proof state after:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ trans_clos (refl_clos R) x x

case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
a✝ : trans_clos R x y
⊢ trans_clos (refl_clos R) x y
Theorem: refl_trans_is_trans_refl
Proof state before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ trans_clos (refl_clos R) x x

case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
a✝ : trans_clos R x y
⊢ trans_clos (refl_clos R) x y
Tactic:
. aesop
Proof state after:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
a✝ : trans_clos R x y
⊢ trans_clos (refl_clos R) x y
Theorem: refl_trans_is_trans_refl
Proof state before:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
a✝ : trans_clos R x y
⊢ trans_clos (refl_clos R) x y
Tactic:
. apply trans_clos_monotone R <;> aesop
Proof state after:
no goals
Theorem: refl_trans_is_trans_refl
Proof state before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ trans_clos (refl_clos R) x x
Tactic:
aesop
Proof state after:
no goals
Theorem: refl_trans_is_trans_refl
Proof state before:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
a✝ : trans_clos R x y
⊢ trans_clos (refl_clos R) x y
Tactic:
apply trans_clos_monotone R <;> aesop
Proof state after:
no goals
Theorem: refl_trans_is_trans_refl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : trans_clos (refl_clos R) x y
⊢ refl_clos (trans_clos R) x y
Tactic:
induction' hyp with _ _ rc _ _ _ rc step ih
Proof state after:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ : A
rc : refl_clos R a✝ b✝
⊢ refl_clos (trans_clos R) a✝ b✝

case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ c✝ : A
rc : refl_clos R a✝ b✝
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝
Theorem: refl_trans_is_trans_refl
Proof state before:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ : A
rc : refl_clos R a✝ b✝
⊢ refl_clos (trans_clos R) a✝ b✝

case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ c✝ : A
rc : refl_clos R a✝ b✝
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝
Tactic:
. cases rc <;> aesop
Proof state after:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ c✝ : A
rc : refl_clos R a✝ b✝
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝
Theorem: refl_trans_is_trans_refl
Proof state before:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ c✝ : A
rc : refl_clos R a✝ b✝
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝
Tactic:
. cases rc; trivial
  apply refl_clos.base; aesop
Proof state after:
no goals
Theorem: refl_trans_is_trans_refl
Proof state before:
case a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ : A
rc : refl_clos R a✝ b✝
⊢ refl_clos (trans_clos R) a✝ b✝
Tactic:
cases rc <;> aesop
Proof state after:
no goals
Theorem: refl_trans_is_trans_refl
Proof state before:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ c✝ : A
rc : refl_clos R a✝ b✝
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝
Tactic:
cases rc
Proof state after:
case a.step.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ c✝ : A
step : trans_clos (refl_clos R) a✝ c✝
ih : refl_clos (trans_clos R) a✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝

case a.step.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ refl_clos (trans_clos R) a✝¹ c✝
Theorem: refl_trans_is_trans_refl
Proof state before:
case a.step.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ c✝ : A
step : trans_clos (refl_clos R) a✝ c✝
ih : refl_clos (trans_clos R) a✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝

case a.step.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ refl_clos (trans_clos R) a✝¹ c✝
Tactic:
trivial
Proof state after:
case a.step.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ refl_clos (trans_clos R) a✝¹ c✝
Theorem: refl_trans_is_trans_refl
Proof state before:
case a.step.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ refl_clos (trans_clos R) a✝¹ c✝
Tactic:
apply refl_clos.base
Proof state after:
case a.step.base.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ trans_clos R a✝¹ c✝