awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
A : Type u_4
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a
⊢ (↑‖x‖₊ : ℝ) ∈ spectrum ℝ a
have this : 0 ≤ x
Tactic: have : 0 ≤ x := ha'.rightInvOn hx₁ ▸ NNReal.zero_le_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_4
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
ha' : SpectrumRestricts (R := ℝ≥0) (S := ℝ) a (⇑ContinuousMap.realToNNReal : (a : ℝ) → ℝ≥0)
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a
this : 0 ≤ x
⊢ (↑‖x‖₊ : ℝ) ∈ spectrum ℝ a
have h : (↑‖x‖₊ : ℝ) = x
Tactic: convert! hx₁
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_4
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
have obtain : ∀ (x : ℝ) (hx₁ : x ∈ spectrum ℝ a) (hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a),
  (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
Tactic: obtain ⟨x, hx₁, hx₂⟩ := spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty ha
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
A : Type u_4
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
a : A
ha : (spectrum ℝ a).Nonempty
x : ℝ
hx₁ : x ∈ spectrum ℝ a
hx₂ : (↑‖x‖₊ : ℝ≥0∞) = spectralRadius ℝ a
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
have simp : |x| ∈ spectrum ℝ a ∨ -|x| ∈ spectrum ℝ a
Tactic: simp only [← hx₂, ENNReal.coe_toReal, coe_nnnorm, Real.norm_eq_abs]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
R : Type u_3
S : Type u_4
A : Type u_5
inst : Semifield R
inst_1 : Field S
inst_2 : NonUnitalRing A
inst_3 : Algebra R S
inst_4 : Module R A
inst_5 : Module S A
inst_6 : IsScalarTower S A A
inst_7 : SMulCommClass S A A
inst_8 : IsScalarTower R S A
inst_9 : TopologicalSpace R
inst_10 : TopologicalSpace S
a : A
f : C(S, R)
h : QuasispectrumRestricts.{u_3, u_4, u_5} (R := R) (S := S) a (⇑f : (a : S) → R)
h_cpct : CompactSpace.{u_4} (↑(σₙ S a) : Type u_4)
⊢ CompactSpace.{u_3} (↑(σₙ R a) : Type u_3)
have rw : ∀ (h_cpct : IsCompact (σₙ S a)), IsCompact (σₙ R a)
Tactic: rw [← isCompact_iff_compactSpace] at h_cpct ⊢
Cleared hypotheses: h_cpct
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
⊢ ∀ (x : A), UpperHemicontinuousAt (spectrum 𝕜) x
have refine_1 : ∀ (a₀ : A), ∀ᶠ (x : A) in 𝓝 a₀, spectrum 𝕜 x ⊆ Metric.closedBall 0 ((‖a₀‖ + 1) * norm.{u_2} (E := A) 1)
Tactic: refine fun a₀ ↦ .of_sequences
    (isCompact_closedBall 0 ((‖a₀‖ + 1) * ‖(1 : A)‖)).isSeqCompact ?_ <|
    fun a ha x hx_mem x₀ hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
refine_1 : ∀ (a₀ : A), ∀ᶠ (x : A) in 𝓝 a₀, spectrum 𝕜 x ⊆ Metric.closedBall 0 ((‖a₀‖ + 1) * norm.{u_2} (E := A) 1)
⊢ ∀ (x : A), UpperHemicontinuousAt (spectrum 𝕜) x
have refine_2 : ∀ (a₀ : A) (a : ℕ → A) (ha : Tendsto a atTop (𝓝 a₀)) (x : ℕ → 𝕜) (hx_mem : ∀ (n : ℕ), x n ∈ spectrum 𝕜 (a n)) (x₀ : 𝕜)
  (hx : Tendsto x atTop (𝓝 x₀)), x₀ ∈ spectrum 𝕜 a₀
Tactic: refine fun a₀ ↦ .of_sequences
    (isCompact_closedBall 0 ((‖a₀‖ + 1) * ‖(1 : A)‖)).isSeqCompact ?_ <|
    fun a ha x hx_mem x₀ hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ : A
⊢ ∀ᶠ (x : A) in 𝓝 a₀, spectrum 𝕜 x ⊆ Metric.closedBall 0 ((‖a₀‖ + 1) * norm.{u_2} (E := A) 1)
have h : ∀ (a : A) (ha : a ∈ Metric.closedBall a₀ 1), spectrum 𝕜 a ⊆ Metric.closedBall 0 ((‖a₀‖ + 1) * norm.{u_2} (E := A) 1)
Tactic: filter_upwards [Metric.closedBall_mem_nhds a₀ zero_lt_one] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
⊢ spectrum 𝕜 a ⊆ Metric.closedBall 0 ((‖a₀‖ + 1) * norm.{u_2} (E := A) 1)
have apply : ‖a‖ * norm.{u_2} (E := A) 1 ≤ (‖a₀‖ + 1) * norm.{u_2} (E := A) 1
Tactic: apply spectrum.subset_closedBall_norm_mul a |>.trans <| Metric.closedBall_subset_closedBall ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
⊢ ‖a‖ * norm.{u_2} (E := A) 1 ≤ (‖a₀‖ + 1) * norm.{u_2} (E := A) 1
have hbc : ‖a‖ ≤ ‖a₀‖ + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
⊢ ‖a‖ ≤ ‖a₀‖ + 1
have hbc : ‖a₀‖ + ‖a - a₀‖ ≤ ‖a₀‖ + 1
Tactic: apply norm_le_norm_add_norm_sub' a a₀ |>.trans
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NormedRing A
inst_3 : NormedAlgebra 𝕜 A
inst_4 : CompleteSpace A
a₀ a : A
ha : a ∈ Metric.closedBall a₀ 1
⊢ ‖a₀‖ + ‖a - a₀‖ ≤ ‖a₀‖ + 1
have hbc : ‖a - a₀‖ ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
⊢ UpperHemicontinuous.{u_2, 0} (α := A) (spectrum ℝ≥0)
have h₂ : IsClosed (range NNReal.toReal)
Tactic: obtain ⟨⟨h₁, -⟩, h₂⟩ : IsClosedEmbedding ((↑) : ℝ≥0 → ℝ) := NNReal.isClosedEmbedding_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
h₂ : IsClosed (range NNReal.toReal)
⊢ UpperHemicontinuous.{u_2, 0} (α := A) (spectrum ℝ≥0)
have h₁ : IsInducing NNReal.toReal
Tactic: obtain ⟨⟨h₁, -⟩, h₂⟩ : IsClosedEmbedding ((↑) : ℝ≥0 → ℝ) := NNReal.isClosedEmbedding_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : CompleteSpace A
⊢ UpperHemicontinuous.{u_2, u_1} (α := A) (quasispectrum 𝕜)
have h : Eq (α := A → Set 𝕜) (quasispectrum 𝕜)
  (Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A))
