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_2 : 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
this : IsAddHaarMeasure (G := ↥S × ↥T) (map (⇑M.symm : (a : E) → ↥S × ↥T) μ)
⊢ (↑(addHaarScalarFactor (map (⇑M.symm : (a : E) → ↥S × ↥T) μ) (μS.prod μT)) : ℝ≥0∞) ≠ 0

Tactic:
simpa only [ne_eq, ENNReal.coe_eq_zero] using
      (addHaarScalarFactor_pos_of_isAddHaarMeasure (μ.map M.symm) (μS.prod μT)).ne'

Premises used: LinearEquiv.symm, ENNReal.coe_eq_zero, ne_eq, LT.lt.ne', MeasureTheory.Measure.prod, MeasureTheory.Measure.map, MeasureTheory.Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure, DFunLike.coe
-- 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
obtain :
  ∀ (c₀ : ℝ≥0∞) (c₀_pos : c₀ ≠ 0) (c₀_fin : c₀ ≠ ∞) (h₀ : map (⇑M.symm : (a : E) → ↥S × ↥T) μ = c₀ • μS.prod μT),
    ∃ (c : ℝ≥0∞),
      0 < c ∧
        c < ∞ ∧
          map (⇑L : (a : E) → F) μ =
            HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
⊢ ∃ (c : ℝ≥0∞),
    0 < c ∧
      c < ∞ ∧
        map (⇑L : (a : E) → F) μ =
          HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν

Tactic:
obtain ⟨c₀, c₀_pos, c₀_fin, h₀⟩ :
      ∃ c₀ : ℝ≥0∞, c₀ ≠ 0 ∧ c₀ ≠ ∞ ∧ μ.map M.symm = c₀ • μS.prod μT := by
    have : IsAddHaarMeasure (μ.map M.symm) :=
      M.toContinuousLinearEquiv.symm.isAddHaarMeasure_map μ
    refine ⟨addHaarScalarFactor (μ.map M.symm) (μS.prod μT), ?_, ENNReal.coe_ne_top,
      isAddLeftInvariant_eq_smul _ _⟩
    simpa only [ne_eq, ENNReal.coe_eq_zero] using
      (addHaarScalarFactor_pos_of_isAddHaarMeasure (μ.map M.symm) (μS.prod μT)).ne'

Premises used: LinearEquiv.symm, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, DFunLike.coe
-- 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
⊢ map (⇑P : (a : ↥S × ↥T) → ↥T) (μS.prod μT) = HSMul.hSMul (α := ℝ≥0∞) ((μS : (a : Set ↥S) → ℝ≥0∞) univ : ℝ≥0∞) μT

