Theorem: dirichletKernel_eq_ae (Carleson/Theorem1_1/Dirichlet_kernel.lean)

State before:
N : ℕ
⊢ ∀ᵐ (x : ℝ), dirichletKernel N x = dirichletKernel' N x
Tactic:
rw [MeasureTheory.ae_iff]
State after:
N : ℕ
⊢ MeasureTheory.volume {a | ¬dirichletKernel N a = dirichletKernel' N a} = 0

State before:
N : ℕ
⊢ MeasureTheory.volume {a | ¬dirichletKernel N a = dirichletKernel' N a} = 0
Tactic:
have : {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n : ℤ, x = n * (2 * Real.pi)} := by
  ext x
  simp
  constructor
  . sorry
  . sorry
State after:
N : ℕ
this : {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n, x = ↑n * (2 * Real.pi)}
⊢ MeasureTheory.volume {a | ¬dirichletKernel N a = dirichletKernel' N a} = 0

State before:
N : ℕ
this : {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n, x = ↑n * (2 * Real.pi)}
⊢ MeasureTheory.volume {a | ¬dirichletKernel N a = dirichletKernel' N a} = 0
Tactic:
rw [this]
State after:
N : ℕ
this : {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n, x = ↑n * (2 * Real.pi)}
⊢ MeasureTheory.volume {x | ∃ n, x = ↑n * (2 * Real.pi)} = 0

State before:
N : ℕ
this : {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n, x = ↑n * (2 * Real.pi)}
⊢ MeasureTheory.volume {x | ∃ n, x = ↑n * (2 * Real.pi)} = 0
Tactic:
sorry
State after:
no goals

State before:
N : ℕ
⊢ {x | ¬dirichletKernel N x = dirichletKernel' N x} = {x | ∃ n, x = ↑n * (2 * Real.pi)}
Tactic:
ext x
State after:
case h
N : ℕ
x : ℝ
⊢ x ∈ {x | ¬dirichletKernel N x = dirichletKernel' N x} ↔ x ∈ {x | ∃ n, x = ↑n * (2 * Real.pi)}

State before:
case h
N : ℕ
x : ℝ
⊢ x ∈ {x | ¬dirichletKernel N x = dirichletKernel' N x} ↔ x ∈ {x | ∃ n, x = ↑n * (2 * Real.pi)}
Tactic:
simp
State after:
case h
N : ℕ
x : ℝ
⊢ ¬dirichletKernel N x = dirichletKernel' N x ↔ ∃ n, x = ↑n * (2 * Real.pi)

State before:
case h
N : ℕ
x : ℝ
⊢ ¬dirichletKernel N x = dirichletKernel' N x ↔ ∃ n, x = ↑n * (2 * Real.pi)
Tactic:
constructor
State after:
case h.mp
N : ℕ
x : ℝ
⊢ ¬dirichletKernel N x = dirichletKernel' N x → ∃ n, x = ↑n * (2 * Real.pi)

case h.mpr
N : ℕ
x : ℝ
⊢ (∃ n, x = ↑n * (2 * Real.pi)) → ¬dirichletKernel N x = dirichletKernel' N x

State before:
case h.mp
N : ℕ
x : ℝ
⊢ ¬dirichletKernel N x = dirichletKernel' N x → ∃ n, x = ↑n * (2 * Real.pi)

case h.mpr
N : ℕ
x : ℝ
⊢ (∃ n, x = ↑n * (2 * Real.pi)) → ¬dirichletKernel N x = dirichletKernel' N x
Tactic:
. sorry
State after:
case h.mpr
N : ℕ
x : ℝ
⊢ (∃ n, x = ↑n * (2 * Real.pi)) → ¬dirichletKernel N x = dirichletKernel' N x

State before:
case h.mpr
N : ℕ
x : ℝ
⊢ (∃ n, x = ↑n * (2 * Real.pi)) → ¬dirichletKernel N x = dirichletKernel' N x
Tactic:
. sorry
State after:
no goals

State before:
case h.mp
N : ℕ
x : ℝ
⊢ ¬dirichletKernel N x = dirichletKernel' N x → ∃ n, x = ↑n * (2 * Real.pi)
Tactic:
sorry
State after:
no goals

State before:
case h.mpr
N : ℕ
x : ℝ
⊢ (∃ n, x = ↑n * (2 * Real.pi)) → ¬dirichletKernel N x = dirichletKernel' N x
Tactic:
sorry
State after:
no goals