-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem polarCoord_source_ae_eq_univ : polarCoord.source =ᵐ[volume] univ

Proof state:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ polarCoord.source =ᶠ[ae volume] univ

Tactic:
have B : volume (LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) : Set (ℝ × ℝ)) = 0 := by
  apply Measure.addHaar_submodule
  rw [Ne, LinearMap.ker_eq_top]
  intro h
  have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
  simp at this

Result:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ polarCoord.source =ᶠ[ae volume] univ

Proof state:
x : ℝ × ℝ
hx : x ∈ polarCoord.sourceᶜ
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))

Tactic:
simp only [polarCoord_source, compl_union, mem_inter_iff, mem_compl_iff, mem_setOf_eq, not_lt,
  Classical.not_not] at hx

Result:
x : ℝ × ℝ
hx : x.1 ≤ 0 ∧ x.2 = 0
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))

Proof state:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ (LinearMap.snd ℝ ℝ ℝ) (0, 1) = 0 (0, 1)

Tactic:
rw [h]

Result:
no goals

Proof state:
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ ¬LinearMap.snd ℝ ℝ ℝ = 0

Tactic:
intro h

Result:
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ False

Proof state:
⊢ polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))

Tactic:
intro x hx

Result:
x : ℝ × ℝ
hx : x ∈ polarCoord.sourceᶜ
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))

Proof state:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ volume polarCoord.sourceᶜ = 0

Tactic:
exact le_antisymm ((measure_mono A).trans (le_of_eq B)) bot_le

Result:
no goals

Proof state:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0

Tactic:
apply Measure.addHaar_submodule

Result:
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) ≠ ⊤

Proof state:
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
this : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = 0 (0, 1)
⊢ False

Tactic:
simp at this

Result:
no goals

Proof state:
x : ℝ × ℝ
hx : x.1 ≤ 0 ∧ x.2 = 0
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))

Tactic:
exact hx.2

Result:
no goals

Proof state:
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ False

Tactic:
have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]

Result:
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
this : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = 0 (0, 1)
⊢ False

Proof state:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ polarCoord.source =ᶠ[ae volume] univ

Tactic:
simp only [ae_eq_univ]

Result:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ volume polarCoord.sourceᶜ = 0

Proof state:
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) ≠ ⊤

Tactic:
rw [Ne, LinearMap.ker_eq_top]

Result:
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ ¬LinearMap.snd ℝ ℝ ℝ = 0

Proof state:
⊢ polarCoord.source =ᶠ[ae volume] univ

Tactic:
have A : polarCoord.sourceᶜ ⊆ LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) := by
  intro x hx
  simp only [polarCoord_source, compl_union, mem_inter_iff, mem_compl_iff, mem_setOf_eq, not_lt,
    Classical.not_not] at hx
  exact hx.2

Result:
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ polarCoord.source =ᶠ[ae volume] univ