awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Algebra.Basic
Goal:
K : Type u_1
L : Type u_2
inst : NontriviallyNormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
F : IntermediateField K L
k : K
hk : 1 < ‖k‖
⊢ 1 < norm.{u_2} (E := ↥F) ((algebraMap K ↥F : (a : K) → ↥F) k : ↥F)

Tactic:
simp [hk]
-- Module: Mathlib.Analysis.Normed.Algebra.Basic
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
⊢ norm (E := StrongDual 𝕜 A)
      ((toStrongDual : (a : WeakDual 𝕜 A) → StrongDual 𝕜 A) (↑φ : WeakDual 𝕜 A) : StrongDual 𝕜 A) ≤
    norm.{u_2} (E := A) 1

Tactic:
ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg (1 : A)) fun a =>
    mul_comm ‖a‖ ‖(1 : A)‖ ▸ spectrum.norm_le_norm_mul_of_mem (apply_mem_spectrum φ a)

Premises used: Norm.norm, WeakDual.CharacterSpace.apply_mem_spectrum, spectrum.norm_le_norm_mul_of_mem, Eq.rec, ContinuousLinearMap.opNorm_le_bound, mul_comm, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Algebra.Basic
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : ProperSpace 𝕜
rw : IsCompact (X := WeakDual 𝕜 A) (characterSpace 𝕜 A)
⊢ CompactSpace (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))

Tactic:
rw [← isCompact_iff_compactSpace]

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Analysis.Normed.Algebra.Basic
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : ProperSpace 𝕜
φ : WeakDual 𝕜 A
hφ : Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ
rw :
  norm (E := StrongDual 𝕜 A) ((toStrongDual : (a : WeakDual 𝕜 A) → StrongDual 𝕜 A) φ : StrongDual 𝕜 A) ≤
    norm.{u_2} (E := A) 1
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A))
    (Set.preimage (β := StrongDual 𝕜 A) (⇑toStrongDual : (a : WeakDual 𝕜 A) → StrongDual 𝕜 A)
      (Metric.closedBall 0 (norm.{u_2} (E := A) 1)))
    φ

Tactic:
rw [Set.mem_preimage, mem_closedBall_zero_iff]

Premises used: mem_closedBall_zero_iff, Set.mem_preimage
-- Module: Mathlib.Analysis.Normed.Algebra.Basic
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : ProperSpace 𝕜
φ : WeakDual 𝕜 A
hφ : Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ
⊢ norm (E := StrongDual 𝕜 A) ((toStrongDual : (a : WeakDual 𝕜 A) → StrongDual 𝕜 A) φ : StrongDual 𝕜 A) ≤
    norm.{u_2} (E := A) 1

Tactic:
(norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ :)

Premises used: Subtype.mk, And.right, And.left, WeakDual.CharacterSpace.norm_le_norm_one, And.intro
-- Module: Mathlib.Analysis.Normed.Algebra.Basic
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : ProperSpace 𝕜
φ : WeakDual 𝕜 A
hφ : Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ
⊢ norm (E := StrongDual 𝕜 A) ((toStrongDual : (a : WeakDual 𝕜 A) → StrongDual 𝕜 A) φ : StrongDual 𝕜 A) ≤
    norm.{u_2} (E := A) 1

Tactic:
exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ :)

Premises used: Subtype.mk, And.right, And.left, WeakDual.CharacterSpace.norm_le_norm_one, And.intro
-- Module: Mathlib.Analysis.Normed.Algebra.Basic
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : ProperSpace 𝕜
⊢ Subset (α := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A)
    (Set.preimage (β := StrongDual 𝕜 A) (⇑toStrongDual : (a : WeakDual 𝕜 A) → StrongDual 𝕜 A)
      (Metric.closedBall 0 (norm.{u_2} (E := A) 1)))

Tactic:
have h : characterSpace 𝕜 A ⊆ toStrongDual ⁻¹' Metric.closedBall 0 ‖(1 : A)‖ := by
    intro φ hφ
    rw [Set.mem_preimage, mem_closedBall_zero_iff]
    exact (norm_le_norm_one ⟨φ, ⟨hφ.1, hφ.2⟩⟩ :)
