awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
y : AddMonoidAlgebra ℂ W
z : W →₀ ℂ := Finsupp.mapRange star ⋯ y
f : W ↪ W := { toFun := fun (x : W) ↦ -x, inj' := ⋯ }
⊢ ∃ (x : AddMonoidAlgebra ℂ W),
    Eq.{u_1 + 1} (α := V →ᵇ ℂ) ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) x : V →ᵇ ℂ)
      (star ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) y) : V →ᵇ ℂ)

Tactic:
⟨z.embDomain f, ?_⟩

Premises used: Exists.intro, Finsupp.embDomain
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
y : AddMonoidAlgebra ℂ W
z : W →₀ ℂ := Finsupp.mapRange star ⋯ y
f : W ↪ W := { toFun := fun (x : W) ↦ -x, inj' := ⋯ }
refine :
  Eq.{u_1 + 1} (α := V →ᵇ ℂ) ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) (Finsupp.embDomain f z) : V →ᵇ ℂ)
    (star ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) y) : V →ᵇ ℂ)
⊢ ∃ (x : AddMonoidAlgebra ℂ W),
    Eq.{u_1 + 1} (α := V →ᵇ ℂ) ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) x : V →ᵇ ℂ)
      (star ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) y) : V →ᵇ ℂ)

Tactic:
refine ⟨z.embDomain f, ?_⟩
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
y : AddMonoidAlgebra ℂ W
z : W →₀ ℂ := Finsupp.mapRange star ⋯ y
f : W ↪ W := { toFun := fun (x : W) ↦ -x, inj' := ⋯ }
h :
  ∀ (u : V),
    Eq (α := ℂ)
      ((((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) (Finsupp.embDomain f z) : V →ᵇ ℂ) : (a : V) → ℂ) u :
        ℂ)
      (((star ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) y) : V →ᵇ ℂ) : (a : V) → ℂ) u : ℂ)
⊢ Eq.{u_1 + 1} (α := V →ᵇ ℂ) ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) (Finsupp.embDomain f z) : V →ᵇ ℂ)
    (star ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) y) : V →ᵇ ℂ)

Tactic:
ext1 u
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
y : AddMonoidAlgebra ℂ W
z : W →₀ ℂ := Finsupp.mapRange star ⋯ y
f : W ↪ W := { toFun := fun (x : W) ↦ -x, inj' := ⋯ }
u : V
h :
  Eq (α := ℂ)
    (∑ x ∈ z.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((z : (a : W) → ℂ) x : ℂ)
        ((↑((e : (a : ℝ) → Circle)
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) u : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) ((f : (a : W) → W) x : W))) :
            ℂ) :
          ℂ))
    (∑ x ∈ y.support,
      HMul.hMul (α := ℂ) (β := ℂ) (star ((y : (a : W) → ℂ) x) : ℂ)
        ((↑((e : (a : ℝ) → Circle) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) u : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) x)) : ℂ) : ℂ))
⊢ Eq (α := ℂ)
    ((((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) (Finsupp.embDomain f z) : V →ᵇ ℂ) : (a : V) → ℂ) u : ℂ)
    (((star ((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) y) : V →ᵇ ℂ) : (a : V) → ℂ) u : ℂ)

Tactic:
simp only [charAlgHom_apply, Finsupp.support_embDomain, Finset.sum_map,
    Finsupp.embDomain_apply_self, star_apply, star_sum, star_mul', Circle.star_addChar]

Premises used: BoundedContinuousFunction.charAlgHom_apply, Finset.sum_map, star_sum, Circle.star_addChar, Finsupp.embDomain_apply_self, BoundedContinuousFunction.star_apply, Finsupp.support_embDomain, star_mul'
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
y : AddMonoidAlgebra ℂ W
z : W →₀ ℂ := Finsupp.mapRange star ⋯ y
f : W ↪ W := { toFun := fun (x : W) ↦ -x, inj' := ⋯ }
u : V
h :
  Eq (α := ℂ)
    (∑ x ∈ y.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((z : (a : W) → ℂ) x : ℂ)
        ((↑((e : (a : ℝ) → Circle)
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) u : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) ((f : (a : W) → W) x : W))) :
            ℂ) :
          ℂ))
    (∑ x ∈ y.support,
      HMul.hMul (α := ℂ) (β := ℂ) (star ((y : (a : W) → ℂ) x) : ℂ)
        ((↑((e : (a : ℝ) → Circle) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) u : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) x)) : ℂ) : ℂ))
