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
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this_1 :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
this :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
rw :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ _x ∈ {i}ᶜ, 1 : ℂ) =
    (fourier 1 : (a : AddCircle 1) → ℂ) (z i)
rw₁ :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (1 : ℂ) =
    (fourier 1 : (a : AddCircle 1) → ℂ) (z i)
rw₂ :
  Eq (α := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
⊢ Eq (α := ℂ) (∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ)
    ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
have rw₃ : Eq (α := ℂ) ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ) ((fourier 1 : (a : AddCircle 1) → ℂ) (z i) : ℂ)
Tactic: rw [← this, Finset.prod_const_one, mul_one, Pi.single_eq_same]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (hypothesis)
Goal:
d : Type u_1
inst : Fintype d
inst_1 : DecidableEq d
z : d → AddCircle (𝕜 := ℝ) 1
i : d
this :
  HMul.hMul (α := ℂ) (β := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i) : (a : AddCircle 1) → ℂ) (z i) : ℂ)
      (∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1) : ℂ) =
    ∏ i_1 : d, (fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 i_1) : (a : AddCircle 1) → ℂ) (z i_1)
j : d
hj : Membership.mem (γ := Finset d) {i}ᶜ j
⊢ Eq (α := ℂ) ((fourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1 j) : (a : AddCircle 1) → ℂ) (z j) : ℂ) (1 : ℂ)
have hj₁ : ¬j = i
Tactic: rw [Finset.mem_compl, Finset.mem_singleton] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d_1 : Type u_1
inst : Fintype d_1
d : Type u_2
inst_1 : Fintype d
⊢ LE.le.{u_2} (α := Subalgebra ℂ C(UnitAddTorus d, ℂ)) (adjoin ℂ (range mFourier)) (star (adjoin ℂ (range mFourier)))
have refine : range mFourier ⊆ (↑(star (adjoin ℂ (range mFourier))) : Set C(UnitAddTorus d, ℂ))
Tactic: refine adjoin_le ?_
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d_1 : Type u_1
inst : Fintype d_1
d : Type u_2
inst_1 : Fintype d
n : d → ℤ
⊢ mFourier n ∈ (↑(star (adjoin ℂ (range mFourier))) : Set C(UnitAddTorus d, ℂ))
have refine : mFourier (-n) = star (mFourier n)
Tactic: refine subset_adjoin ⟨-n, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d_1 : Type u_1
inst : Fintype d_1
d : Type u_2
inst_1 : Fintype d
n : d → ℤ
⊢ mFourier (-n) = star (mFourier n)
have h : ∀ (x : UnitAddTorus d),
  Eq (α := ℂ) ((mFourier (-n) : (a : UnitAddTorus d) → ℂ) x : ℂ) ((star (mFourier n) : (a : UnitAddTorus d) → ℂ) x : ℂ)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
⊢ Eq (α := Submodule ℂ C(UnitAddTorus d, ℂ))
    ((Subalgebra.toSubmodule : (a : Subalgebra ℂ C(UnitAddTorus d, ℂ)) → Submodule ℂ C(UnitAddTorus d, ℂ))
        (mFourierSubalgebra d).toSubalgebra :
      Submodule ℂ C(UnitAddTorus d, ℂ))
    (span ℂ (range mFourier) : Submodule ℂ C(UnitAddTorus d, ℂ))
have hs : (↑(Submonoid.closure (range mFourier)) : Set C(UnitAddTorus d, ℂ)) ⊆
  (↑(span ℂ (range mFourier)) : Set C(UnitAddTorus d, ℂ))
Tactic: apply adjoin_eq_span_of_subset
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
⊢ (↑(Submonoid.closure (range mFourier)) : Set C(UnitAddTorus d, ℂ)) ⊆
    (↑(span ℂ (range mFourier)) : Set C(UnitAddTorus d, ℂ))
