awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
⊢ ∃ (c : E), c ≠ 0

Tactic:
exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
obtain : ∀ (c : E) (hc : c ≠ 0), AccPt x (𝓟 univ)
⊢ AccPt x (𝓟 univ)

Tactic:
obtain ⟨c, hc⟩ : ∃ (c : E), c ≠ 0 := exists_ne 0

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
apply : Tendsto (fun (x : ℕ) ↦ r ^ x • c) atTop (𝓝 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))
⊢ Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))

Tactic:
apply Tendsto.add tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
⊢ Tendsto (fun (x : ℕ) ↦ r ^ x • c) atTop (𝓝 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))

Tactic:
(tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).smul tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.smul, tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
⊢ Tendsto (fun (x : ℕ) ↦ r ^ x • c) atTop (𝓝 (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))

Tactic:
exact (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).smul tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.smul, tendsto_pow_atTop_nhds_zero_of_norm_lt_one
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
⊢ Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))

Tactic:
have A : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + (0 : 𝕜) • c)) := by
    apply Tendsto.add tendsto_const_nhds
    exact (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).smul tendsto_const_nhds
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))
⊢ Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 x)

Tactic:
simp only [zero_smul, add_zero] at A

Premises used: zero_smul, add_zero
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 x)
⊢ Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x)

Tactic:
simp [tendsto_nhdsWithin_iff, A, hc, norm_pos_iff.mp hr₀]

Premises used: norm_pos_iff, tendsto_nhdsWithin_iff, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))
⊢ Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x)

Tactic:
have B : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x) := by
    simp only [zero_smul, add_zero] at A
    simp [tendsto_nhdsWithin_iff, A, hc, norm_pos_iff.mp hr₀]
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))
B : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x)
⊢ AccPt x (𝓟 univ)

Tactic:
accPt_principal_iff_nhdsWithin.mpr ((atTop_neBot.map _).mono B)

Premises used: Iff.mpr, Filter.NeBot.mono, accPt_principal_iff_nhdsWithin, Filter.atTop_neBot, Filter.NeBot.map
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
x : E
hx : Membership.mem (γ := Set E) univ x
r : 𝕜
hr₀ : 0 < ‖r‖
hr : ‖r‖ < 1
c : E
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝 (x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 c))
B : Tendsto (fun (n : ℕ) ↦ x + r ^ n • c) atTop (𝓝[univ \ {x}] x)
⊢ AccPt x (𝓟 univ)

Tactic:
exact accPt_principal_iff_nhdsWithin.mpr ((atTop_neBot.map _).mono B)

Premises used: Iff.mpr, Filter.NeBot.mono, accPt_principal_iff_nhdsWithin, Filter.atTop_neBot, Filter.NeBot.map
-- Module: Mathlib.Topology.Algebra.Module.PerfectSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Nontrivial E
inst_4 : TopologicalSpace E
inst_5 : ContinuousAdd E
inst_6 : ContinuousSMul 𝕜 E
⊢ PerfectSpace 𝕜

Tactic:
perfectSpace_of_module 𝕜 𝕜

Premises used: perfectSpace_of_module
-- Module: Mathlib.Topology.Algebra.Module.Simple
Goal:
R : Type u
M : Type v
N : Type w
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : Module R N
inst_8 : ContinuousAdd M
inst_9 : IsSimpleModule R N
l : M →ₗ[R] N
inl :
  ∀ (hl : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑l : (a : M) → N)),
    IsClosed (↑l.ker : Set M) ∨ Dense (↑l.ker : Set M)
inr :
  IsClosed (↑(ker.{u, u, v, w} (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R) 0) : Set M) ∨
    Dense (↑(ker.{u, u, v, w} (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R) 0) : Set M)
⊢ IsClosed (↑l.ker : Set M) ∨ Dense (↑l.ker : Set M)

Tactic:
rcases l.surjective_or_eq_zero with (hl | rfl)

