[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Mul α
a : α
x✝ : IsSquare (op a)
c : αᵐᵒᵖ
hc : op a = c * c
⊢ a = unop c * unop c
[PROOFSTEP]
rw [← unop_mul, ← hc, unop_op]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Mul α
a : α
x✝ : IsSquare a
c : α
hc : a = c * c
⊢ IsSquare (op a)
[PROOFSTEP]
simp [hc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MonoidHomClass F α β
m : α
f : F
⊢ IsSquare m → IsSquare (↑f m)
[PROOFSTEP]
rintro ⟨m, rfl⟩
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MonoidHomClass F α β
f : F
m : α
⊢ IsSquare (↑f (m * m))
[PROOFSTEP]
exact ⟨f m, by simp⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MonoidHomClass F α β
f : F
m : α
⊢ ↑f (m * m) = ↑f m * ↑f m
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Monoid α
n : ℕ
a m : α
⊢ IsSquare m ↔ ∃ c, m = c ^ 2
[PROOFSTEP]
simp [IsSquare, pow_two]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Monoid α
n✝ : ℕ
a : α
n : ℕ
⊢ IsSquare a → IsSquare (a ^ n)
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Monoid α
n✝ n : ℕ
a : α
⊢ IsSquare ((a * a) ^ n)
[PROOFSTEP]
exact ⟨a ^ n, (Commute.refl _).mul_pow _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Monoid α
n : ℕ
a : α
⊢ Even n → ∀ (a : α), IsSquare (a ^ n)
[PROOFSTEP]
rintro ⟨n, rfl⟩ a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Monoid α
a✝ : α
n : ℕ
a : α
⊢ IsSquare (a ^ (n + n))
[PROOFSTEP]
exact ⟨a ^ n, pow_add _ _ _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
n : ℕ
a : α
inst✝ : HasDistribNeg α
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n
[PROOFSTEP]
rintro ⟨c, rfl⟩ a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
a✝ : α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
[PROOFSTEP]
simp_rw [← two_mul, pow_mul, neg_sq]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
n : ℕ
a : α
inst✝ : HasDistribNeg α
h : Even n
⊢ (-1) ^ n = 1
[PROOFSTEP]
rw [h.neg_pow, one_pow]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : CommSemigroup α
a b : α
⊢ IsSquare a → IsSquare b → IsSquare (a * b)
[PROOFSTEP]
rintro ⟨a, rfl⟩ ⟨b, rfl⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : CommSemigroup α
a b : α
⊢ IsSquare (a * a * (b * b))
[PROOFSTEP]
exact ⟨a * b, mul_mul_mul_comm _ _ _ _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a⁻¹ ↔ IsSquare a
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare a
[PROOFSTEP]
rw [← isSquare_op_iff, ← inv_inv a]
[GOAL]
case refine'_1
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare (op a⁻¹⁻¹)
[PROOFSTEP]
exact h.map (MulEquiv.inv' α)
[GOAL]
case refine'_2
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
a : α
h : IsSquare a
⊢ IsSquare a⁻¹
[PROOFSTEP]
exact ((isSquare_op_iff a).mpr h).map (MulEquiv.inv' α).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
a : α
n : ℤ
⊢ IsSquare a → IsSquare (a ^ n)
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionMonoid α
n : ℤ
a : α
⊢ IsSquare ((a * a) ^ n)
[PROOFSTEP]
exact ⟨a ^ n, (Commute.refl _).mul_zpow _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : DivisionMonoid α
a : α
inst✝ : HasDistribNeg α
n : ℤ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n
[PROOFSTEP]
rintro ⟨c, rfl⟩ a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : DivisionMonoid α
a✝ : α
inst✝ : HasDistribNeg α
c : ℤ
a : α
⊢ (-a) ^ (c + c) = a ^ (c + c)
[PROOFSTEP]
exact zpow_bit0_neg _ _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : DivisionMonoid α
a : α
inst✝ : HasDistribNeg α
n : ℤ
h : Even n
⊢ (-1) ^ n = 1
[PROOFSTEP]
rw [h.neg_zpow, one_zpow]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
⊢ Even |a| ↔ Even a
[PROOFSTEP]
cases abs_choice a
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : |a| = a
⊢ Even |a| ↔ Even a
[PROOFSTEP]
have h : abs a = a := by assumption
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : |a| = a
⊢ |a| = a
[PROOFSTEP]
assumption
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ h : |a| = a
⊢ Even |a| ↔ Even a
[PROOFSTEP]
simp only [h, even_neg]
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : |a| = -a
⊢ Even |a| ↔ Even a
[PROOFSTEP]
have h : abs a = -a := by assumption
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ : |a| = -a
⊢ |a| = -a
[PROOFSTEP]
assumption
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : SubtractionMonoid α
inst✝ : LinearOrder α
a : α
h✝ h : |a| = -a
⊢ Even |a| ↔ Even a
[PROOFSTEP]
simp only [h, even_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a / b)
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : DivisionCommMonoid α
a b : α
ha : IsSquare a
hb : IsSquare b
⊢ IsSquare (a * b⁻¹)
[PROOFSTEP]
exact ha.mul hb.inv
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Group α
n : ℤ
⊢ Even n → ∀ (a : α), IsSquare (a ^ n)
[PROOFSTEP]
rintro ⟨n, rfl⟩ a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Group α
n : ℤ
a : α
⊢ IsSquare (a ^ (n + n))
[PROOFSTEP]
exact ⟨a ^ n, zpow_add _ _ _⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
m n : α
hm : Even m
hn : Even n
⊢ Even (m - n)
[PROOFSTEP]
obtain ⟨a, rfl⟩ := hm
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : α
hn : Even n
a : α
⊢ Even (a + a - n)
[PROOFSTEP]
obtain ⟨b, rfl⟩ := hn
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ Even (a + a - (b + b))
[PROOFSTEP]
refine' ⟨a - b, _⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ a + a - (b + b) = a - b + (a - b)
[PROOFSTEP]
obtain h | h := le_total a b
[GOAL]
case intro.intro.inl
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
h : a ≤ b
⊢ a + a - (b + b) = a - b + (a - b)
[PROOFSTEP]
rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
[GOAL]
case intro.intro.inr
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝³ : CanonicallyLinearOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)
[PROOFSTEP]
exact (tsub_add_tsub_comm h h).symm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m✝ n m : α
⊢ Even m ↔ ∃ c, m = 2 * c
[PROOFSTEP]
simp [even_iff_exists_two_nsmul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n a : α
⊢ Even a ↔ 2 ∣ a
[PROOFSTEP]
simp [Even, Dvd.dvd, two_mul]
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_5
inst✝ : Semiring α
⊢ (Set.range fun x => 2 * x) = {a | Even a}
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
α✝ : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_5
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x) ↔ x ∈ {a | Even a}
[PROOFSTEP]
simp [eq_comm, two_mul, Even]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ 2 = 1 + 1
[PROOFSTEP]
rw [one_add_one_eq_two]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Even m
a : ℕ
x✝ : a + 1 ≠ 0
⊢ Even (m ^ (a + 1))
[PROOFSTEP]
rw [pow_succ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Even m
a : ℕ
x✝ : a + 1 ≠ 0
⊢ Even (m * m ^ a)
[PROOFSTEP]
exact hm.mul_right _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n a b : α
⊢ a = 2 * b + 1 ↔ a = bit1 b
[PROOFSTEP]
rw [two_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n a b : α
⊢ a = b + b + 1 ↔ a = bit1 b
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α✝ : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_5
inst✝ : Semiring α
⊢ (Set.range fun x => 2 * x + 1) = {a | Odd a}
[PROOFSTEP]
ext x
[GOAL]
case h
F : Type u_1
α✝ : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α✝
inst✝¹ : Semiring β
m n : α✝
α : Type u_5
inst✝ : Semiring α
x : α
⊢ (x ∈ Set.range fun x => 2 * x + 1) ↔ x ∈ {a | Odd a}
[PROOFSTEP]
simp [Odd, eq_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Even m → Odd n → Odd (m + n)
[PROOFSTEP]
rintro ⟨m, rfl⟩ ⟨n, rfl⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (m + m + (2 * n + 1))
[PROOFSTEP]
exact ⟨m + n, by rw [mul_add, ← two_mul, add_assoc]⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ m + m + (2 * n + 1) = 2 * (m + n) + 1
[PROOFSTEP]
rw [mul_add, ← two_mul, add_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
he : Even m
ho : Odd n
⊢ Odd (n + m)
[PROOFSTEP]
simp only [he.add_odd ho, add_comm n m]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
hn : Even n
⊢ Odd (m + n)
[PROOFSTEP]
rw [add_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
hn : Even n
⊢ Odd (n + m)
[PROOFSTEP]
exact hn.add_odd hm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd m → Odd n → Even (m + n)
[PROOFSTEP]
rintro ⟨m, rfl⟩ ⟨n, rfl⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Even (2 * m + 1 + (2 * n + 1))
[PROOFSTEP]
refine' ⟨n + m + 1, _⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ 2 * m + 1 + (2 * n + 1) = n + m + 1 + (n + m + 1)
[PROOFSTEP]
rw [two_mul, two_mul]
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ m + m + 1 + (n + n + 1) = n + m + 1 + (n + m + 1)
[PROOFSTEP]
ac_rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (m + (m + 1))
[PROOFSTEP]
simp [← add_assoc]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (m + 1 + m)
[PROOFSTEP]
simp [add_comm _ m]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (m + (1 + m))
[PROOFSTEP]
simp [add_comm 1 m]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd (1 + m + m)
[PROOFSTEP]
simp [add_comm 1 m]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α
inst✝¹ : Semiring β
m n : α
inst✝ : RingHomClass F α β
f : F
⊢ Odd m → Odd (↑f m)
[PROOFSTEP]
rintro ⟨m, rfl⟩
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α
inst✝¹ : Semiring β
n : α
inst✝ : RingHomClass F α β
f : F
m : α
⊢ Odd (↑f (2 * m + 1))
[PROOFSTEP]
exact ⟨f m, by simp [two_mul]⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝² : Semiring α
inst✝¹ : Semiring β
n : α
inst✝ : RingHomClass F α β
f : F
m : α
⊢ ↑f (2 * m + 1) = 2 * ↑f m + 1
[PROOFSTEP]
simp [two_mul]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd m → Odd n → Odd (m * n)
[PROOFSTEP]
rintro ⟨m, rfl⟩ ⟨n, rfl⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ Odd ((2 * m + 1) * (2 * n + 1))
[PROOFSTEP]
refine' ⟨2 * m * n + n + m, _⟩
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
⊢ (2 * m + 1) * (2 * n + 1) = 2 * (2 * m * n + n + m) + 1
[PROOFSTEP]
rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc, ← Nat.cast_two, ←
  Nat.cast_comm]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
⊢ Odd (m ^ 0)
[PROOFSTEP]
rw [pow_zero]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
⊢ Odd 1
[PROOFSTEP]
exact odd_one
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
a : ℕ
⊢ Odd (m ^ (a + 1))
[PROOFSTEP]
rw [pow_succ]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
a : ℕ
⊢ Odd (m * m ^ a)
[PROOFSTEP]
exact hm.mul <| Odd.pow hm
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : α
n : ℕ
⊢ Odd n → ∀ (a : α), (-a) ^ n = -a ^ n
[PROOFSTEP]
rintro ⟨c, rfl⟩ a
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a✝ : α
c : ℕ
a : α
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)
[PROOFSTEP]
simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
a : α
n : ℕ
h : Odd n
⊢ (-1) ^ n = -1
[PROOFSTEP]
rw [h.neg_pow, one_pow]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
n : α
hn : Odd n
⊢ 0 < n
[PROOFSTEP]
obtain ⟨k, rfl⟩ := hn
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
k : α
⊢ 0 < 2 * k + 1
[PROOFSTEP]
rw [pos_iff_ne_zero, Ne.def, add_eq_zero_iff, not_and']
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : CanonicallyOrderedCommSemiring α
inst✝ : Nontrivial α
k : α
⊢ 1 = 0 → ¬2 * k = 0
[PROOFSTEP]
exact fun h => (one_ne_zero h).elim
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
⊢ Even (-2)
[PROOFSTEP]
simp only [even_neg, even_two]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
hp : Odd a
⊢ Odd (-a)
[PROOFSTEP]
obtain ⟨k, hk⟩ := hp
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
k : α
hk : a = 2 * k + 1
⊢ Odd (-a)
[PROOFSTEP]
use-(k + 1)
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
k : α
hk : a = 2 * k + 1
⊢ -a = 2 * -(k + 1) + 1
[PROOFSTEP]
rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right, ← neg_add, hk]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
⊢ Odd (-1)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Odd a
hb : Even b
⊢ Odd (a - b)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Odd a
hb : Even b
⊢ Odd (a + -b)
[PROOFSTEP]
exact ha.add_even hb.neg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Even a
hb : Odd b
⊢ Odd (a - b)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Even a
hb : Odd b
⊢ Odd (a + -b)
[PROOFSTEP]
exact ha.add_odd hb.neg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Odd a
hb : Odd b
⊢ Even (a - b)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : Ring α
a b : α
n : ℕ
ha : Odd a
hb : Odd b
⊢ Even (a + -b)
[PROOFSTEP]
exact ha.add_odd hb.neg
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Ring α
a b : α
n : ℕ
inst✝ : LinearOrder α
⊢ Odd |a| ↔ Odd a
[PROOFSTEP]
cases' abs_choice a with h h
[GOAL]
case inl
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Ring α
a b : α
n : ℕ
inst✝ : LinearOrder α
h : |a| = a
⊢ Odd |a| ↔ Odd a
[PROOFSTEP]
simp only [h, odd_neg]
[GOAL]
case inr
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝¹ : Ring α
a b : α
n : ℕ
inst✝ : LinearOrder α
h : |a| = -a
⊢ Odd |a| ↔ Odd a
[PROOFSTEP]
simp only [h, odd_neg]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a✝ : R
n : ℕ
hn : Even n
a : R
⊢ 0 ≤ a ^ n
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a✝ : R
n : ℕ
a : R
k : ℕ
hk : n = k + k
⊢ 0 ≤ a ^ n
[PROOFSTEP]
simpa only [hk, two_mul] using pow_bit0_nonneg a k
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Even n
ha : a ≠ 0
⊢ 0 < a ^ n
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
ha : a ≠ 0
k : ℕ
hk : n = k + k
⊢ 0 < a ^ n
[PROOFSTEP]
simpa only [hk, two_mul] using pow_bit0_pos ha k
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Odd n
ha : a ≤ 0
⊢ a ^ n ≤ 0
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
ha : a ≤ 0
k : ℕ
hk : n = 2 * k + 1
⊢ a ^ n ≤ 0
[PROOFSTEP]
simpa only [hk, two_mul] using pow_bit1_nonpos_iff.mpr ha
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Odd n
ha : a < 0
⊢ a ^ n < 0
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
ha : a < 0
k : ℕ
hk : n = 2 * k + 1
⊢ a ^ n < 0
[PROOFSTEP]
simpa only [hk, two_mul] using pow_bit1_neg_iff.mpr ha
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Even n
h₀ : 0 < n
h : 0 < a ^ n
ha : a = 0
⊢ False
[PROOFSTEP]
rw [ha, zero_pow h₀] at h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Even n
h₀ : 0 < n
h : 0 < 0
ha : a = 0
⊢ False
[PROOFSTEP]
exact lt_irrefl 0 h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a✝ : R
n p : ℕ
hp : Even p
a : R
⊢ |a| ^ p = a ^ p
[PROOFSTEP]
rw [← abs_pow, abs_eq_self]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a✝ : R
n p : ℕ
hp : Even p
a : R
⊢ 0 ≤ a ^ p
[PROOFSTEP]
exact hp.pow_nonneg _
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : Odd n
⊢ StrictMono fun a => a ^ n
[PROOFSTEP]
cases' hn with k hk
[GOAL]
case intro
F : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
inst✝ : LinearOrderedRing R
a : R
n k : ℕ
hk : n = 2 * k + 1
⊢ StrictMono fun a => a ^ n
[PROOFSTEP]
simpa only [hk, two_mul] using strictMono_pow_bit1 _


[GOAL]
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n : ℕ
⊢ mk i a ^ n = mk (n • i) (GMonoid.gnpow n a)
[PROOFSTEP]
match n with
| 0 =>
  rw [pow_zero]
  exact (GMonoid.gnpow_zero' ⟨_, a⟩).symm
| n + 1 =>
  rw [pow_succ, mk_pow a n, mk_mul_mk]
  exact (GMonoid.gnpow_succ' n ⟨_, a⟩).symm
[GOAL]
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n : ℕ
⊢ mk i a ^ 0 = mk (0 • i) (GMonoid.gnpow 0 a)
[PROOFSTEP]
rw [pow_zero]
[GOAL]
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n : ℕ
⊢ 1 = mk (0 • i) (GMonoid.gnpow 0 a)
[PROOFSTEP]
exact (GMonoid.gnpow_zero' ⟨_, a⟩).symm
[GOAL]
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n✝ n : ℕ
⊢ mk i a ^ (n + 1) = mk ((n + 1) • i) (GMonoid.gnpow (n + 1) a)
[PROOFSTEP]
rw [pow_succ, mk_pow a n, mk_mul_mk]
[GOAL]
ι : Type u_1
A : ι → Type u_2
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
i : ι
a : A i
n✝ n : ℕ
⊢ mk (i + n • i) (GMul.mul a (GMonoid.gnpow n a)) = mk ((n + 1) • i) (GMonoid.gnpow (n + 1) a)
[PROOFSTEP]
exact (GMonoid.gnpow_succ' n ⟨_, a⟩).symm
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GradedMonoid.GMonoid A
l : List α
fι : α → ι
⊢ dProdIndex l fι = sum (map fι l)
[PROOFSTEP]
match l with
| [] => simp
| head :: tail => simp [List.dProdIndex_eq_map_sum tail fι]
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GradedMonoid.GMonoid A
l : List α
fι : α → ι
⊢ dProdIndex [] fι = sum (map fι [])
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GradedMonoid.GMonoid A
l : List α
fι : α → ι
head : α
tail : List α
⊢ dProdIndex (head :: tail) fι = sum (map fι (head :: tail))
[PROOFSTEP]
simp [List.dProdIndex_eq_map_sum tail fι]
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk (List.dProdIndex l fι) (List.dProd l fι fA) = List.prod (List.map (fun a => mk (fι a) (fA a)) l)
[PROOFSTEP]
match l with
| [] => simp; rfl
| head :: tail => simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk (List.dProdIndex [] fι) (List.dProd [] fι fA) = List.prod (List.map (fun a => mk (fι a) (fA a)) [])
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ mk 0 GOne.one = 1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
⊢ mk (List.dProdIndex (head :: tail) fι) (List.dProd (head :: tail) fι fA) =
    List.prod (List.map (fun a => mk (fι a) (fA a)) (head :: tail))
[PROOFSTEP]
simp [← GradedMonoid.mk_list_dProd tail _ _, GradedMonoid.mk_mul_mk, List.prod_cons]
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ List.prod (List.map f l) =
    mk (List.dProdIndex l fun i => (f i).fst) (List.dProd l (fun i => (f i).fst) fun i => (f i).snd)
[PROOFSTEP]
rw [GradedMonoid.mk_list_dProd, GradedMonoid.mk]
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
l : List α
f : α → GradedMonoid A
⊢ List.prod (List.map f l) = List.prod (List.map (fun a => { fst := (f a).fst, snd := (f a).snd }) l)
[PROOFSTEP]
simp_rw [Sigma.eta]
[GOAL]
ι : Type u_1
α : Type u_2
A : ι → Type u_3
inst✝¹ : AddMonoid ι
inst✝ : GMonoid A
n : ℕ
f : Fin n → GradedMonoid A
⊢ List.prod (List.ofFn f) =
    mk (List.dProdIndex (List.finRange n) fun i => (f i).fst)
      (List.dProd (List.finRange n) (fun i => (f i).fst) fun i => (f i).snd)
[PROOFSTEP]
rw [List.ofFn_eq_map, GradedMonoid.list_prod_map_eq_dProd]
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ dProd l fι fA = prod (map fA l)
[PROOFSTEP]
match l with
| [] =>
  rw [List.dProd_nil, List.map_nil, List.prod_nil]
  rfl
| head :: tail =>
  rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]
  rfl
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ dProd [] fι fA = prod (map fA [])
[PROOFSTEP]
rw [List.dProd_nil, List.map_nil, List.prod_nil]
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
⊢ GradedMonoid.GOne.one = 1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ dProd (head :: tail) fι fA = prod (map fA (head :: tail))
[PROOFSTEP]
rw [List.dProd_cons, List.map_cons, List.prod_cons, List.dProd_monoid tail _ _]
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
inst✝¹ : AddMonoid ι
inst✝ : Monoid R
l : List α
fι : α → ι
fA : α → R
head : α
tail : List α
⊢ GradedMonoid.GMul.mul (fA head) (prod (map fA tail)) = fA head * prod (map fA tail)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ r ^ n ∈ A (n • i)
[PROOFSTEP]
match n with
| 0 =>
  rw [pow_zero, zero_nsmul]
  exact one_mem_graded _
| n + 1 =>
  rw [pow_succ', succ_nsmul']
  exact mul_mem_graded (pow_mem_graded n h) h
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ r ^ 0 ∈ A (0 • i)
[PROOFSTEP]
rw [pow_zero, zero_nsmul]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
r : R
i : ι
h : r ∈ A i
⊢ 1 ∈ A 0
[PROOFSTEP]
exact one_mem_graded _
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r ^ (n + 1) ∈ A ((n + 1) • i)
[PROOFSTEP]
rw [pow_succ', succ_nsmul']
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n✝ : ℕ
r : R
i : ι
h : r ∈ A i
n : ℕ
⊢ r ^ n * r ∈ A (n • i + i)
[PROOFSTEP]
exact mul_mem_graded (pow_mem_graded n h) h
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), j ∈ l → r j ∈ A (i j)
⊢ List.prod (List.map r l) ∈ A (List.sum (List.map i l))
[PROOFSTEP]
match l with
| [] =>
  rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]
  exact one_mem_graded _
| head :: tail =>
  rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]
  exact
    mul_mem_graded (h _ <| List.mem_cons_self _ _)
      (list_prod_map_mem_graded tail _ _ <| fun j hj => h _ <| List.mem_cons_of_mem _ hj)
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), j ∈ [] → r j ∈ A (i j)
⊢ List.prod (List.map r []) ∈ A (List.sum (List.map i []))
[PROOFSTEP]
rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ (j : ι'), j ∈ [] → r j ∈ A (i j)
⊢ 1 ∈ A 0
[PROOFSTEP]
exact one_mem_graded _
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ (j : ι'), j ∈ head :: tail → r j ∈ A (i j)
⊢ List.prod (List.map r (head :: tail)) ∈ A (List.sum (List.map i (head :: tail)))
[PROOFSTEP]
rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ (j : ι'), j ∈ head :: tail → r j ∈ A (i j)
⊢ r head * List.prod (List.map r tail) ∈ A (i head + List.sum (List.map i tail))
[PROOFSTEP]
exact
  mul_mem_graded (h _ <| List.mem_cons_self _ _)
    (list_prod_map_mem_graded tail _ _ <| fun j hj => h _ <| List.mem_cons_of_mem _ hj)
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ List.prod (List.ofFn r) ∈ A (List.sum (List.ofFn i))
[PROOFSTEP]
rw [List.ofFn_eq_map, List.ofFn_eq_map]
[GOAL]
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
n : ℕ
i : Fin n → ι
r : Fin n → R
h : ∀ (j : Fin n), r j ∈ A (i j)
⊢ List.prod (List.map r (List.finRange n)) ∈ A (List.sum (List.map i (List.finRange n)))
[PROOFSTEP]
exact list_prod_map_mem_graded _ _ _ fun _ _ => h _
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → { x // x ∈ A (fι a) }
l : List α
⊢ ↑(List.dProd l fι fA) = List.prod (List.map (fun a => ↑(fA a)) l)
[PROOFSTEP]
match l with
| [] => rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
| head :: tail => rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons, SetLike.coe_list_dProd _ _ _ tail]
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → { x // x ∈ A (fι a) }
l : List α
⊢ ↑(List.dProd [] fι fA) = List.prod (List.map (fun a => ↑(fA a)) [])
[PROOFSTEP]
rw [List.dProd_nil, coe_gOne, List.map_nil, List.prod_nil]
[GOAL]
ι : Type u_1
R : Type u_2
α : Type u_3
S : Type u_4
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
fι : α → ι
fA : (a : α) → { x // x ∈ A (fι a) }
l : List α
head : α
tail : List α
⊢ ↑(List.dProd (head :: tail) fι fA) = List.prod (List.map (fun a => ↑(fA a)) (head :: tail))
[PROOFSTEP]
rw [List.dProd_cons, coe_gMul, List.map_cons, List.prod_cons, SetLike.coe_list_dProd _ _ _ tail]


[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
a✝ b : M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
mul : ∀ (a b : M₀'), f (a * b) = f a * f b
a : M₀'
⊢ f (0 * a) = f 0
[PROOFSTEP]
simp only [mul, zero, zero_mul]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
a✝ b : M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
mul : ∀ (a b : M₀'), f (a * b) = f a * f b
a : M₀'
⊢ f (a * 0) = f 0
[PROOFSTEP]
simp only [mul, zero, mul_zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
a b : M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀ → M₀'
hf : Surjective f
zero : f 0 = 0
mul : ∀ (a b : M₀), f (a * b) = f a * f b
x : M₀
⊢ 0 * f x = 0
[PROOFSTEP]
simp only [← zero, ← mul, zero_mul]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝² : MulZeroClass M₀
a b : M₀
inst✝¹ : Mul M₀'
inst✝ : Zero M₀'
f : M₀ → M₀'
hf : Surjective f
zero : f 0 = 0
mul : ∀ (a b : M₀), f (a * b) = f a * f b
x : M₀
⊢ f x * 0 = 0
[PROOFSTEP]
simp only [← zero, ← mul, mul_zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a✝ b✝ : M₀
H : a✝ * b✝ = 0
⊢ f (?m.2223 H) * f (?m.2224 H) = 0
[PROOFSTEP]
rw [← mul, H, zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a✝ b✝ : M₀
H✝ : a✝ * b✝ = 0
this : f a✝ * f b✝ = 0
H : f a✝ = 0
⊢ f a✝ = f 0
[PROOFSTEP]
rwa [zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : NoZeroDivisors M₀'
a✝ b✝ : M₀
H✝ : a✝ * b✝ = 0
this : f a✝ * f b✝ = 0
H : f b✝ = 0
⊢ f b✝ = f 0
[PROOFSTEP]
rwa [zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
⊢ b✝ = c✝
[PROOFSTEP]
have := congr_arg f He
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
this : f (a✝ * b✝) = f (a✝ * c✝)
⊢ b✝ = c✝
[PROOFSTEP]
rw [mul, mul] at this
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
this : f a✝ * f b✝ = f a✝ * f c✝
⊢ b✝ = c✝
[PROOFSTEP]
exact hf (mul_left_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsLeftCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : a✝ ≠ 0
He : a✝ * b✝ = a✝ * c✝
this : f a✝ * f b✝ = f a✝ * f c✝
Hfa : f a✝ = 0
⊢ f a✝ = f 0
[PROOFSTEP]
rw [Hfa, zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
⊢ a✝ = c✝
[PROOFSTEP]
have := congr_arg f He
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
this : f (a✝ * b✝) = f (c✝ * b✝)
⊢ a✝ = c✝
[PROOFSTEP]
rw [mul, mul] at this
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
this : f a✝ * f b✝ = f c✝ * f b✝
⊢ a✝ = c✝
[PROOFSTEP]
exact hf (mul_right_cancel₀ (fun Hfa => Hne <| hf <| by rw [Hfa, zero]) this)
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : Mul M₀
inst✝³ : Zero M₀
inst✝² : Mul M₀'
inst✝¹ : Zero M₀'
f : M₀ → M₀'
hf : Injective f
zero : f 0 = 0
mul : ∀ (x y : M₀), f (x * y) = f x * f y
inst✝ : IsRightCancelMulZero M₀'
a✝ b✝ c✝ : M₀
Hne : b✝ ≠ 0
He : a✝ * b✝ = c✝ * b✝
this : f a✝ * f b✝ = f c✝ * f b✝
Hfa : f b✝ = 0
⊢ f b✝ = f 0
[PROOFSTEP]
rw [Hfa, zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : CancelMonoidWithZero M₀
a b c : M₀
inst✝³ : Zero M₀'
inst✝² : Mul M₀'
inst✝¹ : One M₀'
inst✝ : Pow M₀' ℕ
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : M₀'), f (x * y) = f x * f y
npow : ∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n
src✝¹ : Monoid M₀' := Injective.monoid f hf one mul npow
src✝ : MulZeroClass M₀' := Injective.mulZeroClass f hf zero mul
a✝ b✝ c✝ : M₀'
hx : a✝ ≠ 0
H : a✝ * b✝ = a✝ * c✝
⊢ f a✝ * f b✝ = f a✝ * f c✝
[PROOFSTEP]
erw [← mul, ← mul, H]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁴ : CancelMonoidWithZero M₀
a b c : M₀
inst✝³ : Zero M₀'
inst✝² : Mul M₀'
inst✝¹ : One M₀'
inst✝ : Pow M₀' ℕ
f : M₀' → M₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : M₀'), f (x * y) = f x * f y
npow : ∀ (x : M₀') (n : ℕ), f (x ^ n) = f x ^ n
src✝¹ : Monoid M₀' := Injective.monoid f hf one mul npow
src✝ : MulZeroClass M₀' := Injective.mulZeroClass f hf zero mul
a✝ b✝ c✝ : M₀'
hx : b✝ ≠ 0
H : a✝ * b✝ = c✝ * b✝
⊢ f a✝ * f b✝ = f c✝ * f b✝
[PROOFSTEP]
erw [← mul, ← mul, H]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
a b c g h x : G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
src✝² : MonoidWithZero G₀' := Injective.monoidWithZero f hf zero one mul npow
src✝¹ : DivInvMonoid G₀' := Injective.divInvMonoid f hf one mul inv div npow zpow
src✝ : Nontrivial G₀' := pullback_nonzero f zero one
⊢ f 0⁻¹ = f 0
[PROOFSTEP]
erw [inv, zero, inv_zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
a b c g h x✝ : G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
src✝² : MonoidWithZero G₀' := Injective.monoidWithZero f hf zero one mul npow
src✝¹ : DivInvMonoid G₀' := Injective.divInvMonoid f hf one mul inv div npow zpow
src✝ : Nontrivial G₀' := pullback_nonzero f zero one
x : G₀'
hx : x ≠ 0
⊢ f (x * x⁻¹) = f 1
[PROOFSTEP]
erw [one, mul, inv, mul_inv_cancel ((hf.ne_iff' zero).2 hx)]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
a b c g h x : G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
src✝¹ : MonoidWithZero G₀' := Surjective.monoidWithZero f hf zero one mul npow
src✝ : DivInvMonoid G₀' := Surjective.divInvMonoid f hf one mul inv div npow zpow
⊢ 0⁻¹ = 0
[PROOFSTEP]
erw [← zero, ← inv, inv_zero]
[GOAL]
M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
a b c g h x✝ : G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
src✝¹ : MonoidWithZero G₀' := Surjective.monoidWithZero f hf zero one mul npow
src✝ : DivInvMonoid G₀' := Surjective.divInvMonoid f hf one mul inv div npow zpow
x : G₀
hx : f x ≠ 0
⊢ f x * (f x)⁻¹ = 1
[PROOFSTEP]
erw [← inv, ← mul, mul_inv_cancel (mt (congr_arg f) <| fun h ↦ hx (h.trans zero)), one]


[GOAL]
K : Type u_1
v : K
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
n : ℕ
⊢ convergents (of v) (n + 1) = ↑⌊v⌋ + 1 / convergents (of (Int.fract v)⁻¹) n
[PROOFSTEP]
rw [of_convergents_eq_convergents', convergents'_succ, of_convergents_eq_convergents']
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
⊢ ∀ (ε : K), ε > 0 → ∃ N, ∀ (n : ℕ), n ≥ N → |v - convergents (of v) n| < ε
[PROOFSTEP]
intro ε ε_pos
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v - convergents (of v) n| < ε
[PROOFSTEP]
rcases(exists_nat_gt (1 / ε) : ∃ N' : ℕ, 1 / ε < N') with ⟨N', one_div_ε_lt_N'⟩
[GOAL]
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v - convergents (of v) n| < ε
[PROOFSTEP]
let N :=
  max N'
    5
      -- set minimum to 5 to have N ≤ fib N work
[GOAL]
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → |v - convergents (of v) n| < ε
[PROOFSTEP]
exists N
[GOAL]
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
⊢ ∀ (n : ℕ), n ≥ N → |v - convergents (of v) n| < ε
[PROOFSTEP]
intro n n_ge_N
[GOAL]
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
let g := of v
[GOAL]
case intro
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
cases' Decidable.em (g.TerminatedAt n) with terminated_at_n not_terminated_at_n
[GOAL]
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
terminated_at_n : TerminatedAt g n
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
have : v = g.convergents n := of_correctness_of_terminatedAt terminated_at_n
[GOAL]
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
terminated_at_n : TerminatedAt g n
this : v = convergents g n
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
have : v - g.convergents n = 0 := sub_eq_zero.mpr this
[GOAL]
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
terminated_at_n : TerminatedAt g n
this✝ : v = convergents g n
this : v - convergents g n = 0
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
rw [this]
[GOAL]
case intro.inl
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
terminated_at_n : TerminatedAt g n
this✝ : v = convergents g n
this : v - convergents g n = 0
⊢ |0| < ε
[PROOFSTEP]
exact_mod_cast ε_pos
[GOAL]
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
let B := g.denominators n
[GOAL]
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
let nB := g.denominators (n + 1)
[GOAL]
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
have abs_v_sub_conv_le : |v - g.convergents n| ≤ 1 / (B * nB) := abs_sub_convergents_le not_terminated_at_n
[GOAL]
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
⊢ |v - convergents (of v) n| < ε
[PROOFSTEP]
suffices : 1 / (B * nB) < ε
[GOAL]
case intro.inr
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
this : 1 / (B * nB) < ε
⊢ |v - convergents (of v) n| < ε
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
exact lt_of_le_of_lt abs_v_sub_conv_le this
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
have nB_ineq : (fib (n + 2) : K) ≤ nB :=
  haveI : ¬g.TerminatedAt (n + 1 - 1) := not_terminated_at_n
  succ_nth_fib_le_of_nth_denom (Or.inr this)
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
have B_ineq : (fib (n + 1) : K) ≤ B :=
  haveI : ¬g.TerminatedAt (n - 1) := mt (terminated_stable n.pred_le) not_terminated_at_n
  succ_nth_fib_le_of_nth_denom (Or.inr this)
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
have zero_lt_B : 0 < B :=
  haveI : (0 : K) < fib (n + 1) := by exact_mod_cast fib_pos n.zero_lt_succ
  lt_of_lt_of_le this B_ineq
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
⊢ 0 < ↑(fib (n + 1))
[PROOFSTEP]
exact_mod_cast fib_pos n.zero_lt_succ
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
have zero_lt_mul_conts : 0 < B * nB :=
  by
  have : 0 < nB :=
    haveI : (0 : K) < fib (n + 2) := by exact_mod_cast fib_pos (n + 1).zero_lt_succ
    lt_of_lt_of_le this nB_ineq
  solve_by_elim [mul_pos]
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
⊢ 0 < B * nB
[PROOFSTEP]
have : 0 < nB :=
  haveI : (0 : K) < fib (n + 2) := by exact_mod_cast fib_pos (n + 1).zero_lt_succ
  lt_of_lt_of_le this nB_ineq
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
⊢ 0 < ↑(fib (n + 2))
[PROOFSTEP]
exact_mod_cast fib_pos (n + 1).zero_lt_succ
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
this : 0 < nB
⊢ 0 < B * nB
[PROOFSTEP]
solve_by_elim [mul_pos]
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
⊢ 1 / (B * nB) < ε
[PROOFSTEP]
suffices : 1 < ε * (B * nB)
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
this : 1 < ε * (B * nB)
⊢ 1 / (B * nB) < ε
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
⊢ 1 < ε * (B * nB)
[PROOFSTEP]
exact (div_lt_iff zero_lt_mul_conts).mpr this
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
⊢ 1 < ε * (B * nB)
[PROOFSTEP]
have one_lt_ε_mul_N : 1 < ε * n :=
  by
  have one_lt_ε_mul_N' : 1 < ε * (N' : K) := (div_lt_iff' ε_pos).mp one_div_ε_lt_N'
  have : (N' : K) ≤ N := by exact_mod_cast le_max_left _ _
  have : ε * N' ≤ ε * n := (mul_le_mul_left ε_pos).mpr (le_trans this (by exact_mod_cast n_ge_N))
  exact lt_of_lt_of_le one_lt_ε_mul_N' this
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
⊢ 1 < ε * ↑n
[PROOFSTEP]
have one_lt_ε_mul_N' : 1 < ε * (N' : K) := (div_lt_iff' ε_pos).mp one_div_ε_lt_N'
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N' : 1 < ε * ↑N'
⊢ 1 < ε * ↑n
[PROOFSTEP]
have : (N' : K) ≤ N := by exact_mod_cast le_max_left _ _
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N' : 1 < ε * ↑N'
⊢ ↑N' ≤ ↑N
[PROOFSTEP]
exact_mod_cast le_max_left _ _
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N' : 1 < ε * ↑N'
this : ↑N' ≤ ↑N
⊢ 1 < ε * ↑n
[PROOFSTEP]
have : ε * N' ≤ ε * n := (mul_le_mul_left ε_pos).mpr (le_trans this (by exact_mod_cast n_ge_N))
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N' : 1 < ε * ↑N'
this : ↑N' ≤ ↑N
⊢ ↑N ≤ ↑n
[PROOFSTEP]
exact_mod_cast n_ge_N
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N' : 1 < ε * ↑N'
this✝ : ↑N' ≤ ↑N
this : ε * ↑N' ≤ ε * ↑n
⊢ 1 < ε * ↑n
[PROOFSTEP]
exact lt_of_lt_of_le one_lt_ε_mul_N' this
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ 1 < ε * (B * nB)
[PROOFSTEP]
suffices : ε * n ≤ ε * (B * nB)
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
this : ε * ↑n ≤ ε * (B * nB)
⊢ 1 < ε * (B * nB)
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ε * ↑n ≤ ε * (B * nB)
[PROOFSTEP]
exact lt_of_lt_of_le one_lt_ε_mul_N this
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ε * ↑n ≤ ε * (B * nB)
[PROOFSTEP]
suffices : (n : K) ≤ B * nB
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
this : ↑n ≤ B * nB
⊢ ε * ↑n ≤ ε * (B * nB)
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑n ≤ B * nB
[PROOFSTEP]
exact (mul_le_mul_left ε_pos).mpr this
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑n ≤ B * nB
[PROOFSTEP]
show (n : K) ≤ B * nB
[GOAL]
case this
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑n ≤ B * nB
[PROOFSTEP]
calc
  (n : K) ≤ fib n := by exact_mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N
  _ ≤ fib (n + 1) := by exact_mod_cast fib_le_fib_succ
  _ ≤ fib (n + 1) * fib (n + 1) := by exact_mod_cast (fib (n + 1)).le_mul_self
  _ ≤ fib (n + 1) * fib (n + 2) :=
    (mul_le_mul_of_nonneg_left (by exact_mod_cast fib_le_fib_succ) (by exact_mod_cast (fib (n + 1)).zero_le))
  _ ≤ B * nB := mul_le_mul B_ineq nB_ineq (by exact_mod_cast (fib (n + 2)).zero_le) (le_of_lt zero_lt_B)
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑n ≤ ↑(fib n)
[PROOFSTEP]
exact_mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑(fib n) ≤ ↑(fib (n + 1))
[PROOFSTEP]
exact_mod_cast fib_le_fib_succ
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑(fib (n + 1)) ≤ ↑(fib (n + 1)) * ↑(fib (n + 1))
[PROOFSTEP]
exact_mod_cast (fib (n + 1)).le_mul_self
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ ↑(fib (n + 1)) ≤ ↑(fib (n + 2))
[PROOFSTEP]
exact_mod_cast fib_le_fib_succ
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ 0 ≤ ↑(fib (n + 1))
[PROOFSTEP]
exact_mod_cast (fib (n + 1)).zero_le
[GOAL]
K : Type u_1
v : K
inst✝² : LinearOrderedField K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
g : GeneralizedContinuedFraction K := of v
not_terminated_at_n : ¬TerminatedAt g n
B : K := denominators g n
nB : K := denominators g (n + 1)
abs_v_sub_conv_le : |v - convergents g n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
B_ineq : ↑(fib (n + 1)) ≤ B
zero_lt_B : 0 < B
zero_lt_mul_conts : 0 < B * nB
one_lt_ε_mul_N : 1 < ε * ↑n
⊢ 0 ≤ ↑(fib (n + 2))
[PROOFSTEP]
exact_mod_cast (fib (n + 2)).zero_le
[GOAL]
K : Type u_1
v : K
inst✝³ : LinearOrderedField K
inst✝² : FloorRing K
inst✝¹ : Archimedean K
inst✝ : OrderTopology K
⊢ Filter.Tendsto (convergents (of v)) Filter.atTop (nhds v)
[PROOFSTEP]
simpa [LinearOrderedAddCommGroup.tendsto_nhds, abs_sub_comm] using of_convergence_epsilon v


[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ TerminatedAt g n ↔ Stream'.Seq.TerminatedAt g.s n
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ TerminatedAt g n ↔ Stream'.Seq.get? g.s n = none
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ Stream'.Seq.get? (partialNumerators g) n = none ↔ Stream'.Seq.get? g.s n = none
[PROOFSTEP]
cases s_nth_eq : g.s.get? n
[GOAL]
case none
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
s_nth_eq : Stream'.Seq.get? g.s n = none
⊢ Stream'.Seq.get? (partialNumerators g) n = none ↔ none = none
[PROOFSTEP]
simp [partialNumerators, s_nth_eq]
[GOAL]
case some
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
val✝ : Pair α
s_nth_eq : Stream'.Seq.get? g.s n = some val✝
⊢ Stream'.Seq.get? (partialNumerators g) n = none ↔ some val✝ = none
[PROOFSTEP]
simp [partialNumerators, s_nth_eq]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ TerminatedAt g n ↔ Stream'.Seq.get? (partialNumerators g) n = none
[PROOFSTEP]
rw [terminatedAt_iff_s_none, part_num_none_iff_s_none]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ Stream'.Seq.get? (partialDenominators g) n = none ↔ Stream'.Seq.get? g.s n = none
[PROOFSTEP]
cases s_nth_eq : g.s.get? n
[GOAL]
case none
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
s_nth_eq : Stream'.Seq.get? g.s n = none
⊢ Stream'.Seq.get? (partialDenominators g) n = none ↔ none = none
[PROOFSTEP]
simp [partialDenominators, s_nth_eq]
[GOAL]
case some
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
val✝ : Pair α
s_nth_eq : Stream'.Seq.get? g.s n = some val✝
⊢ Stream'.Seq.get? (partialDenominators g) n = none ↔ some val✝ = none
[PROOFSTEP]
simp [partialDenominators, s_nth_eq]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
⊢ TerminatedAt g n ↔ Stream'.Seq.get? (partialDenominators g) n = none
[PROOFSTEP]
rw [terminatedAt_iff_s_none, part_denom_none_iff_s_none]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
gp : Pair α
s_nth_eq : Stream'.Seq.get? g.s n = some gp
⊢ Stream'.Seq.get? (partialNumerators g) n = some gp.a
[PROOFSTEP]
simp [partialNumerators, s_nth_eq]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
gp : Pair α
s_nth_eq : Stream'.Seq.get? g.s n = some gp
⊢ Stream'.Seq.get? (partialDenominators g) n = some gp.b
[PROOFSTEP]
simp [partialDenominators, s_nth_eq]
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
a : α
nth_part_num_eq : Stream'.Seq.get? (partialNumerators g) n = some a
⊢ ∃ gp, Stream'.Seq.get? g.s n = some gp ∧ gp.a = a
[PROOFSTEP]
simpa [partialNumerators, Stream'.Seq.map_get?] using nth_part_num_eq
[GOAL]
α : Type u_1
g : GeneralizedContinuedFraction α
n : ℕ
b : α
nth_part_denom_eq : Stream'.Seq.get? (partialDenominators g) n = some b
⊢ ∃ gp, Stream'.Seq.get? g.s n = some gp ∧ gp.b = b
[PROOFSTEP]
simpa [partialDenominators, Stream'.Seq.map_get?] using nth_part_denom_eq
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
A : K
nth_num_eq : numerators g n = A
⊢ ∃ conts, continuants g n = conts ∧ conts.a = A
[PROOFSTEP]
simpa
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
B : K
nth_denom_eq : denominators g n = B
⊢ ∃ conts, continuants g n = conts ∧ conts.b = B
[PROOFSTEP]
simpa
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
⊢ convergents g 0 = g.h
[PROOFSTEP]
simp [convergent_eq_num_div_denom, num_eq_conts_a, denom_eq_conts_b, div_one]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ continuantsAux g 2 = { a := gp.b * g.h + gp.a, b := gp.b }
[PROOFSTEP]
simp [zeroth_s_eq, continuantsAux, nextContinuants, nextDenominator, nextNumerator]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ continuants g 1 = { a := gp.b * g.h + gp.a, b := gp.b }
[PROOFSTEP]
simp [nth_cont_eq_succ_nth_cont_aux]
  -- porting note: simp used to work here, but now it can't figure out that 1 + 1 = 2
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ continuantsAux g (1 + 1) = { a := gp.b * g.h + gp.a, b := gp.b }
[PROOFSTEP]
convert second_continuant_aux_eq zeroth_s_eq
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ numerators g 1 = gp.b * g.h + gp.a
[PROOFSTEP]
simp [num_eq_conts_a, first_continuant_eq zeroth_s_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
gp : Pair K
zeroth_s_eq : Stream'.Seq.get? g.s 0 = some gp
⊢ denominators g 1 = gp.b
[PROOFSTEP]
simp [denom_eq_conts_b, first_continuant_eq zeroth_s_eq]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n : ℕ
inst✝ : DivisionRing K
⊢ convergents' g 0 = g.h
[PROOFSTEP]
simp [convergents']
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
h : Stream'.Seq.head s = none
n : ℕ
⊢ convergents'Aux s (n + 1) = 0
[PROOFSTEP]
simp [convergents'Aux, h, convergents'Aux.match_1]
[GOAL]
K : Type u_1
g : GeneralizedContinuedFraction K
n✝ : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
p : Pair K
h : Stream'.Seq.head s = some p
n : ℕ
⊢ convergents'Aux s (n + 1) = p.a / (p.b + convergents'Aux (Stream'.Seq.tail s) n)
[PROOFSTEP]
simp [convergents'Aux, h, convergents'Aux.match_1]


[GOAL]
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ a
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 ∣ 0
[PROOFSTEP]
exact ⟨0, by simp⟩
[GOAL]
α : Type u_1
inst✝ : SemigroupWithZero α
a : α
h : a = 0
⊢ 0 = 0 * 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : SemigroupWithZero α
a✝ a : α
⊢ a * 0 = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : CancelMonoidWithZero α
a b c : α
ha : a ≠ 0
d : α
⊢ a * c = a * b * d ↔ c = b * d
[PROOFSTEP]
rw [mul_assoc, mul_right_inj' ha]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a b c : α
hc : c ≠ 0
d : α
⊢ b * c = a * c * d ↔ b = a * d
[PROOFSTEP]
rw [mul_right_comm, mul_left_inj' hc]
[GOAL]
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ DvdNotUnit a b
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ a ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
b : α
hd : 0 ∣ b
hnd : ¬b ∣ 0
⊢ False
[PROOFSTEP]
exact hnd (dvd_zero _)
[GOAL]
case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x
[PROOFSTEP]
rcases hd with ⟨c, rfl⟩
[GOAL]
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ∃ x, ¬IsUnit x ∧ a * c = a * x
[PROOFSTEP]
refine' ⟨c, _, rfl⟩
[GOAL]
case right.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a c : α
hnd : ¬a * c ∣ a
⊢ ¬IsUnit c
[PROOFSTEP]
rintro ⟨u, rfl⟩
[GOAL]
case right.intro.intro
α : Type u_1
inst✝ : CommMonoidWithZero α
a : α
u : αˣ
hnd : ¬a * ↑u ∣ a
⊢ False
[PROOFSTEP]
simp at hnd
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
hx0 : x = 0
⊢ False
[PROOFSTEP]
simp [hx0] at hyx
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : x ∣ y ∧ ¬y ∣ x
d : α
hd : y = x * d
hyx : ¬y ∣ x
x✝ : d ∣ 1
e : α
he : 1 = d * e
⊢ x = y * e
[PROOFSTEP]
rw [hd, mul_assoc, ← he, mul_one]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
⊢ x * 1 = x * (d * e)
[PROOFSTEP]
conv =>
  lhs
  rw [he, hdx]
  simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1 = x * (d * e)
[PROOFSTEP]
  lhs
  rw [he, hdx]
  simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1 = x * (d * e)
[PROOFSTEP]
  lhs
  rw [he, hdx]
  simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1 = x * (d * e)
[PROOFSTEP]
lhs
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1
[PROOFSTEP]
rw [he, hdx]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * d * e * 1
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : MonoidWithZero α
p q : α
h₁ : q ≠ 0
h₂ : p ∣ q
⊢ p ≠ 0
[PROOFSTEP]
rcases h₂ with ⟨u, rfl⟩
[GOAL]
case intro
α : Type u_1
inst✝ : MonoidWithZero α
p u : α
h₁ : p * u ≠ 0
⊢ p ≠ 0
[PROOFSTEP]
exact left_ne_zero_of_mul h₁
[GOAL]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
a b : α
⊢ a ∣ b → b ∣ a → a = b
[PROOFSTEP]
rintro ⟨c, rfl⟩ ⟨d, hcd⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
a c d : α
hcd : a = a * c * d
⊢ a = a * c
[PROOFSTEP]
rw [mul_assoc, eq_comm, mul_right_eq_self₀, mul_eq_one] at hcd
[GOAL]
case intro.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
a c d : α
hcd : c = 1 ∧ d = 1 ∨ a = 0
⊢ a = a * c
[PROOFSTEP]
obtain ⟨rfl, -⟩ | rfl := hcd
[GOAL]
case intro.intro.inl.intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
a d : α
⊢ a = a * 1
[PROOFSTEP]
simp
[GOAL]
case intro.intro.inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Subsingleton αˣ
c d : α
⊢ 0 = 0 * c
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
⊢ inverse (a * b) = inverse b * inverse a
[PROOFSTEP]
by_cases hab : IsUnit (a * b)
[GOAL]
case pos
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a
[PROOFSTEP]
obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab
[GOAL]
case pos.intro.intro.intro
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀ˣ
h : Commute ↑a ↑b
hab : IsUnit (↑a * ↑b)
⊢ inverse (↑a * ↑b) = inverse ↑b * inverse ↑a
[PROOFSTEP]
rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]
[GOAL]
case neg
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a
[PROOFSTEP]
obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)
[GOAL]
case neg.inl
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
⊢ inverse (a * b) = inverse b * inverse a
[PROOFSTEP]
rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]
[GOAL]
case neg.inr
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ inverse (a * b) = inverse b * inverse a
[PROOFSTEP]
rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a / b) c
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
α : Type u_1
M₀ : Type u_2
G₀ : Type u_3
M₀' : Type u_4
G₀' : Type u_5
F : Type u_6
F' : Type u_7
inst✝¹ : MonoidWithZero M₀
inst✝ : GroupWithZero G₀
a b c : G₀
hac : Commute a c
hbc : Commute b c
⊢ Commute (a * b⁻¹) c
[PROOFSTEP]
exact hac.mul_left hbc.inv_left₀