awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
⊢ HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0

Tactic:
have h₁ : φ 1 * (1 - φ 1) = 0 := by rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
-- 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))
h₁ : HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0
inl :
  ∀ (h₂ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (0 : 𝕜)),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
inr :
  ∀ (h₂ : HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) = 0),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)

Tactic:
rcases mul_eq_zero.mp h₁ with (h₂ | h₂)

Premises used: mul_eq_zero, Iff.mp
-- 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))
h₁ : HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0
h₂ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (0 : 𝕜)
a : A
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) (a * 1) : 𝕜) (0 : 𝕜)

Tactic:
simp only [map_mul φ, h₂, mul_zero]

Premises used: MulZeroClass.mul_zero, map_mul
-- 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))
h₁ : HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0
h₂ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (0 : 𝕜)
⊢ ∀ (a : A), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) (a * 1) : 𝕜) (0 : 𝕜)

Tactic:
have : ∀ a, φ (a * 1) = 0 := fun a => by simp only [map_mul φ, h₂, mul_zero]
-- 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))
h₁ : HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0
h₂ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (0 : 𝕜)
this : ∀ (a : A), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) (a * 1) : 𝕜) (0 : 𝕜)
⊢ ∀ (x : A), Eq.{u_1 + 1} (α := 𝕜) (((↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜) ((0 : (a : A) → 𝕜) x : 𝕜)

Tactic:
simpa only [mul_one] using this

Premises used: mul_one
-- 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))
h₁ : HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0
h₂ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (0 : 𝕜)
this : ∀ (a : A), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) (a * 1) : 𝕜) (0 : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)

Tactic:
exact False.elim (φ.prop.1 <| ContinuousLinearMap.ext <| by simpa only [mul_one] using this)

Premises used: False.elim, And.left, Subtype.prop, ContinuousLinearMap.ext
-- 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))
h₁ : HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0
h₂ : HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) = 0
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)

Tactic:
(sub_eq_zero.mp h₂).symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm
-- 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))
h₁ : HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0
h₂ : HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) = 0
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)

Tactic:
exact (sub_eq_zero.mp h₂).symm

Premises used: sub_eq_zero, Iff.mp, Eq.symm
-- 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
map_one' : ∀ (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
r : 𝕜
rw : (φ : (a : A) → 𝕜) (HSMul.hSMul (β := A) r 1) = r
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) r : A) : 𝕜)
    ((algebraMap 𝕜 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_self, RingHom.id_apply]

Premises used: RingHom.id_apply, Algebra.algebraMap_self, Algebra.algebraMap_eq_smul_one
-- 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
map_one' : ∀ (φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
r : 𝕜
rw : HSMul.hSMul (β := 𝕜) r ((φ : (a : A) → 𝕜) 1 : 𝕜) = r
rw₁ : HMul.hMul (β := 𝕜) r ((φ : (a : A) → 𝕜) 1 : 𝕜) = r
rw₂ : r * 1 = r
rw₃ rw₄ : r = r
⊢ (φ : (a : A) → 𝕜) (HSMul.hSMul (β := A) r 1) = r

Tactic:
rw [map_smul, smul_eq_mul, map_one' φ, mul_one]

Premises used: smul_eq_mul, mul_one, map_smul
-- 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
inst_8 : Nontrivial 𝕜
h :
  ∀ (φ : WeakDual 𝕜 A),
    Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ ↔
      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 : 𝕜)}
        φ
⊢ Eq (α := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 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 : 𝕜)}

Tactic:
ext φ
-- 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
inst_8 : Nontrivial 𝕜
φ : WeakDual 𝕜 A
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ ↔
    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 : 𝕜)}
      φ

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- 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
inst_8 : Nontrivial 𝕜
φ : WeakDual 𝕜 A
h :
  Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ →
    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 : 𝕜)}
      φ
h₁ :
  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 : 𝕜)}
      φ →
    Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ ↔
    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 : 𝕜)}
      φ

Tactic:
refine ⟨?_, ?_⟩
-- 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
inst_8 : Nontrivial 𝕜
φ : WeakDual 𝕜 A
hφ : Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ

Tactic:
hφ
-- 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
inst_8 : Nontrivial 𝕜
φ : WeakDual 𝕜 A
hφ : Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ
h :
  ∀ (φ : { x : WeakDual 𝕜 A // Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) x }),
    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 : 𝕜)}
      (↑φ : WeakDual 𝕜 A)
⊢ 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 : 𝕜)}
    φ

Tactic:
lift φ to characterSpace 𝕜 A using hφ

