awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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) → 𝕜)) ψ)
⊢ φ = ψ
have a : (↑φ : WeakDual 𝕜 A) = (↑ψ : WeakDual 𝕜 A)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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) → 𝕜)) ψ)
⊢ (↑φ : WeakDual 𝕜 A) = (↑ψ : WeakDual 𝕜 A)
have a : ∀ (x : A), Eq.{u_1 + 1} (α := 𝕜) (((↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜) (((↑ψ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) (((↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜) ((0 : (a : A) → 𝕜) x : 𝕜)
have rw : Eq.{u_1 + 1} (α := 𝕜) (((↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) 0 : 𝕜) ((0 : (a : A) → 𝕜) 0 : 𝕜)
Tactic: rw [show x = 0 from Subsingleton.elim x 0, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) (((↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜) ((0 : (a : A) → 𝕜) x : 𝕜)
have rw₁ : Eq.{u_1 + 1} (α := 𝕜) (0 : 𝕜) ((0 : (a : A) → 𝕜) 0 : 𝕜)
Tactic: rw [show x = 0 from Subsingleton.elim x 0, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) (((↑φ : WeakDual 𝕜 A) : (a : A) → 𝕜) x : 𝕜) ((0 : (a : A) → 𝕜) x : 𝕜)
have rw₂ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [show x = 0 from Subsingleton.elim x 0, map_zero, map_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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) (characterSpace 𝕜 A ∪ {0})
have 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 : 𝕜)})
Tactic: simp only [union_zero, Set.setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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
have rw : HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜) -
    HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) =
  0
Tactic: rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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
⊢ HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0
have rw₁ : HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜) =
  HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)
Tactic: rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 : 𝕜)
⊢ HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0
have rw₂ : (φ : (a : A) → 𝕜) 1 = HMul.hMul (α := 𝕜) (β := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)
Tactic: rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 : 𝕜)
⊢ HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0
have rw₃ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) ((φ : (a : A) → 𝕜) (HMul.hMul (α := A) 1 1) : 𝕜)
Tactic: rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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) : 𝕜)
⊢ HMul.hMul (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)) = 0
have rw₄ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜)
Tactic: rw [mul_sub, sub_eq_zero, mul_one, ← map_mul φ, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (hypothesis)
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))
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
have h₁ : 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
have inl : ∀ (h₂ : Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (0 : 𝕜)),
  Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
Tactic: rcases mul_eq_zero.mp h₁ with (h₂ | h₂)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
have inr : ∀ (h₂ : HSub.hSub (α := 𝕜) (β := 𝕜) (1 : 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) = 0),
  Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
Tactic: rcases mul_eq_zero.mp h₁ with (h₂ | h₂)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (hypothesis)
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 : 𝕜)
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) 1 : 𝕜) (1 : 𝕜)
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 : 𝕜
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) ((algebraMap 𝕜 A : (a : 𝕜) → A) r : A) : 𝕜)
    ((algebraMap 𝕜 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
have rw : (φ : (a : A) → 𝕜) (HSMul.hSMul (β := A) r 1) = r
Tactic: rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_self, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 : 𝕜
⊢ (φ : (a : A) → 𝕜) (HSMul.hSMul (β := A) r 1) = r
have rw : HSMul.hSMul (β := 𝕜) r ((φ : (a : A) → 𝕜) 1 : 𝕜) = r
Tactic: rw [map_smul, smul_eq_mul, map_one' φ, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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
⊢ (φ : (a : A) → 𝕜) (HSMul.hSMul (β := A) r 1) = r
have rw₁ : HMul.hMul (β := 𝕜) r ((φ : (a : A) → 𝕜) 1 : 𝕜) = r
Tactic: rw [map_smul, smul_eq_mul, map_one' φ, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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
⊢ (φ : (a : A) → 𝕜) (HSMul.hSMul (β := A) r 1) = r
have rw₂ : r * 1 = r
Tactic: rw [map_smul, smul_eq_mul, map_one' φ, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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
⊢ (φ : (a : A) → 𝕜) (HSMul.hSMul (β := A) r 1) = r
have rw₃ : r = r
Tactic: rw [map_smul, smul_eq_mul, map_one' φ, mul_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 𝕜
⊢ 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 : 𝕜)}
have 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 : 𝕜)}
      φ
Tactic: ext φ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 : 𝕜)}
      φ
have 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 : 𝕜)}
    φ
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 : 𝕜)}
      φ
⊢ 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 : 𝕜)}
      φ
have 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) φ
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 : 𝕜)}
    φ
have 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)
Tactic: lift φ to characterSpace 𝕜 A using hφ
Cleared hypotheses: φ, hφ
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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) φ
have h : φ ≠ 0
Tactic: refine ⟨?_, hφ₂⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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) (characterSpace 𝕜 A)
have 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 : 𝕜)})
Tactic: rw [eq_set_map_one_map_mul, Set.setOf_and]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 : 𝕜)})
have 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 : 𝕜)}
Tactic: refine IsClosed.inter (isClosed_eq (eval_continuous _) continuous_const) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (goal)
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 ψ)
⊢ φ = ψ
have h₁ : ∀ (x : A), Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace (hypothesis)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) ((φ : (a : A) → 𝕜) x : 𝕜) ((ψ : (a : A) → 𝕜) x : 𝕜)
have this : 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)