Tactic:
have J : (μS.prod μT).map P = (μS univ) • μT := map_snd_prod
-- 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
⊢ IsAddHaarMeasure.{u_3} (G := F) (map (⇑L' : (a : ↥T) → F) μT)

Tactic:
have : IsAddHaarMeasure (μT.map L') :=
      L'.toContinuousLinearEquiv.isAddHaarMeasure_map μT
-- 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_2 : 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
this : IsAddHaarMeasure.{u_3} (G := F) (map (⇑L' : (a : ↥T) → F) μT)
⊢ ∃ (c₁ : ℝ≥0∞), c₁ ≠ 0 ∧ c₁ ≠ ∞ ∧ map (⇑L' : (a : ↥T) → F) μT = c₁ • ν

Tactic:
⟨addHaarScalarFactor (μT.map L') ν, ?_, ENNReal.coe_ne_top,
      isAddLeftInvariant_eq_smul _ _⟩

Premises used: ENNReal.ofNNReal, MeasureTheory.Measure.addHaarScalarFactor, MeasureTheory.Measure.map, And.intro, Exists.intro, DFunLike.coe, MeasureTheory.Measure.isAddLeftInvariant_eq_smul, ENNReal.coe_ne_top
-- 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_2 : 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
this : IsAddHaarMeasure.{u_3} (G := F) (map (⇑L' : (a : ↥T) → F) μT)
refine : (↑(addHaarScalarFactor (map (⇑L' : (a : ↥T) → F) μT) ν) : ℝ≥0∞) ≠ 0
⊢ ∃ (c₁ : ℝ≥0∞), c₁ ≠ 0 ∧ c₁ ≠ ∞ ∧ map (⇑L' : (a : ↥T) → F) μT = c₁ • ν

Tactic:
refine ⟨addHaarScalarFactor (μT.map L') ν, ?_, ENNReal.coe_ne_top,
      isAddLeftInvariant_eq_smul _ _⟩
-- 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_2 : 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
this : IsAddHaarMeasure.{u_3} (G := F) (map (⇑L' : (a : ↥T) → F) μT)
⊢ (↑(addHaarScalarFactor (map (⇑L' : (a : ↥T) → F) μT) ν) : ℝ≥0∞) ≠ 0

Tactic:
simpa only [ne_eq, ENNReal.coe_eq_zero] using
      (addHaarScalarFactor_pos_of_isAddHaarMeasure (μT.map L') ν).ne'

Premises used: ENNReal.coe_eq_zero, ne_eq, LT.lt.ne', MeasureTheory.Measure.map, MeasureTheory.Measure.addHaarScalarFactor_pos_of_isAddHaarMeasure, DFunLike.coe
-- 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
obtain :
  ∀ (c₁ : ℝ≥0∞) (c₁_pos : c₁ ≠ 0) (c₁_fin : c₁ ≠ ∞) (h₁ : map (⇑L' : (a : ↥T) → F) μT = c₁ • ν),
    ∃ (c : ℝ≥0∞),
      0 < c ∧
        c < ∞ ∧
          map (⇑L : (a : E) → F) μ =
            HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
⊢ ∃ (c : ℝ≥0∞),
    0 < c ∧
      c < ∞ ∧
        map (⇑L : (a : E) → F) μ =
          HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν

Tactic:
obtain ⟨c₁, c₁_pos, c₁_fin, h₁⟩ : ∃ c₁ : ℝ≥0∞, c₁ ≠ 0 ∧ c₁ ≠ ∞ ∧ μT.map L' = c₁ • ν := by
    have : IsAddHaarMeasure (μT.map L') :=
      L'.toContinuousLinearEquiv.isAddHaarMeasure_map μT
    refine ⟨addHaarScalarFactor (μT.map L') ν, ?_, ENNReal.coe_ne_top,
      isAddLeftInvariant_eq_smul _ _⟩
    simpa only [ne_eq, ENNReal.coe_eq_zero] using
      (addHaarScalarFactor_pos_of_isAddHaarMeasure (μT.map L') ν).ne'

Premises used: MeasureTheory.Measure.map, DFunLike.coe
-- 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₁ • ν
⊢ 0 < c₀ * c₁

Tactic:
simp [pos_iff_ne_zero, c₀_pos, c₁_pos]

Premises used: pos_iff_ne_zero
-- 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₁ • ν
refine :
  map (⇑L : (a : E) → F) μ =
    HMul.hMul (β := ℝ≥0∞) (c₀ * c₁) (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
⊢ ∃ (c : ℝ≥0∞),
    0 < c ∧
      c < ∞ ∧
        map (⇑L : (a : E) → F) μ =
          HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν

Tactic:
refine ⟨c₀ * c₁, by simp [pos_iff_ne_zero, c₀_pos, c₁_pos],
    ENNReal.mul_lt_top c₀_fin.lt_top c₁_fin.lt_top, ?_⟩
-- 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₁ • ν
simp :
  (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∞) • ν
⊢ map (⇑L : (a : E) → F) μ =
    HMul.hMul (β := ℝ≥0∞) (c₀ * c₁) (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν

Tactic:
simp only [I, h₀, Measure.map_smul, J, smul_smul, h₁]

Premises used: smul_smul, MeasureTheory.Measure.map_smul