awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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
h : v ≠ v'
w : W
hw : Ne (α := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ((0 : (a : W) → ℝ) w : ℝ)
a : ℝ
ha : Ne (α := Circle) ((e : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)
⊢ ¬Eq (α := ↥(Submonoid.unitSphere ℂ))
      ((e : (a : ℝ) → Circle)
          (HAdd.hAdd (α := ℝ) (β := ℝ)
            (-(((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
                  ((a /
                      HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                        ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) •
                    w) :
              ℝ)
            ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
                ((a /
                    HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                      ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) •
                  w) :
              ℝ)) :
        Circle)
      (1 : ↥(Submonoid.unitSphere ℂ))
have h₁ : ∀
  (hw :
    HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
        ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ≠
      0),
  ¬Eq (α := ↥(Submonoid.unitSphere ℂ))
      ((e : (a : ℝ) → Circle)
          (-HMul.hMul (β := ℝ)
                (a /
                  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                    ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) +
            HMul.hMul (β := ℝ)
              (a /
                HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                  ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))
              ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) :
        Circle)
      (1 : ↥(Submonoid.unitSphere ℂ))
Tactic: simp only [map_sub, LinearMap.sub_apply, LinearMap.zero_apply, AddChar.one_apply,
    map_smul, smul_eq_mul] at ha hw ⊢
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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
h : v ≠ v'
w : W
a : ℝ
ha : Ne (α := Circle) ((e : (a : ℝ) → Circle) a : Circle) (1 : Circle)
hw :
  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
      ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ≠
    0
⊢ ¬Eq (α := ↥(Submonoid.unitSphere ℂ))
      ((e : (a : ℝ) → Circle)
          (-HMul.hMul (β := ℝ)
                (a /
                  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                    ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) +
            HMul.hMul (β := ℝ)
              (a /
                HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                  ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))
              ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)) :
        Circle)
      (1 : ↥(Submonoid.unitSphere ℂ))
have h₁ : ¬Eq (α := ↥(Submonoid.unitSphere ℂ))
    ((e : (a : ℝ) → Circle)
        (HMul.hMul (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) *
            (HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))⁻¹ -
          HMul.hMul (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) *
            (HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))⁻¹) :
      Circle)
    (1 : ↥(Submonoid.unitSphere ℂ))
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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
h : v ≠ v'
w : W
a : ℝ
ha : Ne (α := Circle) ((e : (a : ℝ) → Circle) a : Circle) (1 : Circle)
hw :
  HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
      ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ≠
    0
⊢ ¬Eq (α := ↥(Submonoid.unitSphere ℂ))
      ((e : (a : ℝ) → Circle)
          (HMul.hMul (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) *
              (HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                  ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))⁻¹ -
            HMul.hMul (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) *
              (HSub.hSub (α := ℝ) (β := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ)
                  ((((L : (a : V) → W →ₗ[ℝ] ℝ) v' : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ))⁻¹) :
        Circle)
      (1 : ↥(Submonoid.unitSphere ℂ))
have h₁ : ¬Eq (α := ↥(Submonoid.unitSphere ℂ)) ((e : (a : ℝ) → Circle) a : Circle) (1 : ↥(Submonoid.unitSphere ℂ))
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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 : AddMonoidAlgebra ℂ W
v : V
⊢ Eq (α := ℂ) ((((charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) w : V →ᵇ ℂ) : (a : V) → ℂ) v : ℂ)
    (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)
have simp : Eq (α := ℂ)
  ((Finsupp.sum w fun (a : W) (b : ℂ) ↦
          HSMul.hSMul (β := V →ᵇ ℂ) b
            ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
                ((Multiplicative.ofAdd : (a : W) → Multiplicative W) a) :
              V →ᵇ ℂ) :
        (a : V) → ℂ)
      v :
    ℂ)
  (∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
    ℂ)
Tactic: simp only [charAlgHom, AddMonoidAlgebra.lift_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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 : AddMonoidAlgebra ℂ W
v : V
⊢ Eq (α := ℂ)
    ((Finsupp.sum w fun (a : W) (b : ℂ) ↦
            HSMul.hSMul (β := V →ᵇ ℂ) b
              ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
                  ((Multiplicative.ofAdd : (a : W) → Multiplicative W) a) :
                V →ᵇ ℂ) :
          (a : V) → ℂ)
        v :
      ℂ)
    (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)
have rw : Eq (α := ℂ)
  ((∑ x ∈ w.support,
          HSMul.hSMul (α := ℂ) (β := V →ᵇ ℂ) ((w : (a : W) → ℂ) x : ℂ)
            ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
                ((Multiplicative.ofAdd : (a : W) → Multiplicative W) x) :
              V →ᵇ ℂ) :
        (a : V) → ℂ)
      v :
    ℂ)
  (∑ a ∈ w.support,
      HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
        ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
    ℂ)
Tactic: rw [Finsupp.sum_of_support_subset w subset_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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 : AddMonoidAlgebra ℂ W
v : V
rw :
  Eq (α := ℂ)
    ((∑ x ∈ w.support,
            HSMul.hSMul (α := ℂ) (β := V →ᵇ ℂ) ((w : (a : W) → ℂ) x : ℂ)
              ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
                  ((Multiplicative.ofAdd : (a : W) → Multiplicative W) x) :
                V →ᵇ ℂ) :
          (a : V) → ℂ)
        v :
      ℂ)
    (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)
⊢ Eq (α := ℂ)
    ((Finsupp.sum w fun (a : W) (b : ℂ) ↦
            HSMul.hSMul (β := V →ᵇ ℂ) b
              ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
                  ((Multiplicative.ofAdd : (a : W) → Multiplicative W) a) :
                V →ᵇ ℂ) :
          (a : V) → ℂ)
        v :
      ℂ)
    (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)
have h : ∀ i ∈ w.support,
  HSMul.hSMul (α := ℂ) (β := V →ᵇ ℂ) 0
      ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ) ((Multiplicative.ofAdd : (a : W) → Multiplicative W) i) :
        V →ᵇ ℂ) =
    0