-- Module: Mathlib.Analysis.Normed.Algebra.Basic
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : ProperSpace 𝕜
h :
  Subset (α := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A)
    (Set.preimage (β := StrongDual 𝕜 A) (⇑toStrongDual : (a : WeakDual 𝕜 A) → StrongDual 𝕜 A)
      (Metric.closedBall 0 (norm.{u_2} (E := A) 1)))
⊢ IsCompact (X := WeakDual 𝕜 A) (characterSpace 𝕜 A)

Tactic:
(isCompact_closedBall 0 _).of_isClosed_subset CharacterSpace.isClosed h

Premises used: WeakDual.isCompact_closedBall, IsCompact.of_isClosed_subset, OfNat.ofNat, WeakDual.CharacterSpace.isClosed
-- Module: Mathlib.Analysis.Normed.Algebra.Basic
Goal:
𝕜 : Type u_1
A : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing A
inst_2 : NormedAlgebra 𝕜 A
inst_3 : CompleteSpace A
inst_4 : ProperSpace 𝕜
h :
  Subset (α := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A)
    (Set.preimage (β := StrongDual 𝕜 A) (⇑toStrongDual : (a : WeakDual 𝕜 A) → StrongDual 𝕜 A)
      (Metric.closedBall 0 (norm.{u_2} (E := A) 1)))
⊢ IsCompact (X := WeakDual 𝕜 A) (characterSpace 𝕜 A)

Tactic:
exact (isCompact_closedBall 0 _).of_isClosed_subset CharacterSpace.isClosed h

Premises used: WeakDual.isCompact_closedBall, IsCompact.of_isClosed_subset, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Algebra.DualNumber
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra ℚ R
inst_2 : UniformSpace R
inst_3 : IsTopologicalRing R
inst_4 : T2Space R
⊢ exp ε = HAdd.hAdd (α := R[ε]) 1 ε

Tactic:
exp_inr _

Premises used: TrivSqZeroExt.exp_inr, DualNumber.eps
-- Module: Mathlib.Analysis.Normed.Algebra.DualNumber
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra ℚ R
inst_2 : UniformSpace R
inst_3 : IsTopologicalRing R
inst_4 : T2Space R
r : R
rw : exp (HSMul.hSMul (β := R[ε]) r (inr 1)) = 1 + HSMul.hSMul (β := R[ε]) r (inr 1)
rw₁ : exp (inr (HSMul.hSMul (β := R) r 1)) = HAdd.hAdd (α := R[ε]) 1 (inr (HSMul.hSMul (β := R) r 1))
rw₂ rw₃ :
  HAdd.hAdd (α := TrivSqZeroExt R R) 1 (inr (HSMul.hSMul (β := R) r 1)) =
    HAdd.hAdd (α := R[ε]) 1 (inr (HSMul.hSMul (β := R) r 1))
⊢ exp (HSMul.hSMul (β := R[ε]) r ε) = 1 + HSMul.hSMul (β := R[ε]) r ε

Tactic:
rw [eps, ← inr_smul, exp_inr]

