A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ polarCoord.source =ᵐ[volume] univ
⊢ polarCoord.source =ᵐ[volume] univ
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
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : ↑↑volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ polarCoord.source =ᵐ[volume] univ
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ polarCoord.source =ᵐ[volume] univ
have B : volume (LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) : Set (ℝ × ℝ)) = 0 := by
  apply Measure.add_haar_submodule
  rw [Ne.def, LinearMap.ker_eq_top]
  intro h
  have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
  simp at this
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : ↑↑volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ ↑↑volume (polarCoord.sourceᶜ) = 0
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : ↑↑volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ polarCoord.source =ᵐ[volume] univ
simp only [ae_eq_univ]
no goals
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
B : ↑↑volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
⊢ ↑↑volume (polarCoord.sourceᶜ) = 0
exact le_antisymm ((measure_mono A).trans (le_of_eq B)) bot_le
x : ℝ × ℝ
hx : x ∈ polarCoord.sourceᶜ
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
intro x hx
x : ℝ × ℝ
hx : x.fst ≤ 0 ∧ x.snd = 0
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
x : ℝ × ℝ
hx : x ∈ polarCoord.sourceᶜ
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
simp only [polarCoord_source, compl_union, mem_inter_iff, mem_compl_iff, mem_setOf_eq, not_lt,
  Classical.not_not] at hx
no goals
x : ℝ × ℝ
hx : x.fst ≤ 0 ∧ x.snd = 0
⊢ x ∈ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
exact hx.2
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) ≠ ⊤
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ ↑↑volume ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ)) = 0
apply Measure.add_haar_submodule
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ ¬LinearMap.snd ℝ ℝ ℝ = 0
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) ≠ ⊤
rw [Ne.def, LinearMap.ker_eq_top]
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ False
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
⊢ ¬LinearMap.snd ℝ ℝ ℝ = 0
intro h
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
this : ↑(LinearMap.snd ℝ ℝ ℝ) (0, 1) = ↑0 (0, 1)
⊢ False
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ False
have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
no goals
case hs
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
this : ↑(LinearMap.snd ℝ ℝ ℝ) (0, 1) = ↑0 (0, 1)
⊢ False
simp at this
no goals
A : polarCoord.sourceᶜ ⊆ ↑(LinearMap.ker (LinearMap.snd ℝ ℝ ℝ))
h : LinearMap.snd ℝ ℝ ℝ = 0
⊢ ↑(LinearMap.snd ℝ ℝ ℝ) (0, 1) = ↑0 (0, 1)
rw [h]