internlm/Lean-Github huggingface dataset:
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ Euclid 0 q
Tactic:
let m := 0
Proof state after:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
⊢ Euclid 0 q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
⊢ Euclid 0 q
Tactic:
let r := 0
Proof state after:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
⊢ Euclid 0 q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
⊢ Euclid 0 q
Tactic:
have r_bounded : r < q := ‹0 < q›
Proof state after:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
r_bounded : r < q
⊢ Euclid 0 q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
r_bounded : r < q
⊢ Euclid 0 q
Tactic:
have n_divided : 0 ≃ m * q + r := calc
  0         ≃ _ := Rel.symm Natural.zero_mul
  0 * q     ≃ _ := Rel.symm Natural.add_zero
  0 * q + 0 ≃ _ := Rel.refl
  m * q + r ≃ _ := Rel.refl
Proof state after:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
r_bounded : r < q
n_divided : 0 ≃ m * q + r
⊢ Euclid 0 q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n q : ℕ
x✝ : Positive q
this : 0 < q
m : Nat := 0
r : Nat := 0
r_bounded : r < q
n_divided : 0 ≃ m * q + r
⊢ Euclid 0 q
Tactic:
exact Euclid.intro m r r_bounded n_divided
Proof state after:
no goals
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n q : ℕ
x✝ : Positive q
this : 0 < q
⊢ ∀ (m : ℕ), Euclid m q → Euclid (step m) q
Tactic:
intro n (ih : Euclid n q)
Proof state after:
n✝ q : ℕ
x✝ : Positive q
this : 0 < q
n : ℕ
ih : Euclid n q
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n✝ q : ℕ
x✝ : Positive q
this : 0 < q
n : ℕ
ih : Euclid n q
⊢ Euclid (step n) q
Tactic:
have ⟨m', r', (_ : r' < q), (_ : n ≃ m' * q + r')⟩ := ih
Proof state after:
n✝ q : ℕ
x✝ : Positive q
this : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n✝ q : ℕ
x✝ : Positive q
this : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
⊢ Euclid (step n) q
Tactic:
have : step r' ≤ q := Natural.lt_step_le.mp ‹r' < q›
Proof state after:
n✝ q : ℕ
x✝ : Positive q
this✝ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this : step r' ≤ q
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n✝ q : ℕ
x✝ : Positive q
this✝ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this : step r' ≤ q
⊢ Euclid (step n) q
Tactic:
have : step r' < q ∨ step r' ≃ q := Natural.le_split ‹step r' ≤ q›
Proof state after:
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ Euclid (step n) q
Tactic:
apply Or.elim ‹step r' < q ∨ step r' ≃ q›
Proof state after:
case left
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ step r' < q → Euclid (step n) q

case right
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ step r' ≃ q → Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case left
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ step r' < q → Euclid (step n) q
Tactic:
intro (_ : step r' < q)
Proof state after:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
⊢ Euclid (step n) q
Tactic:
let m := m'
Proof state after:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
⊢ Euclid (step n) q
Tactic:
let r := step r'
Proof state after:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
⊢ Euclid (step n) q
Tactic:
have : r < q := ‹step r' < q›
Proof state after:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝² : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝¹ : step r' ≤ q
this✝ : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
this : r < q
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝² : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝¹ : step r' ≤ q
this✝ : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
this : r < q
⊢ Euclid (step n) q
Tactic:
have : step n ≃ m * q + r := calc
  step n             ≃ _ := AA.subst₁ ‹n ≃ m' * q + r'›
  step (m' * q + r') ≃ _ := Rel.symm Natural.add_step
  m' * q + step r'   ≃ _ := Rel.refl
  m * q + r          ≃ _ := Rel.refl
Proof state after:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝³ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝² : step r' ≤ q
this✝¹ : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
this✝ : r < q
this : step n ≃ m * q + r
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case left
n✝ q : ℕ
x✝¹ : Positive q
this✝³ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝² : step r' ≤ q
this✝¹ : step r' < q ∨ step r' ≃ q
x✝ : step r' < q
m : ℕ := m'
r : ℕ := step r'
this✝ : r < q
this : step n ≃ m * q + r
⊢ Euclid (step n) q
Tactic:
exact ⟨m, r, ‹r < q›, ‹step n ≃ m * q + r›⟩
Proof state after:
no goals
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case right
n✝ q : ℕ
x✝ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
⊢ step r' ≃ q → Euclid (step n) q
Tactic:
intro (_ : step r' ≃ q)
Proof state after:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
⊢ Euclid (step n) q
Tactic:
let m := step m'
Proof state after:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
⊢ Euclid (step n) q
Tactic:
let r := 0
Proof state after:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝¹ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝ : step r' ≤ q
this : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
⊢ Euclid (step n) q
Tactic:
have : r < q := ‹0 < q›
Proof state after:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝² : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝¹ : step r' ≤ q
this✝ : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
this : r < q
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝² : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝¹ : step r' ≤ q
this✝ : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
this : r < q
⊢ Euclid (step n) q
Tactic:
have : step n ≃ m * q + r := calc
  step n             ≃ _ := AA.subst₁ ‹n ≃ m' * q + r'›
  step (m' * q + r') ≃ _ := Rel.symm Natural.add_step
  m' * q + step r'   ≃ _ := AA.substR ‹step r' ≃ q›
  m' * q + q         ≃ _ := Rel.symm Natural.step_mul
  step m' * q        ≃ _ := Rel.symm Natural.add_zero
  step m' * q + 0    ≃ _ := Rel.refl
  m * q + r          ≃ _ := Rel.refl
Proof state after:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝³ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝² : step r' ≤ q
this✝¹ : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
this✝ : r < q
this : step n ≃ m * q + r
⊢ Euclid (step n) q
Theorem: AnalysisI.Ch2.euclidean_algorithm
Proof state before:
case right
n✝ q : ℕ
x✝¹ : Positive q
this✝³ : 0 < q
n : ℕ
ih : Euclid n q
m' r' : ℕ
r_bounded✝ : r' < q
n_divided✝ : n ≃ m' * q + r'
this✝² : step r' ≤ q
this✝¹ : step r' < q ∨ step r' ≃ q
x✝ : step r' ≃ q
m : ℕ := step m'
r : Nat := 0
this✝ : r < q
this : step n ≃ m * q + r
⊢ Euclid (step n) q
Tactic:
exact ⟨m, r, ‹r < q›, ‹step n ≃ m * q + r›⟩
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Positive x ↔ AltPositive x
Tactic:
apply Iff.intro
Proof state after:
case mp
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Positive x → AltPositive x

case mpr
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltPositive x → Positive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Positive x → AltPositive x
Tactic:
case mp =>
  intro (_ : Positive x)
  show AltPositive x
  have (Rational.AsRatio.intro a b (_ : Integer.Nonzero b) x_eqv) :=
    Rational.as_ratio x
  have : x ≃ a / b := x_eqv
  have : sgn a * sgn b ≃ 1 := calc
    sgn a * sgn b     ≃ _ := Rel.symm Rational.sgn_div_integers
    sgn ((a : ℚ) / b) ≃ _ := Rational.sgn_subst (Rel.symm ‹x ≃ a / b›)
    sgn x             ≃ _ := Rational.sgn_positive.mp ‹Positive x›
    1                 ≃ _ := Rel.refl
  have (And.intro (_ : Integer.Sqrt1 (sgn b)) (_ : sgn a ≃ sgn b)) :=
    Integer.mul_sqrt1_eqv.mp this
  have : sgn b ≃ 1 ∨ sgn b ≃ -1 :=
    Integer.sqrt1_cases.mp ‹Integer.Sqrt1 (sgn b)›
  match this with
  | Or.inl (_ : sgn b ≃ 1) =>
    have : sgn a ≃ 1 := Rel.trans ‹sgn a ≃ sgn b› ‹sgn b ≃ 1›
    have : AP (Positive a) := AP.mk (Integer.sgn_positive.mpr ‹sgn a ≃ 1›)
    have : AP (Positive b) := AP.mk (Integer.sgn_positive.mpr ‹sgn b ≃ 1›)
    exact AltPositive.mk ‹x ≃ a / b›
  | Or.inr (_ : sgn b ≃ -1) =>
    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
    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
    have : Positive (-a) := Integer.sgn_positive.mpr ‹sgn (-a) ≃ 1›
    have : Positive (-b) := Integer.sgn_positive.mpr ‹sgn (-b) ≃ 1›
    have : AP (Positive (-a)) := AP.mk ‹Positive (-a)›
    have : AP (Positive (-b)) := AP.mk ‹Positive (-b)›
    have neg_eqv {z : ℤ} : -(z : ℚ) ≃ ((-z : ℤ) : ℚ) :=
      Rational.eqv_symm Rational.neg_compat_from_integer
    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
    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:
case mpr =>
  intro (_ : AltPositive x)
  show Positive x
  have (AltPositive.intro (a : ℤ) (b : ℤ) a_pos b_pos x_eqv) :=
    ‹AltPositive x›
  have : AP (Positive a) := a_pos
  have : sgn a ≃ 1 := Integer.sgn_positive.mp this.ev
  have : AP (Positive b) := b_pos
  have : sgn b ≃ 1 := Integer.sgn_positive.mp this.ev
  have : x ≃ a / b := x_eqv
  have : sgn a ≃ sgn b := Rel.trans ‹sgn a ≃ 1› (Rel.symm ‹sgn b ≃ 1›)
  have : Integer.Nonzero b := Integer.nonzero_from_positive_inst
  have : Integer.Sqrt1 (sgn b) := Integer.sgn_nonzero.mp this
  have : sgn a * sgn b ≃ 1 :=
    Integer.mul_sqrt1_eqv.mpr (And.intro this ‹sgn a ≃ sgn b›)
  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
  have : Positive x := Rational.sgn_positive.mpr this
  exact this
Proof state after:
no goals
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ Positive x → AltPositive x
Tactic:
intro (_ : Positive x)
Proof state after:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
⊢ AltPositive x
Theorem: AnalysisI.Ch4.Sec2.alt_positive
Proof state before:
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
⊢ AltPositive x
Tactic:
have (Rational.AsRatio.intro a b (_ : Integer.Nonzero b) x_eqv) :=
  Rational.as_ratio x
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
⊢ 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
⊢ AltPositive x
Tactic:
have : x ≃ a / b := x_eqv
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
⊢ 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
⊢ AltPositive x
Tactic:
have : sgn a * sgn b ≃ 1 := calc
  sgn a * sgn b     ≃ _ := Rel.symm Rational.sgn_div_integers
  sgn ((a : ℚ) / b) ≃ _ := Rational.sgn_subst (Rel.symm ‹x ≃ a / b›)
  sgn x             ≃ _ := Rational.sgn_positive.mp ‹Positive x›
  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
⊢ 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
⊢ AltPositive x
Tactic:
have (And.intro (_ : Integer.Sqrt1 (sgn b)) (_ : sgn a ≃ sgn b)) :=
  Integer.mul_sqrt1_eqv.mp this
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
⊢ 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
⊢ AltPositive x
Tactic:
have : sgn b ≃ 1 ∨ sgn b ≃ -1 :=
  Integer.sqrt1_cases.mp ‹Integer.Sqrt1 (sgn 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
⊢ 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
⊢ AltPositive x
Tactic:
match this with
| Or.inl (_ : sgn b ≃ 1) =>
  have : sgn a ≃ 1 := Rel.trans ‹sgn a ≃ sgn b› ‹sgn b ≃ 1›
  have : AP (Positive a) := AP.mk (Integer.sgn_positive.mpr ‹sgn a ≃ 1›)
  have : AP (Positive b) := AP.mk (Integer.sgn_positive.mpr ‹sgn b ≃ 1›)
  exact AltPositive.mk ‹x ≃ a / b›
| Or.inr (_ : sgn b ≃ -1) =>
  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
  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
  have : Positive (-a) := Integer.sgn_positive.mpr ‹sgn (-a) ≃ 1›
  have : Positive (-b) := Integer.sgn_positive.mpr ‹sgn (-b) ≃ 1›
  have : AP (Positive (-a)) := AP.mk ‹Positive (-a)›
  have : AP (Positive (-b)) := AP.mk ‹Positive (-b)›
  have neg_eqv {z : ℤ} : -(z : ℚ) ≃ ((-z : ℤ) : ℚ) :=
    Rational.eqv_symm Rational.neg_compat_from_integer
  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
  exact AltPositive.mk this
Proof state after:
no goals
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 a ≃ 1 := Rel.trans ‹sgn a ≃ sgn b› ‹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 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 a ≃ 1
⊢ AltPositive x
Tactic:
have : AP (Positive a) := AP.mk (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 a ≃ 1
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 a ≃ 1
this : AP (Positive a)
⊢ AltPositive x
Tactic:
have : AP (Positive b) := AP.mk (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 a ≃ 1
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 a ≃ 1
this✝ : AP (Positive a)
this : AP (Positive b)
⊢ AltPositive x
Tactic:
exact AltPositive.mk ‹x ≃ a / b›
Proof state after:
no goals