awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : ν.OuterRegular
inst_6 : IsFiniteMeasureOnCompacts ν
inst_7 : IsFiniteMeasureOnCompacts μ
hμν : ∀ (f : X →C_c ℝ), LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
ε : NNReal
hε : 0 < ε
hν : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hνK : Ne (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
hμK : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
V : Set X
pV1 : V ⊇ K
pV2 : IsOpen[inst] V
pV3 : (ν : (a : Set X) → ℝ≥0∞) V ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) (↑ε : ℝ≥0∞)
VltTop : LT.lt (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞)
f : X →C_c ℝ
pf1 : EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 K
pf2 : tsupport (α := ℝ) (⇑f : (a : X) → ℝ) ⊆ V
pf3 : ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)
hfV : ∀ (x : X), LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (V.indicator 1 x : ℝ)
hfK : ∀ (x : X), LE.le (α := ℝ) (K.indicator 1 x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K₁ : LE.le (α := ℝ) (∫ (x : X), K.indicator 1 x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
K₂ : LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν) (∫ (x : X), V.indicator 1 x ∂ν)
⊢ μ.real K ≤ ν.real K + (↑ε : ℝ)
have K₃ : ∫ (x : X), V.indicator 1 x ∂ν ≤ ENNReal.toReal ((ν : (a : Set X) → ℝ≥0∞) K) + (↑ε : ℝ)
Tactic: calc
    μ.real K = ∫ x, K.indicator 1 x ∂μ := integral_indicator_one hK.measurableSet |>.symm
    _ ≤ ∫ x, f x ∂μ := by
      refine integral_mono ?_ f.integrable hfK
      exact (continuousOn_const.integrableOn_compact hK).integrable_indicator hK.measurableSet
    _ ≤ ∫ x, f x ∂ν := hμν f
    _ ≤ ∫ x, V.indicator 1 x ∂ν := by
      refine integral_mono f.integrable ?_ hfV
      exact IntegrableOn.integrable_indicator integrableOn_const pV2.measurableSet
    _ ≤ (ν K).toReal + ↑ε := by
      rwa [integral_indicator_one pV2.measurableSet, measureReal_def,
        ← ENNReal.coe_toReal, ← ENNReal.toReal_add, ENNReal.toReal_le_toReal]
      all_goals finiteness
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
⊢ μ = ν
have hμν₁ : ∀ (U : Set X), IsOpen[inst] U → Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞)
Tactic: apply Measure.OuterRegular.ext_isOpen
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
⊢ ∀ (U : Set X), IsOpen[inst] U → Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞)
have hμν₁ : ∀ (U : Set X), IsCompact U → Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞)
Tactic: apply Measure.InnerRegularWRT.eq_of_innerRegularWRT_of_forall_eq Measure.Regular.innerRegular
    Measure.Regular.innerRegular
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)
have hμν₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ ν : Measure X
inst_4 : LocallyCompactSpace X
inst_5 : μ.Regular
inst_6 : ν.Regular
hμν : ∀ (f : X →C_c ℝ), Eq (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (∫ (x : X), (f : (a : X) → ℝ) x ∂ν)
K : Set X
hK : IsCompact K
hμν₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)
have hμν₂ : LE.le (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
⊢ integralPositiveLinearMap (rieszMeasure Λ) = Λ
have h : ∀ (x : X →C_c ℝ),
  Eq (α := ℝ) ((integralPositiveLinearMap (rieszMeasure Λ) : (a : X →C_c ℝ) → ℝ) x : ℝ) ((Λ : (a : X →C_c ℝ) → ℝ) x : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ_1 : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : CompactSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
⊢ IsFiniteMeasure (m0 := inst_2) (rieszMeasure Λ)
have measure_univ_lt_top : LT.lt (α := ℝ≥0∞) (((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
Λ_1 : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : CompactSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
o : X →C_c ℝ := { toContinuousMap := 1, hasCompactSupport' := ⋯ }
⊢ LT.lt (α := ℝ≥0∞) (((rieszMeasure Λ : Measure X) : (a : Set X) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have calc : ENNReal.ofReal ((Λ : (a : X →C_c ℝ) → ℝ) o) < ∞
Tactic: calc rieszMeasure Λ univ
  _ ≤ ENNReal.ofReal (Λ o) :=
    rieszMeasure_le_of_eq_one _ (fun x ↦ zero_le_one) isCompact_univ (fun x hx ↦ rfl)
  _ < ⊤ := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
inst_4 : CompactSpace X
μ : Measure X
inst_5 : IsFiniteMeasure μ
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ :=
  { toFun := fun (g : X →C_c ℝ) ↦ ∫ (x : X), (g : (a : X) → ℝ) x ∂μ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
⊢ ∃ (ν : Measure X),
    ν.Regular ∧
      IsFiniteMeasure ν ∧
        ∀ (g : X →ᵇ ℝ), Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ) (∫ (x : X), (g : (a : X) → ℝ) x ∂ν)
have refine : ∀ (g : X →ᵇ ℝ),
  Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ)
    (@integral _ _ _ _ inst_2 (rieszMeasure Λ) fun (x : X) ↦ (g : (a : X) → ℝ) x)
Tactic: refine ⟨RealRMK.rieszMeasure Λ, by infer_instance, by infer_instance, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
⊢ ∃ (ν : Measure (↑K : Type u_1)),
    ν.Regular ∧
      IsFiniteMeasure ν ∧
        ∀ (g : (↑K : Type u_1) →ᵇ ℝ),
          Eq (α := ℝ) (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂μ')
            (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂ν)
have this : CompactSpace.{u_1} (↑K : Type u_1)
Tactic: have : CompactSpace K := isCompact_iff_compactSpace.mp hK
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
⊢ ∃ (ν : Measure X),
    ν.InnerRegular ∧
      IsFiniteMeasure ν ∧
        Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          ∀ (g : X →ᵇ ℝ), Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ) (∫ (x : X), (g : (a : X) → ℝ) x ∂ν)
have obtain : ∀ (ν' : Measure (↑K : Type u_1)) (ν'_reg : ν'.Regular) (ν'_fin : IsFiniteMeasure ν')
  (hν' :
    ∀ (g : (↑K : Type u_1) →ᵇ ℝ),
      Eq (α := ℝ) (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂μ')
        (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂ν')),
  ∃ (ν : Measure X),
    ν.InnerRegular ∧
      IsFiniteMeasure ν ∧
        Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          ∀ (g : X →ᵇ ℝ), Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ) (∫ (x : X), (g : (a : X) → ℝ) x ∂ν)
Tactic: obtain ⟨ν', ν'_reg, ν'_fin, hν'⟩ : ∃ (ν : Measure K), ν.Regular ∧ IsFiniteMeasure ν ∧
      ∀ g : K →ᵇ ℝ, ∫ x, g x ∂μ' = ∫ x, g x ∂ν := by
    have : CompactSpace K := isCompact_iff_compactSpace.mp hK
    exact Measure.exists_regular_eq_of_compactSpace μ'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
ν' : Measure (↑K : Type u_1)
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' :
  ∀ (g : (↑K : Type u_1) →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂μ')
      (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂ν')
⊢ ∃ (ν : Measure X),
    ν.InnerRegular ∧
      IsFiniteMeasure ν ∧
        Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          ∀ (g : X →ᵇ ℝ), Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ) (∫ (x : X), (g : (a : X) → ℝ) x ∂ν)
have refine_1 : Eq (α := ℝ≥0∞) (((Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν' : Measure X) : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: refine ⟨ν'.map Subtype.val, Measure.InnerRegular.map_of_continuous (by fun_prop),
    by infer_instance, ?_, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
ν' : Measure (↑K : Type u_1)
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' :
  ∀ (g : (↑K : Type u_1) →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂μ')
      (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂ν')
refine_1 :
  Eq (α := ℝ≥0∞)
    (((Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν' : Measure X) : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (ν : Measure X),
    ν.InnerRegular ∧
      IsFiniteMeasure ν ∧
        Eq (α := ℝ≥0∞) ((ν : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
          ∀ (g : X →ᵇ ℝ), Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ) (∫ (x : X), (g : (a : X) → ℝ) x ∂ν)
have refine_2 : ∀ (g : X →ᵇ ℝ),
  Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ)
    (@integral _ _ _ _ inst_2 (Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν') fun (x : X) ↦
      (g : (a : X) → ℝ) x)
Tactic: refine ⟨ν'.map Subtype.val, Measure.InnerRegular.map_of_continuous (by fun_prop),
    by infer_instance, ?_, fun g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
ν' : Measure (↑K : Type u_1)
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' :
  ∀ (g : (↑K : Type u_1) →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂μ')
      (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂ν')
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν' : Measure X) : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1 : Eq (α := ℝ≥0∞) ((ν' : (a : Set { x : X // x ∈ K }) → ℝ≥0∞) (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' Kᶜ) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rw [Measure.map_apply (by fun_prop) hK.measurableSet.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
ν' : Measure (↑K : Type u_1)
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' :
  ∀ (g : (↑K : Type u_1) →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂μ')
      (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂ν')
g : X →ᵇ ℝ
⊢ Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ)
    (@integral _ _ _ _ inst_2 (Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν') fun (x : X) ↦
      (g : (a : X) → ℝ) x)
have h₁ : Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ)
  (∫ (x : (↑K : Type u_1)),
    (g.compContinuous { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := sorry } :
        (a : (↑K : Type u_1)) → ℝ)
      x ∂μ')
Tactic: convert! hν' (g.compContinuous ⟨Subtype.val, by fun_prop⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
ν' : Measure (↑K : Type u_1)
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' :
  ∀ (g : (↑K : Type u_1) →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂μ')
      (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂ν')
g : X →ᵇ ℝ
h₁ :
  Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ)
    (∫ (x : (↑K : Type u_1)),
      (g.compContinuous { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ } :
          (a : (↑K : Type u_1)) → ℝ)
        x ∂μ')
⊢ Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ)
    (@integral _ _ _ _ inst_2 (Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν') fun (x : X) ↦
      (g : (a : X) → ℝ) x)
have h₂ : Eq (α := ℝ)
  (@integral _ _ _ _ inst_2 (Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν') fun (x : X) ↦ (g : (a : X) → ℝ) x)
  (∫ (x : (↑K : Type u_1)),
    (g.compContinuous { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := sorry } :
        (a : (↑K : Type u_1)) → ℝ)
      x ∂ν')
Tactic: convert! hν' (g.compContinuous ⟨Subtype.val, by fun_prop⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
ν' : Measure (↑K : Type u_1)
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' :
  ∀ (g : (↑K : Type u_1) →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂μ')
      (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂ν')
g : X →ᵇ ℝ
⊢ Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ)
    (∫ (x : (↑K : Type u_1)),
      (g.compContinuous { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ } :
          (a : (↑K : Type u_1)) → ℝ)
        x ∂μ')
have h₁ : Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ) (∫ (x : (↑K : Type u_1)), (g : (a : X) → ℝ) (↑x : X) ∂μ')
Tactic: simp only [BoundedContinuousFunction.compContinuous_apply, ContinuousMap.coe_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
ν' : Measure (↑K : Type u_1)
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' :
  ∀ (g : (↑K : Type u_1) →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂μ')
      (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂ν')
g : X →ᵇ ℝ
⊢ Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ) (∫ (x : (↑K : Type u_1)), (g : (a : X) → ℝ) (↑x : X) ∂μ')
have h₁ : Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ)
  (@integral _ _ _ _ inst_2 (Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ') fun (y : X) ↦ (g : (a : X) → ℝ) y)
Tactic: rw [← integral_map (φ := Subtype.val) (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
μ : Measure X
inst_4 : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
μ' : Measure (↑K : Type u_1) := Measure.comap (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ
ν' : Measure (↑K : Type u_1)
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' :
  ∀ (g : (↑K : Type u_1) →ᵇ ℝ),
    Eq (α := ℝ) (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂μ')
      (∫ (x : (↑K : Type u_1)), (g : (a : (↑K : Type u_1)) → ℝ) x ∂ν')
g : X →ᵇ ℝ
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ inst_2 (Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν') fun (x : X) ↦
      (g : (a : X) → ℝ) x)
    (∫ (x : (↑K : Type u_1)),
      (g.compContinuous { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := ⋯ } :
          (a : (↑K : Type u_1)) → ℝ)
        x ∂ν')
have h₁ : Eq (α := ℝ) (∫ (x : { x : X // x ∈ K }), (g : (a : X) → ℝ) (↑x : X) ∂ν')
  (∫ (x : (↑K : Type u_1)),
    (g.compContinuous { toFun := Subtype.val (p := fun (x : X) ↦ x ∈ K), continuous_toFun := sorry } :
        (a : (↑K : Type u_1)) → ℝ)
      x ∂ν')
Tactic: rw [integral_map (φ := Subtype.val) (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
⊢ ‖f‖ = ∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) * ‖x‖
have rw : (∫⁻ (x : α), enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) x : G) ∂μ).toReal =
  ∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) * ‖x‖
Tactic: rw [norm_toSimpleFunc, eLpNorm_one_eq_lintegral_enorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
⊢ (∫⁻ (x : α), enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) x : G) ∂μ).toReal =
    ∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) * ‖x‖
have h_eq : ∀ (a : α),
  ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
    enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
Tactic: have h_eq := SimpleFunc.map_apply (‖·‖ₑ) (toSimpleFunc f)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
⊢ (∫⁻ (x : α),
        ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) x ∂μ).toReal =
    ∑ x ∈ (toSimpleFunc f).range,
      ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
have rw : Eq (α := ℝ)
  (∑ a ∈ (toSimpleFunc f).range,
    (HMul.hMul (β := ℝ≥0∞) ‖a‖ₑ
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {a}) : ℝ≥0∞)).toReal)
  (∑ x ∈ (toSimpleFunc f).range,
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖)
Tactic: rw [SimpleFunc.lintegral_eq_lintegral, SimpleFunc.map_lintegral, ENNReal.toReal_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
rw :
  Eq (α := ℝ)
    (∑ a ∈ (toSimpleFunc f).range,
      (HMul.hMul (β := ℝ≥0∞) ‖a‖ₑ
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {a}) : ℝ≥0∞)).toReal)
    (∑ x ∈ (toSimpleFunc f).range,
      ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖)
⊢ (∫⁻ (x : α),
        ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) x ∂μ).toReal =
    ∑ x ∈ (toSimpleFunc f).range,
      ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
have rw₁ : ∀ a ∈ (toSimpleFunc f).range,
  HMul.hMul (β := ℝ≥0∞) ‖a‖ₑ
      ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {a}) : ℝ≥0∞) ≠
    ∞
Tactic: rw [SimpleFunc.lintegral_eq_lintegral, SimpleFunc.map_lintegral, ENNReal.toReal_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
h_eq :
  ∀ (a : α),
    ((SimpleFunc.map (fun (x : G) ↦ ‖x‖ₑ) (toSimpleFunc f) : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) a =
      enorm.{u_5} (E := G) ((toSimpleFunc f : (a : α) → G) a : G)
⊢ Eq (α := ℝ)
    (∑ a ∈ (toSimpleFunc f).range,
      (HMul.hMul (β := ℝ≥0∞) ‖a‖ₑ
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {a}) : ℝ≥0∞)).toReal)
    (∑ x ∈ (toSimpleFunc f).range,
      ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖)
have e_f : Eq.{u_5 + 1} (α := G → ℝ)
  (fun (a : G) ↦
    (HMul.hMul (β := ℝ≥0∞) ‖a‖ₑ
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {a}) : ℝ≥0∞)).toReal)
  fun (x : G) ↦
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
Tactic: congr