awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
h : Nontrivial R
x : Rˣ
refine : ∀ (y : R) (hy : y ∈ Metric.ball (↑x : R) ‖(↑x⁻¹ : R)‖⁻¹), Membership.mem (γ := Set R) {x : R | IsUnit x} y
⊢ ∃ ε > 0, Metric.ball (↑x : R) ε ⊆ {x : R | IsUnit x}

Tactic:
refine ⟨‖(↑x⁻¹ : R)‖⁻¹, _root_.inv_pos.mpr (Units.norm_pos x⁻¹), fun y hy ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
h : Nontrivial R
x : Rˣ
y : R
hy : y ∈ Metric.ball (↑x : R) ‖(↑x⁻¹ : R)‖⁻¹
⊢ ‖y - (↑x : R)‖ < ‖(↑x⁻¹ : R)‖⁻¹

Tactic:
rw [mem_ball_iff_norm] at hy

Premises used: mem_ball_iff_norm
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
h : Nontrivial R
x : Rˣ
y : R
hy : ‖y - (↑x : R)‖ < ‖(↑x⁻¹ : R)‖⁻¹
⊢ Membership.mem (γ := Set R) {x : R | IsUnit x} y

Tactic:
(x.ofNearby y hy).isUnit

Premises used: Units.ofNearby, Set.Mem, setOf, IsUnit, Units.isUnit
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
h : Nontrivial R
x : Rˣ
y : R
hy : ‖y - (↑x : R)‖ < ‖(↑x⁻¹ : R)‖⁻¹
⊢ Membership.mem (γ := Set R) {x : R | IsUnit x} y

Tactic:
exact (x.ofNearby y hy).isUnit

Premises used: Units.ofNearby, Units.isUnit
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ {x : R | IsUnit x} ∈ 𝓝 (↑x : R)

Tactic:
IsOpen.mem_nhds Units.isOpen x.isUnit

Premises used: Units.isOpen, IsOpen.mem_nhds, Units.isUnit
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : R
hx : x ∈ nonunits R
h₁ : Membership.mem (γ := Set R) (Metric.ball 1 1) x
rwa rwa₁ rwa₂ rwa₃ : ∀ (h₁ : ‖1 - x‖ < 1), ‖1 - x‖ < 1
⊢ ‖1 - x‖ < 1

Tactic:
rwa [mem_ball_iff_norm'] at h₁

Premises used: mem_ball_iff_norm'
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (nonunits R)

Tactic:
Units.isOpen.isClosed_compl

Premises used: Set.Mem, setOf, IsUnit, nonunits, IsOpen.isClosed_compl, Units.isOpen
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
h : ‖t‖ < 1
rw : (1 - t)⁻¹ʳ = (↑(Units.oneSub t h) : R)⁻¹ʳ
rw₁ rw₂ : (1 - t)⁻¹ʳ = (1 - t)⁻¹ʳ
⊢ (1 - t)⁻¹ʳ = (↑(Units.oneSub t h)⁻¹ : R)

Tactic:
rw [← inverse_unit (Units.oneSub t h), Units.val_oneSub]

Premises used: Units.oneSub, Ring.inverse_unit, Units.val_oneSub
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h : Nontrivial R
rw : ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → ((↑x : R) + y)⁻¹ʳ = (1 + (↑x⁻¹ : R) * y)⁻¹ʳ * (↑x⁻¹ : R)
⊢ ∀ᶠ (t : R) in 𝓝 0, ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)

Tactic:
rw [Metric.eventually_nhds_iff]

Premises used: Metric.eventually_nhds_iff
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h : Nontrivial R
cancel_denoms cancel_denoms₁ cancel_denoms₂ : LT.lt (α := ℝ) 0 1
cancel_denoms₃ : 1 / 1 * (1 * HMul.hMul (α := ℝ) 1 0) < 1 / 1 * (1 * (1 * ‖(↑x⁻¹ : R)‖⁻¹))
⊢ ‖(↑x⁻¹ : R)‖⁻¹ > 0

Tactic:
cancel_denoms
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h : Nontrivial R
refine : ∀ (t : R) (ht : dist t 0 < ‖(↑x⁻¹ : R)‖⁻¹), ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
⊢ ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → ((↑x : R) + y)⁻¹ʳ = (1 + (↑x⁻¹ : R) * y)⁻¹ʳ * (↑x⁻¹ : R)

