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_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₁ • ν
⊢ (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∞) • ν
have 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∞) • ν
Tactic: rw [mul_assoc, mul_comm _ c₁, ← mul_assoc]
-- 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₁ • ν
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∞) • ν
⊢ (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∞) • ν
have 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∞) • ν
Tactic: rw [mul_assoc, mul_comm _ c₁, ← mul_assoc]
-- 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₁ • ν
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∞) • ν
⊢ (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∞) • ν
have 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∞) • ν
Tactic: rw [mul_assoc, mul_comm _ c₁, ← mul_assoc]
-- 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)
⊢ ∃ (c : ℝ≥0∞), 0 < c ∧ map (⇑L : (a : E) → F) μ = c • ν
have 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 • ν
Tactic: rcases L.exists_map_addHaar_eq_smul_addHaar' μ ν h with ⟨c, c_pos, -, hc⟩
-- 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)
s : Set F
hs : MeasurableSet s
⊢ (∀ᵐ (x : E) ∂μ, Membership.mem (α := F) s ((L : (a : E) → F) x : F)) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have this : FiniteDimensional 𝕜 E
Tactic: have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
-- 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)
s : Set F
hs : MeasurableSet s
this : FiniteDimensional 𝕜 E
⊢ (∀ᵐ (x : E) ∂μ, Membership.mem (α := F) s ((L : (a : E) → F) x : F)) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have this₁ : AEMeasurable.{u_2, u_3} (β := F) (⇑L : (a : E) → F) μ
Tactic: have : AEMeasurable L μ := L.continuous_of_finiteDimensional.aemeasurable
-- 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)
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this : AEMeasurable.{u_2, u_3} (β := F) (⇑L : (a : E) → F) μ
⊢ (∀ᵐ (x : E) ∂μ, Membership.mem (α := F) s ((L : (a : E) → F) x : F)) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have apply : (∀ᵐ (y : F) ∂map (⇑L : (a : E) → F) μ, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
Tactic: apply (ae_map_iff this hs).symm.trans
-- 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)
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this : AEMeasurable.{u_2, u_3} (β := F) (⇑L : (a : E) → F) μ
⊢ (∀ᵐ (y : F) ∂map (⇑L : (a : E) → F) μ, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have 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
Tactic: rcases L.exists_map_addHaar_eq_smul_addHaar μ ν h with ⟨c, c_pos, hc⟩
-- 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)
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) ∂map (⇑L : (a : E) → F) μ, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have rw : (∀ᵐ (y : F) ∂c • ν, s y) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
Tactic: rw [hc]
-- 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
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have this : FiniteDimensional 𝕜 E
Tactic: have : FiniteDimensional 𝕜 E := .of_locallyCompactSpace 𝕜
-- 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
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this : FiniteDimensional 𝕜 E
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have this₁ : FiniteDimensional 𝕜 F
Tactic: have : FiniteDimensional 𝕜 F := .of_locallyCompactSpace 𝕜
-- 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
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this : FiniteDimensional 𝕜 F
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have this₁ : ProperSpace E
Tactic: have : ProperSpace E := .of_locallyCompactSpace 𝕜
-- 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
inst_13 : LocallyCompactSpace F
s : Set F
hs : MeasurableSet s
this_1 : FiniteDimensional 𝕜 E
this_2 : FiniteDimensional 𝕜 F
this : ProperSpace E
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have this₁ : ProperSpace F
Tactic: have : ProperSpace F := .of_locallyCompactSpace 𝕜
-- 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
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
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have M_cont : Continuous (X := F × E) (Y := F) (⇑M : (a : F × E) → F)
Tactic: have M_cont : Continuous M := M.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
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)
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have hM : 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]
-- 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
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)
⊢ (∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, HAdd.hAdd (β := F) y ((L : (a : E) → F) x : F) ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have 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
Tactic: have A : ∀ x, M x ∈ s ↔ x ∈ M ⁻¹' s := fun x ↦ Iff.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
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) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
have 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
Tactic: simp_rw [← ae_comp_linearMap_mem_iff M (ν.prod μ) ν hM hs, 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
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 × E) ∂ν.prod μ, Membership.mem (γ := Set (F × E)) ((⇑M : (a : F × E) → F) ⁻¹' s) x
have 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)
Tactic: rw [Measure.ae_prod_mem_iff_ae_ae_mem]
-- 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
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)
⊢ (∀ᵐ (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
have rw₁ : MeasurableSet (α := F × E) ((⇑M : (a : F × E) → F) ⁻¹' s)
Tactic: rw [Measure.ae_prod_mem_iff_ae_ae_mem]