Premises used: LinearMap.surjective_or_eq_zero, rfl
-- Module: Mathlib.Topology.Algebra.Module.Simple
Goal:
R : Type u
M : Type v
N : Type w
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : Module R N
inst_8 : ContinuousAdd M
inst_9 : IsSimpleModule R N
l : M →ₗ[R] N
hl : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑l : (a : M) → N)
⊢ IsClosed (↑l.ker : Set M) ∨ Dense (↑l.ker : Set M)

Tactic:
(LinearMap.ker l).isClosed_or_dense_of_isCoatom (LinearMap.isCoatom_ker_of_surjective hl)

Premises used: LinearMap.ker, LinearMap.isCoatom_ker_of_surjective, Submodule.isClosed_or_dense_of_isCoatom
-- Module: Mathlib.Topology.Algebra.Module.Simple
Goal:
R : Type u
M : Type v
N : Type w
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : Module R N
inst_8 : ContinuousAdd M
inst_9 : IsSimpleModule R N
l : M →ₗ[R] N
hl : Function.Surjective.{v + 1, w + 1} (α := M) (β := N) (⇑l : (a : M) → N)
⊢ IsClosed (↑l.ker : Set M) ∨ Dense (↑l.ker : Set M)

Tactic:
exact (LinearMap.ker l).isClosed_or_dense_of_isCoatom (LinearMap.isCoatom_ker_of_surjective hl)

Premises used: LinearMap.ker, LinearMap.isCoatom_ker_of_surjective, Submodule.isClosed_or_dense_of_isCoatom
-- Module: Mathlib.Topology.Algebra.Module.Simple
Goal:
R : Type u
M : Type v
N : Type w
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : Module R N
inst_8 : ContinuousAdd M
inst_9 : IsSimpleModule R N
inr : IsClosed (↑⊤ : Set M) ∨ Dense (↑⊤ : Set M)
⊢ IsClosed (↑(ker.{u, u, v, w} (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R) 0) : Set M) ∨
    Dense (↑(ker.{u, u, v, w} (R₂ := R) (M₂ := N) (τ₁₂ := RingHom.id R) 0) : Set M)

Tactic:
rw [LinearMap.ker_zero]

Premises used: LinearMap.ker_zero
-- Module: Mathlib.Topology.Algebra.Module.Simple
Goal:
R : Type u
M : Type v
N : Type w
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : Module R N
inst_8 : ContinuousAdd M
inst_9 : IsSimpleModule R N
inr : IsClosed (↑⊤ : Set M)
⊢ IsClosed (↑⊤ : Set M) ∨ Dense (↑⊤ : Set M)

Tactic:
left
-- Module: Mathlib.Topology.Algebra.Module.Simple
Goal:
R : Type u
M : Type v
N : Type w
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : Module R N
inst_8 : ContinuousAdd M
inst_9 : IsSimpleModule R N
⊢ IsClosed (↑⊤ : Set M)

Tactic:
isClosed_univ

Premises used: isClosed_univ, Set.univ, setOf
-- Module: Mathlib.Topology.Algebra.Module.Simple
Goal:
R : Type u
M : Type v
N : Type w
inst : Ring R
inst_1 : TopologicalSpace R
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : ContinuousSMul R M
inst_7 : Module R N
inst_8 : ContinuousAdd M
inst_9 : IsSimpleModule R N
⊢ IsClosed (↑⊤ : Set M)

Tactic:
exact isClosed_univ

