awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : FiniteDimensional 𝕜 E
⊢ ∃ (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 this₁ : ProperSpace F
Tactic: have : ProperSpace F := by
    rcases subsingleton_or_nontrivial E with hE | hE
    · have : Subsingleton F := Function.Surjective.subsingleton h
      infer_instance
    · have : ProperSpace 𝕜 := .of_locallyCompact_module 𝕜 E
      have : FiniteDimensional 𝕜 F := Module.Finite.of_surjective L h
      exact FiniteDimensional.proper 𝕜 F
-- 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
⊢ ∃ (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 : ∀ (T : Submodule 𝕜 E) (hT : IsCompl 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∞) • ν
Tactic: obtain ⟨T, hT⟩ : ∃ T : Submodule 𝕜 E, IsCompl S T := Submodule.exists_isCompl S
-- 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
⊢ ∃ (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 M_cont : Continuous (X := E) (Y := ↥S × ↥T) (⇑M.symm : (a : E) → ↥S × ↥T)
Tactic: have M_cont : Continuous M.symm := LinearMap.continuous_of_finiteDimensional _
-- 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
⊢ ∃ (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 P_cont : Continuous (X := ↥S × ↥T) (Y := ↥T) (⇑P : (a : ↥S × ↥T) → ↥T)
Tactic: have P_cont : Continuous P := LinearMap.continuous_of_finiteDimensional _
-- 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)
⊢ ∃ (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 : Function.Bijective.{u_2 + 1, u_3 + 1} (α := ↥T) (β := F) (⇑(L.domRestrict T) : (a : ↥T) → F)
Tactic: have I : Function.Bijective (LinearMap.domRestrict L T) :=
    ⟨LinearMap.injective_domRestrict_iff.2 (IsCompl.inf_eq_bot hT.symm),
    (LinearMap.surjective_domRestrict_iff h).2 hT.symm.sup_eq_top⟩
-- 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
⊢ ∃ (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 L'_cont : Continuous.{u_2, u_3} (X := ↥T) (Y := F) (⇑L' : (a : ↥T) → F)
Tactic: have L'_cont : Continuous L' := LinearMap.continuous_of_finiteDimensional _
-- 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)
⊢ L = (↑L' : ↥T →ₗ[𝕜] F) ∘ₗ P ∘ₗ (↑M.symm : E →ₗ[𝕜] ↥S × ↥T)
have h₁ : ∀ (x : E),
  Eq.{u_3 + 1} (α := F) ((L : (a : E) → F) x : F)
    (((↑L' : ↥T →ₗ[𝕜] F) ∘ₗ P ∘ₗ (↑M.symm : E →ₗ[𝕜] ↥S × ↥T) : (a : E) → F) x : F)
Tactic: ext x
-- 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)
x : E
⊢ Eq.{u_3 + 1} (α := F) ((L : (a : E) → F) x : F)
    (((↑L' : ↥T →ₗ[𝕜] F) ∘ₗ P ∘ₗ (↑M.symm : E →ₗ[𝕜] ↥S × ↥T) : (a : E) → F) x : F)
have h₁ : ∀ (y : ↥S) (z : ↥T) (hyz : (M.symm : (a : E) → ↥S × ↥T) x = (y, z)),
  Eq.{u_3 + 1} (α := F) ((L : (a : E) → F) x : F)
    (((↑L' : ↥T →ₗ[𝕜] F) ∘ₗ P ∘ₗ (↑M.symm : E →ₗ[𝕜] ↥S × ↥T) : (a : E) → F) x : F)
Tactic: obtain ⟨y, z, hyz⟩ : ∃ (y : S) (z : T), M.symm x = (y, z) := ⟨_, _, rfl⟩
-- 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)
x : E
y : ↥S
z : ↥T
hyz : (M.symm : (a : E) → ↥S × ↥T) x = (y, z)
⊢ x = (M : (a : ↥S × ↥T) → E) (y, z)
have rw : x = (M : (a : ↥S × ↥T) → E) ((M.symm : (a : E) → ↥S × ↥T) x : ↥S × ↥T)
Tactic: rw [← hyz]
-- 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)
x : E
y : ↥S
z : ↥T
hyz : (M.symm : (a : E) → ↥S × ↥T) x = (y, z)
⊢ Eq.{u_3 + 1} (α := F) ((L : (a : E) → F) x : F)
    (((↑L' : ↥T →ₗ[𝕜] F) ∘ₗ P ∘ₗ (↑M.symm : E →ₗ[𝕜] ↥S × ↥T) : (a : E) → F) x : F)
have this₁ : x = (M : (a : ↥S × ↥T) → E) (y, z)
Tactic: have : x = M (y, z) := by
      rw [← hyz]; simp only [LinearEquiv.apply_symm_apply]
-- 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)
⊢ ∃ (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 A : L = (↑L' : ↥T →ₗ[𝕜] F) ∘ₗ P ∘ₗ (↑M.symm : E →ₗ[𝕜] ↥S × ↥T)
Tactic: have A : L = (L' : T →ₗ[𝕜] F).comp (P.comp (M.symm : E →ₗ[𝕜] (S × T))) := by
    ext x
    obtain ⟨y, z, hyz⟩ : ∃ (y : S) (z : T), M.symm x = (y, z) := ⟨_, _, rfl⟩
    have : x = M (y, z) := by
      rw [← hyz]; simp only [LinearEquiv.apply_symm_apply]
    simp [L', P, M, this]
-- 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)
⊢ 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 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))
    μ)
Tactic: rw [Measure.map_map, Measure.map_map, A]
-- 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))
      μ)
⊢ 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 hg : Measurable.{u_2, u_3} (α := ↥S × ↥T) (β := F) (Function.comp (β := ↥T) (⇑L' : (a : ↥T) → F) (⇑P : (a : ↥S × ↥T) → ↥T))
Tactic: rw [Measure.map_map, Measure.map_map, A]
-- 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))
⊢ 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 (α := E) (β := ↥S × ↥T) (⇑M.symm : (a : E) → ↥S × ↥T)
Tactic: rw [Measure.map_map, Measure.map_map, A]
-- 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)
⊢ 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 hg₁ : Measurable.{u_2, u_3} (α := ↥T) (β := F) (⇑L' : (a : ↥T) → F)
Tactic: rw [Measure.map_map, Measure.map_map, A]