Premises used: TrivSqZeroExt.exp_inr, TrivSqZeroExt.inr_smul, DualNumber.eps
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
simp_rw :
  ∀ (n : ℕ),
    Eq (α := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (expSeries 𝕂 𝔸 n)
      (ofScalars 𝔸 (fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹) n)
simp_rw₁ :
  ∀ (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (β := ContinuousMultilinearMap 𝕂 (fun (i : Fin n) ↦ 𝔸) 𝔸) (↑n ! : 𝕂)⁻¹
        (ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸) =
      ofScalars 𝔸 (fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹) n
simp_rw₂ : ∀ (n : ℕ), True
⊢ Eq (α := FormalMultilinearSeries 𝕂 𝔸 𝔸) (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸)
    (ofScalars 𝔸 fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹ : FormalMultilinearSeries 𝕂 𝔸 𝔸)

Tactic:
simp_rw [FormalMultilinearSeries.ext_iff, expSeries, ofScalars, implies_true]

Premises used: FormalMultilinearSeries.ext_iff, implies_true, NormedSpace.expSeries, FormalMultilinearSeries.ofScalars
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸)
x : 𝔸
rw :
  Eq.{u_2 + 1} (α := 𝔸)
    (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
      FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x
    else 1)
    1
rw₁ rw₂ : Eq.{u_2 + 1} (α := 𝔸) 1 1
⊢ exp x = 1

Tactic:
rw [exp, dif_neg (not_nonempty_iff.mpr ‹_›)]

Premises used: Iff.mpr, NormedSpace.exp, dif_neg, not_nonempty_iff
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)

Tactic:
simp [expSeries]

Premises used: NormedSpace.expSeries
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
x : 𝔸
⊢ Eq.{u_2 + 1} (α := (n : ℕ) → 𝔸) (fun (n : ℕ) ↦ (expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x_1 : Fin n) ↦ x)
    fun (n : ℕ) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)

Tactic:
funext (expSeries_apply_eq x)

Premises used: NormedSpace.expSeries_apply_eq, funext
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
x : 𝔸
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
    ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)

Tactic:
tsum_congr fun n => expSeries_apply_eq x n

Premises used: tsum_congr, NormedSpace.expSeries_apply_eq, FormalMultilinearSeries.sum
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : Algebra ℚ 𝔸
h :
  ∀ (x : 𝔸),
    FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
      FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) =
    FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸)

Tactic:
ext
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : Algebra ℚ 𝔸
x : 𝔸
h :
  Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n))
    (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n))
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
    FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x

Tactic:
simp_rw [expSeries_sum_eq, inv_natCast_smul_eq 𝕂 ℚ]

Premises used: inv_natCast_smul_eq, Rat, NormedSpace.expSeries_sum_eq
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : Algebra ℚ 𝔸
n : ℕ
h :
  ∀ (c : (i : Fin n) → 𝔸),
    Eq (α := 𝔸) ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) c : 𝔸)
      ((expSeries ℚ 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) c : 𝔸)
⊢ Eq (α := (a : (i : Fin n) → 𝔸) → 𝔸) (⇑(expSeries 𝕂 𝔸 n) : (a : (i : Fin n) → 𝔸) → 𝔸)
    (⇑(expSeries ℚ 𝔸 n) : (a : (i : Fin n) → 𝔸) → 𝔸)

Tactic:
ext c
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : Algebra ℚ 𝔸
n : ℕ
c : (i : Fin n) → 𝔸
⊢ Eq (α := 𝔸) ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) c : 𝔸)
    ((expSeries ℚ 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) c : 𝔸)

Tactic:
simp [expSeries, inv_natCast_smul_eq 𝕂 ℚ]

Premises used: inv_natCast_smul_eq, Rat, NormedSpace.expSeries
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
h : ∀ (x : 𝔸), exp x = FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
⊢ exp = FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸)

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
h :
  (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
      FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x
    else 1) =
    FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
h₁ :
  FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) x =
    FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
h₂ h₃ :
  FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
    FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x
⊢ exp x = FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x

Tactic:
rw [exp, dif_pos ⟨RestrictScalars.algebra ℚ 𝕂 𝔸⟩, ← @expSeries_sum_eq_rat (𝕂 := 𝕂)]

Premises used: NormedSpace.exp, dif_pos, NormedSpace.expSeries_sum_eq_rat
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
rw :
  FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) = fun (x : 𝔸) ↦
    ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)
⊢ Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) exp fun (x : 𝔸) ↦
    ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)

Tactic:
rw [exp_eq_expSeries_sum 𝕂]

Premises used: NormedSpace.exp_eq_expSeries_sum
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
h :
  ∀ (x : 𝔸),
    FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
      ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) = fun (x : 𝔸) ↦
    ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
    ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)

Tactic:
expSeries_sum_eq x

