internlm/Lean-Github huggingface dataset:
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
⊢ AltPositive x
Tactic:
have : sgn (-b) ≃ 1 := calc
  sgn (-b)   ≃ _ := Integer.sgn_compat_neg
  (-(sgn b)) ≃ _ := AA.subst₁ ‹sgn b ≃ -1›
  (-(-1))    ≃ _ := Integer.neg_involutive
  1          ≃ _ := Rel.refl
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this : sgn (-b) ≃ 1
⊢ AltPositive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this : sgn (-b) ≃ 1
⊢ AltPositive x
Tactic:
have : sgn (-a) ≃ 1 := calc
  sgn (-a)   ≃ _ := Integer.sgn_compat_neg
  (-(sgn a)) ≃ _ := AA.subst₁ ‹sgn a ≃ sgn b›
  (-(sgn b)) ≃ _ := Rel.symm Integer.sgn_compat_neg
  sgn (-b)   ≃ _ := ‹sgn (-b) ≃ 1›
  1          ≃ _ := Rel.refl
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝¹ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝ : sgn (-b) ≃ 1
this : sgn (-a) ≃ 1
⊢ AltPositive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝¹ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝ : sgn (-b) ≃ 1
this : sgn (-a) ≃ 1
⊢ AltPositive x
Tactic:
have : Positive (-a) := Integer.sgn_positive.mpr ‹sgn (-a) ≃ 1›
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝² : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝¹ : sgn (-b) ≃ 1
this✝ : sgn (-a) ≃ 1
this : Positive (-a)
⊢ AltPositive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝² : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝¹ : sgn (-b) ≃ 1
this✝ : sgn (-a) ≃ 1
this : Positive (-a)
⊢ AltPositive x
Tactic:
have : Positive (-b) := Integer.sgn_positive.mpr ‹sgn (-b) ≃ 1›
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁵ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝³ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝² : sgn (-b) ≃ 1
this✝¹ : sgn (-a) ≃ 1
this✝ : Positive (-a)
this : Positive (-b)
⊢ AltPositive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁵ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝³ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝² : sgn (-b) ≃ 1
this✝¹ : sgn (-a) ≃ 1
this✝ : Positive (-a)
this : Positive (-b)
⊢ AltPositive x
Tactic:
have : AP (Positive (-a)) := AP.mk ‹Positive (-a)›
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁶ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁵ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝⁴ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝³ : sgn (-b) ≃ 1
this✝² : sgn (-a) ≃ 1
this✝¹ : Positive (-a)
this✝ : Positive (-b)
this : AP (Positive (-a))
⊢ AltPositive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁶ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁵ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝⁴ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝³ : sgn (-b) ≃ 1
this✝² : sgn (-a) ≃ 1
this✝¹ : Positive (-a)
this✝ : Positive (-b)
this : AP (Positive (-a))
⊢ AltPositive x
Tactic:
have : AP (Positive (-b)) := AP.mk ‹Positive (-b)›
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁶ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝⁵ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝⁴ : sgn (-b) ≃ 1
this✝³ : sgn (-a) ≃ 1
this✝² : Positive (-a)
this✝¹ : Positive (-b)
this✝ : AP (Positive (-a))
this : AP (Positive (-b))
⊢ AltPositive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁶ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝⁵ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝⁴ : sgn (-b) ≃ 1
this✝³ : sgn (-a) ≃ 1
this✝² : Positive (-a)
this✝¹ : Positive (-b)
this✝ : AP (Positive (-a))
this : AP (Positive (-b))
⊢ AltPositive x
Tactic:
have neg_eqv {z : ℤ} : -(z : ℚ) ≃ ((-z : ℤ) : ℚ) :=
  Rational.eqv_symm Rational.neg_compat_from_integer
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁶ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝⁵ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝⁴ : sgn (-b) ≃ 1
this✝³ : sgn (-a) ≃ 1
this✝² : Positive (-a)
this✝¹ : Positive (-b)
this✝ : AP (Positive (-a))
this : AP (Positive (-b))
neg_eqv : ∀ {z : ℤ}, -Rational.from_integer z ≃ Rational.from_integer (-z)
⊢ AltPositive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁶ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝⁵ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝⁴ : sgn (-b) ≃ 1
this✝³ : sgn (-a) ≃ 1
this✝² : Positive (-a)
this✝¹ : Positive (-b)
this✝ : AP (Positive (-a))
this : AP (Positive (-b))
neg_eqv : ∀ {z : ℤ}, -Rational.from_integer z ≃ Rational.from_integer (-z)
⊢ AltPositive x
Tactic:
have : x ≃ ((-a : ℤ) : ℚ) / ((-b : ℤ) : ℚ) := calc
  x                               ≃ _ := ‹x ≃ a / b›
  (a : ℚ) / b                     ≃ _ := Rel.symm Rational.div_neg_cancel
  (-(a : ℚ)) / (-(b : ℚ))         ≃ _ := Rational.div_substL neg_eqv
  ((-a : ℤ) : ℚ) / (-b : ℚ)       ≃ _ := Rational.div_substR neg_eqv
  ((-a : ℤ) : ℚ) / ((-b : ℤ) : ℚ) ≃ _ := Rational.eqv_refl
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁸ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝⁶ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝⁵ : sgn (-b) ≃ 1
this✝⁴ : sgn (-a) ≃ 1
this✝³ : Positive (-a)
this✝² : Positive (-b)
this✝¹ : AP (Positive (-a))
this✝ : AP (Positive (-b))
neg_eqv : ∀ {z : ℤ}, -Rational.from_integer z ≃ Rational.from_integer (-z)
this : x ≃ Rational.from_integer (-a) / Rational.from_integer (-b)
⊢ AltPositive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁸ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝⁶ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝⁵ : sgn (-b) ≃ 1
this✝⁴ : sgn (-a) ≃ 1
this✝³ : Positive (-a)
this✝² : Positive (-b)
this✝¹ : AP (Positive (-a))
this✝ : AP (Positive (-b))
neg_eqv : ∀ {z : ℤ}, -Rational.from_integer z ≃ Rational.from_integer (-z)
this : x ≃ Rational.from_integer (-a) / Rational.from_integer (-b)
⊢ AltPositive x
Tactic:
exact AltPositive.mk this
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltPositive x → Positive x
Tactic:
intro (_ : AltPositive x)
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
⊢ Positive x
Tactic:
have (AltPositive.intro (a : ℤ) (b : ℤ) a_pos b_pos x_eqv) :=
  ‹AltPositive x›
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
⊢ Positive x
Tactic:
have : AP (Positive a) := a_pos
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this : AP (Positive a)
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this : AP (Positive a)
⊢ Positive x
Tactic:
have : sgn a ≃ 1 := Integer.sgn_positive.mp this.ev
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : AP (Positive a)
this : sgn a ≃ 1
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : AP (Positive a)
this : sgn a ≃ 1
⊢ Positive x
Tactic:
have : AP (Positive b) := b_pos
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : AP (Positive a)
this✝ : sgn a ≃ 1
this : AP (Positive b)
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : AP (Positive a)
this✝ : sgn a ≃ 1
this : AP (Positive b)
⊢ Positive x
Tactic:
have : sgn b ≃ 1 := Integer.sgn_positive.mp this.ev
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : AP (Positive a)
this✝¹ : sgn a ≃ 1
this✝ : AP (Positive b)
this : sgn b ≃ 1
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : AP (Positive a)
this✝¹ : sgn a ≃ 1
this✝ : AP (Positive b)
this : sgn b ≃ 1
⊢ Positive x
Tactic:
have : x ≃ a / b := x_eqv
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : AP (Positive a)
this✝² : sgn a ≃ 1
this✝¹ : AP (Positive b)
this✝ : sgn b ≃ 1
this : x ≃ Rational.from_integer a / Rational.from_integer b
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : AP (Positive a)
this✝² : sgn a ≃ 1
this✝¹ : AP (Positive b)
this✝ : sgn b ≃ 1
this : x ≃ Rational.from_integer a / Rational.from_integer b
⊢ Positive x
Tactic:
have : sgn a ≃ sgn b := Rel.trans ‹sgn a ≃ 1› (Rel.symm ‹sgn b ≃ 1›)
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : AP (Positive a)
this✝³ : sgn a ≃ 1
this✝² : AP (Positive b)
this✝¹ : sgn b ≃ 1
this✝ : x ≃ Rational.from_integer a / Rational.from_integer b
this : sgn a ≃ sgn b
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : AP (Positive a)
this✝³ : sgn a ≃ 1
this✝² : AP (Positive b)
this✝¹ : sgn b ≃ 1
this✝ : x ≃ Rational.from_integer a / Rational.from_integer b
this : sgn a ≃ sgn b
⊢ Positive x
Tactic:
have : Integer.Nonzero b := Integer.nonzero_from_positive_inst
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁵ : AP (Positive a)
this✝⁴ : sgn a ≃ 1
this✝³ : AP (Positive b)
this✝² : sgn b ≃ 1
this✝¹ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : sgn a ≃ sgn b
this : Nonzero b
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁵ : AP (Positive a)
this✝⁴ : sgn a ≃ 1
this✝³ : AP (Positive b)
this✝² : sgn b ≃ 1
this✝¹ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : sgn a ≃ sgn b
this : Nonzero b
⊢ Positive x
Tactic:
have : Integer.Sqrt1 (sgn b) := Integer.sgn_nonzero.mp this
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁶ : AP (Positive a)
this✝⁵ : sgn a ≃ 1
this✝⁴ : AP (Positive b)
this✝³ : sgn b ≃ 1
this✝² : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : sgn a ≃ sgn b
this✝ : Nonzero b
this : Integer.Sqrt1 (sgn b)
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁶ : AP (Positive a)
this✝⁵ : sgn a ≃ 1
this✝⁴ : AP (Positive b)
this✝³ : sgn b ≃ 1
this✝² : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : sgn a ≃ sgn b
this✝ : Nonzero b
this : Integer.Sqrt1 (sgn b)
⊢ Positive x
Tactic:
have : sgn a * sgn b ≃ 1 :=
  Integer.mul_sqrt1_eqv.mpr (And.intro this ‹sgn a ≃ sgn b›)
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : AP (Positive a)
this✝⁶ : sgn a ≃ 1
this✝⁵ : AP (Positive b)
this✝⁴ : sgn b ≃ 1
this✝³ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : sgn a ≃ sgn b
this✝¹ : Nonzero b
this✝ : Integer.Sqrt1 (sgn b)
this : sgn a * sgn b ≃ 1
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : AP (Positive a)
this✝⁶ : sgn a ≃ 1
this✝⁵ : AP (Positive b)
this✝⁴ : sgn b ≃ 1
this✝³ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : sgn a ≃ sgn b
this✝¹ : Nonzero b
this✝ : Integer.Sqrt1 (sgn b)
this : sgn a * sgn b ≃ 1
⊢ Positive x
Tactic:
have : sgn x ≃ 1 := calc
  sgn x                   ≃ _ := Rational.sgn_subst ‹x ≃ a / b›
  sgn ((a : ℚ) / (b : ℚ)) ≃ _ := Rational.sgn_div_integers
  sgn a * sgn b           ≃ _ := ‹sgn a * sgn b ≃ 1›
  1                       ≃ _ := Rel.refl
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁸ : AP (Positive a)
this✝⁷ : sgn a ≃ 1
this✝⁶ : AP (Positive b)
this✝⁵ : sgn b ≃ 1
this✝⁴ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : sgn a ≃ sgn b
this✝² : Nonzero b
this✝¹ : Integer.Sqrt1 (sgn b)
this✝ : sgn a * sgn b ≃ 1
this : sgn x ≃ 1
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁸ : AP (Positive a)
this✝⁷ : sgn a ≃ 1
this✝⁶ : AP (Positive b)
this✝⁵ : sgn b ≃ 1
this✝⁴ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : sgn a ≃ sgn b
this✝² : Nonzero b
this✝¹ : Integer.Sqrt1 (sgn b)
this✝ : sgn a * sgn b ≃ 1
this : sgn x ≃ 1
⊢ Positive x
Tactic:
have : Positive x := Rational.sgn_positive.mpr this
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁹ : AP (Positive a)
this✝⁸ : sgn a ≃ 1
this✝⁷ : AP (Positive b)
this✝⁶ : sgn b ≃ 1
this✝⁵ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : sgn a ≃ sgn b
this✝³ : Nonzero b
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : sgn a * sgn b ≃ 1
this✝ : sgn x ≃ 1
this : Positive x
⊢ Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁹ : AP (Positive a)
this✝⁸ : sgn a ≃ 1
this✝⁷ : AP (Positive b)
this✝⁶ : sgn b ≃ 1
this✝⁵ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁴ : sgn a ≃ sgn b
this✝³ : Nonzero b
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : sgn a * sgn b ≃ 1
this✝ : sgn x ≃ 1
this : Positive x
⊢ Positive x
Tactic:
exact this
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x ↔ ∃ y, Positive y ∧ x ≃ -y
Tactic:
apply Iff.intro
Proof state after:
case mp
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → ∃ y, Positive y ∧ x ≃ -y