Premises used: WeakDual.characterSpace
-- 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
inst_8 : Nontrivial 𝕜
φ : { x : WeakDual 𝕜 A // Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) x }
⊢ 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 : 𝕜)}
    (↑φ : WeakDual 𝕜 A)

Tactic:
⟨map_one φ, map_mul φ⟩

Premises used: Set.Mem, setOf, map_mul, map_one, And.intro
-- 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
inst_8 : Nontrivial 𝕜
φ : { x : WeakDual 𝕜 A // Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) x }
⊢ 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 : 𝕜)}
    (↑φ : WeakDual 𝕜 A)

Tactic:
exact ⟨map_one φ, map_mul φ⟩
-- 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
inst_8 : Nontrivial 𝕜
φ : WeakDual 𝕜 A
hφ₁ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
hφ₂ :
  ∀ (x y : A),
    (φ : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((φ : (a : A) → 𝕜) y : 𝕜)
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ

Tactic:
⟨?_, hφ₂⟩

Premises used: Set.Mem, setOf, WeakDual.characterSpace, And.intro
-- 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
inst_8 : Nontrivial 𝕜
φ : WeakDual 𝕜 A
hφ₁ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
hφ₂ :
  ∀ (x y : A),
    (φ : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((φ : (a : A) → 𝕜) y : 𝕜)
h : φ ≠ 0
⊢ Membership.mem (γ := Set (WeakDual 𝕜 A)) (characterSpace 𝕜 A) φ

Tactic:
refine ⟨?_, hφ₂⟩
-- 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
inst_8 : Nontrivial 𝕜
hφ₁ : Eq.{u_1 + 1} (α := 𝕜) ((0 : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
hφ₂ :
  ∀ (x y : A),
    (0 : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((0 : (a : A) → 𝕜) x : 𝕜) ((0 : (a : A) → 𝕜) y : 𝕜)
⊢ False

Tactic:
zero_ne_one hφ₁

Premises used: zero_ne_one
-- 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
inst_8 : Nontrivial 𝕜
hφ₁ : Eq.{u_1 + 1} (α := 𝕜) ((0 : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
hφ₂ :
  ∀ (x y : A),
    (0 : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((0 : (a : A) → 𝕜) x : 𝕜) ((0 : (a : A) → 𝕜) y : 𝕜)
⊢ False

Tactic:
exact zero_ne_one hφ₁

Premises used: zero_ne_one
-- 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
inst_8 : Nontrivial 𝕜
inst_9 : T2Space 𝕜
inst_10 : ContinuousMul 𝕜
rw :
  IsClosed (X := WeakDual 𝕜 A)
    ({a : WeakDual 𝕜 A | Eq.{u_1 + 1} (α := 𝕜) ((a : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)} ∩
      {a : WeakDual 𝕜 A |
        ∀ (x y : A),
          (a : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((a : (a : A) → 𝕜) x : 𝕜) ((a : (a : A) → 𝕜) y : 𝕜)})
⊢ IsClosed (X := WeakDual 𝕜 A) (characterSpace 𝕜 A)

Tactic:
rw [eq_set_map_one_map_mul, Set.setOf_and]

Premises used: Set.setOf_and, WeakDual.CharacterSpace.eq_set_map_one_map_mul
-- 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
inst_8 : Nontrivial 𝕜
inst_9 : T2Space 𝕜
inst_10 : ContinuousMul 𝕜
⊢ IsClosed (X := WeakDual 𝕜 A)
    ({a : WeakDual 𝕜 A | Eq.{u_1 + 1} (α := 𝕜) ((a : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)} ∩
      {a : WeakDual 𝕜 A |
        ∀ (x y : A),
          (a : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((a : (a : A) → 𝕜) x : 𝕜) ((a : (a : A) → 𝕜) y : 𝕜)})

Tactic:
IsClosed.inter (isClosed_eq (eval_continuous _) continuous_const) ?_

Premises used: continuous_const, isClosed_eq, IsClosed.inter, 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
inst_8 : Nontrivial 𝕜
inst_9 : T2Space 𝕜
inst_10 : ContinuousMul 𝕜
refine :
  IsClosed (X := WeakDual 𝕜 A)
    {a : WeakDual 𝕜 A |
      ∀ (x y : A),
        (a : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((a : (a : A) → 𝕜) x : 𝕜) ((a : (a : A) → 𝕜) y : 𝕜)}
⊢ IsClosed (X := WeakDual 𝕜 A)
    ({a : WeakDual 𝕜 A | Eq.{u_1 + 1} (α := 𝕜) ((a : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)} ∩
      {a : WeakDual 𝕜 A |
        ∀ (x y : A),
          (a : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((a : (a : A) → 𝕜) x : 𝕜) ((a : (a : A) → 𝕜) y : 𝕜)})

Tactic:
refine IsClosed.inter (isClosed_eq (eval_continuous _) continuous_const) ?_

Premises used: continuous_const, isClosed_eq, IsClosed.inter, 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
inst_8 : Nontrivial 𝕜
inst_9 : T2Space 𝕜
inst_10 : ContinuousMul 𝕜
⊢ IsClosed (X := WeakDual 𝕜 A)
    {a : WeakDual 𝕜 A |
      ∀ (x y : A),
        (a : (a : A) → 𝕜) (x * y) = HMul.hMul (α := 𝕜) (β := 𝕜) ((a : (a : A) → 𝕜) x : 𝕜) ((a : (a : A) → 𝕜) y : 𝕜)}

Tactic:
simpa only [(union_zero 𝕜 A).symm] using union_zero_isClosed _ _

Premises used: WeakDual.CharacterSpace.union_zero_isClosed, WeakDual.CharacterSpace.union_zero, Eq.symm
-- 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 : Ring A
inst_7 : Algebra 𝕜 A
inst_8 : Nontrivial 𝕜
φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
a : A
⊢ Membership.mem (α := 𝕜) (spectrum 𝕜 a) ((φ : (a : A) → 𝕜) a : 𝕜)

Tactic:
AlgHom.apply_mem_spectrum φ a

Premises used: AlgHom.apply_mem_spectrum, Set.Mem
-- 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 : Ring A
inst_7 : Algebra 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h : Eq (α := Ideal A) (RingHom.ker φ) (RingHom.ker ψ)
h₁ : ∀ (x : A), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
⊢ φ = ψ

Tactic:
ext x
-- 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 : Ring A
inst_7 : Algebra 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h : Eq (α := Ideal A) (RingHom.ker φ) (RingHom.ker ψ)
x : A
⊢ Membership.mem (γ := Ideal A) (RingHom.ker φ)
    (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A))

Tactic:
simpa only [h, RingHom.mem_ker, map_sub, AlgHomClass.commutes] using sub_self (ψ x)

Premises used: map_sub, sub_self, RingHom.mem_ker, AlgHomClass.commutes, DFunLike.coe
-- 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 : Ring A
inst_7 : Algebra 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h : Eq (α := Ideal A) (RingHom.ker φ) (RingHom.ker ψ)
x : A
⊢ Membership.mem (γ := Ideal A) (RingHom.ker φ)
    (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A))

Tactic:
have : x - algebraMap 𝕜 A (ψ x) ∈ RingHom.ker φ := by
    simpa only [h, RingHom.mem_ker, map_sub, AlgHomClass.commutes] using sub_self (ψ x)
-- 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 : Ring A
inst_7 : Algebra 𝕜 A
φ ψ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
h : Eq (α := Ideal A) (RingHom.ker φ) (RingHom.ker ψ)
x : A
this :
  Membership.mem (γ := Ideal A) (RingHom.ker φ)
    (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A))
h₁ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := 𝕜)
        ((φ : (a : A) → 𝕜) (HSub.hSub (β := A) x ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A)) : 𝕜)
        (0 : 𝕜)),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
h₂ :
  ∀
    (this :
      HSub.hSub (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜)
          ((φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) ((ψ : (a : A) → 𝕜) x : 𝕜) : A) : 𝕜) =
        0),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
h₃ :
  ∀
    (this :
      HSub.hSub (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜)
          ((algebraMap 𝕜 𝕜 : (a : 𝕜) → 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜) : 𝕜) =
        0),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
h₄ h₅ h₆ h₇ :
  ∀
    (this :
      Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((algebraMap 𝕜 𝕜 : (a : 𝕜) → 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜) : 𝕜)),
    Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)

Tactic:
rwa [RingHom.mem_ker, map_sub, AlgHomClass.commutes, sub_eq_zero] at this

Premises used: map_sub, sub_eq_zero, RingHom.mem_ker, AlgHomClass.commutes
-- Module: Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : ContinuousAdd 𝕜
inst_3 : ContinuousConstSMul 𝕜 𝕜
inst_4 : Ring A
inst_5 : TopologicalSpace A
inst_6 : Algebra 𝕜 A
φ : (↑(characterSpace 𝕜 A) : Type (max u_1 u_2))
z : 𝕜
⊢ (φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) z : A) = z

Tactic:
simp [AlgHomClass.commutes]

Premises used: AlgHomClass.commutes