awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Ultra (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
n : ℕ
zero : nnnorm.{u_1} (E := R) (↑0 : R) ≤ 1
⊢ nnnorm.{u_1} (E := R) (↑n : R) ≤ 1
have succ : ∀ (n : ℕ) (hn : nnnorm.{u_1} (E := R) (↑n : R) ≤ 1), nnnorm.{u_1} (E := R) (↑(n + 1) : R) ≤ 1
Tactic: induction n with
  | zero => simp only [Nat.cast_zero, nnnorm_zero, zero_le]
  | succ n hn => simpa only [Nat.cast_add, Nat.cast_one, hn, max_eq_right] using
    nnnorm_add_one_le_max_nnnorm_one (n : R)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Ultra (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
z : ℤ
⊢ nnnorm.{u_1} (E := R) (↑z : R) ≤ 1
have ofNat : ∀ (a : ℕ), nnnorm.{u_1} (E := R) (↑(Int.ofNat a) : R) ≤ 1
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Ultra (goal)
Goal:
R : Type u_1
inst : SeminormedRing R
inst_1 : NormOneClass R
inst_2 : IsUltrametricDist R
z : ℤ
ofNat : ∀ (a : ℕ), nnnorm.{u_1} (E := R) (↑(Int.ofNat a) : R) ≤ 1
⊢ nnnorm.{u_1} (E := R) (↑z : R) ≤ 1
have negSucc : ∀ (a : ℕ), nnnorm.{u_1} (E := R) (↑(Int.negSucc a) : R) ≤ 1
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
⊢ ‖-((↑x⁻¹ : R) * t)‖ < 1
have a : Nontrivial R
Tactic: nontriviality R using zero_lt_one
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
⊢ ‖-((↑x⁻¹ : R) * t)‖ < 1
have hpos : 0 < ‖(↑x⁻¹ : R)‖
Tactic: have hpos : 0 < ‖(↑x⁻¹ : R)‖ := Units.norm_pos x⁻¹
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
hpos : 0 < ‖(↑x⁻¹ : R)‖
⊢ ‖-((↑x⁻¹ : R) * t)‖ = ‖(↑x⁻¹ : R) * t‖
have rw : ‖(↑x⁻¹ : R) * t‖ = ‖(↑x⁻¹ : R) * t‖
Tactic: rw [norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
hpos : 0 < ‖(↑x⁻¹ : R)‖
⊢ ‖(↑x⁻¹ : R)‖ * ‖t‖ < ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹
have nlinarith : ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹ ≤ ‖(↑x⁻¹ : R)‖ * ‖t‖ → HMul.hMul (α := ℝ) 1 1 = 1
Tactic: nlinarith only [h, hpos]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
hpos : 0 < ‖(↑x⁻¹ : R)‖
nlinarith nlinarith₁ : ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹ ≤ ‖(↑x⁻¹ : R)‖ * ‖t‖ → HMul.hMul (α := ℝ) 1 1 = 1
⊢ ‖(↑x⁻¹ : R)‖ * ‖t‖ < ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹
have nlinarith₂ : ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹ ≤ ‖(↑x⁻¹ : R)‖ * ‖t‖ →
  1 * ‖(↑x⁻¹ : R)‖ * (1 * ‖(↑x⁻¹ : R)‖⁻¹) - 1 * ‖(↑x⁻¹ : R)‖ * (1 * ‖t‖) +
      (0 - (1 * ‖t‖ - 1 * ‖(↑x⁻¹ : R)‖⁻¹) * (HMul.hMul (α := ℝ) 1 0 - 1 * ‖(↑x⁻¹ : R)‖)) =
    0
Tactic: nlinarith only [h, hpos]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
hpos : 0 < ‖(↑x⁻¹ : R)‖
⊢ ‖-((↑x⁻¹ : R) * t)‖ < 1
have by : ‖-((↑x⁻¹ : R) * t)‖ = ‖(↑x⁻¹ : R) * t‖
Tactic: 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
t : R
h : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
h_1 : Nontrivial R
hpos : 0 < ‖(↑x⁻¹ : R)‖
by : ‖-((↑x⁻¹ : R) * t)‖ = ‖(↑x⁻¹ : R) * t‖
⊢ ‖-((↑x⁻¹ : R) * t)‖ < 1
have by₁ : ‖(↑x⁻¹ : R)‖ * ‖t‖ < ‖(↑x⁻¹ : R)‖ * ‖(↑x⁻¹ : R)‖⁻¹
Tactic: 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : R | IsUnit x}
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
h : Nontrivial R
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {x : R | IsUnit x}
have rw : ∀ (x : R), Membership.mem (γ := Set R) {x : R | IsUnit x} x → ∃ ε > 0, Metric.ball x ε ⊆ {x : R | IsUnit x}
Tactic: rw [Metric.isOpen_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
h : Nontrivial R
x : Rˣ
⊢ ∃ ε > 0, Metric.ball (↑x : R) ε ⊆ {x : R | IsUnit x}
have refine : ∀ (y : R) (hy : y ∈ Metric.ball (↑x : R) ‖(↑x⁻¹ : R)‖⁻¹), Membership.mem (γ := Set R) {x : R | IsUnit x} y
Tactic: refine ⟨‖(↑x⁻¹ : R)‖⁻¹, _root_.inv_pos.mpr (Units.norm_pos x⁻¹), fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
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)‖⁻¹
⊢ Membership.mem (γ := Set R) {x : R | IsUnit x} y
have hy₁ : ‖y - (↑x : R)‖ < ‖(↑x⁻¹ : R)‖⁻¹
Tactic: rw [mem_ball_iff_norm] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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
⊢ ‖1 - x‖ < 1
have rwa : ∀ (h₁ : ‖1 - x‖ < 1), ‖1 - x‖ < 1
Tactic: rwa [mem_ball_iff_norm'] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
h : ‖t‖ < 1
⊢ (1 - t)⁻¹ʳ = (↑(Units.oneSub t h)⁻¹ : R)
have rw : (1 - t)⁻¹ʳ = (↑(Units.oneSub t h) : R)⁻¹ʳ
Tactic: rw [← inverse_unit (Units.oneSub t h), Units.val_oneSub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)⁻¹ʳ
⊢ (1 - t)⁻¹ʳ = (↑(Units.oneSub t h)⁻¹ : R)
have rw₁ : (1 - t)⁻¹ʳ = (1 - t)⁻¹ʳ
Tactic: rw [← inverse_unit (Units.oneSub t h), Units.val_oneSub]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
⊢ ∀ᶠ (t : R) in 𝓝 0, ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h : Nontrivial R
⊢ ∀ᶠ (t : R) in 𝓝 0, ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have rw : ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → ((↑x : R) + y)⁻¹ʳ = (1 + (↑x⁻¹ : R) * y)⁻¹ʳ * (↑x⁻¹ : R)
Tactic: rw [Metric.eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h : Nontrivial R
⊢ ‖(↑x⁻¹ : R)‖⁻¹ > 0
have cancel_denoms : LT.lt (α := ℝ) 0 1
Tactic: cancel_denoms
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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
⊢ ‖(↑x⁻¹ : R)‖⁻¹ > 0
have cancel_denoms₃ : 1 / 1 * (1 * HMul.hMul (α := ℝ) 1 0) < 1 / 1 * (1 * (1 * ‖(↑x⁻¹ : R)‖⁻¹))
Tactic: cancel_denoms
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h : Nontrivial R
⊢ ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → ((↑x : R) + y)⁻¹ʳ = (1 + (↑x⁻¹ : R) * y)⁻¹ʳ * (↑x⁻¹ : R)
have refine : ∀ (t : R) (ht : dist t 0 < ‖(↑x⁻¹ : R)‖⁻¹), ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
Tactic: refine ⟨‖(↑x⁻¹ : R)‖⁻¹, by cancel_denoms, fun t ht ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
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)‖⁻¹
⊢ ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have ht₁ : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
Tactic: rw [dist_zero_right] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
h : Nontrivial R
t : R
ht : ‖t‖ < ‖(↑x⁻¹ : R)‖⁻¹
⊢ ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have rw : (↑(x.add t ht) : R)⁻¹ʳ = (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)
⊢ ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have rw₁ : (↑(x.add t ht)⁻¹ : R) = (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)
⊢ ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have rw₂ : (↑((x * Units.oneSub (-((↑x⁻¹ : R) * t)) sorry).copy ((↑x : R) + t) sorry (↑(x * Units.oneSub (-((↑x⁻¹ : R) * t)) sorry)⁻¹ : R)
          sorry)⁻¹ :
    R) =
  (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)
⊢ ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have rw₃ : (↑(x * Units.oneSub (-((↑x⁻¹ : R) * t)) sorry)⁻¹ : R) = (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)
⊢ ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have rw₄ : (↑((Units.oneSub (-((↑x⁻¹ : R) * t)) sorry)⁻¹ * x⁻¹) : R) = (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)
⊢ ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have rw₅ : (↑(Units.oneSub (-((↑x⁻¹ : R) * t)) sorry)⁻¹ : R) * (↑x⁻¹ : R) = (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)
⊢ ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have rw₆ : (↑(Units.oneSub (-((↑x⁻¹ : R) * t)) sorry) : R)⁻¹ʳ * (↑x⁻¹ : R) = (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)
⊢ ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have rw₇ : (1 - -((↑x⁻¹ : R) * t))⁻¹ʳ * (↑x⁻¹ : R) = (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)
⊢ ((↑x : R) + t)⁻¹ʳ = (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R)
have rw₈ : (1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R) = (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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
⊢ HAdd.hAdd (α := R) (∑ i ∈ range n, t ^ i) (∑' (i : ℕ), t ^ (i + n)) = ∑ i ∈ range n, t ^ i + t ^ n * (1 - t)⁻¹ʳ
have simp : ∑ i ∈ range n, t ^ i + t ^ n * ∑' (i : ℕ), t ^ i = ∑ i ∈ range n, t ^ i + t ^ n * (↑(Units.oneSub t ht)⁻¹ : R)
Tactic: simp only [inverse_one_sub t ht, add_comm _ n, pow_add, this.tsum_mul_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
x : Rˣ
n : ℕ
⊢ ∀ᶠ (t : R) in 𝓝 0,
    ((↑x : R) + t)⁻¹ʳ = (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((↑x : R) + t)⁻¹ʳ
have hzero : 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 _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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) in 𝓝 0,
    ((↑x : R) + t)⁻¹ʳ = (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((↑x : R) + t)⁻¹ʳ
have 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)⁻¹ʳ
Tactic: filter_upwards [inverse_add x, hzero.eventually (inverse_one_sub_nth_order n)] with t ht ht'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
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)⁻¹ʳ
⊢ ((↑x : R) + t)⁻¹ʳ = (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((↑x : R) + t)⁻¹ʳ
have ht'₁ : (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'
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)⁻¹ʳ
| ((↑x : R) + t)⁻¹ʳ
have rw : (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((1 + (↑x⁻¹ : R) * t)⁻¹ʳ * (↑x⁻¹ : R))
Tactic: rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)⁻¹ʳ
⊢ ((↑x : R) + t)⁻¹ʳ = (∑ i ∈ range n, (-(↑x⁻¹ : R) * t) ^ i) * (↑x⁻¹ : R) + (-(↑x⁻¹ : R) * t) ^ n * ((↑x : R) + t)⁻¹ʳ
have 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)⁻¹ʳ
Tactic: conv_lhs => rw [ht, ht', add_mul, ← neg_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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)⁻¹ʳ
⊢ (∑ 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)⁻¹ʳ
have 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))
Tactic: rw [ht]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
⊢ IsBigO (E := R) (F := ℝ) (𝓝 0) (fun (t : R) ↦ (1 - t)⁻¹ʳ) fun (_t : R) ↦ 1
have simp : ∃ (c : ℝ), ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → ‖(1 - y)⁻¹ʳ‖ ≤ c * norm (E := ℝ) 1
Tactic: simp only [IsBigO, IsBigOWith, Metric.eventually_nhds_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
⊢ ∃ (c : ℝ), ∃ ε > 0, ∀ ⦃y : R⦄, dist y 0 < ε → ‖(1 - y)⁻¹ʳ‖ ≤ c * norm (E := ℝ) 1
have refine : ∀ (t : R) (ht : dist t 0 < 2⁻¹), ‖(1 - t)⁻¹ʳ‖ ≤ (norm.{u_1} (E := R) 1 + 1) * norm (E := ℝ) 1
Tactic: refine ⟨‖(1 : R)‖ + 1, (2 : ℝ)⁻¹, by simp, fun t ht ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : dist t 0 < 2⁻¹
⊢ ‖(1 - t)⁻¹ʳ‖ ≤ (norm.{u_1} (E := R) 1 + 1) * norm (E := ℝ) 1
have ht₁ : ‖t‖ < 2⁻¹
Tactic: rw [dist_zero_right] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
⊢ ‖t‖ < 1
have linarith : 1 ≤ ‖t‖ → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : HasSummableGeomSeries R
t : R
ht : ‖t‖ < 2⁻¹
linarith : 1 ≤ ‖t‖ → 2 / 2 = 1
⊢ ‖t‖ < 1
have linarith₁ : 1 ≤ ‖t‖ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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
⊢ ‖t‖ < 1
have linarith₂ : 1 ≤ ‖t‖ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Units (goal)
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
⊢ ‖t‖ < 1
have linarith₃ : 1 ≤ ‖t‖ → -1 + (2 * ‖t‖ - HMul.hMul (α := ℝ) 1 1) + 2 * (1 - ‖t‖) = 0
Tactic: linarith