⊢ Eq (α := ℂ)
    (∑ x ∈ z.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((z : (a : W) → ℂ) x : ℂ)
        ((↑((e : (a : ℝ) → Circle)
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) u : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) ((f : (a : W) → W) x : W))) :
            ℂ) :
          ℂ))
    (∑ x ∈ y.support,
      HMul.hMul (α := ℂ) (β := ℂ) (star ((y : (a : W) → ℂ) x) : ℂ)
        ((↑((e : (a : ℝ) → Circle) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) u : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) x)) : ℂ) : ℂ))

Tactic:
rw [Finsupp.support_mapRange_of_injective (star_zero _) y star_injective]

Premises used: star_injective, star_zero, Finsupp.support_mapRange_of_injective
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
y : AddMonoidAlgebra ℂ W
z : W →₀ ℂ := Finsupp.mapRange star ⋯ y
f : W ↪ W := { toFun := fun (x : W) ↦ -x, inj' := ⋯ }
u : V
⊢ Eq (α := ℂ)
    (∑ x ∈ y.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((z : (a : W) → ℂ) x : ℂ)
        ((↑((e : (a : ℝ) → Circle)
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) u : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) ((f : (a : W) → W) x : W))) :
            ℂ) :
          ℂ))
    (∑ x ∈ y.support,
      HMul.hMul (α := ℂ) (β := ℂ) (star ((y : (a : W) → ℂ) x) : ℂ)
        ((↑((e : (a : ℝ) → Circle) (-(((L : (a : V) → W →ₗ[ℝ] ℝ) u : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) x)) : ℂ) : ℂ))

Tactic:
simp [z, f]
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
f : V →ᵇ ℂ
⊢ f ∈ (charAlgHom he hL).range ↔
    ∃ (w : AddMonoidAlgebra ℂ W),
      Eq (α := (a : V) → ℂ) (⇑f : (a : V) → ℂ) fun (x : V) ↦
        ∑ a ∈ w.support,
          HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
            ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)

Tactic:
simp [BoundedContinuousFunction.ext_iff, funext_iff, eq_comm]

Premises used: funext_iff, eq_comm, BoundedContinuousFunction.ext_iff
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
rw :
  ∃ (w_1 : AddMonoidAlgebra ℂ W),
    Eq (α := (a : V) → ℂ) (⇑(char he hL w) : (a : V) → ℂ) fun (x : V) ↦
      ∑ a ∈ w_1.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w_1 : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
⊢ char he hL w ∈ charPoly he hL

Tactic:
rw [mem_charPoly]

Premises used: BoundedContinuousFunction.mem_charPoly
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
⊢ ∃ (w_1 : AddMonoidAlgebra ℂ W),
    Eq (α := (a : V) → ℂ) (⇑(char he hL w) : (a : V) → ℂ) fun (x : V) ↦
      ∑ a ∈ w_1.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w_1 : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)

Tactic:
⟨AddMonoidAlgebra.single w 1, ?_⟩

Premises used: Exists.intro, OfNat.ofNat, AddMonoidAlgebra.single
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
refine :
  Eq (α := (a : V) → ℂ) (⇑(char he hL w) : (a : V) → ℂ) fun (x : V) ↦
    ∑ a ∈ Finsupp.support (M := ℂ) (AddMonoidAlgebra.single w 1),
      HMul.hMul (α := ℂ) (β := ℂ) ((AddMonoidAlgebra.single w 1 : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)
⊢ ∃ (w_1 : AddMonoidAlgebra ℂ W),
    Eq (α := (a : V) → ℂ) (⇑(char he hL w) : (a : V) → ℂ) fun (x : V) ↦
      ∑ a ∈ w_1.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w_1 : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)

Tactic:
refine ⟨AddMonoidAlgebra.single w 1, ?_⟩
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
h :
  ∀ (v : V),
    Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ)
      (∑ a ∈ Finsupp.support (M := ℂ) (AddMonoidAlgebra.single w 1),
          HMul.hMul (α := ℂ) (β := ℂ) ((AddMonoidAlgebra.single w 1 : (a : W) → ℂ) a : ℂ)
            ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
        ℂ)
⊢ Eq (α := (a : V) → ℂ) (⇑(char he hL w) : (a : V) → ℂ) fun (x : V) ↦
    ∑ a ∈ Finsupp.support (M := ℂ) (AddMonoidAlgebra.single w 1),
      HMul.hMul (α := ℂ) (β := ℂ) ((AddMonoidAlgebra.single w 1 : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ)

Tactic:
ext v
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
v : V
h :
  Eq (α := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
    (∑ x ∈ Finsupp.support (M := ℂ) (Finsupp.single w 1),
      HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) x : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) x)) : ℂ) : ℂ))