Tactic: convert!
    upperHemicontinuous_spectrum 𝕜 (WithLp 1 (Unitization 𝕜 A)) |>.comp
      unitization_isometry_inr.continuous
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : CompleteSpace A
⊢ Eq (α := A → Set 𝕜) (quasispectrum 𝕜)
    (Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A))
have h : ∀ (a : A),
  quasispectrum 𝕜 a =
    Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) (fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A)) a
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : ProperSpace 𝕜
inst_2 : NonUnitalNormedRing A
inst_3 : NormedSpace 𝕜 A
inst_4 : SMulCommClass 𝕜 A A
inst_5 : IsScalarTower 𝕜 A A
inst_6 : CompleteSpace A
a : A
⊢ quasispectrum 𝕜 a =
    Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) (fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A)) a
have h : spectrum 𝕜 (A := WithLp 1 (Unitization 𝕜 A))
    ((AlgEquiv.symm (unitizationAlgEquiv 𝕜) : (a : Unitization 𝕜 A) → WithLp 1 (Unitization 𝕜 A))
        (↑a : Unitization 𝕜 A) :
      WithLp 1 (Unitization 𝕜 A)) =
  Function.comp (β := WithLp 1 (Unitization 𝕜 A)) (spectrum 𝕜) (fun (x : A) ↦ toLp 1 (↑x : Unitization 𝕜 A)) a
