-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem orthonormal_fourier : Orthonormal ℂ (@fourierLp T _ 2 _)

Proof state:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ -i + j ≠ 0

Tactic:
rw [add_comm]

Result:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ j + -i ≠ 0

Proof state:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ ⇑(fourier 0) = fun x => 1

Tactic:
ext1

Result:
case h
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
x✝ : AddCircle T
⊢ (fourier 0) x✝ = 1

Proof state:
case neg
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
hij : -i + j ≠ 0
⊢ ∫ (x : AddCircle T), (fourier (-i + j)) x ∂haarAddCircle = 0

Tactic:
convert integral_eq_zero_of_add_right_eq_neg (μ := haarAddCircle)
  (fourier_add_half_inv_index hij hT.elim)

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ j + -i ≠ 0

Tactic:
exact sub_ne_zero.mpr (Ne.symm h)

Result:
no goals

Proof state:
case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
this : ⇑(fourier 0) = fun x => 1
⊢ ∫ (x : AddCircle T), (fourier 0) x ∂haarAddCircle = 1

Tactic:
rw [this, integral_const, measure_univ, ENNReal.one_toReal, Complex.real_smul,
  Complex.ofReal_one, mul_one]

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ ∫ (x : AddCircle T), (fourier (-i + j)) x ∂haarAddCircle = if i = j then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ ∫ (x : AddCircle T), (fourier (-i + j)) x ∂haarAddCircle = 1

case neg
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ ∫ (x : AddCircle T), (fourier (-i + j)) x ∂haarAddCircle = 0

Proof state:
T : ℝ
hT : Fact (0 < T)
⊢ Orthonormal ℂ (fourierLp 2)

Tactic:
rw [orthonormal_iff_ite]

Result:
T : ℝ
hT : Fact (0 < T)
⊢ ∀ (i j : ℤ), inner (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0

Proof state:
case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ ∫ (x : AddCircle T), (fourier (-i + j)) x ∂haarAddCircle = 1

Tactic:
simp_rw [h, neg_add_cancel]

Result:
case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ ∫ (x : AddCircle T), (fourier 0) x ∂haarAddCircle = 1

Proof state:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ inner (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0

Tactic:
rw [ContinuousMap.inner_toLp (@haarAddCircle T hT) (fourier i) (fourier j)]

Result:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ ∫ (x : AddCircle T), (starRingEnd ℂ) ((fourier i) x) * (fourier j) x ∂haarAddCircle = if i = j then 1 else 0

Proof state:
case neg
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
⊢ ∫ (x : AddCircle T), (fourier (-i + j)) x ∂haarAddCircle = 0

Tactic:
have hij : -i + j ≠ 0 := by
  rw [add_comm]
  exact sub_ne_zero.mpr (Ne.symm h)

Result:
case neg
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : ¬i = j
hij : -i + j ≠ 0
⊢ ∫ (x : AddCircle T), (fourier (-i + j)) x ∂haarAddCircle = 0

Proof state:
case h
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
x✝ : AddCircle T
⊢ (fourier 0) x✝ = 1

Tactic:
exact fourier_zero

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ ∫ (x : AddCircle T), (starRingEnd ℂ) ((fourier i) x) * (fourier j) x ∂haarAddCircle = if i = j then 1 else 0

Tactic:
simp_rw [← fourier_neg, ← fourier_add]

Result:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ ∫ (x : AddCircle T), (fourier (-i + j)) x ∂haarAddCircle = if i = j then 1 else 0

Proof state:
case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
⊢ ∫ (x : AddCircle T), (fourier 0) x ∂haarAddCircle = 1

Tactic:
have : ⇑(@fourier T 0) = (fun _ => 1 : AddCircle T → ℂ) := by ext1; exact fourier_zero

Result:
case pos
T : ℝ
hT : Fact (0 < T)
i j : ℤ
h : i = j
this : ⇑(fourier 0) = fun x => 1
⊢ ∫ (x : AddCircle T), (fourier 0) x ∂haarAddCircle = 1

Proof state:
T : ℝ
hT : Fact (0 < T)
⊢ ∀ (i j : ℤ), inner (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0

Tactic:
intro i j

Result:
T : ℝ
hT : Fact (0 < T)
i j : ℤ
⊢ inner (fourierLp 2 i) (fourierLp 2 j) = if i = j then 1 else 0