awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
n : ℕ
hn : n ≠ 0
h : ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n‖ ≤ ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n
⊢ ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n‖ / (↑(n + 1).factorial : ℝ) ≤
    ‖HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)‖ ^ n / (↑n.factorial : ℝ)
have h₁ : n ≤ n + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
⊢ exp z ∈ spectrum 𝕜 (exp a)
have hb : Summable.{u_2, 0} (α := A) fun (n : ℕ) ↦
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
Tactic: have hb : Summable fun n : ℕ => ((n + 1).factorial⁻¹ : 𝕜) • (a - ↑ₐ z) ^ n := by
    refine .of_norm_bounded_eventually (Real.summable_pow_div_factorial ‖a - ↑ₐ z‖) ?_
    filter_upwards [Filter.eventually_cofinite_ne 0] with n hn
    rw [norm_smul, mul_comm, norm_inv, RCLike.norm_natCast, ← div_eq_mul_inv]
    gcongr
    · exact norm_pow_le' _ (pos_iff_ne_zero.mpr hn)
    · exact n.le_succ
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
hb :
  Summable.{u_2, 0} (α := A) fun (n : ℕ) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
⊢ exp z ∈ spectrum 𝕜 (exp a)
have h₀ : ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
  HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
Tactic: have h₀ : (∑' n : ℕ, ((n + 1).factorial⁻¹ : 𝕜) • (a - ↑ₐ z) ^ (n + 1)) = (a - ↑ₐ z) * b := by
    simpa only [mul_smul_comm, pow_succ'] using hb.tsum_mul_left (a - ↑ₐ z)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
hb :
  Summable.{u_2, 0} (α := A) fun (n : ℕ) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
h₀ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
⊢ exp z ∈ spectrum 𝕜 (exp a)
have h₁ : ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
  b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
Tactic: have h₁ : (∑' n : ℕ, ((n + 1).factorial⁻¹ : 𝕜) • (a - ↑ₐ z) ^ (n + 1)) = b * (a - ↑ₐ z) := by
    simpa only [pow_succ, Algebra.smul_mul_assoc] using hb.tsum_mul_right (a - ↑ₐ z)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
hb :
  Summable.{u_2, 0} (α := A) fun (n : ℕ) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
h₀ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
⊢ exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) = 1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
have rw : (fun (x : A) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x ^ n) : A))
    (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) =
  1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
Tactic: rw [exp_eq_tsum 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
hb :
  Summable.{u_2, 0} (α := A) fun (n : ℕ) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
h₀ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
⊢ (fun (x : A) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x ^ n) : A))
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) =
    1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
have h : 1 =
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(Nat.factorial 0) : 𝕜)⁻¹
    (HPow.hPow (β := ℕ) (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) 0)
Tactic: convert! (expSeries_summable' (𝕂 := 𝕜) (a - ↑ₐ z)).tsum_eq_zero_add
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
hb :
  Summable.{u_2, 0} (α := A) fun (n : ℕ) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
h₀ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
h :
  1 =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(Nat.factorial 0) : 𝕜)⁻¹
      (HPow.hPow (β := ℕ) (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) 0)
⊢ (fun (x : A) ↦ (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x ^ n) : A))
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) =
    1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
have h₂ : HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b =
  ∑' (b : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(b + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (b + 1))
Tactic: convert! (expSeries_summable' (𝕂 := 𝕜) (a - ↑ₐ z)).tsum_eq_zero_add
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
hb :
  Summable.{u_2, 0} (α := A) fun (n : ℕ) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
h₀ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
⊢ exp z ∈ spectrum 𝕜 (exp a)
have h₃ : exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) = 1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
Tactic: have h₃ : exp (a - ↑ₐ z) = 1 + (a - ↑ₐ z) * b := by
    rw [exp_eq_tsum 𝕜]
    convert! (expSeries_summable' (𝕂 := 𝕜) (a - ↑ₐ z)).tsum_eq_zero_add
    · simp only [Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, one_smul]
    · exact h₀.symm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : RCLike 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
a : A
z : 𝕜
hz : z ∈ spectrum 𝕜 a
this : NormedAlgebra ℚ A
hexpmul :
  exp a = HMul.hMul (β := A) (exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A))) ((↑ₐ : (a : 𝕜) → A) (exp z) : A)
b : A :=
  ∑' (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
hb :
  Summable.{u_2, 0} (α := A) fun (n : ℕ) ↦
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ n)
h₀ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
h₁ :
  ∑' (n : ℕ),
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
        (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) ^ (n + 1)) =
    b * HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)
h₃ : exp (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) = 1 + HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A) * b
⊢ exp z ∈ spectrum 𝕜 (exp a)
have rw : ¬((IsUnit (HSub.hSub (β := A) a ((↑ₐ : (a : 𝕜) → A) z : A)) ∧ IsUnit b) ∧
    IsUnit.{u_2} (M := A) ((↑ₐ : (a : 𝕜) → A) (exp z) : A))
Tactic: rw [spectrum.mem_iff, IsUnit.sub_iff, ← one_mul (↑ₐ (exp z)), hexpmul, ← _root_.sub_mul,
    Commute.isUnit_mul_iff (Algebra.commutes (exp z) (exp (a - ↑ₐ z) - 1)).symm,
    sub_eq_iff_eq_add'.mpr h₃, Commute.isUnit_mul_iff (h₀ ▸ h₁ : (a - ↑ₐ z) * b = b * (a - ↑ₐ z))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : CompleteSpace A
inst_3 : NormedAlgebra 𝕜 A
f : A →ₐ[𝕜] 𝕜
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) f.toContinuousLinearMap
have rw : Membership.mem (γ := Set (WeakDual 𝕜 A))
  {φ : WeakDual 𝕜 A |
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜) ∧
      ∀ (x y : A),
        (φ : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((φ : (a : A) → 𝕜) y : 𝕜)}
  f.toContinuousLinearMap