Tactic: rw [Unitization.quasispectrum_eq_spectrum_inr,
    ← AlgEquiv.spectrum_eq (unitizationAlgEquiv 𝕜 (𝕜 := 𝕜) (A := A) |>.symm)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : CompleteSpace A
⊢ UpperHemicontinuous.{u_2, 0} (α := A) (quasispectrum ℝ≥0)
have h₂ : IsClosed (range NNReal.toReal)
Tactic: obtain ⟨⟨h₁, -⟩, h₂⟩ := NNReal.isClosedEmbedding_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.Spectrum (hypothesis)
Goal:
A : Type u_2
inst : NonUnitalNormedRing A
inst_1 : NormedSpace ℝ A
inst_2 : SMulCommClass ℝ A A
inst_3 : IsScalarTower ℝ A A
inst_4 : CompleteSpace A
h₂ : IsClosed (range NNReal.toReal)
⊢ UpperHemicontinuous.{u_2, 0} (α := A) (quasispectrum ℝ≥0)
have h₁ : IsInducing NNReal.toReal
Tactic: obtain ⟨⟨h₁, -⟩, h₂⟩ := NNReal.isClosedEmbedding_coe
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
⊢ snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd
have simp_rw : (HSMul.hSMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1))).snd =
  HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
Tactic: simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
    ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
    Nat.cast_mul, mul_inv_rev,
    inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
simp_rw :
  (HSMul.hSMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1))).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
⊢ snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd
have simp_rw₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1)).snd =
  HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
Tactic: simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
    ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
    Nat.cast_mul, mul_inv_rev,
    inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
simp_rw :
  (HSMul.hSMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1))).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1)).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
⊢ snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd
have simp_rw₂ : HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ ((n + 1) • x.fst ^ (n + 1).pred • x.snd) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
Tactic: simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
    ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
    Nat.cast_mul, mul_inv_rev,
    inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
simp_rw :
  (HSMul.hSMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1))).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1)).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₂ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ ((n + 1) • x.fst ^ (n + 1).pred • x.snd) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
⊢ snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd
have simp_rw₃ : HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
    (HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1) : 𝕜) (x.fst ^ (n + 1).pred • x.snd)) =
  HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
Tactic: simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
    ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
    Nat.cast_mul, mul_inv_rev,
    inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
simp_rw :
  (HSMul.hSMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1))).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1)).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₂ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ ((n + 1) • x.fst ^ (n + 1).pred • x.snd) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₃ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1) : 𝕜) (x.fst ^ (n + 1).pred • x.snd)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
⊢ snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd
have simp_rw₄ : HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
  HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
Tactic: simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
    ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
    Nat.cast_mul, mul_inv_rev,
    inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
simp_rw :
  (HSMul.hSMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1))).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1)).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₂ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ ((n + 1) • x.fst ^ (n + 1).pred • x.snd) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₃ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1) : 𝕜) (x.fst ^ (n + 1).pred • x.snd)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₄ :
  HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
⊢ snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd
have simp_rw₅ : HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
Tactic: simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
    ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
    Nat.cast_mul, mul_inv_rev,
    inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt (goal)
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
simp_rw :
  (HSMul.hSMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1))).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1)).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₂ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ ((n + 1) • x.fst ^ (n + 1).pred • x.snd) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₃ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1) : 𝕜) (x.fst ^ (n + 1).pred • x.snd)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₄ :
  HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₅ :
  HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
⊢ snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd
have simp_rw₆ : HMul.hMul (α := 𝕜) (↑((n + 1) * n.factorial) : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
Tactic: simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
    ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
    Nat.cast_mul, mul_inv_rev,
    inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]