awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t)) =
    mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i
have h : (ae (F := Measure (UnitAddTorus d)) volume).EventuallyEq (β := (fun (x : d → ℤ) ↦ ℂ) i)
  (fun (a : UnitAddTorus d) ↦
    HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a))
  fun (a : UnitAddTorus d) ↦
  HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
    ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ (ae (F := Measure (UnitAddTorus d)) volume).EventuallyEq (β := (fun (x : d → ℤ) ↦ ℂ) i)
    (fun (a : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a))
    fun (a : UnitAddTorus d) ↦
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
have h : ∀ (a : UnitAddTorus d)
  (ht :
    (↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a =
      (mFourier i : (a : UnitAddTorus d) → ℂ) a),
  HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
Tactic: filter_upwards [coeFn_mFourierLp 2 i] with _ ht
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a : UnitAddTorus d
ht :
  (↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a =
    (mFourier i : (a : UnitAddTorus d) → ℂ) a
⊢ HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
have h : HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((mFourier i : (a : UnitAddTorus d) → ℂ) a : ℂ) : ℂ)
    ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
  HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
    ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
Tactic: rw [ht, ← mFourier_neg, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a : UnitAddTorus d
ht :
  (↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a =
    (mFourier i : (a : UnitAddTorus d) → ℂ) a
h :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((mFourier i : (a : UnitAddTorus d) → ℂ) a : ℂ) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
⊢ HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
have h₁ : HMul.hMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
    ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
  HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
    ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
Tactic: rw [ht, ← mFourier_neg, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a : UnitAddTorus d
ht :
  (↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a =
    (mFourier i : (a : UnitAddTorus d) → ℂ) a
h :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((mFourier i : (a : UnitAddTorus d) → ℂ) a : ℂ) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
h₁ :
  HMul.hMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
⊢ HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
have h₂ : HMul.hMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
    ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
  HMul.hMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
    ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
Tactic: rw [ht, ← mFourier_neg, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
f g : ↥(Lp ℂ 2 volume)
⊢ 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))
have 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) : ℂ))
Tactic: simp_rw [mul_comm (conj _)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
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) : ℂ))
have 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
Tactic: refine HasSum.congr_fun (mFourierBasis.hasSum_inner_mul_inner f g) (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (hypothesis)
Goal:
d : Type u_1
inst : Fintype d
f : C(UnitAddTorus d, ℂ)
h : Summable (α := ℂ) (β := d → ℤ) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ))
⊢ HasSum (fun (i : d → ℤ) ↦ HSMul.hSMul (α := ℂ) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ) i) (mFourier i)) f
have 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))
Tactic: have sum_L2 := hasSum_mFourier_series_L2 (ContinuousMap.toLp 2 volume ℂ f)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (hypothesis)
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 (fun (i : d → ℤ) ↦ HSMul.hSMul (α := ℂ) (mFourierCoeff (⇑f : (a : UnitAddTorus d) → ℂ) i) (mFourier i)) f
have 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))
Tactic: simp only [mFourierCoeff_toLp] at sum_L2
Cleared hypotheses: sum_L2
-- 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_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
have 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
Tactic: refine ⟨2, fun x y ↦ ?_⟩
-- 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_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)) : ℂ) ≤
    2
have calc : HAdd.hAdd (α := ℝ) 1 1 = 2
Tactic: calc dist _ _
      ≤ (‖_‖ : ℝ) + ‖_‖ := dist_le_norm_add_norm _ _
    _ ≤ 1 + 1 := add_le_add (by simp) (by simp)
    _ = 2 := by ring
-- 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
⊢ char he hL 0 = 1
have h : ∀ (x : V), Eq (α := ℂ) ((char he hL 0 : (a : V) → ℂ) x : ℂ) ((1 : (a : V) → ℂ) x : ℂ)
Tactic: ext
-- 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 y : W
⊢ char he hL (x + y) = char he hL x * char he hL y
have 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 : ℂ)
Tactic: ext
-- 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) = star (char he hL w)
have h : ∀ (x : V), Eq (α := ℂ) ((char he hL (-w) : (a : V) → ℂ) x : ℂ) ((star (char he hL w) : (a : V) → ℂ) x : ℂ)
Tactic: ext
-- 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 : ∀ (w : W), Eq (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
⊢ v = v'
have contrapose! : ∀ (h : v ≠ v'), ∃ (w : W), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
Tactic: contrapose! h
Cleared hypotheses: h
-- 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), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
have 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' : ℂ)
Tactic: obtain ⟨w, hw⟩ := DFunLike.ne_iff.mp (hL' (v - v') (sub_ne_zero_of_ne h))
-- 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 : ℝ)
⊢ ∃ (w : W), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
have 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' : ℂ)
Tactic: obtain ⟨a, ha⟩ := DFunLike.ne_iff.mp he'
-- 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)
⊢ ∃ (w : W), Ne (α := ℂ) ((char he hL w : (a : V) → ℂ) v : ℂ) ((char he hL w : (a : V) → ℂ) v' : ℂ)
have h₁ : Ne (α := ℂ)
  ((char he hL (HDiv.hDiv (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) • w) :
        (a : V) → ℂ)
      v :
    ℂ)
  ((char he hL (HDiv.hDiv (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) • w) :
        (a : V) → ℂ)
      v' :
    ℂ)
Tactic: use (a / (L (v - v') w)) • w
-- 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)
⊢ Ne (α := ℂ)
    ((char he hL (HDiv.hDiv (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) • w) :
          (a : V) → ℂ)
        v :
      ℂ)
    ((char he hL (HDiv.hDiv (β := ℝ) a ((((L : (a : V) → W →ₗ[ℝ] ℝ) (v - v') : W →ₗ[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) • w) :
          (a : V) → ℂ)
        v' :
      ℂ)
have h₁ : ¬Eq (α := ℂ)
    (↑((e : (a : ℝ) → Circle)
          ((((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))) :
      ℂ)
    (↑((e : (a : ℝ) → Circle)
          ((((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))) :
      ℂ)
Tactic: simp only [map_sub, LinearMap.sub_apply, char_apply, ne_eq]
-- 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 (α := ℂ)
      (↑((e : (a : ℝ) → Circle)
            ((((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))) :
        ℂ)
      (↑((e : (a : ℝ) → Circle)
            ((((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))) :
        ℂ)
have h₁ : ¬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 ℂ))
Tactic: rw [← div_eq_one_iff_eq (Circle.coe_ne_zero _), div_eq_inv_mul, ← Metric.unitSphere.coe_inv,
    ← e.map_neg_eq_inv, ← Submonoid.coe_mul, ← e.map_add_eq_mul, OneMemClass.coe_eq_one]