case mpr
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ (∃ y, Positive y ∧ x ≃ -y) → Negative x
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → ∃ y, Positive y ∧ x ≃ -y
Tactic:
case mp =>
  intro (_ : Negative x)
  show ∃ (y : ℚ), Positive y ∧ x ≃ -y
  have : sgn x ≃ -1 := Rational.sgn_negative.mp ‹Negative x›
  have : sgn (-x) ≃ 1 := calc
    sgn (-x) ≃ _ := Rational.sgn_compat_neg
    (-sgn x) ≃ _ := AA.subst₁ ‹sgn x ≃ -1›
    (-(-1))  ≃ _ := Integer.neg_involutive
    1        ≃ _ := Rel.refl
  have : Positive (-x) := Rational.sgn_positive.mpr ‹sgn (-x) ≃ 1›
  have : x ≃ -(-x) := Rational.eqv_symm Rational.neg_involutive
  exact Exists.intro (-x) (And.intro ‹Positive (-x)› ‹x ≃ -(-x)›)
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ (∃ y, Positive y ∧ x ≃ -y) → Negative x
Tactic:
case mpr =>
  intro (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y)))
  show Negative x
  have : sgn y ≃ 1 := Rational.sgn_positive.mp ‹Positive y›
  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
  have : Negative x := Rational.sgn_negative.mpr this
  exact this
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Negative x → ∃ y, Positive y ∧ x ≃ -y
Tactic:
intro (_ : Negative x)
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
⊢ ∃ y, Positive y ∧ x ≃ -y
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
⊢ ∃ y, Positive y ∧ x ≃ -y
Tactic:
have : sgn x ≃ -1 := Rational.sgn_negative.mp ‹Negative x›
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this : sgn x ≃ -1
⊢ ∃ y, Positive y ∧ x ≃ -y
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this : sgn x ≃ -1
⊢ ∃ y, Positive y ∧ x ≃ -y
Tactic:
have : sgn (-x) ≃ 1 := calc
  sgn (-x) ≃ _ := Rational.sgn_compat_neg
  (-sgn x) ≃ _ := AA.subst₁ ‹sgn x ≃ -1›
  (-(-1))  ≃ _ := Integer.neg_involutive
  1        ≃ _ := Rel.refl
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝ : sgn x ≃ -1
this : sgn (-x) ≃ 1
⊢ ∃ y, Positive y ∧ x ≃ -y
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝ : sgn x ≃ -1
this : sgn (-x) ≃ 1
⊢ ∃ y, Positive y ∧ x ≃ -y
Tactic:
have : Positive (-x) := Rational.sgn_positive.mpr ‹sgn (-x) ≃ 1›
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝¹ : sgn x ≃ -1
this✝ : sgn (-x) ≃ 1
this : Positive (-x)
⊢ ∃ y, Positive y ∧ x ≃ -y
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝¹ : sgn x ≃ -1
this✝ : sgn (-x) ≃ 1
this : Positive (-x)
⊢ ∃ y, Positive y ∧ x ≃ -y
Tactic:
have : x ≃ -(-x) := Rational.eqv_symm Rational.neg_involutive
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝² : sgn x ≃ -1
this✝¹ : sgn (-x) ≃ 1
this✝ : Positive (-x)
this : x ≃ - -x
⊢ ∃ y, Positive y ∧ x ≃ -y
Theorem: AnalysisI.Ch4.Sec2.negative_iff_neg_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Negative x
this✝² : sgn x ≃ -1
this✝¹ : sgn (-x) ≃ 1
this✝ : Positive (-x)
this : x ≃ - -x
⊢ ∃ y, Positive y ∧ x ≃ -y
Tactic:
exact Exists.intro (-x) (And.intro ‹Positive (-x)› ‹x ≃ -(-x)›)
Proof state after:
no goals