Premises used: isClosed_univ
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h :
  Eq (α := (a : A) → 𝕜)
    ((fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ ((⇑(↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) : (a : A) → 𝕜)) φ)
    ((fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ ((⇑(↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) : (a : A) → 𝕜)) ψ)
a : (↑φ : WeakDual 𝕜 A) = (↑ψ : WeakDual 𝕜 A)
⊢ φ = ψ

Tactic:
ext1
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h :
  Eq (α := (a : A) → 𝕜)
    ((fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ ((⇑(↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) : (a : A) → 𝕜)) φ)
    ((fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ ((⇑(↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) : (a : A) → 𝕜)) ψ)
a :
  ∀ (x : A),
    Eq.{u_1 + 1} (α := 𝕜) (((↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜) (((↑ψ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜)
⊢ (↑φ : WeakDual 𝕜 A) = (↑ψ : WeakDual 𝕜 A)

Tactic:
apply DFunLike.ext

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h :
  Eq (α := (a : A) → 𝕜)
    ((fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ ((⇑(↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) : (a : A) → 𝕜)) φ)
    ((fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ ((⇑(↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) : (a : A) → 𝕜)) ψ)
⊢ ∀ (x : A),
    Eq.{u_1 + 1} (α := 𝕜) (((↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜) (((↑ψ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜)

Tactic:
congr_fun h

Premises used: congr_fun
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h :
  Eq (α := (a : A) → 𝕜)
    ((fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ ((⇑(↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) : (a : A) → 𝕜)) φ)
    ((fun (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))) ↦ ((⇑(↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) : (a : A) → 𝕜)) ψ)
⊢ ∀ (x : A),
    Eq.{u_1 + 1} (α := 𝕜) (((↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜) (((↑ψ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜)

Tactic:
exact congr_fun h

Premises used: congr_fun
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
⊢ Eq (α := (a : A) → 𝕜) (⇑(↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) (⇑φ : (a : A) → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h : ∀ (x : A), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
⊢ φ = ψ

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
⊢ Eq (α := (a : A) → 𝕜) (⇑(toCLM φ) : (a : A) → 𝕜) (⇑φ : (a : A) → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
⊢ NonUnitalAlgHomClass (↑(characterSpace 𝕜 A) : Type (max u_1 u_2)) 𝕜 A 𝕜

Tactic:
{ CharacterSpace.instContinuousLinearMapClass with
    map_smulₛₗ := fun φ => map_smul φ
    map_zero := fun φ => map_zero φ
    map_mul := fun φ => φ.prop.2 }

Premises used: WeakDual.CharacterSpace.instContinuousLinearMapClass, NonUnitalAlgSemiHomClass.mk
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
⊢ Eq (α := (a : A) → 𝕜) (⇑(toNonUnitalAlgHom φ) : (a : A) → 𝕜) (⇑φ : (a : A) → 𝕜)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
inst_7 : Subsingleton A
φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
x : A
rw : Eq.{u_1 + 1} (α := 𝕜) (((↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) 0 : 𝕜) ((0 : (a : A) → 𝕜) 0 : 𝕜)
rw₁ : Eq.{u_1 + 1} (α := 𝕜) (0 : 𝕜) ((0 : (a : A) → 𝕜) 0 : 𝕜)
rw₂ rw₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ Eq.{u_1 + 1} (α := 𝕜) (((↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜) ((0 : (a : A) → 𝕜) x : 𝕜)

Tactic:
rw [show x = 0 from Subsingleton.elim x 0, map_zero, map_zero]

Premises used: map_zero, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
φ : WeakDual 𝕜 A
hφ : Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A))
    {φ : WeakDual 𝕜 A |
      ∀ (x y : A),
        (φ : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((φ : (a : A) → 𝕜) y : 𝕜)}
    φ

Tactic:
hφ.2

Premises used: Set.Mem, setOf, And.right
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
φ : WeakDual 𝕜 A
hφ : Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A))
    {φ : WeakDual 𝕜 A |
      ∀ (x y : A),
        (φ : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((φ : (a : A) → 𝕜) y : 𝕜)}
    φ

Tactic:
exact hφ.2

Premises used: And.right
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
x x_1 : A
⊢ (0 : (a : A) → 𝕜) (x * x_1) = HMul.hMul (α := 𝕜) (β := 𝕜) ((0 : (a : A) → 𝕜) x : 𝕜) ((0 : (a : A) → 𝕜) x_1 : 𝕜)

Tactic:
(zero_mul (0 : 𝕜)).symm

Premises used: MulZeroClass.zero_mul, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
x x_1 : A
⊢ (0 : (a : A) → 𝕜) (x * x_1) = HMul.hMul (α := 𝕜) (β := 𝕜) ((0 : (a : A) → 𝕜) x : 𝕜) ((0 : (a : A) → 𝕜) x_1 : 𝕜)

Tactic:
exact (zero_mul (0 : 𝕜)).symm

Premises used: MulZeroClass.zero_mul, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A))
    {φ : WeakDual 𝕜 A |
      ∀ (x y : A),
        (φ : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((φ : (a : A) → 𝕜) y : 𝕜)}
    0

Tactic:
exact fun _ _ => by exact (zero_mul (0 : 𝕜)).symm
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
inst_7 : T2Space 𝕜
inst_8 : ContinuousMul 𝕜
simp :
  IsClosed (X := WeakDual 𝕜 A)
    (⋂ (i : A),
      ⋂ (i_1 : A),
        {x : WeakDual 𝕜 A |
          (x : (a : A) → 𝕜) (i * i_1) =
            HMul.hMul (α := 𝕜) (β := 𝕜) ((x : (a : A) → 𝕜) i : 𝕜) ((x : (a : A) → 𝕜) i_1 : 𝕜)})
⊢ IsClosed (X := WeakDual 𝕜 A) (characterSpace 𝕜 A ∪ {0})

Tactic:
simp only [union_zero, Set.setOf_forall]

Premises used: WeakDual.CharacterSpace.union_zero, Set.setOf_forall
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
inst_7 : T2Space 𝕜
inst_8 : ContinuousMul 𝕜
⊢ IsClosed (X := WeakDual 𝕜 A)
    (⋂ (i : A),
      ⋂ (i_1 : A),
        {x : WeakDual 𝕜 A |
          (x : (a : A) → 𝕜) (i * i_1) =
            HMul.hMul (α := 𝕜) (β := 𝕜) ((x : (a : A) → 𝕜) i : 𝕜) ((x : (a : A) → 𝕜) i_1 : 𝕜)})

Tactic:
isClosed_iInter fun x =>
      isClosed_iInter fun y =>
        isClosed_eq (eval_continuous _) <| (eval_continuous _).mul (eval_continuous _)

Premises used: HMul.hMul, Continuous.mul, isClosed_eq, isClosed_iInter, WeakDual.eval_continuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommSemiring 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : NonUnitalNonAssocSemiring A
inst_5 : TopologicalSpace A
inst_6 : Module 𝕜 A
inst_7 : T2Space 𝕜
inst_8 : ContinuousMul 𝕜
⊢ IsClosed (X := WeakDual 𝕜 A)
    (⋂ (i : A),
      ⋂ (i_1 : A),
        {x : WeakDual 𝕜 A |
          (x : (a : A) → 𝕜) (i * i_1) =
            HMul.hMul (α := 𝕜) (β := 𝕜) ((x : (a : A) → 𝕜) i : 𝕜) ((x : (a : A) → 𝕜) i_1 : 𝕜)})

Tactic:
exact
    isClosed_iInter fun x =>
      isClosed_iInter fun y =>
        isClosed_eq (eval_continuous _) <| (eval_continuous _).mul (eval_continuous _)

Premises used: Continuous.mul, isClosed_eq, isClosed_iInter, WeakDual.eval_continuous
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : CommRing 𝕜
inst_1 : NoZeroDivisors 𝕜
inst_2 : TopologicalSpace 𝕜
inst_3 : ContinuousAdd 𝕜
inst_4 : ContinuousConstSMul 𝕜 𝕜
inst_5 : TopologicalSpace A
inst_6 : Semiring A
inst_7 : Algebra 𝕜 A
φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
rw :
  HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜) -
      HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) =
    0
rw₁ :
  HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜) =
    HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)
rw₂ : (φ : (a : A) → 𝕜) 1 = HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)
rw₃ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) ((φ : (a : A) → 𝕜) (HMul.hMul (α := A) 1 1) : 𝕜)
rw₄ rw₅ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)
⊢ HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0

Tactic:
rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]

Premises used: mul_sub, sub_eq_zero, map_mul, mul_one, one_mul