awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f g : ↥(Lp ℂ 2 volume)
simp_rw :
  HasSum (α := ℂ)
    (fun (i : d → ℤ) ↦
      HMul.hMul (β := ℂ) (mFourierCoeff (↑(↑g : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i) :
          ℂ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (β := ℂ) ((↑(↑g : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) : ℂ))
⊢ HasSum (α := ℂ)
    (fun (i : d → ℤ) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i) : ℂ)
        (mFourierCoeff (↑(↑g : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) : ℂ)
        ((↑(↑g : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t))

Tactic:
simp_rw [mul_comm (conj _)]

Premises used: mul_comm, starRingEnd, DFunLike.coe
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f g : ↥(Lp ℂ 2 volume)
⊢ HasSum (α := ℂ)
    (fun (i : d → ℤ) ↦
      HMul.hMul (β := ℂ) (mFourierCoeff (↑(↑g : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i) :
          ℂ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (β := ℂ) ((↑(↑g : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) : ℂ))

Tactic:
HasSum.congr_fun (mFourierBasis.hasSum_inner_mul_inner f g) (fun n ↦ ?_)

Premises used: HasSum.congr_fun, UnitAddTorus.mFourierBasis, HilbertBasis.hasSum_inner_mul_inner
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f g : ↥(Lp ℂ 2 volume)
refine :
  ∀ (n : d → ℤ),
    HMul.hMul (β := ℂ) (mFourierCoeff (↑(↑g : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) n)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) n) :
          ℂ) =
      inner ℂ f ((mFourierBasis : (a : d → ℤ) → ↥(Lp ℂ 2 volume)) n) *
        inner ℂ ((mFourierBasis : (a : d → ℤ) → ↥(Lp ℂ 2 volume)) n) g
⊢ HasSum (α := ℂ)
    (fun (i : d → ℤ) ↦
      HMul.hMul (β := ℂ) (mFourierCoeff (↑(↑g : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) (mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i) :
          ℂ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (β := ℂ) ((↑(↑g : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) : ℂ))

Tactic:
refine HasSum.congr_fun (mFourierBasis.hasSum_inner_mul_inner f g) (fun n ↦ ?_)

Premises used: HasSum.congr_fun, UnitAddTorus.mFourierBasis, HilbertBasis.hasSum_inner_mul_inner
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f g : ↥(Lp ℂ 2 volume)
n : d → ℤ
⊢ HMul.hMul (β := ℂ) (mFourierCoeff (↑(↑g : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) n)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) (mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) n) : ℂ) =
    inner ℂ f ((mFourierBasis : (a : d → ℤ) → ↥(Lp ℂ 2 volume)) n) *
      inner ℂ ((mFourierBasis : (a : d → ℤ) → ↥(Lp ℂ 2 volume)) n) g

Tactic:
simp only [← mFourierBasis_repr, HilbertBasis.repr_apply_apply, inner_conj_symm,
    mul_comm (inner ℂ f _)]

Premises used: Inner.inner, HilbertBasis.repr_apply_apply, mul_comm, UnitAddTorus.mFourierBasis_repr, Complex, inner_conj_symm
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
⊢ HasSum (α := ℝ)
    (fun (i : d → ℤ) ↦
      HPow.hPow (β := ℕ) ‖mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i‖ 2)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HPow.hPow (β := ℕ) ‖(↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t‖ 2)

Tactic:
simpa only [← RCLike.inner_apply', inner_self_eq_norm_sq, ← integral_re
    (L2.integrable_inner f f)] using RCLike.hasSum_re ℂ (hasSum_prod_mFourierCoeff f f)

Premises used: RCLike.inner_apply', inner_self_eq_norm_sq, RCLike.hasSum_re, UnitAddTorus.hasSum_prod_mFourierCoeff, MeasureTheory.L2.integrable_inner, Complex, integral_re
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : C(UnitAddTorus d, ℂ)
n : d → ℤ
⊢ Eq (α := ℂ)
    (mFourierCoeff
      (↑(↑((ContinuousMap.toLp 2 volume ℂ : (a : C(UnitAddTorus d, ℂ)) → ↥(Lp ℂ 2 volume)) f) :
            UnitAddTorus d →ₘ[volume] ℂ) :
        UnitAddTorus d → ℂ)
      n)
    (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ) n)

Tactic:
integral_congr_ae (ae_eq_rfl.mul <| f.coeFn_toAEEqFun _)

Premises used: MeasureTheory.ae_eq_rfl, ContinuousMap.coeFn_toAEEqFun, Filter.EventuallyEq.mul, MeasureTheory.integral_congr_ae, UnitAddTorus.mFourierCoeff
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (α := ℂ) (β := d → ℤ) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ))
⊢ HasSum (α := ↥(Lp ℂ 2 volume))
    (fun (i : d → ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 volume))
        (mFourierCoeff
          (↑(↑((ContinuousMap.toLp 2 volume ℂ : (a : C(UnitAddTorus d, ℂ)) → ↥(Lp ℂ 2 volume)) f) :
                UnitAddTorus d →ₘ[volume] ℂ) :
            UnitAddTorus d → ℂ)
          i)
        (mFourierLp 2 i))
    ((ContinuousMap.toLp 2 volume ℂ : (a : C(UnitAddTorus d, ℂ)) → ↥(Lp ℂ 2 volume)) f : ↥(Lp ℂ 2 volume))

Tactic:
have sum_L2 := hasSum_mFourier_series_L2 (ContinuousMap.toLp 2 volume ℂ f)
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (α := ℂ) (β := d → ℤ) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ))
sum_L2 :
  HasSum (α := ↥(Lp ℂ 2 volume))
    (fun (i : d → ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 volume))
        (mFourierCoeff
          (↑(↑((ContinuousMap.toLp 2 volume ℂ : (a : C(UnitAddTorus d, ℂ)) → ↥(Lp ℂ 2 volume)) f) :
                UnitAddTorus d →ₘ[volume] ℂ) :
            UnitAddTorus d → ℂ)
          i)
        (mFourierLp 2 i))
    ((ContinuousMap.toLp 2 volume ℂ : (a : C(UnitAddTorus d, ℂ)) → ↥(Lp ℂ 2 volume)) f : ↥(Lp ℂ 2 volume))