have hs : ∀ (x : C(UnitAddTorus d, ℂ)), Eq.{u_1 + 1} (α := C(UnitAddTorus d, ℂ)) (mFourier 0) 1
Tactic: refine .trans (fun x ↦ Submonoid.closure_induction (fun _ ↦ id) ⟨0, ?_⟩ ?_) subset_span
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
hs : ∀ (x : C(UnitAddTorus d, ℂ)), Eq.{u_1 + 1} (α := C(UnitAddTorus d, ℂ)) (mFourier 0) 1
⊢ (↑(Submonoid.closure (range mFourier)) : Set C(UnitAddTorus d, ℂ)) ⊆
    (↑(span ℂ (range mFourier)) : Set C(UnitAddTorus d, ℂ))
have hs₁ : ∀ (x x y : C(UnitAddTorus d, ℂ))
  (hx : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) x)
  (hy : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) y),
  Membership.mem (γ := Set C(UnitAddTorus d, ℂ)) (range mFourier) x →
    Membership.mem (γ := Set C(UnitAddTorus d, ℂ)) (range mFourier) y →
      Membership.mem (γ := Set C(UnitAddTorus d, ℂ)) (range mFourier) (x * y)
Tactic: refine .trans (fun x ↦ Submonoid.closure_induction (fun _ ↦ id) ⟨0, ?_⟩ ?_) subset_span
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
x : C(UnitAddTorus d, ℂ)
⊢ Eq.{u_1 + 1} (α := C(UnitAddTorus d, ℂ)) (mFourier 0) 1
have hs : ∀ (z : UnitAddTorus d),
  Eq (α := ℂ) ((mFourier 0 : (a : UnitAddTorus d) → ℂ) z : ℂ) ((1 : (a : UnitAddTorus d) → ℂ) z : ℂ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier m)
n : d → ℤ
hy : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier n)
⊢ Membership.mem (γ := Set C(UnitAddTorus d, ℂ)) (range mFourier) (mFourier m * mFourier n)
have hs : mFourier (m + n) = mFourier m * mFourier n
Tactic: refine ⟨m + n, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
x : C(UnitAddTorus d, ℂ)
m : d → ℤ
hx : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier m)
n : d → ℤ
hy : Membership.mem (γ := Submonoid C(UnitAddTorus d, ℂ)) (Submonoid.closure (range mFourier)) (mFourier n)
⊢ mFourier (m + n) = mFourier m * mFourier n
have hs : ∀ (z : UnitAddTorus d),
  Eq (α := ℂ) ((mFourier (m + n) : (a : UnitAddTorus d) → ℂ) z : ℂ)
    ((mFourier m * mFourier n : (a : UnitAddTorus d) → ℂ) z : ℂ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (hypothesis)
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
hxy : x ≠ y
⊢ ∃ (f : UnitAddTorus d → ℂ),
    Membership.mem (γ := Set (UnitAddTorus d → ℂ))
        ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
          (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
        f ∧
      f x ≠ f y
have hxy₁ : ∃ (x_1 : d), ¬x x_1 = y x_1
Tactic: rw [Ne, funext_iff, not_forall] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
hxy : ∃ (x_1 : d), ¬x x_1 = y x_1
⊢ ∃ (f : UnitAddTorus d → ℂ),
    Membership.mem (γ := Set (UnitAddTorus d → ℂ))
        ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
          (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
        f ∧
      f x ≠ f y
have obtain : ∀ (i : d) (hi : ¬x i = y i),
  ∃ (f : UnitAddTorus d → ℂ),
    Membership.mem (γ := Set (UnitAddTorus d → ℂ))
        ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
          (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
        f ∧
      f x ≠ f y
Tactic: obtain ⟨i, hi⟩ := hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ ∃ (f : UnitAddTorus d → ℂ),
    Membership.mem (γ := Set (UnitAddTorus d → ℂ))
        ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
          (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
        f ∧
      f x ≠ f y
have refine : Ne (α := ℂ)
  ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
    (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) x)
  ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
    (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) y)
Tactic: refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ Ne (α := ℂ) ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) x : ℂ)
    ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) y : ℂ)