Tactic:
refine ⟨‖(↑x⁻¹ : R)‖⁻¹, by cancel_denoms, fun t ht ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h : Nontrivial R
t : R
ht : dist t 0 < ‖(↑x⁻¹ : R)‖⁻¹
⊢ ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹

Tactic:
rw [dist_zero_right] at ht

Premises used: dist_zero_right
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h : Nontrivial R
t : R
ht : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
rw : (↑(x.add t ht) : R)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
rw₁ : (↑(x.add t ht)⁻¹ : R) = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
rw₂ :
  (↑((x * Units.oneSub (-((↑x⁻¹ : R) * t)) ⋯).copy ((↑x : R) + t) ⋯ (↑(x * Units.oneSub (-((↑x⁻¹ : R) * t)) ⋯)⁻¹ : R)
            ⋯)⁻¹ :
      R) =
    (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
rw₃ : (↑(x * Units.oneSub (-((↑x⁻¹ : R) * t)) ⋯)⁻¹ : R) = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
rw₄ : (↑((Units.oneSub (-((↑x⁻¹ : R) * t)) ⋯)⁻¹ * x⁻¹) : R) = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
rw₅ : (↑(Units.oneSub (-((↑x⁻¹ : R) * t)) ⋯)⁻¹ : R) * (↑x⁻¹ : R) = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
rw₆ : (↑(Units.oneSub (-((↑x⁻¹ : R) * t)) ⋯) : R)⁻¹ʳ * (↑x⁻¹ : R) = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
rw₇ : (1 - -((↑x⁻¹ : R) * t))⁻¹ʳ * (↑x⁻¹ : R) = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
rw₈ rw₉ : (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R) = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
⊢ ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)

Tactic:
rw [← x.val_add t ht, inverse_unit, Units.add, Units.copy_eq, mul_inv_rev, Units.val_mul,
    ← inverse_unit, Units.val_oneSub, sub_neg_eq_add]

