case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : ⊥ ≠ ⊤
⊢ ↑↑μ ↑⊥ = 0

case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : AffineSubspace ℝ E
hs : s ≠ ⊤
hne : Set.Nonempty ↑s
⊢ ↑↑μ ↑s = 0
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : AffineSubspace ℝ E
hs : s ≠ ⊤
⊢ ↑↑μ ↑s = 0
rcases s.eq_bot_or_nonempty with (rfl | hne)
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : AffineSubspace ℝ E
hs : ¬AffineSubspace.direction s = ⊤
hne : Set.Nonempty ↑s
⊢ ↑↑μ ↑s = 0
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : AffineSubspace ℝ E
hs : s ≠ ⊤
hne : Set.Nonempty ↑s
⊢ ↑↑μ ↑s = 0
rw [Ne.def, ← AffineSubspace.direction_eq_top_iff_of_nonempty hne] at hs
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : AffineSubspace ℝ E
hs : ¬AffineSubspace.direction s = ⊤
x : E
hx : x ∈ s
⊢ ↑↑μ ↑s = 0
case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : AffineSubspace ℝ E
hs : ¬AffineSubspace.direction s = ⊤
hne : Set.Nonempty ↑s
⊢ ↑↑μ ↑s = 0
rcases hne with ⟨x, hx : x ∈ s⟩
no goals
case inr.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
s : AffineSubspace ℝ E
hs : ¬AffineSubspace.direction s = ⊤
x : E
hx : x ∈ s
⊢ ↑↑μ ↑s = 0
simpa only [AffineSubspace.coe_direction_eq_vsub_set_right hx, vsub_eq_sub, sub_eq_add_neg,
  image_add_right, neg_neg, measure_preimage_add_right] using add_haar_submodule μ s.direction hs
no goals
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : IsAddHaarMeasure μ
hs : ⊥ ≠ ⊤
⊢ ↑↑μ ↑⊥ = 0
rw [AffineSubspace.bot_coe, measure_empty]