Tactic: rw [Finsupp.sum_of_support_subset w subset_rfl]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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 : AddMonoidAlgebra ℂ W
v : V
⊢ Eq (α := ℂ)
    ((∑ x ∈ w.support,
            HSMul.hSMul (α := ℂ) (β := V →ᵇ ℂ) ((w : (a : W) → ℂ) x : ℂ)
              ((charMonoidHom he hL : (a : Multiplicative W) → V →ᵇ ℂ)
                  ((Multiplicative.ofAdd : (a : W) → Multiplicative W) x) :
                V →ᵇ ℂ) :
          (a : V) → ℂ)
        v :
      ℂ)
    (∑ a ∈ w.support,
        HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
          ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ) :
      ℂ)
have simp : Eq (α := ℂ)
  (∑ c ∈ w.support,
    HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) c : ℂ)
      ((↑((e : (a : ℝ) → Circle)
              ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ)
                ((Multiplicative.ofAdd : (a : W) → Multiplicative W) c : Multiplicative W))) :
          ℂ) :
        ℂ))
  (∑ a ∈ w.support,
    HMul.hMul (α := ℂ) (β := ℂ) ((w : (a : W) → ℂ) a : ℂ)
      ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) a)) : ℂ) : ℂ))
Tactic: simp only [coe_sum, coe_smul, charMonoidHom_apply, smul_eq_mul, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (hypothesis)
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
x : V →ᵇ ℂ
hx : x ∈ (charAlgHom he hL).range
⊢ star x ∈ (charAlgHom he hL).range
have hx₁ : ∃ (x_1 : AddMonoidAlgebra ℂ W), (charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) x_1 = x
Tactic: simp only [AlgHom.mem_range] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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
x : V →ᵇ ℂ
hx : ∃ (x_1 : AddMonoidAlgebra ℂ W), (charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) x_1 = x
⊢ ∃ (x_1 : AddMonoidAlgebra ℂ W), (charAlgHom he hL : (a : AddMonoidAlgebra ℂ W) → V →ᵇ ℂ) x_1 = star x
have obtain : ∀ (y : AddMonoidAlgebra ℂ W),
  ∃ (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: obtain ⟨y, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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 →ᵇ ℂ)
have 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 →ᵇ ℂ)
Tactic: refine ⟨z.embDomain f, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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' := ⋯ }
⊢ 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 →ᵇ ℂ)
have 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 : ℂ)
Tactic: ext1 u
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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 (α := ℂ)
    ((((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 : ℂ)
have 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)) : ℂ) : ℂ))
Tactic: simp only [charAlgHom_apply, Finsupp.support_embDomain, Finset.sum_map,
    Finsupp.embDomain_apply_self, star_apply, star_sum, star_mul', Circle.star_addChar]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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 ∈ 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)) : ℂ) : ℂ))
have 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)) : ℂ) : ℂ))
Tactic: rw [Finsupp.support_mapRange_of_injective (star_zero _) y star_injective]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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
⊢ char he hL w ∈ charPoly he hL
have 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)) : ℂ) : ℂ)
Tactic: rw [mem_charPoly]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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)) : ℂ) : ℂ)
have 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)) : ℂ) : ℂ)
Tactic: refine ⟨AddMonoidAlgebra.single w 1, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar (goal)
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
⊢ 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)) : ℂ) : ℂ)
have 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)) : ℂ) : ℂ) :
      ℂ)
Tactic: ext v