Premises used: Units.copy_eq, Ring.inverse_unit, Units.val_add, Units.val_oneSub, mul_inv_rev, Units.add, Units.val_mul, sub_neg_eq_add
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ t ^ n
simp : ∑ i ∈ range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i = ∑ i ∈ range n, t ^ i + t ^ n * (↑(Units.oneSub t ht)⁻¹ : R)
⊢ HAdd.hAdd (α := R) (∑ i ∈ range n, t ^ i) (∑' (i : ℕ), t ^ (i + n)) = ∑ i ∈ range n, t ^ i + t ^ n * (1 - t)⁻¹ʳ

Tactic:
simp only [inverse_one_sub t ht, add_comm _ n, pow_add, this.tsum_mul_left]

Premises used: pow_add, Summable.tsum_mul_left, NormedRing.inverse_one_sub, add_comm
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
n : ℕ
t : R
ht : ‖t‖ < 1
this : Summable.{u_1, 0} (α := R) fun (n : ℕ) ↦ t ^ n
⊢ ∑ i ∈ range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i = ∑ i ∈ range n, t ^ i + t ^ n * (↑(Units.oneSub t ht)⁻¹ : R)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
n : ℕ
t : R
ht : dist t 0 < 1
rwa rwa₁ rwa₂ rwa₃ : dist t 0 < 1
⊢ ‖t‖ < 1

Tactic:
rwa [← dist_zero_right]

Premises used: dist_zero_right
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ Tendsto (β := R) (fun (x_1 : R) ↦ -(↑x⁻¹ : R) * x_1) (𝓝 0) (𝓝 0)

Tactic:
have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) :=
    (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
hzero : Tendsto (β := R) (fun (x_1 : R) ↦ -(↑x⁻¹ : R) * x_1) (𝓝 0) (𝓝 0)
h :
  ∀ (t : R) (ht : ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R))
    (ht' :
      (1 - -(↑x⁻¹ : R) * t)⁻¹ʳ =
        ∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i + (-(↑x⁻¹ : R) * t) ^ n * (1 - -(↑x⁻¹ : R) * t)⁻¹ʳ),
    ((↑x : R) + t)⁻¹ʳ = (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((↑x : R) + t)⁻¹ʳ
⊢ ∀ᶠ (t : R) in 𝓝 0,
    ((↑x : R) + t)⁻¹ʳ = (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((↑x : R) + t)⁻¹ʳ

Tactic:
filter_upwards [inverse_add x, hzero.eventually (inverse_one_sub_nth_order n)] with t ht ht'

Premises used: NormedRing.inverse_one_sub_nth_order, NormedRing.inverse_add, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
hzero : Tendsto (β := R) (fun (x_1 : R) ↦ -(↑x⁻¹ : R) * x_1) (𝓝 0) (𝓝 0)
t : R
ht : ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
ht' : (1 - -(↑x⁻¹ : R) * t)⁻¹ʳ = ∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i + (-(↑x⁻¹ : R) * t) ^ n * (1 - -(↑x⁻¹ : R) * t)⁻¹ʳ
⊢ (1 + (↑x⁻¹ : R) * t)⁻¹ʳ = ∑ i ∈ range n, (-((↑x⁻¹ : R) * t)) ^ i + (-((↑x⁻¹ : R) * t)) ^ n * (1 + (↑x⁻¹ : R) * t)⁻¹ʳ

Tactic:
rw [neg_mul, sub_neg_eq_add] at ht'

Premises used: neg_mul, sub_neg_eq_add
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
hzero : Tendsto (β := R) (fun (x_1 : R) ↦ -(↑x⁻¹ : R) * x_1) (𝓝 0) (𝓝 0)
t : R
ht : ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
ht' :
  (1 + (↑x⁻¹ : R) * t)⁻¹ʳ = ∑ i ∈ range n, (-((↑x⁻¹ : R) * t)) ^ i + (-((↑x⁻¹ : R) * t)) ^ n * (1 + (↑x⁻¹ : R) * t)⁻¹ʳ
rw :
  (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R))
| ((↑x : R) + t)⁻¹ʳ

Tactic:
rw [ht, ht', add_mul, ← neg_mul, mul_assoc]

Premises used: add_mul, mul_assoc, neg_mul
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
hzero : Tendsto (β := R) (fun (x_1 : R) ↦ -(↑x⁻¹ : R) * x_1) (𝓝 0) (𝓝 0)
t : R
ht : ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
ht' :
  (1 + (↑x⁻¹ : R) * t)⁻¹ʳ = ∑ i ∈ range n, (-((↑x⁻¹ : R) * t)) ^ i + (-((↑x⁻¹ : R) * t)) ^ n * (1 + (↑x⁻¹ : R) * t)⁻¹ʳ
h :
  (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)) =
    (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((↑x : R) + t)⁻¹ʳ
⊢ ((↑x : R) + t)⁻¹ʳ = (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((↑x : R) + t)⁻¹ʳ

Tactic:
conv_lhs => rw [ht, ht', add_mul, ← neg_mul, mul_assoc]

Premises used: add_mul, mul_assoc, neg_mul
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
hzero : Tendsto (β := R) (fun (x_1 : R) ↦ -(↑x⁻¹ : R) * x_1) (𝓝 0) (𝓝 0)
t : R
ht : ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
ht' :
  (1 + (↑x⁻¹ : R) * t)⁻¹ʳ = ∑ i ∈ range n, (-((↑x⁻¹ : R) * t)) ^ i + (-((↑x⁻¹ : R) * t)) ^ n * (1 + (↑x⁻¹ : R) * t)⁻¹ʳ
h h₁ :
  (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)) =
    (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R))
⊢ (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)) =
    (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((↑x : R) + t)⁻¹ʳ

Tactic:
rw [ht]
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
simp : ∃ (c : ℝ), ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → ‖(1 - y)⁻¹ʳ‖ ≤ c * norm (E := ℝ) 1
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ (1 - t)⁻¹ʳ) fun (_t : R) ↦ 1

Tactic:
simp only [IsBigO, IsBigOWith, Metric.eventually_nhds_iff]

Premises used: Asymptotics.IsBigOWith, Asymptotics.IsBigO, Metric.eventually_nhds_iff
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
⊢ GT.gt (α := ℝ) 2⁻¹ 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
refine : ∀ (t : R) (ht : dist t 0 < 2⁻¹), ‖(1 - t)⁻¹ʳ‖ ≤ (norm.{u_1} (E := R) 1 + 1) * norm (E := ℝ) 1
⊢ ∃ (c : ℝ), ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → ‖(1 - y)⁻¹ʳ‖ ≤ c * norm (E := ℝ) 1

Tactic:
refine ⟨‖(1 : R)‖ + 1, (2 : ℝ)⁻¹, by simp, fun t ht ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : dist t 0 < 2⁻¹
⊢ ‖t‖ < 2⁻¹

Tactic:
rw [dist_zero_right] at ht

Premises used: dist_zero_right
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
linarith : 1 ≤ ‖t‖ → 2 / 2 = 1
linarith₁ : 1 ≤ ‖t‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 ≤ ‖t‖ → GT.gt (α := ℝ) 2 0
linarith₃ : 1 ≤ ‖t‖ → -1 + (2 * ‖t‖ - HMul.hMul (α := ℝ) 1 1) + 2 * (1 - ‖t‖) = 0
linarith₄ : 1 ≤ ‖t‖ → GT.gt (α := ℝ) 2 0
⊢ ‖t‖ < 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
⊢ ‖t‖ < 1

Tactic:
have ht' : ‖t‖ < 1 := by linarith
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
simp : ‖(↑(Units.oneSub t ht')⁻¹ : R)‖ ≤ norm.{u_1} (E := R) 1 + 1
⊢ ‖(1 - t)⁻¹ʳ‖ ≤ (norm.{u_1} (E := R) 1 + 1) * norm (E := ℝ) 1

Tactic:
simp only [inverse_one_sub t ht', norm_one, mul_one]

Premises used: NormOneClass.norm_one, NormedRing.inverse_one_sub, mul_one
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
change : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 + 1
⊢ ‖(↑(Units.oneSub t ht')⁻¹ : R)‖ ≤ norm.{u_1} (E := R) 1 + 1

Tactic:
change ‖∑' n : ℕ, t ^ n‖ ≤ _
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
⊢ norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹

Tactic:
have := tsum_geometric_le_of_norm_lt_one t ht'
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
⊢ LT.lt (α := ℝ) 0 2

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
linarith : 1 - ‖t‖ < 2⁻¹ → 2 / 2 = 1
linarith₁ : 1 - ‖t‖ < 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 - ‖t‖ < 2⁻¹ → GT.gt (α := ℝ) 2 0
linarith₃ : 1 - ‖t‖ < 2⁻¹ → 2 / 2 = 1
linarith₄ : 1 - ‖t‖ < 2⁻¹ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : 1 - ‖t‖ < 2⁻¹ → GT.gt (α := ℝ) 2 0
linarith₆ :
  1 - ‖t‖ < 2⁻¹ → 2 * ‖t‖ - HMul.hMul (α := ℝ) 1 1 + (HMul.hMul (α := ℝ) 2 1 - 2 * ‖t‖ - HMul.hMul (α := ℝ) 1 1) = 0
⊢ 2⁻¹ ≤ 1 - ‖t‖

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
⊢ (1 - ‖t‖)⁻¹ ≤ 2

Tactic:
have : (1 - ‖t‖)⁻¹ ≤ 2 := inv_le_of_inv_le₀ (by simp) (by linarith)
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
ht' : ‖t‖ < 1
this_1 : norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 - 1 + (1 - ‖t‖)⁻¹
this : (1 - ‖t‖)⁻¹ ≤ 2
linarith : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → 2 / 2 = 1
linarith₁ : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) → GT.gt (α := ℝ) 2 0
linarith₃ :
  norm.{u_1} (E := R) 1 + 1 < norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) →
    1 * norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) -
            (1 * norm.{u_1} (E := R) 1 - HMul.hMul (α := ℝ) 1 1 + 1 * (1 - ‖t‖)⁻¹) +
          (1 * (1 - ‖t‖)⁻¹ - HMul.hMul (α := ℝ) 1 2) +
        (norm.{u_1} (E := R) 1 + 1 - norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n)) =
      0
⊢ norm.{u_1} (E := R) (∑' (n : ℕ), t ^ n) ≤ norm.{u_1} (E := R) 1 + 1

Tactic:
linarith
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ) fun (_t : R) ↦ 1

Tactic:
EventuallyEq.trans_isBigO (inverse_add x) (one_mul (1 : ℝ) ▸ ?_)

Premises used: Eq.rec, NormedRing.inverse_add, OfNat.ofNat, one_mul, Filter.EventuallyEq.trans_isBigO
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
refine :
  IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (1 + (↑x⁻¹ : R) * x_1)⁻¹ʳ * (↑x⁻¹ : R)) fun (_t : R) ↦
    HMul.hMul (α := ℝ) 1 1
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ) fun (_t : R) ↦ 1