⊢ HasSum (α := ↥(Lp ℂ 2 volume))
    (fun (i : d → ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 volume)) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ) i) (mFourierLp 2 i))
    ((ContinuousMap.toLp 2 volume ℂ : (a : C(UnitAddTorus d, ℂ)) → ↥(Lp ℂ 2 volume)) f : ↥(Lp ℂ 2 volume))

Tactic:
simp only [mFourierCoeff_toLp] at sum_L2

Premises used: UnitAddTorus.mFourierCoeff_toLp
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (α := ℂ) (β := d → ℤ) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ))
sum_L2 :
  HasSum (α := ↥(Lp ℂ 2 volume))
    (fun (i : d → ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 volume)) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ) i) (mFourierLp 2 i))
    ((ContinuousMap.toLp 2 volume ℂ : (a : C(UnitAddTorus d, ℂ)) → ↥(Lp ℂ 2 volume)) f : ↥(Lp ℂ 2 volume))
⊢ HasSum (fun (i : d → ℤ) ↦ HSMul.hSMul (α := ℂ) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ) i) (mFourier i)) f

Tactic:
ContinuousMap.hasSum_of_hasSum_Lp (.of_norm ?_) sum_L2

Premises used: Summable.of_norm, ContinuousMap.hasSum_of_hasSum_Lp
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (α := ℂ) (β := d → ℤ) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ))
sum_L2 :
  HasSum (α := ↥(Lp ℂ 2 volume))
    (fun (i : d → ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ↥(Lp ℂ 2 volume)) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ) i) (mFourierLp 2 i))
    ((ContinuousMap.toLp 2 volume ℂ : (a : C(UnitAddTorus d, ℂ)) → ↥(Lp ℂ 2 volume)) f : ↥(Lp ℂ 2 volume))
⊢ Summable (α := ℝ) fun (a : d → ℤ) ↦
    ‖HSMul.hSMul (α := ℂ) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ) a) (mFourier a)‖

Tactic:
simpa only [norm_smul, mFourier_norm, mul_one] using h.norm

Premises used: norm_smul, UnitAddTorus.mFourier_norm, Summable.norm, mul_one
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (α := ℂ) (β := d → ℤ) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ))
x : UnitAddTorus d
⊢ HasSum (α := ℂ)
    (fun (i : d → ℤ) ↦
      HSMul.hSMul (α := ℂ) (β := ℂ) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ) i)
        ((mFourier i : (a : UnitAddTorus d) → ℂ) x : ℂ))
    ((f : (a : UnitAddTorus d) → ℂ) x : ℂ)

Tactic:
simpa only [map_smul] using (ContinuousMap.evalCLM ℂ x).hasSum
    (hasSum_mFourier_series_of_summable h)

Premises used: ContinuousLinearMap.hasSum, ContinuousMap.evalCLM, UnitAddTorus.hasSum_mFourier_series_of_summable, Complex, map_smul
-- 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_1 : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL_1 : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
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
⊢ ∃ (C : ℝ),
    ∀ (x y : V),
      dist (α := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
          (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) y : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) ≤
        C

Tactic:
⟨2, fun x y ↦ ?_⟩

Premises used: Exists.intro, OfNat.ofNat
-- 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_1 : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL_1 : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
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 :
  ∀ (x y : V),
    dist (α := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
        (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) y : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) ≤
      2