have rw : ¬AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
Tactic: rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ ¬AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
have contrapose : ∀ (hi : AddCircle.toCircle (x i) = AddCircle.toCircle (y i)), x i = y i
Tactic: contrapose hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
⊢ (mFourierSubalgebra d).SeparatesPoints
have intro : ∀ ⦃x y : UnitAddTorus d⦄,
  x ≠ y →
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
Tactic: classical
  intro x y hxy
  rw [Ne, funext_iff, not_forall] at hxy
  obtain ⟨i, hi⟩ := hxy
  refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩
  dsimp only
  rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]
  contrapose hi
  exact AddCircle.injective_toCircle one_ne_zero hi
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
intro intro₁ intro₂ :
  ∀ ⦃x y : UnitAddTorus d⦄ (hxy : x ≠ y),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
⊢ (mFourierSubalgebra d).SeparatesPoints
have intro₃ : ∀ ⦃x y : UnitAddTorus d⦄ (hxy : ∃ (x_1 : d), ¬x x_1 = y x_1),
  ∃ (f : UnitAddTorus d → ℂ),
    Membership.mem (γ := Set (UnitAddTorus d → ℂ))
        ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
          (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
        f ∧
      f x ≠ f y
Tactic: classical
  intro x y hxy
  rw [Ne, funext_iff, not_forall] at hxy
  obtain ⟨i, hi⟩ := hxy
  refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩
  dsimp only
  rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]
  contrapose hi
  exact AddCircle.injective_toCircle one_ne_zero hi
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
intro intro₁ intro₂ :
  ∀ ⦃x y : UnitAddTorus d⦄ (hxy : x ≠ y),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₃ :
  ∀ ⦃x y : UnitAddTorus d⦄ (hxy : ∃ (x_1 : d), ¬x x_1 = y x_1),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
⊢ (mFourierSubalgebra d).SeparatesPoints
have intro₄ : ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
  ∃ (f : UnitAddTorus d → ℂ),
    Membership.mem (γ := Set (UnitAddTorus d → ℂ))
        ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
          (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
        f ∧
      f x ≠ f y
Tactic: classical
  intro x y hxy
  rw [Ne, funext_iff, not_forall] at hxy
  obtain ⟨i, hi⟩ := hxy
  refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩
  dsimp only
  rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]
  contrapose hi
  exact AddCircle.injective_toCircle one_ne_zero hi
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
intro intro₁ intro₂ :
  ∀ ⦃x y : UnitAddTorus d⦄ (hxy : x ≠ y),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₃ :
  ∀ ⦃x y : UnitAddTorus d⦄ (hxy : ∃ (x_1 : d), ¬x x_1 = y x_1),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₄ :
  ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
⊢ (mFourierSubalgebra d).SeparatesPoints
have intro₅ : ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
  Ne (α := ℂ)
    ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
      (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) x)
    ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
      (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) y)
Tactic: classical
  intro x y hxy
  rw [Ne, funext_iff, not_forall] at hxy
  obtain ⟨i, hi⟩ := hxy
  refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩
  dsimp only
  rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]
  contrapose hi
  exact AddCircle.injective_toCircle one_ne_zero hi
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
intro intro₁ intro₂ :
  ∀ ⦃x y : UnitAddTorus d⦄ (hxy : x ≠ y),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₃ :
  ∀ ⦃x y : UnitAddTorus d⦄ (hxy : ∃ (x_1 : d), ¬x x_1 = y x_1),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₄ :
  ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₅ :
  ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
    Ne (α := ℂ)
      ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
        (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) x)
      ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
        (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) y)
intro₆ :
  ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
    Ne (α := ℂ) ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) x : ℂ)
      ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) y : ℂ)