Tactic:
refine EventuallyEq.trans_isBigO (inverse_add x) (one_mul (1 : ℝ) ▸ ?_)

Premises used: NormedRing.inverse_add, Filter.EventuallyEq.trans_isBigO
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
simp :
  IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (1 - -(↑x⁻¹ : R) * x_1)⁻¹ʳ * (↑x⁻¹ : R)) fun (_t : R) ↦
    HMul.hMul (α := ℝ) 1 1
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (1 + (↑x⁻¹ : R) * x_1)⁻¹ʳ * (↑x⁻¹ : R)) fun (_t : R) ↦
    HMul.hMul (α := ℝ) 1 1

Tactic:
simp only [← sub_neg_eq_add, ← neg_mul]

Premises used: neg_mul, sub_neg_eq_add
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ Tendsto (β := R) (fun (x_1 : R) ↦ -(↑x⁻¹ : R) * x_1) (𝓝 0) (𝓝 0)

Tactic:
have hzero : Tendsto (-(↑x⁻¹ : R) * ·) (𝓝 0) (𝓝 0) :=
    (mulLeft_continuous _).tendsto' _ _ <| mul_zero _
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
hzero : Tendsto (β := R) (fun (x_1 : R) ↦ -(↑x⁻¹ : R) * x_1) (𝓝 0) (𝓝 0)
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (1 - -(↑x⁻¹ : R) * x_1)⁻¹ʳ * (↑x⁻¹ : R)) fun (_t : R) ↦
    HMul.hMul (α := ℝ) 1 1

