-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
theorem mFourierSubalgebra_separatesPoints : (mFourierSubalgebra d).SeparatesPoints

Proof state:
case intro
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(mFourierSubalgebra d).toSubalgebra, f x ≠ f y

Tactic:
refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩

Result:
case intro
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ (fun f => ⇑f) (mFourier (Pi.single i 1)) x ≠ (fun f => ⇑f) (mFourier (Pi.single i 1)) y

Proof state:
case intro
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ (fun f => ⇑f) (mFourier (Pi.single i 1)) x ≠ (fun f => ⇑f) (mFourier (Pi.single i 1)) y

Tactic:
dsimp only

Result:
case intro
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ (mFourier (Pi.single i 1)) x ≠ (mFourier (Pi.single i 1)) y

Proof state:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
hxy : ∃ x_1, ¬x x_1 = y x_1
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(mFourierSubalgebra d).toSubalgebra, f x ≠ f y

Tactic:
obtain ⟨i, hi⟩ := hxy

Result:
case intro
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(mFourierSubalgebra d).toSubalgebra, f x ≠ f y

Proof state:
case intro
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)

Tactic:
contrapose! hi

Result:
case intro
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
⊢ x i = y i

Proof state:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
hxy : x ≠ y
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(mFourierSubalgebra d).toSubalgebra, f x ≠ f y

Tactic:
rw [Ne, funext_iff, not_forall] at hxy

Result:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
hxy : ∃ x_1, ¬x x_1 = y x_1
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(mFourierSubalgebra d).toSubalgebra, f x ≠ f y

Proof state:
case intro
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : ¬x i = y i
⊢ (mFourier (Pi.single i 1)) x ≠ (mFourier (Pi.single i 1)) y

Tactic:
rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]

Result:
case intro
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)

Proof state:
d : Type u_1
inst✝ : Fintype d
⊢ (mFourierSubalgebra d).SeparatesPoints

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

Result:
no goals

Proof state:
case intro
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
i : d
hi : AddCircle.toCircle (x i) = AddCircle.toCircle (y i)
⊢ x i = y i

Tactic:
exact AddCircle.injective_toCircle one_ne_zero hi

Result:
no goals

Proof state:
d : Type u_1
inst✝ : Fintype d
⊢ (mFourierSubalgebra d).SeparatesPoints

Tactic:
intro x y hxy

Result:
d : Type u_1
inst✝ : Fintype d
x y : UnitAddTorus d
hxy : x ≠ y
⊢ ∃ f ∈ (fun f => ⇑f) '' ↑(mFourierSubalgebra d).toSubalgebra, f x ≠ f y