⊢ ∃ (C : ℝ),
    ∀ (x y : V),
      dist (α := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
          (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) y : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) ≤
        C

Tactic:
refine ⟨2, fun x y ↦ ?_⟩
-- 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_1 : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL_1 : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
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
x y : V
⊢ dist (α := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
      (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) y : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) ≤
    norm (E := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) +
      norm (E := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) y : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)

Tactic:
dist_le_norm_add_norm _ _

Premises used: dist_le_norm_add_norm
-- 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_1 : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL_1 : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
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
x y : V
⊢ norm (E := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) ≤ 1

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_1 : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL_1 : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
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
x y : V
⊢ norm (E := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) y : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) ≤ 1

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_1 : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL_1 : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
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
x y : V
⊢ HAdd.hAdd (α := ℝ) 1 1 = 2

Tactic:
ring
-- 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_1 : Continuous (X := ℝ) (Y := Circle) (⇑e : (a : ℝ) → Circle)
hL_1 : Continuous (Y := ℝ) fun (p : V × W) ↦ (((L : (a : V) → W →ₗ[ℝ] ℝ) p.1 : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) p.2
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
x y : V
calc : HAdd.hAdd (α := ℝ) 1 1 = 2
⊢ dist (α := ℂ) (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) x : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
      (↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) y : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) ≤
    2

Tactic:
calc dist _ _
      ≤ (‖_‖ : ℝ) + ‖_‖ := dist_le_norm_add_norm _ _
    _ ≤ 1 + 1 := add_le_add (by simp) (by simp)
    _ = 2 := by ring

Premises used: Norm.norm, dist_le_norm_add_norm, add_le_add, Dist.dist
-- 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
⊢ Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ)
    ((↑((e : (a : ℝ) → Circle) ((((L : (a : V) → W →ₗ[ℝ] ℝ) v : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) : ℂ)

Tactic:
rfl

Premises used: rfl
-- 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
h : ∀ (x : V), Eq (α := ℂ) ((char he hL 0 : (a : V) → ℂ) x : ℂ) ((1 : (a : V) → ℂ) x : ℂ)
⊢ char he hL 0 = 1

Tactic:
ext
-- 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
x : V
⊢ Eq (α := ℂ) ((char he hL 0 : (a : V) → ℂ) x : ℂ) ((1 : (a : V) → ℂ) x : ℂ)

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
x y : W
h :
  ∀ (x_1 : V),
    Eq (α := ℂ) ((char he hL (x + y) : (a : V) → ℂ) x_1 : ℂ) ((char he hL x * char he hL y : (a : V) → ℂ) x_1 : ℂ)
⊢ char he hL (x + y) = char he hL x * char he hL y

Tactic:
ext
-- 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
x y : W
x_1 : V
⊢ Eq (α := ℂ) ((char he hL (x + y) : (a : V) → ℂ) x_1 : ℂ) ((char he hL x * char he hL y : (a : V) → ℂ) x_1 : ℂ)

Tactic:
simp [e.map_add_eq_mul]

Premises used: AddChar.map_add_eq_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
w : W
h : ∀ (x : V), Eq (α := ℂ) ((char he hL (-w) : (a : V) → ℂ) x : ℂ) ((star (char he hL w) : (a : V) → ℂ) x : ℂ)
⊢ char he hL (-w) = star (char he hL w)

Tactic:
ext
-- 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
x : V
⊢ Eq (α := ℂ) ((char he hL (-w) : (a : V) → ℂ) x : ℂ) ((star (char he hL w) : (a : V) → ℂ) x : ℂ)

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
h : ∀ (w : W), Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
contrapose! :
  ∀ (h : v ≠ v'), ∃ (w : W), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
⊢ v = v'

Tactic:
contrapose! h
-- 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
h : v ≠ v'
obtain :
  ∀ (w : W)
    (hw :
      Ne (α := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ((0 : (a : W) → ℝ) w : ℝ)),
    ∃ (w : W), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
⊢ ∃ (w : W), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)

Tactic:
obtain ⟨w, hw⟩ := DFunLike.ne_iff.mp (hL' (v - v') (sub_ne_zero_of_ne h))

Premises used: HSub.hSub, sub_ne_zero_of_ne, DFunLike.ne_iff, Iff.mp
-- 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
h : v ≠ v'
w : W
hw : Ne (α := ℝ) ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) ((0 : (a : W) → ℝ) w : ℝ)
obtain :
  ∀ (a : ℝ) (ha : Ne (α := Circle) ((e : (a : ℝ) → Circle) a : Circle) ((1 : (a : ℝ) → Circle) a : Circle)),
    ∃ (w : W), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
⊢ ∃ (w : W), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)

Tactic:
obtain ⟨a, ha⟩ := DFunLike.ne_iff.mp he'

Premises used: DFunLike.ne_iff, Iff.mp