Premises used: NormedSpace.expSeries_sum_eq
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
x : 𝔸
⊢ FormalMultilinearSeries.sum (expSeries 𝕂 𝔸 : FormalMultilinearSeries 𝕂 𝔸 𝔸) x =
    ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)

Tactic:
exact expSeries_sum_eq x

Premises used: NormedSpace.expSeries_sum_eq
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : Algebra ℚ 𝔸
⊢ Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) exp fun (x : 𝔸) ↦ ∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)

Tactic:
exp_eq_tsum ℚ

Premises used: NormedSpace.exp_eq_tsum, Rat
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
inst_5 : CharZero 𝕂
rw :
  Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) (fun (x : 𝔸) ↦ ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n))
    (ofScalarsSum.{u_1, u_2} (𝕜 := 𝕂) fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) (fun (x : 𝔸) ↦ ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n))
    fun (x : 𝔸) ↦ ∑' (n : ℕ), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (x ^ n)
⊢ Eq.{u_2 + 1} (α := (x : 𝔸) → 𝔸) exp (ofScalarsSum.{u_1, u_2} (𝕜 := 𝕂) fun (n : ℕ) ↦ (↑n ! : 𝕂)⁻¹)

Tactic:
rw [exp_eq_tsum 𝕂, ofScalarsSum_eq_tsum]

Premises used: NormedSpace.exp_eq_tsum, FormalMultilinearSeries.ofScalarsSum_eq_tsum
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
n : ℕ
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) 0 n) = Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n
⊢ Eq (α := 𝔸) ((expSeries 𝕂 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x : Fin n) ↦ 0 : 𝔸)
    (Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n : 𝔸)

Tactic:
rw [expSeries_apply_eq]

Premises used: NormedSpace.expSeries_apply_eq
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
n : ℕ
zero :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑0! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) (β := ℕ) 0 0) =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 0
succ :
  ∀ (n : ℕ),
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑(n + 1)! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) 0 (n + 1)) =
      Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑n ! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) 0 n) = Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n

Tactic:
rcases n with - | n
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑0! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) (β := ℕ) 0 0) =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝕂 : Type u_1
𝔸 : Type u_2
inst : Field 𝕂
inst_1 : Ring 𝔸
inst_2 : Algebra 𝕂 𝔸
inst_3 : TopologicalSpace 𝔸
inst_4 : IsTopologicalRing 𝔸
n : ℕ
succ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (β := 𝔸) (↑(n + 1)! : 𝕂)⁻¹ 0 = Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)
succ₁ : Eq.{u_2 + 1} (α := 𝔸) (0 : 𝔸) (Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1) : 𝔸)
succ₂ succ₃ : Eq.{u_2 + 1} (α := 𝔸) 0 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕂) (↑(n + 1)! : 𝕂)⁻¹ (HPow.hPow (α := 𝔸) 0 (n + 1)) =
    Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 (n + 1)

Tactic:
rw [zero_pow (Nat.succ_ne_zero _), smul_zero, Pi.single_eq_of_ne n.succ_ne_zero]

Premises used: smul_zero, Pi.single_eq_of_ne, Nat.succ_ne_zero, zero_pow
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
rw :
  Eq.{u_2 + 1} (α := 𝔸)
    (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
      FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0
    else 1)
    1
⊢ Eq.{u_2 + 1} (α := 𝔸) (exp 0) 1

Tactic:
rw [exp]

Premises used: NormedSpace.exp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
pos :
  ∀ (h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸)),
    FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0 = 1
