awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (goal)
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 : 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
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)
rw :
  Eq.{u_3 + 1} (α := Measure F) (map (⇑((↑L' : ↥T →ₗ[𝕜] F) ∘ₗ P ∘ₗ (↑M.symm : E →ₗ[𝕜] ↥S × ↥T)) : (a : E) → F) μ)
    (map
      (Function.comp (β := ↥S × ↥T) (Function.comp (β := ↥T) (⇑L' : (a : ↥T) → F) (⇑P : (a : ↥S × ↥T) → ↥T))
        (⇑M.symm : (a : E) → ↥S × ↥T))
      μ)
hg :
  Measurable.{u_2, u_3} (α := ↥S × ↥T) (β := F) (Function.comp (β := ↥T) (⇑L' : (a : ↥T) → F) (⇑P : (a : ↥S × ↥T) → ↥T))
hf : Measurable (α := E) (β := ↥S × ↥T) (⇑M.symm : (a : E) → ↥S × ↥T)
hg₁ : Measurable.{u_2, u_3} (α := ↥T) (β := F) (⇑L' : (a : ↥T) → F)
⊢ 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) μ)))
have hf₁ : Measurable (α := ↥S × ↥T) (β := ↥T) (⇑P : (a : ↥S × ↥T) → ↥T)
Tactic: rw [Measure.map_map, Measure.map_map, A]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (hypothesis)
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 : 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
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)
⊢ ∃ (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∞) • ν
have 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) μ)))
Tactic: have I : μ.map L = ((μ.map M.symm).map P).map L' := by
    rw [Measure.map_map, Measure.map_map, A]
    · rfl
    · exact L'_cont.measurable.comp P_cont.measurable
    · exact M_cont.measurable
    · exact L'_cont.measurable
    · exact P_cont.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (hypothesis)
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₀ ≠ 0 ∧ c₀ ≠ ∞ ∧ map (⇑M.symm : (a : E) → ↥S × ↥T) μ = c₀ • μS.prod μT
have this₁ : IsAddHaarMeasure (G := ↥S × ↥T) (map (⇑M.symm : (a : E) → ↥S × ↥T) μ)
Tactic: have : IsAddHaarMeasure (μ.map M.symm) :=
      M.toContinuousLinearEquiv.symm.isAddHaarMeasure_map μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (goal)
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) μ)
⊢ ∃ (c₀ : ℝ≥0∞), c₀ ≠ 0 ∧ c₀ ≠ ∞ ∧ map (⇑M.symm : (a : E) → ↥S × ↥T) μ = c₀ • μS.prod μT
have refine : (↑(addHaarScalarFactor (map (⇑M.symm : (a : E) → ↥S × ↥T) μ) (μS.prod μT)) : ℝ≥0∞) ≠ 0
Tactic: refine ⟨addHaarScalarFactor (μ.map M.symm) (μS.prod μT), ?_, ENNReal.coe_ne_top,
      isAddLeftInvariant_eq_smul _ _⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (goal)
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∞),
    0 < c ∧
      c < ∞ ∧
        map (⇑L : (a : E) → F) μ =
          HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
have 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∞) • ν
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'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (hypothesis)
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
⊢ ∃ (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∞) • ν
have J : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (hypothesis)
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₁ ≠ 0 ∧ c₁ ≠ ∞ ∧ map (⇑L' : (a : ↥T) → F) μT = c₁ • ν
have this₁ : IsAddHaarMeasure.{u_3} (G := F) (map (⇑L' : (a : ↥T) → F) μT)
Tactic: have : IsAddHaarMeasure (μT.map L') :=
      L'.toContinuousLinearEquiv.isAddHaarMeasure_map μT
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (goal)
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₁ • ν
have refine : (↑(addHaarScalarFactor (map (⇑L' : (a : ↥T) → F) μT) ν) : ℝ≥0∞) ≠ 0
Tactic: refine ⟨addHaarScalarFactor (μT.map L') ν, ?_, ENNReal.coe_ne_top,
      isAddLeftInvariant_eq_smul _ _⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (goal)
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∞),
    0 < c ∧
      c < ∞ ∧
        map (⇑L : (a : E) → F) μ =
          HMul.hMul (β := ℝ≥0∞) c (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
have 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∞) • ν
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'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (goal)
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₁ • ν
⊢ ∃ (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∞) • ν
have refine : map (⇑L : (a : E) → F) μ =
  HMul.hMul (β := ℝ≥0∞) (c₀ * 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, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Disintegration (goal)
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₁ • ν
⊢ map (⇑L : (a : E) → F) μ =
    HMul.hMul (β := ℝ≥0∞) (c₀ * c₁) (((addHaar : Measure ↥L.ker) : (a : Set ↥L.ker) → ℝ≥0∞) univ : ℝ≥0∞) • ν
have 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∞) • ν
Tactic: simp only [I, h₀, Measure.map_smul, J, smul_smul, h₁]