Tactic:
(inverse_one_sub_norm.comp_tendsto hzero).mul (isBigO_const_const _ one_ne_zero _)

Premises used: NormedRing.inverse_one_sub_norm, Asymptotics.IsBigO.mul, Ring.inverse, Asymptotics.isBigO_const_const, dite, Asymptotics.IsBigO.comp_tendsto, one_ne_zero
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
hzero : Tendsto (β := R) (fun (x_1 : R) ↦ -(↑x⁻¹ : R) * x_1) (𝓝 0) (𝓝 0)
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (1 - -(↑x⁻¹ : R) * x_1)⁻¹ʳ * (↑x⁻¹ : R)) fun (_t : R) ↦
    HMul.hMul (α := ℝ) 1 1

Tactic:
exact (inverse_one_sub_norm.comp_tendsto hzero).mul (isBigO_const_const _ one_ne_zero _)

Premises used: NormedRing.inverse_one_sub_norm, Asymptotics.IsBigO.mul, Asymptotics.isBigO_const_const, Asymptotics.IsBigO.comp_tendsto, one_ne_zero
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R))
    fun (t : R) ↦ ‖t‖ ^ n

Tactic:
EventuallyEq.trans_isBigO (.fun_sub (inverse_add_nth_order x n) (.refl _ _)) ?_

Premises used: Filter.EventuallyEq.fun_sub, Filter.EventuallyEq.refl, NormedRing.inverse_add_nth_order, Filter.EventuallyEq.trans_isBigO
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
refine :
  IsBigO (E := R) (F := ℝ) (𝓝 0)
    (fun (i : R) ↦
      (∑ i_1 ∈ range n, (-(↑x⁻¹ : R) * i) ^ i_1) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * i) ^ n * ((↑x : R) + i)⁻¹ʳ -
        (∑ i_1 ∈ range n, (-(↑x⁻¹ : R) * i) ^ i_1) * (↑x⁻¹ : R))
    fun (t : R) ↦ ‖t‖ ^ n
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R))
    fun (t : R) ↦ ‖t‖ ^ n

Tactic:
refine EventuallyEq.trans_isBigO (.fun_sub (inverse_add_nth_order x n) (.refl _ _)) ?_