⊢ (mFourierSubalgebra d).SeparatesPoints
have intro₇ : ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i), ¬AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
Tactic: classical
  intro x y hxy
  rw [Ne, funext_iff, not_forall] at hxy
  obtain ⟨i, hi⟩ := hxy
  refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩
  dsimp only
  rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]
  contrapose hi
  exact AddCircle.injective_toCircle one_ne_zero hi
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
intro intro₁ intro₂ :
  ∀ ⦃x y : UnitAddTorus d⦄ (hxy : x ≠ y),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₃ :
  ∀ ⦃x y : UnitAddTorus d⦄ (hxy : ∃ (x_1 : d), ¬x x_1 = y x_1),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₄ :
  ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
    ∃ (f : UnitAddTorus d → ℂ),
      Membership.mem (γ := Set (UnitAddTorus d → ℂ))
          ((fun (f : C(UnitAddTorus d, ℂ)) ↦ (⇑f : (a : UnitAddTorus d) → ℂ)) ''
            (↑(mFourierSubalgebra d).toSubalgebra : Set C(UnitAddTorus d, ℂ)))
          f ∧
        f x ≠ f y
intro₅ :
  ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
    Ne (α := ℂ)
      ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
        (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) x)
      ((fun (f : C(UnitAddTorus d, ℂ)) ↦ ((⇑f : (a : UnitAddTorus d) → ℂ) : (a : UnitAddTorus d) → ℂ))
        (mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1)) y)
intro₆ :
  ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i),
    Ne (α := ℂ) ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) x : ℂ)
      ((mFourier (Pi.single (M := fun (a : d) ↦ ℤ) i 1) : (a : UnitAddTorus d) → ℂ) y : ℂ)
intro₇ : ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : ¬x i = y i), ¬AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
⊢ (mFourierSubalgebra d).SeparatesPoints
have intro₈ : ∀ ⦃x y : UnitAddTorus d⦄ (i : d) (hi : AddCircle.toCircle (x i) = AddCircle.toCircle (y i)), x i = y i
Tactic: classical
  intro x y hxy
  rw [Ne, funext_iff, not_forall] at hxy
  obtain ⟨i, hi⟩ := hxy
  refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩
  dsimp only
  rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]
  contrapose hi
  exact AddCircle.injective_toCircle one_ne_zero hi
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
⊢ Eq.{u_1 + 1} (α := Submodule ℂ C(UnitAddTorus d, ℂ)) (topologicalClosure (span ℂ (range mFourier))) ⊤
have rw : Eq.{u_1 + 1} (α := Submodule ℂ C(UnitAddTorus d, ℂ))
  (topologicalClosure
    ((Subalgebra.toSubmodule : (a : Subalgebra ℂ C(UnitAddTorus d, ℂ)) → Submodule ℂ C(UnitAddTorus d, ℂ))
      (mFourierSubalgebra d).toSubalgebra))
  ⊤
Tactic: rw [← mFourierSubalgebra_coe]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (goal)
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
⊢ MeasurePreserving (α := UnitAddTorus d) (β := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
    (⇑(measurableEquivPiIoc a) : (a_1 : UnitAddTorus d) → { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) volume
    (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)
have refine : Eq (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
  (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
    (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
    (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
Tactic: refine (⟨(measurableEquivPiIoc a).symm.measurable, symm ?_⟩ :
    MeasurePreserving (measurableEquivPiIoc a).symm _ _).symm
-- Lean 4 proof step from Mathlib.Analysis.Fourier.AddCircleMulti (hypothesis)
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
⊢ Eq (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
have this : Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
  (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
  (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
    ((fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1)) ∘
      Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
    (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
Tactic: have := Measure.map_map (μ := volume.comap Subtype.val) (measurable_pi_lambda
    (fun (x : d → ℝ) => (fun i => x i : UnitAddTorus d))
    (fun i => AddCircle.measurable_mk'.comp (measurable_pi_apply i)))
    measurable_subtype_coe (α := {x : d → ℝ // ∀ i, x i ∈ Ioc (a i) (a i + 1)})