neg : ¬Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) → Eq.{u_2 + 1} (α := 𝔸) 1 1
⊢ Eq.{u_2 + 1} (α := 𝔸)
    (if h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸) then
      FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0
    else 1)
    1

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
h : Nonempty.{u_2 + 1} (Algebra ℚ 𝔸)
pos : Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (HPow.hPow (α := 𝔸) 0 n)) 1
pos₁ : Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), (expSeries ℚ 𝔸 n : (a : (i : Fin n) → 𝔸) → 𝔸) fun (x : Fin n) ↦ 0) 1
pos₂ : Eq.{u_2 + 1} (α := 𝔸) (∑' (n : ℕ), Pi.single (M := fun (x : ℕ) ↦ 𝔸) 0 1 n) 1
⊢ FormalMultilinearSeries.sum (expSeries ℚ 𝔸 : FormalMultilinearSeries ℚ 𝔸 𝔸) 0 = 1

Tactic:
simp_rw [expSeries_sum_eq, ← expSeries_apply_eq, expSeries_apply_zero, tsum_pi_single]

Premises used: NormedSpace.expSeries_sum_eq, NormedSpace.expSeries_apply_eq, NormedSpace.expSeries_apply_zero, tsum_pi_single
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
h : ¬Nonempty.{u_2 + 1} (Algebra ℚ 𝔸)
⊢ Eq.{u_2 + 1} (α := 𝔸) 1 1

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸
inl : ∀ (h : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸)), exp (MulOpposite.op x) = MulOpposite.op (exp x)
inr : ∀ (val : Algebra ℚ 𝔸), exp (MulOpposite.op x) = MulOpposite.op (exp x)
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)

Tactic:
obtain h | ⟨⟨_⟩⟩ := isEmpty_or_nonempty (Algebra ℚ 𝔸)

Premises used: Rat, Algebra, isEmpty_or_nonempty
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸
h : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸)
⊢ IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸ᵐᵒᵖ)

Tactic:
have : IsEmpty (Algebra ℚ 𝔸ᵐᵒᵖ) := ⟨fun _ => h.elim <| (RingEquiv.opOp 𝔸).algebra ℚ⟩
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸
h : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸)
this : IsEmpty.{max (u_2 + 1) 1} (Algebra ℚ 𝔸ᵐᵒᵖ)
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸
val : Algebra ℚ 𝔸
inr :
  Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ)
    ((fun (x : 𝔸ᵐᵒᵖ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸ᵐᵒᵖ)) (MulOpposite.op x))
    (MulOpposite.op ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) x))
⊢ exp (MulOpposite.op x) = MulOpposite.op (exp x)

Tactic:
rw [exp_eq_tsum ℚ, exp_eq_tsum ℚ]

Premises used: NormedSpace.exp_eq_tsum, Rat
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸
val : Algebra ℚ 𝔸
inr inr₁ :
  Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (MulOpposite.op x ^ n))
    (MulOpposite.op (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
inr₂ :
  Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ) (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (MulOpposite.op (x ^ n)))
    (MulOpposite.op (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
inr₃ :
  Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ) (∑' (n : ℕ), MulOpposite.op (HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
    (MulOpposite.op (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n)))
⊢ Eq.{u_2 + 1} (α := 𝔸ᵐᵒᵖ)
    ((fun (x : 𝔸ᵐᵒᵖ) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸ᵐᵒᵖ)) (MulOpposite.op x))
    (MulOpposite.op ((fun (x : 𝔸) ↦ (∑' (n : ℕ), HSMul.hSMul (α := ℚ) (↑n ! : ℚ)⁻¹ (x ^ n) : 𝔸)) x))

Tactic:
simp_rw [← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]

Premises used: MulOpposite.op_pow, MulOpposite.op_smul, tsum_op
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
x : 𝔸ᵐᵒᵖ
h : ∀ (X : 𝔸), exp (MulOpposite.unop (MulOpposite.op X)) = MulOpposite.unop (exp (MulOpposite.op X))
⊢ exp (MulOpposite.unop x) = MulOpposite.unop (exp x)

Tactic:
induction x
-- Module: Mathlib.Analysis.Normed.Algebra.Exponential
Goal:
𝔸 : Type u_2
inst : Ring 𝔸
inst_1 : TopologicalSpace 𝔸
inst_2 : IsTopologicalRing 𝔸
inst_3 : T2Space 𝔸
X : 𝔸
⊢ exp (MulOpposite.unop (MulOpposite.op X)) = MulOpposite.unop (exp (MulOpposite.op X))

Tactic:
simp