[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ ‖-(↑x⁻¹ * t)‖ < 1
[PROOFSTEP]
nontriviality R using zero_lt_one
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
✝ : Nontrivial R
⊢ ‖-(↑x⁻¹ * t)‖ < 1
[PROOFSTEP]
have hpos : 0 < ‖(↑x⁻¹ : R)‖ := Units.norm_pos x⁻¹
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
✝ : Nontrivial R
hpos : 0 < ‖↑x⁻¹‖
⊢ ‖-(↑x⁻¹ * t)‖ < 1
[PROOFSTEP]
calc
  ‖-(↑x⁻¹ * t)‖ = ‖↑x⁻¹ * t‖ := by rw [norm_neg]
  _ ≤ ‖(↑x⁻¹ : R)‖ * ‖t‖ := (norm_mul_le (x⁻¹).1 _)
  _ < ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹ := by nlinarith only [h, hpos]
  _ = 1 := mul_inv_cancel (ne_of_gt hpos)
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
✝ : Nontrivial R
hpos : 0 < ‖↑x⁻¹‖
⊢ ‖-(↑x⁻¹ * t)‖ = ‖↑x⁻¹ * t‖
[PROOFSTEP]
rw [norm_neg]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
✝ : Nontrivial R
hpos : 0 < ‖↑x⁻¹‖
⊢ ‖↑x⁻¹‖ * ‖t‖ < ‖↑x⁻¹‖ * ‖↑x⁻¹‖⁻¹
[PROOFSTEP]
nlinarith only [h, hpos]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
t : R
h : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ ↑x + t = ↑(x * oneSub (-(↑x⁻¹ * t)) (_ : ‖-(↑x⁻¹ * t)‖ < 1))
[PROOFSTEP]
simp [mul_add]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
y : R
h : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹
⊢ y = ↑(add x (y - ↑x) h)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ IsOpen {x | IsUnit x}
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
⊢ IsOpen {x | IsUnit x}
[PROOFSTEP]
apply Metric.isOpen_iff.mpr
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
⊢ ∀ (x : R), x ∈ {x | IsUnit x} → ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ {x | IsUnit x}
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
⊢ ∃ ε, ε > 0 ∧ Metric.ball (↑x) ε ⊆ {x | IsUnit x}
[PROOFSTEP]
refine' ⟨‖(↑x⁻¹ : R)‖⁻¹, _root_.inv_pos.mpr (Units.norm_pos x⁻¹), fun y hy ↦ _⟩
[GOAL]
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
y : R
hy : y ∈ Metric.ball ↑x ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}
[PROOFSTEP]
rw [mem_ball_iff_norm] at hy 
[GOAL]
case intro
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
✝ : Nontrivial R
x : Rˣ
y : R
hy : ‖y - ↑x‖ < ‖↑x⁻¹‖⁻¹
⊢ y ∈ {x | IsUnit x}
[PROOFSTEP]
exact (x.ofNearby y hy).isUnit
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : R
hx : x ∈ nonunits R
h₁ : x ∈ Metric.ball 1 1
⊢ ‖1 - x‖ < 1
[PROOFSTEP]
rwa [mem_ball_iff_norm'] at h₁ 
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
h : ‖t‖ < 1
⊢ inverse (1 - t) = ↑(Units.oneSub t h)⁻¹
[PROOFSTEP]
rw [← inverse_unit (Units.oneSub t h), Units.oneSub_val]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
[PROOFSTEP]
nontriviality R
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
[PROOFSTEP]
rw [Metric.eventually_nhds_iff]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ∃ ε, ε > 0 ∧ ∀ ⦃y : R⦄, dist y 0 < ε → inverse (↑x + y) = inverse (1 + ↑x⁻¹ * y) * ↑x⁻¹
[PROOFSTEP]
refine ⟨‖(↑x⁻¹ : R)‖⁻¹, by cancel_denoms, fun t ht ↦ ?_⟩
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ‖↑x⁻¹‖⁻¹ > 0
[PROOFSTEP]
cancel_denoms
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
⊢ ‖↑x⁻¹‖⁻¹ > 0
[PROOFSTEP]
cancel_denoms
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
t : R
ht : dist t 0 < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
[PROOFSTEP]
rw [dist_zero_right] at ht 
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
✝ : Nontrivial R
t : R
ht : ‖t‖ < ‖↑x⁻¹‖⁻¹
⊢ inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
[PROOFSTEP]
rw [← x.add_val t ht, inverse_unit, Units.add, Units.copy_eq, mul_inv_rev, Units.val_mul, ← inverse_unit,
  Units.oneSub_val, sub_neg_eq_add]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n => t ^ n
⊢ ∑ i in range n, t ^ i + ∑' (i : ℕ), t ^ (i + n) = ∑ i in range n, t ^ i + t ^ n * inverse (1 - t)
[PROOFSTEP]
simp only [inverse_one_sub t ht, add_comm _ n, pow_add, this.tsum_mul_left]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable fun n => t ^ n
⊢ ∑ i in range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i = ∑ i in range n, t ^ i + t ^ n * ↑(Units.oneSub t ht)⁻¹
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
n : ℕ
t : R
ht : dist t 0 < 1
⊢ ‖t‖ < 1
[PROOFSTEP]
rwa [← dist_zero_right]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
[PROOFSTEP]
have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) := (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
⊢ ∀ᶠ (t : R) in 𝓝 0, inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
[PROOFSTEP]
filter_upwards [inverse_add x, hzero.eventually (inverse_one_sub_nth_order n)] with t ht ht'
[GOAL]
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 - -↑x⁻¹ * t) = ∑ i in range n, (-↑x⁻¹ * t) ^ i + (-↑x⁻¹ * t) ^ n * inverse (1 - -↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
[PROOFSTEP]
rw [neg_mul, sub_neg_eq_add] at ht' 
[GOAL]
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ inverse (↑x + t) = (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
[PROOFSTEP]
conv_lhs => rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
| inverse (↑x + t)
[PROOFSTEP]
rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
| inverse (↑x + t)
[PROOFSTEP]
rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
| inverse (↑x + t)
[PROOFSTEP]
rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
[GOAL]
case h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
t : R
ht : inverse (↑x + t) = inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹
ht' : inverse (1 + ↑x⁻¹ * t) = ∑ i in range n, (-(↑x⁻¹ * t)) ^ i + (-(↑x⁻¹ * t)) ^ n * inverse (1 + ↑x⁻¹ * t)
⊢ (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * (inverse (1 + ↑x⁻¹ * t) * ↑x⁻¹) =
    (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * t) ^ n * inverse (↑x + t)
[PROOFSTEP]
rw [ht]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ (fun t => inverse (1 - t)) =O[𝓝 0] fun _t => 1
[PROOFSTEP]
simp only [IsBigO, IsBigOWith, Metric.eventually_nhds_iff]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ ∃ c ε, ε > 0 ∧ ∀ ⦃y : R⦄, dist y 0 < ε → ‖inverse (1 - y)‖ ≤ c * ‖1‖
[PROOFSTEP]
refine ⟨‖(1 : R)‖ + 1, (2 : ℝ)⁻¹, by norm_num, fun t ht ↦ ?_⟩
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ 2⁻¹ > 0
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : dist t 0 < 2⁻¹
⊢ ‖inverse (1 - t)‖ ≤ (‖1‖ + 1) * ‖1‖
[PROOFSTEP]
rw [dist_zero_right] at ht 
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
⊢ ‖inverse (1 - t)‖ ≤ (‖1‖ + 1) * ‖1‖
[PROOFSTEP]
have ht' : ‖t‖ < 1 := by
  have : (2 : ℝ)⁻¹ < 1 := by cancel_denoms
  linarith
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
⊢ ‖t‖ < 1
[PROOFSTEP]
have : (2 : ℝ)⁻¹ < 1 := by cancel_denoms
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
⊢ 2⁻¹ < 1
[PROOFSTEP]
cancel_denoms
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
⊢ 2⁻¹ < 1
[PROOFSTEP]
cancel_denoms
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
this : 2⁻¹ < 1
⊢ ‖t‖ < 1
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ ‖inverse (1 - t)‖ ≤ (‖1‖ + 1) * ‖1‖
[PROOFSTEP]
simp only [inverse_one_sub t ht', norm_one, mul_one, Set.mem_setOf_eq]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ ‖↑(Units.oneSub t ht')⁻¹‖ ≤ ‖1‖ + 1
[PROOFSTEP]
change ‖∑' n : ℕ, t ^ n‖ ≤ _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ + 1
[PROOFSTEP]
have := NormedRing.tsum_geometric_of_norm_lt_1 t ht'
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ + 1
[PROOFSTEP]
have : (1 - ‖t‖)⁻¹ ≤ 2 := by
  rw [← inv_inv (2 : ℝ)]
  refine' inv_le_inv_of_le (by norm_num) _
  have : (2 : ℝ)⁻¹ + (2 : ℝ)⁻¹ = 1 := by ring
  linarith
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ (1 - ‖t‖)⁻¹ ≤ 2
[PROOFSTEP]
rw [← inv_inv (2 : ℝ)]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ (1 - ‖t‖)⁻¹ ≤ 2⁻¹⁻¹
[PROOFSTEP]
refine' inv_le_inv_of_le (by norm_num) _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ 0 < 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ 2⁻¹ ≤ 1 - ‖t‖
[PROOFSTEP]
have : (2 : ℝ)⁻¹ + (2 : ℝ)⁻¹ = 1 := by ring
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
⊢ 2⁻¹ + 2⁻¹ = 1
[PROOFSTEP]
ring
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this✝ : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
this : 2⁻¹ + 2⁻¹ = 1
⊢ 2⁻¹ ≤ 1 - ‖t‖
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this✝ : ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ - 1 + (1 - ‖t‖)⁻¹
this : (1 - ‖t‖)⁻¹ ≤ 2
⊢ ‖∑' (n : ℕ), t ^ n‖ ≤ ‖1‖ + 1
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ (fun t => inverse (↑x + t)) =O[𝓝 0] fun _t => 1
[PROOFSTEP]
refine EventuallyEq.trans_isBigO (inverse_add x) (one_mul (1 : ℝ) ▸ ?_)
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ (fun x_1 => inverse (1 + ↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1
[PROOFSTEP]
simp only [← sub_neg_eq_add, ← neg_mul]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ (fun x_1 => inverse (1 - -↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1
[PROOFSTEP]
have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) := (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
hzero : Tendsto (fun x_1 => -↑x⁻¹ * x_1) (𝓝 0) (𝓝 0)
⊢ (fun x_1 => inverse (1 - -↑x⁻¹ * x_1) * ↑x⁻¹) =O[𝓝 0] fun _t => 1 * 1
[PROOFSTEP]
exact (inverse_one_sub_norm.comp_tendsto hzero).mul (isBigO_const_const _ one_ne_zero _)
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun t => inverse (↑x + t) - (∑ i in range n, (-↑x⁻¹ * t) ^ i) * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ n
[PROOFSTEP]
refine EventuallyEq.trans_isBigO (.sub (inverse_add_nth_order x n) (.refl _ _)) ?_
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 =>
      (∑ i in range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹ + (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1) -
        (∑ i in range n, (-↑x⁻¹ * x_1) ^ i) * ↑x⁻¹) =O[𝓝 0]
    fun t => ‖t‖ ^ n
[PROOFSTEP]
simp only [add_sub_cancel']
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n * inverse (↑x + x_1)) =O[𝓝 0] fun t => ‖t‖ ^ n
[PROOFSTEP]
refine ((isBigO_refl _ _).norm_right.mul (inverse_add_norm x)).trans ?_
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => ‖(-↑x⁻¹ * x_1) ^ n‖ * 1) =O[𝓝 0] fun t => ‖t‖ ^ n
[PROOFSTEP]
simp only [mul_one, isBigO_norm_left]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
n : ℕ
⊢ (fun x_1 => (-↑x⁻¹ * x_1) ^ n) =O[𝓝 0] fun t => ‖t‖ ^ n
[PROOFSTEP]
exact ((isBigO_refl _ _).norm_right.const_mul_left _).pow _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ (fun t => inverse (↑x + t) - ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖
[PROOFSTEP]
simpa using inverse_add_norm_diff_nth_order x 1
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ (fun t => inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =O[𝓝 0] fun t => ‖t‖ ^ 2
[PROOFSTEP]
convert inverse_add_norm_diff_nth_order x 2 using 2
[GOAL]
case h.e'_7.h
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
x✝ : R
⊢ inverse (↑x + x✝) - ↑x⁻¹ + ↑x⁻¹ * x✝ * ↑x⁻¹ = inverse (↑x + x✝) - (∑ i in range 2, (-↑x⁻¹ * x✝) ^ i) * ↑x⁻¹
[PROOFSTEP]
simp only [sum_range_succ, sum_range_zero, zero_add, pow_zero, pow_one, add_mul, one_mul, ← sub_sub, neg_mul,
  sub_neg_eq_add]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
⊢ ContinuousAt inverse ↑x
[PROOFSTEP]
have h_is_o : (fun t : R => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] (fun _ => 1 : R → ℝ) :=
  (inverse_add_norm_diff_first_order x).trans_isLittleO (isLittleO_id_const one_ne_zero).norm_left
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ ContinuousAt inverse ↑x
[PROOFSTEP]
have h_lim : Tendsto (fun y : R => y - x) (𝓝 x) (𝓝 0) :=
  by
  refine' tendsto_zero_iff_norm_tendsto_zero.mpr _
  exact tendsto_iff_norm_tendsto_zero.mp tendsto_id
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
[PROOFSTEP]
refine' tendsto_zero_iff_norm_tendsto_zero.mpr _
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
⊢ Tendsto (fun e => ‖e - ↑x‖) (𝓝 ↑x) (𝓝 0)
[PROOFSTEP]
exact tendsto_iff_norm_tendsto_zero.mp tendsto_id
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ ContinuousAt inverse ↑x
[PROOFSTEP]
rw [ContinuousAt, tendsto_iff_norm_tendsto_zero, inverse_unit]
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
x : Rˣ
h_is_o : (fun t => inverse (↑x + t) - ↑x⁻¹) =o[𝓝 0] fun x => 1
h_lim : Tendsto (fun y => y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ Tendsto (fun e => ‖inverse e - ↑x⁻¹‖) (𝓝 ↑x) (𝓝 0)
[PROOFSTEP]
simpa [(· ∘ ·)] using h_is_o.norm_left.tendsto_div_nhds_zero.comp h_lim
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ 1 ∈ I
[PROOFSTEP]
simpa only [show u.inv * x = 1 by simp] using I.mul_mem_left u.inv hxI
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
x : R
hxI : x ∈ I
hx : ‖1 - x‖ < 1
u : Rˣ := Units.oneSub (1 - x) hx
⊢ u.inv * x = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
hI : I ≠ ⊤
⊢ Ideal.closure I ≠ ⊤
[PROOFSTEP]
have h := closure_minimal (coe_subset_nonunits hI) nonunits.isClosed
[GOAL]
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
I : Ideal R
hI : I ≠ ⊤
h : closure ↑I ⊆ nonunits R
⊢ Ideal.closure I ≠ ⊤
[PROOFSTEP]
simpa only [I.closure.eq_top_iff_one, Ne.def] using mt (@h 1) one_not_mem_nonunits