Premises used: Filter.EventuallyEq.fun_sub, Filter.EventuallyEq.refl, NormedRing.inverse_add_nth_order, Filter.EventuallyEq.trans_isBigO
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
simp : IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (i : R) ↦ (-(↑x⁻¹ : R) * i) ^ n * ((↑x : R) + i)⁻¹ʳ) fun (t : R) ↦ ‖t‖ ^ n
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0)
    (fun (i : R) ↦
      (∑ i_1 ∈ range n, (-(↑x⁻¹ : R) * i) ^ i_1) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * i) ^ n * ((↑x : R) + i)⁻¹ʳ -
        (∑ i_1 ∈ range n, (-(↑x⁻¹ : R) * i) ^ i_1) * (↑x⁻¹ : R))
    fun (t : R) ↦ ‖t‖ ^ n

Tactic:
simp only [add_sub_cancel_left]

Premises used: add_sub_cancel_left
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (i : R) ↦ (-(↑x⁻¹ : R) * i) ^ n * ((↑x : R) + i)⁻¹ʳ) fun (t : R) ↦ ‖t‖ ^ n

Tactic:
((isBigO_refl _ _).norm_right.mul (inverse_add_norm x)).trans ?_

Premises used: Asymptotics.IsBigO.mul, NormedRing.inverse_add_norm, Asymptotics.IsBigO.trans
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
refine : IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ ‖(-(↑x⁻¹ : R) * x_1) ^ n‖ * 1) fun (t : R) ↦ ‖t‖ ^ n
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (i : R) ↦ (-(↑x⁻¹ : R) * i) ^ n * ((↑x : R) + i)⁻¹ʳ) fun (t : R) ↦ ‖t‖ ^ n

Tactic:
refine ((isBigO_refl _ _).norm_right.mul (inverse_add_norm x)).trans ?_

Premises used: Asymptotics.IsBigO.mul, NormedRing.inverse_add_norm, Asymptotics.IsBigO.trans
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
simp : IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (-(↑x⁻¹ : R) * x_1) ^ n) fun (t : R) ↦ ‖t‖ ^ n
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ ‖(-(↑x⁻¹ : R) * x_1) ^ n‖ * 1) fun (t : R) ↦ ‖t‖ ^ n

Tactic:
simp only [mul_one, isBigO_norm_left]

Premises used: Asymptotics.isBigO_norm_left, mul_one
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (-(↑x⁻¹ : R) * x_1) ^ n) fun (t : R) ↦ ‖t‖ ^ n

Tactic:
((isBigO_refl _ _).norm_right.const_mul_left _).pow _

Premises used: Asymptotics.IsBigO.const_mul_left, Asymptotics.IsBigO.pow
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (x_1 : R) ↦ (-(↑x⁻¹ : R) * x_1) ^ n) fun (t : R) ↦ ‖t‖ ^ n

Tactic:
exact ((isBigO_refl _ _).norm_right.const_mul_left _).pow _

Premises used: Asymptotics.IsBigO.const_mul_left, Asymptotics.IsBigO.pow
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R)) fun (t : R) ↦ ‖t‖

Tactic:
simpa using inverse_add_norm_diff_nth_order x 1

Premises used: NormedRing.inverse_add_norm_diff_nth_order, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (∑ i ∈ range 2, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R))
    fun (t : R) ↦ HPow.hPow (β := ℕ) ‖t‖ 2

Tactic:
inverse_add_norm_diff_nth_order x 2

Premises used: NormedRing.inverse_add_norm_diff_nth_order, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Ring.Units
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h :
  ∀ (x_1 : R),
    ((↑x : R) + x_1)⁻¹ʳ - (↑x⁻¹ : R) + (↑x⁻¹ : R) * x_1 * (↑x⁻¹ : R) =
      ((↑x : R) + x_1)⁻¹ʳ - (∑ i ∈ range 2, (-(↑x⁻¹ : R) * x_1) ^ i) * (↑x⁻¹ : R)
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R) + (↑x⁻¹ : R) * t * (↑x⁻¹ : R))
    fun (t : R) ↦ HPow.hPow (β := ℕ) ‖t‖ 2

Tactic:
convert! inverse_add_norm_diff_nth_order x 2 using 2

Premises used: NormedRing.inverse_add_norm_diff_nth_order, OfNat.ofNat