-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem hasFPowerSeriesOnBall_inverse_one_sub_smul [HasSummableGeomSeries A] (a : A) :
    HasFPowerSeriesOnBall (fun z : 𝕜 => Ring.inverse (1 - z • a))
      (fun n => ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) 0 ‖a‖₊⁻¹ :=
  { r_le

Proof state:
case zero
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
⊢ ‖a ^ 0‖₊ * r ^ 0 ≤ 1 ⊔ ‖1‖₊

Tactic:
simp only [le_refl, mul_one, or_true, le_max_iff, pow_zero]

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ EMetric.ball 0 (↑‖a‖₊)⁻¹
h : ¬‖a‖₊ = 0
⊢ ‖y • a‖ < 1

Tactic:
have nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹ := by
  simpa only [← coe_inv h, mem_ball_zero_iff, Metric.emetric_ball_nnreal] using hy

Result:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ EMetric.ball 0 (↑‖a‖₊)⁻¹
h : ¬‖a‖₊ = 0
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
⊢ ‖y • a‖ < 1

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ EMetric.ball 0 (↑‖a‖₊)⁻¹
⊢ ‖y • a‖ < 1

Tactic:
by_cases h : ‖a‖₊ = 0

Result:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ EMetric.ball 0 (↑‖a‖₊)⁻¹
h : ‖a‖₊ = 0
⊢ ‖y • a‖ < 1

case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ EMetric.ball 0 (↑‖a‖₊)⁻¹
h : ¬‖a‖₊ = 0
⊢ ‖y • a‖ < 1

Proof state:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : r * ‖a‖₊ < 1
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ n.succ ≤ 1

Tactic:
simpa only [← mul_pow, mul_comm] using pow_le_one' hr.le n.succ

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a ^ n‖₊ * r ^ n ≤ 1 ⊔ ‖1‖₊

Tactic:
rcases n with - | n

Result:
case zero
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
⊢ ‖a ^ 0‖₊ * r ^ 0 ≤ 1 ⊔ ‖1‖₊

case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a ^ (n + 1)‖₊ * r ^ (n + 1) ≤ 1 ⊔ ‖1‖₊

Proof state:
case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a‖₊ ^ n.succ * r ^ n.succ ≤ 1

Tactic:
by_cases h : ‖a‖₊ = 0

Result:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
h : ‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ n.succ ≤ 1

case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ n.succ ≤ 1

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
⊢ (↑‖a‖₊)⁻¹ ≤ radius fun n => ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)

Tactic:
refine le_of_forall_nnreal_lt fun r hr =>
  le_radius_of_bound_nnreal _ (max 1 ‖(1 : A)‖₊) fun n => ?_

Result:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)‖₊ * r ^ n ≤ 1 ⊔ ‖1‖₊

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ EMetric.ball 0 (↑‖a‖₊)⁻¹
norm_lt : ‖y • a‖ < 1
⊢ HasSum (fun n => (ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) fun x => y) (Ring.inverse (1 - (0 + y) • a))

Tactic:
simpa [← smul_pow, (summable_geometric_of_norm_lt_one norm_lt).hasSum_iff] using
  (NormedRing.inverse_one_sub _ norm_lt).symm

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ EMetric.ball 0 (↑‖a‖₊)⁻¹
h : ¬‖a‖₊ = 0
nnnorm_lt : ‖y‖₊ < ‖a‖₊⁻¹
⊢ ‖y • a‖ < 1

Tactic:
rwa [← coe_nnnorm, ← Real.lt_toNNReal_iff_coe_lt, Real.toNNReal_one, nnnorm_smul,
  ← NNReal.lt_inv_iff_mul_lt h]

Result:
no goals

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)‖₊ * r ^ n ≤ 1 ⊔ ‖1‖₊

Tactic:
rw [← norm_toNNReal, norm_mkPiRing, norm_toNNReal]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a ^ n‖₊ * r ^ n ≤ 1 ⊔ ‖1‖₊

Proof state:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
h : ‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ n.succ ≤ 1

Tactic:
simp only [h, zero_mul, zero_le', pow_succ']

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
y : 𝕜
hy : y ∈ EMetric.ball 0 (↑‖a‖₊)⁻¹
h : ‖a‖₊ = 0
⊢ ‖y • a‖ < 1

Tactic:
simp only [nnnorm_eq_zero.mp h, norm_zero, zero_lt_one, smul_zero]

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a ^ (n + 1)‖₊ * r ^ (n + 1) ≤ 1 ⊔ ‖1‖₊

Tactic:
refine
  le_trans (le_trans (mul_le_mul_right' (nnnorm_pow_le' a n.succ_pos) (r ^ n.succ)) ?_)
    (le_max_left _ _)

Result:
case succ
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
⊢ ‖a‖₊ ^ n.succ * r ^ n.succ ≤ 1

Proof state:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : ↑r < (↑‖a‖₊)⁻¹
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ n.succ ≤ 1

Tactic:
rw [← coe_inv h, coe_lt_coe, NNReal.lt_inv_iff_mul_lt h] at hr

Result:
case neg
𝕜 : Type u_1
A : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
a : A
r : ℝ≥0
hr : r * ‖a‖₊ < 1
n : ℕ
h : ¬‖a‖₊ = 0
⊢ ‖a‖₊ ^ n.succ * r ^ n.succ ≤ 1