-- Mathlib/MeasureTheory/Measure/Haar/Disintegration.lean
/-- Given a linear map `L : E → F`, a property holds almost everywhere in `F` if and only if,
almost everywhere in `F`, it holds almost everywhere along the subspace spanned by the
image of `L`. This is an instance of a disintegration argument for additive Haar measures. -/
lemma ae_ae_add_linearMap_mem_iff [LocallyCompactSpace F] {s : Set F} (hs : MeasurableSet s) :
    (∀ᵐ y ∂ν, ∀ᵐ x ∂μ, y + L x ∈ s) ↔ ∀ᵐ y ∂ν, y ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this✝² : FiniteDimensional 𝕜 E
this✝¹ : FiniteDimensional 𝕜 F
this✝ : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L
M_cont : Continuous ⇑M
hM : Function.Surjective ⇑M
A : ∀ (x : F × E), M x ∈ s ↔ x ∈ ⇑M ⁻¹' s
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (x : F × E) ∂ν.prod μ, x ∈ ⇑M ⁻¹' s

Tactic:
rw [Measure.ae_prod_mem_iff_ae_ae_mem]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this✝² : FiniteDimensional 𝕜 E
this✝¹ : FiniteDimensional 𝕜 F
this✝ : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L
M_cont : Continuous ⇑M
hM : Function.Surjective ⇑M
A : ∀ (x : F × E), M x ∈ s ↔ x ∈ ⇑M ⁻¹' s
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (x : F) ∂ν, ∀ᵐ (y : E) ∂μ, (x, y) ∈ ⇑M ⁻¹' s

𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this✝² : FiniteDimensional 𝕜 E
this✝¹ : FiniteDimensional 𝕜 F
this✝ : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L
M_cont : Continuous ⇑M
hM : Function.Surjective ⇑M
A : ∀ (x : F × E), M x ∈ s ↔ x ∈ ⇑M ⁻¹' s
⊢ MeasurableSet (⇑M ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this✝² : FiniteDimensional 𝕜 E
this✝¹ : FiniteDimensional 𝕜 F
this✝ : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L
M_cont : Continuous ⇑M
hM : Function.Surjective ⇑M
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
have A : ∀ x, M x ∈ s ↔ x ∈ M ⁻¹' s := fun x ↦ Iff.rfl

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this✝² : FiniteDimensional 𝕜 E
this✝¹ : FiniteDimensional 𝕜 F
this✝ : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L
M_cont : Continuous ⇑M
hM : Function.Surjective ⇑M
A : ∀ (x : F × E), M x ∈ s ↔ x ∈ ⇑M ⁻¹' s
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this✝² : FiniteDimensional 𝕜 E
this✝¹ : FiniteDimensional 𝕜 F
this✝ : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L
M_cont : Continuous ⇑M
hM : Function.Surjective ⇑M
A : ∀ (x : F × E), M x ∈ s ↔ x ∈ ⇑M ⁻¹' s
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (x : F) ∂ν, ∀ᵐ (y : E) ∂μ, (x, y) ∈ ⇑M ⁻¹' s

Tactic:
simp only [M, mem_preimage, LinearMap.coprod_apply, LinearMap.id_coe, id_eq]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this✝² : FiniteDimensional 𝕜 E
this✝¹ : FiniteDimensional 𝕜 F
this✝ : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L
M_cont : Continuous ⇑M
⊢ Function.Surjective ⇑M

Tactic:
simp [M, ← LinearMap.range_eq_top (f := _), LinearMap.range_coprod]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this✝¹ : FiniteDimensional 𝕜 E
this✝ : FiniteDimensional 𝕜 F
this : ProperSpace E
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
have : ProperSpace F := .of_locallyCompactSpace 𝕜

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : NontriviallyNormedField 𝕜
inst✝¹² : CompleteSpace 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : BorelSpace E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : MeasurableSpace F
inst✝⁵ : BorelSpace F
inst✝⁴ : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst✝³ : μ.IsAddHaarMeasure
inst✝² : ν.IsAddHaarMeasure
inst✝¹ : LocallyCompactSpace E
inst✝ : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this✝² : FiniteDimensional 𝕜 E
this✝¹ : FiniteDimensional 𝕜 F
this✝ : ProperSpace E
this : ProperSpace F
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s