⊢ Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ)
    (∑ a ∈ Finsupp.support (M := ℂ) (AddMonoidAlgebra.single w 1),
        HMul.hMul (α := ℂ) (β := ℂ) ((AddMonoidAlgebra.single w 1 : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)

Tactic:
simp only [char_apply, AddMonoidAlgebra.single]

Premises used: AddMonoidAlgebra.single, BoundedContinuousFunction.char_apply
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
v : V
h :
  (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) w : ℂ)
      ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) : ℂ)
h₁ :
  ∀ b ∈ Finsupp.support (M := ℂ) (Finsupp.single w 1),
    b ≠ w →
      HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) b : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) b)) : ℂ) : ℂ) =
        0
h₂ :
  w ∉ Finsupp.support (M := ℂ) (Finsupp.single w 1) →
    HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) w : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) : ℂ) =
      0
⊢ Eq (α := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
    (∑ x ∈ Finsupp.support (M := ℂ) (Finsupp.single w 1),
      HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) x : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) x)) : ℂ) : ℂ))

Tactic:
rw [Finset.sum_eq_single w]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
v : V
⊢ (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) w : ℂ)
      ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
v : V
⊢ ∀ b ∈ Finsupp.support (M := ℂ) (Finsupp.single w 1),
    b ≠ w →
      HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) b : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) b)) : ℂ) : ℂ) =
        0

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
w : W
v : V
⊢ w ∉ Finsupp.support (M := ℂ) (Finsupp.single w 1) →
    HMul.hMul (α := ℂ) (β := ℂ) ((Finsupp.single w 1 : (a : W) → ℂ) w : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) : ℂ) =
      0

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
hvv' : v ≠ v'
contrapose! :
  ∀ (hvv' : ∀ (w : W), Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)), v = v'
⊢ ∃ (w : W), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)

Tactic:
contrapose! hvv'
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
hvv' : ∀ (w : W), Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
⊢ v = v'

Tactic:
ext_of_char_eq he he' hL hL' hvv'

Premises used: BoundedContinuousFunction.ext_of_char_eq
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
hvv' : ∀ (w : W), Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
⊢ v = v'

Tactic:
exact ext_of_char_eq he he' hL hL' hvv'

Premises used: BoundedContinuousFunction.ext_of_char_eq
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
hvv' : v ≠ v'
obtain :
  ∀ (w : W) (hw : Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)),
    ∃ (f : V → ℂ),
      Membership.mem (γ := Set (V → ℂ))
          ((fun (f : C(V, ℂ)) ↦ (⇑f : (a : V) → ℂ)) ''
            (↑(StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL))) :
              Set C(V, ℂ)))
          f ∧
        f v ≠ f v'
⊢ ∃ (f : V → ℂ),
    Membership.mem (γ := Set (V → ℂ))
        ((fun (f : C(V, ℂ)) ↦ (⇑f : (a : V) → ℂ)) ''
          (↑(StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL))) : Set C(V, ℂ)))
        f ∧
      f v ≠ f v'

Tactic:
obtain ⟨w, hw⟩ : ∃ w, char he hL w v ≠ char he hL w v' := by
    contrapose! hvv'
    exact ext_of_char_eq he he' hL hL' hvv'
-- Module: Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
Goal:
V : Type u_1
W : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
inst_2 : TopologicalSpace V
inst_3 : AddCommGroup W
inst_4 : Module ℝ W
inst_5 : TopologicalSpace W
e : AddChar ℝ Circle
L : LinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →ₗ[ℝ] ℝ)
he : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
he' : e ≠ 1
hL : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
hL' : ∀ (v : V), v ≠ 0 → Ne.{u_2 + 1} (α := W →ₗ[ℝ] ℝ) ((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) (0 : W →ₗ[ℝ] ℝ)
v v' : V
hvv' : v ≠ v'
w : W
hw : Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
h :
  Membership.mem (γ := Set (V → ℂ))
      ((fun (f : C(V, ℂ)) ↦ (⇑f : (a : V) → ℂ)) ''
        (↑(StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL))) : Set C(V, ℂ)))
      (⇑(char he hL w) : (a : V) → ℂ) ∧
    Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
⊢ ∃ (f : V → ℂ),
    Membership.mem (γ := Set (V → ℂ))
        ((fun (f : C(V, ℂ)) ↦ (⇑f : (a : V) → ℂ)) ''
          (↑(StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ ℂ) (charPoly he hL))) : Set C(V, ℂ)))
        f ∧
      f v ≠ f v'

Tactic:
use char he hL w

Premises used: BoundedContinuousFunction.char