awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
this_1 : FiniteDimensional 𝕜 E
this : ProperSpace F
S : Submodule 𝕜 E := L.ker
T : Submodule 𝕜 E
hT : IsCompl S T
M : (↥S × ↥T) ≃ₗ[𝕜] E := S.prodEquivOfIsCompl T hT
M_cont : Continuous (X := E) (Y := ↥S × ↥T) (⇑M.symm : (a : E) → ↥S × ↥T)
P : ↥S × ↥T →ₗ[𝕜] ↥T := snd 𝕜 ↥S ↥T
P_cont : Continuous (X := ↥S × ↥T) (Y := ↥T) (⇑P : (a : ↥S × ↥T) → ↥T)
I_1 : Function.Bijective.{u_2 + 1, u_3 + 1} (α := ↥T) (β := F) (⇑(L.domRestrict T) : (a : ↥T) → F)
L' : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id 𝕜) (↥T) F := LinearEquiv.ofBijective (L.domRestrict T) I_1
L'_cont : Continuous.{u_2, u_3} (X := ↥T) (Y := F) (⇑L' : (a : ↥T) → F)
A : L = (↑L' : ↥T →ₗ[𝕜] F) ∘ₗ P ∘ₗ (↑M.symm : E →ₗ[𝕜] ↥S × ↥T)
I :
  Eq.{u_3 + 1} (α := Measure F) (map (⇑L : (a : E) → F) μ)
    (map (α := ↥T) (⇑L' : (a : ↥T) → F)
      (map (α := ↥S × ↥T) (⇑P : (a : ↥S × ↥T) → ↥T) (map (⇑M.symm : (a : E) → ↥S × ↥T) μ)))
μS : Measure ↥S := addHaar
μT : Measure ↥T := addHaar
c₀ : ℝ≥0∞
c₀_pos : c₀ ≠ 0
c₀_fin : c₀ ≠ ∞
h₀ : map (⇑M.symm : (a : E) → ↥S × ↥T) μ = c₀ • μS.prod μT
J : map (⇑P : (a : ↥S × ↥T) → ↥T) (μS.prod μT) = HSMul.hSMul (α := ℝ≥0∞) ((μS : (a : Set ↥S) → ℝ≥0∞) univ : ℝ≥0∞) μT
c₁ : ℝ≥0∞
c₁_pos : c₁ ≠ 0
c₁_fin : c₁ ≠ ∞
h₁ : map (⇑L' : (a : ↥T) → F) μT = c₁ • ν
rw :
  (c₀ * HMul.hMul (α := ℝ≥0∞) ((μS : (a : Set ↥S) → ℝ≥0∞) univ : ℝ≥0∞) c₁) • ν =
    HMul.hMul (β := ℝ≥0∞) (c₀ * c₁) (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
rw₁ :
  (c₀ * HMul.hMul (β := ℝ≥0∞) c₁ ((μS : (a : Set ↥S) → ℝ≥0∞) univ : ℝ≥0∞)) • ν =
    HMul.hMul (β := ℝ≥0∞) (c₀ * c₁) (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
rw₂ rw₃ :
  HMul.hMul (β := ℝ≥0∞) (c₀ * c₁) ((μS : (a : Set ↥S) → ℝ≥0∞) univ : ℝ≥0∞) • ν =
    HMul.hMul (β := ℝ≥0∞) (c₀ * c₁) (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
⊢ (HMul.hMul (β := ℝ≥0∞) c₀ ((μS : (a : Set ↥S) → ℝ≥0∞) univ : ℝ≥0∞) * c₁) • ν =
    HMul.hMul (β := ℝ≥0∞) (c₀ * c₁) (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν

Tactic:
rw [mul_assoc, mul_comm _ c₁, ← mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
rcases :
  ∀ (c : ℝ≥0∞) (c_pos : 0 < c)
    (hc :
      map (⇑L : (a : E) → F) μ =
        HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν),
    ∃ (c : ℝ≥0∞), 0 < c ∧ map (⇑L : (a : E) → F) μ = c • ν
⊢ ∃ (c : ℝ≥0∞), 0 < c ∧ map (⇑L : (a : E) → F) μ = c • ν

Tactic:
rcases L.exists_map_addHaar_eq_smul_addHaar' μ ν h with ⟨c, c_pos, -, hc⟩

Premises used: LinearMap.exists_map_addHaar_eq_smul_addHaar'
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
c : ℝ≥0∞
c_pos : 0 < c
hc :
  map (⇑L : (a : E) → F) μ =
    HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
⊢ 0 < HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp [c_pos, NeZero.ne addHaar]

Premises used: MeasureTheory.Measure.addHaar, NeZero.ne
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
c : ℝ≥0∞
c_pos : 0 < c
hc :
  map (⇑L : (a : E) → F) μ =
    HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
⊢ ∃ (c : ℝ≥0∞), 0 < c ∧ map (⇑L : (a : E) → F) μ = c • ν

Tactic:
exact ⟨_, by simp [c_pos, NeZero.ne addHaar], hc⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
s : Set F
hs : MeasurableSet s
⊢ FiniteDimensional 𝕜 E

Tactic:
have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
s : Set F
hs : MeasurableSet s
this : FiniteDimensional 𝕜 E
⊢ AEMeasurable.{u_2, u_3} (β := F) (⇑L : (a : E) → F) μ

Tactic:
have : AEMeasurable L μ := L.continuous_of_finiteDimensional.aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this : AEMeasurable.{u_2, u_3} (β := F) (⇑L : (a : E) → F) μ
apply : (∀ᵐ (y : F) ∂map (⇑L : (a : E) → F) μ, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
⊢ (∀ᵐ (x : E) ∂μ, Membership.mem (α := F) s ((L : (a : E) → F) x : F)) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
apply (ae_map_iff this hs).symm.trans

Premises used: MeasureTheory.ae_map_iff, Iff.trans, Iff.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this : AEMeasurable.{u_2, u_3} (β := F) (⇑L : (a : E) → F) μ
rcases :
  ∀ (c : ℝ≥0∞) (c_pos : 0 < c) (hc : map (⇑L : (a : E) → F) μ = c • ν),
    (∀ᵐ (y : F) ∂map (⇑L : (a : E) → F) μ, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
⊢ (∀ᵐ (y : F) ∂map (⇑L : (a : E) → F) μ, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
rcases L.exists_map_addHaar_eq_smul_addHaar μ ν h with ⟨c, c_pos, hc⟩

Premises used: LinearMap.exists_map_addHaar_eq_smul_addHaar
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this : AEMeasurable.{u_2, u_3} (β := F) (⇑L : (a : E) → F) μ
c : ℝ≥0∞
c_pos : 0 < c
hc : map (⇑L : (a : E) → F) μ = c • ν
rw : (∀ᵐ (y : F) ∂c • ν, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
⊢ (∀ᵐ (y : F) ∂map (⇑L : (a : E) → F) μ, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
rw [hc]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this : AEMeasurable.{u_2, u_3} (β := F) (⇑L : (a : E) → F) μ
c : ℝ≥0∞
c_pos : 0 < c
hc : map (⇑L : (a : E) → F) μ = c • ν
⊢ (∀ᵐ (y : F) ∂c • ν, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
ae_ennreal_smul_measure_iff c_pos.ne'

Premises used: Set.Mem, MeasureTheory.Measure.ae_ennreal_smul_measure_iff, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
h : Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑L : (a : E) → F)
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this : AEMeasurable.{u_2, u_3} (β := F) (⇑L : (a : E) → F) μ
c : ℝ≥0∞
c_pos : 0 < c
hc : map (⇑L : (a : E) → F) μ = c • ν
⊢ (∀ᵐ (y : F) ∂c • ν, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
exact ae_ennreal_smul_measure_iff c_pos.ne'

Premises used: MeasureTheory.Measure.ae_ennreal_smul_measure_iff, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
⊢ FiniteDimensional 𝕜 E

Tactic:
have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this : FiniteDimensional 𝕜 E
⊢ FiniteDimensional 𝕜 F

Tactic:
have : FiniteDimensional 𝕜 F := .of_locallyCompactSpace 𝕜
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this : FiniteDimensional 𝕜 F
⊢ ProperSpace E

Tactic:
have : ProperSpace E := .of_locallyCompactSpace 𝕜
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this_2 : FiniteDimensional 𝕜 F
this : ProperSpace E
⊢ ProperSpace F

Tactic:
have : ProperSpace F := .of_locallyCompactSpace 𝕜
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this_2 : FiniteDimensional 𝕜 F
this_3 : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.coprod LinearMap.id L
⊢ Continuous (X := F × E) (Y := F) (⇑M : (a : F × E) → F)

Tactic:
have M_cont : Continuous M := M.continuous_of_finiteDimensional
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this_2 : FiniteDimensional 𝕜 F
this_3 : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.coprod LinearMap.id L
M_cont : Continuous (X := F × E) (Y := F) (⇑M : (a : F × E) → F)
⊢ Function.Surjective (α := F × E) (β := F) (⇑M : (a : F × E) → F)

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

Premises used: LinearMap.range_eq_top, LinearMap.range_coprod
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this_2 : FiniteDimensional 𝕜 F
this_3 : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.coprod LinearMap.id L
M_cont : Continuous (X := F × E) (Y := F) (⇑M : (a : F × E) → F)
⊢ Function.Surjective (α := F × E) (β := F) (⇑M : (a : F × E) → F)

Tactic:
have hM : Function.Surjective M := by
    simp [M, ← LinearMap.range_eq_top (f := _), LinearMap.range_coprod]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this_2 : FiniteDimensional 𝕜 F
this_3 : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.coprod LinearMap.id L
M_cont : Continuous (X := F × E) (Y := F) (⇑M : (a : F × E) → F)
hM : Function.Surjective (α := F × E) (β := F) (⇑M : (a : F × E) → F)
⊢ ∀ (x : F × E),
    Membership.mem (α := F) s ((M : (a : F × E) → F) x : F) ↔
      Membership.mem (γ := Set (F × E)) ((⇑M : (a : F × E) → F) ⁻¹' s) x

Tactic:
have A : ∀ x, M x ∈ s ↔ x ∈ M ⁻¹' s := fun x ↦ Iff.rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this_2 : FiniteDimensional 𝕜 F
this_3 : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.coprod LinearMap.id L
M_cont : Continuous (X := F × E) (Y := F) (⇑M : (a : F × E) → F)
hM : Function.Surjective (α := F × E) (β := F) (⇑M : (a : F × E) → F)
A :
  ∀ (x : F × E),
    Membership.mem (α := F) s ((M : (a : F × E) → F) x : F) ↔
      Membership.mem (γ := Set (F × E)) ((⇑M : (a : F × E) → F) ⁻¹' s) x
simp_rw :
  (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔
    ∀ᵐ (x : F × E) ∂ν.prod μ, Membership.mem (γ := Set (F × E)) ((⇑M : (a : F × E) → F) ⁻¹' s) x
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s

Tactic:
simp_rw [← ae_comp_linearMap_mem_iff M (ν.prod μ) ν hM hs, A]

Premises used: MeasureTheory.Measure.prod, MeasureTheory.ae_comp_linearMap_mem_iff
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this_2 : FiniteDimensional 𝕜 F
this_3 : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.coprod LinearMap.id L
M_cont : Continuous (X := F × E) (Y := F) (⇑M : (a : F × E) → F)
hM : Function.Surjective (α := F × E) (β := F) (⇑M : (a : F × E) → F)
A :
  ∀ (x : F × E),
    Membership.mem (α := F) s ((M : (a : F × E) → F) x : F) ↔
      Membership.mem (γ := Set (F × E)) ((⇑M : (a : F × E) → F) ⁻¹' s) x
rw :
  (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔
    ∀ᵐ (x : F) ∂ν, ∀ᵐ (y : E) ∂μ, Membership.mem (γ := Set (F × E)) ((⇑M : (a : F × E) → F) ⁻¹' s) (x, y)
rw₁ : MeasurableSet (α := F × E) ((⇑M : (a : F × E) → F) ⁻¹' s)
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔
    ∀ᵐ (x : F × E) ∂ν.prod μ, Membership.mem (γ := Set (F × E)) ((⇑M : (a : F × E) → F) ⁻¹' s) x

Tactic:
rw [Measure.ae_prod_mem_iff_ae_ae_mem]

Premises used: MeasureTheory.Measure.ae_prod_mem_iff_ae_ae_mem
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this_2 : FiniteDimensional 𝕜 F
this_3 : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.coprod LinearMap.id L
M_cont : Continuous (X := F × E) (Y := F) (⇑M : (a : F × E) → F)
hM : Function.Surjective (α := F × E) (β := F) (⇑M : (a : F × E) → F)
A :
  ∀ (x : F × E),
    Membership.mem (α := F) s ((M : (a : F × E) → F) x : F) ↔
      Membership.mem (γ := Set (F × E)) ((⇑M : (a : F × E) → F) ⁻¹' s) x
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔
    ∀ᵐ (x : F) ∂ν, ∀ᵐ (y : E) ∂μ, Membership.mem (γ := Set (F × E)) ((⇑M : (a : F × E) → F) ⁻¹' s) (x, y)

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

Premises used: LinearMap.id_coe, LinearMap.coprod_apply, Set.mem_preimage, id_eq
-- Module: Mathlib.MeasureTheory.Measure.Haar.Disintegration
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : CompleteSpace 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : NormedSpace 𝕜 E
inst_6 : NormedAddCommGroup F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
inst_9 : NormedSpace 𝕜 F
L : E →ₗ[𝕜] F
μ : Measure E
ν : Measure F
inst_10 : μ.IsAddHaarMeasure
inst_11 : ν.IsAddHaarMeasure
inst_12 : LocallyCompactSpace E
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this_2 : FiniteDimensional 𝕜 F
this_3 : ProperSpace E
this : ProperSpace F
M : F × E →ₗ[𝕜] F := LinearMap.coprod LinearMap.id L
M_cont : Continuous (X := F × E) (Y := F) (⇑M : (a : F × E) → F)
hM : Function.Surjective (α := F × E) (β := F) (⇑M : (a : F × E) → F)
A :
  ∀ (x : F × E),
    Membership.mem (α := F) s ((M : (a : F × E) → F) x : F) ↔
      Membership.mem (γ := Set (F × E)) ((⇑M : (a : F × E) → F) ⁻¹' s) x
⊢ MeasurableSet (α := F × E) ((⇑M : (a : F × E) → F) ⁻¹' s)

Tactic:
M_cont.measurable hs

Premises used: Continuous.measurable