Tactic: rw [eq_set_map_one_map_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
⊢ Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
have rw : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (Ring.inverse (↑ha.unit : A)))
Tactic: rw [← Ring.inverse_unit]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
⊢ IsUnit a
have hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
Tactic: have hla₂ : Tendsto Ring.inverse (map (val S) l) (𝓝 (↑ha.unit⁻¹ : A)) := by
    rw [← Ring.inverse_unit]
    exact (NormedRing.inverse_continuousAt _).tendsto.comp <|
      continuousAt_subtype_val.tendsto.comp <| map_mono hla
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
mem : (↑ha.unit⁻¹ : A) ∈ S
⊢ IsUnit a
have refine_1 : a * Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem = 1
Tactic: refine ⟨⟨a, ⟨(↑ha.unit⁻¹ : A), mem⟩, ?_, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
mem : (↑ha.unit⁻¹ : A) ∈ S
refine_1 : a * Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem = 1
⊢ IsUnit a
have refine_2 : Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem * a = 1
Tactic: refine ⟨⟨a, ⟨(↑ha.unit⁻¹ : A), mem⟩, ?_, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
mem : (↑ha.unit⁻¹ : A) ∈ S
⊢ a * Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem = 1
have refine_1 : (↑(a * Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem) : A) = (↑1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
mem : (↑ha.unit⁻¹ : A) ∈ S
⊢ Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem * a = 1
have refine_2 : (↑(Subtype.mk (p := fun (x : A) ↦ x ∈ S) (↑ha.unit⁻¹ : A) mem * a) : A) = (↑1 : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
⊢ IsUnit a
have suffices : (↑ha.unit⁻¹ : A) ∈ S
Tactic: suffices mem : (↑ha.unit⁻¹ : A) ∈ S by
    refine ⟨⟨a, ⟨(↑ha.unit⁻¹ : A), mem⟩, ?_, ?_⟩, rfl⟩
    all_goals ext; simp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
⊢ (↑ha.unit⁻¹ : A) ∈ S
have apply : ∀ᶠ (x : A) in map (⇑(val S) : (a : ↥S) → A) l, Ring.inverse x ∈ (↑S : Set A)
Tactic: apply hS.mem_of_tendsto hla₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
⊢ ∀ᶠ (x : A) in map (⇑(val S) : (a : ↥S) → A) l, Ring.inverse x ∈ (↑S : Set A)
have rw : ∀ᶠ (a : ↥S) in l, Membership.mem (α := A) (↑S : Set A) (Ring.inverse ((val S : (a : ↥S) → A) a) : A)
Tactic: rw [Filter.eventually_map]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
⊢ ∀ᶠ (a : ↥S) in l, Membership.mem (α := A) (↑S : Set A) (Ring.inverse ((val S : (a : ↥S) → A) a) : A)
have apply : ∀ (x : ↥S) (hx : IsUnit x), Membership.mem (α := A) (↑S : Set A) (Ring.inverse ((val S : (a : ↥S) → A) x) : A)
Tactic: apply hl.mono fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
x : ↥S
hx : IsUnit x
⊢ Membership.mem (α := A) (↑S : Set A) (Ring.inverse ((val S : (a : ↥S) → A) x) : A)
have suffices : Eq (α := A) (Ring.inverse ((val S : (a : ↥S) → A) x) : A) ((val S : (a : ↥S) → A) (↑hx.unit⁻¹ : ↥S) : A)
Tactic: suffices Ring.inverse (val S x) = (val S ↑hx.unit⁻¹) from this ▸ Subtype.property _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_3
A : Type u_4
SA : Type u_5
inst : NormedRing A
inst_1 : CompleteSpace A
inst_2 : SetLike SA A
inst_3 : SubringClass SA A
inst_4 : NormedField 𝕜
inst_5 : NormedAlgebra 𝕜 A
instSMulMem : SMulMemClass SA 𝕜 A
S : SA
hS : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑S : Set A)
l : Filter ↥S
a : ↥S
ha : IsUnit (↑a : A)
hla : l ≤ 𝓝 a
hl : ∀ᶠ (x : ↥S) in l, IsUnit x
hl' : l.NeBot
hla₂ : Tendsto Ring.inverse (map (⇑(val S) : (a : ↥S) → A) l) (𝓝 (↑ha.unit⁻¹ : A))
x : ↥S
hx : IsUnit x
⊢ Eq (α := A) (Ring.inverse ((val S : (a : ↥S) → A) x) : A) ((val S : (a : ↥S) → A) (↑hx.unit⁻¹ : ↥S) : A)
have rw : (↑(IsUnit.unit (a :=
          ({ toFun := Subtype.val (p := fun (x : A) ↦ x ∈ S), map_one' := sorry, map_mul' := sorry, map_zero' := sorry,
                map_add' := sorry, commutes' := sorry : ↥S →ₐ[𝕜] A } :
              (a : ↥S) → A)
            x)
          sorry)⁻¹ :
    A) =
  ({ toFun := Subtype.val (p := fun (x : A) ↦ x ∈ S), map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry,
        commutes' := sorry } :
      (a : ↥S) → A)
    (↑hx.unit⁻¹ : ↥S)
Tactic: rw [← (hx.map (val S)).unit_spec, Ring.inverse_unit (hx.map (val S)).unit, val]