-- Mathlib/Analysis/Fourier/AddCircleMulti.lean
lemma mFourier_single [DecidableEq d] (z : d → AddCircle (1 : ℝ)) (i : d) :
    mFourier (Pi.single i 1) z = fourier 1 (z i)

Proof state:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
⊢ ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1) = (fourier 1) (z i)

Tactic:
have := Finset.prod_mul_prod_compl {i} (fun j ↦ fourier ((Pi.single i (1 : ℤ) : d → ℤ) j) (z j))

Result:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this :
  (∏ i_1 ∈ {i}, (fourier (Pi.single i 1 i_1)) (z i_1)) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1)
⊢ ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1) = (fourier 1) (z i)

Proof state:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this :
  (∏ i_1 ∈ {i}, (fourier (Pi.single i 1 i_1)) (z i_1)) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1)
⊢ ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1) = (fourier 1) (z i)

Tactic:
rw [Finset.prod_singleton, Finset.prod_congr rfl (fun j hj ↦ ?_)] at this

Result:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this✝ :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1)
this : (fourier (Pi.single i 1 i)) (z i) * {i}ᶜ.prod ?m.13002 = ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1)
⊢ ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1) = (fourier 1) (z i)

d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1)
⊢ d → ℂ

d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1)
j : d
hj : j ∈ {i}ᶜ
⊢ (fourier (Pi.single i 1 j)) (z j) = ?m.13002 j

Proof state:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this✝ :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1)
this : (fourier (Pi.single i 1 i)) (z i) * {i}ᶜ.prod ?m.13002 = ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1)
⊢ ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1) = (fourier 1) (z i)

Tactic:
rw [← this, Finset.prod_const_one, mul_one, Pi.single_eq_same]

Result:
no goals

Proof state:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1)
j : d
hj : j ∈ {i}ᶜ
⊢ (fourier (Pi.single i 1 j)) (z j) = 1

Tactic:
rw [Finset.mem_compl, Finset.mem_singleton] at hj

Result:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1)
j : d
hj : ¬j = i
⊢ (fourier (Pi.single i 1 j)) (z j) = 1

Proof state:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
this :
  (fourier (Pi.single i 1 i)) (z i) * ∏ i_1 ∈ {i}ᶜ, (fourier (Pi.single i 1 i_1)) (z i_1) =
    ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1)
j : d
hj : ¬j = i
⊢ (fourier (Pi.single i 1 j)) (z j) = 1

Tactic:
simp only [Pi.single_eq_of_ne hj, fourier_zero]

Result:
no goals

Proof state:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
⊢ (mFourier (Pi.single i 1)) z = (fourier 1) (z i)

Tactic:
simp_rw [mFourier, ContinuousMap.coe_mk]

Result:
d : Type u_1
inst✝¹ : Fintype d
inst✝ : DecidableEq d
z : d → AddCircle 1
i : d
⊢ ∏ i_1 : d, (fourier (Pi.single i 1 i_1)) (z i_1) = (fourier 1) (z i)