awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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)) μ
this : CompactSpace.{u_1} (↑K : Type u_1)
⊢ ∃ (ν : 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 ∂ν)

Tactic:
exact Measure.exists_regular_eq_of_compactSpace μ'

Premises used: MeasureTheory.Measure.exists_regular_eq_of_compactSpace
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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)) μ
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 ∂ν)
⊢ ∃ (ν : 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 μ'

Premises used: MeasureTheory.Measure, Set.Elem
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 ∂ν')
⊢ Continuous[instTopologicalSpaceSubtype, inst] (Subtype.val (p := fun (x : X) ↦ x ∈ K))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 ∂ν')
⊢ IsFiniteMeasure (m0 := inst_2) (Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν')

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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∞)
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)
⊢ ∃ (ν : 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:
refine ⟨ν'.map Subtype.val, Measure.InnerRegular.map_of_continuous (by fun_prop),
    by infer_instance, ?_, fun g ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 ∂ν')
⊢ Measurable.{u_1, u_1} (α := { x : X // x ∈ K }) (Subtype.val (p := fun (x : X) ↦ x ∈ K))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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∞) ((ν' : (a : Set { x : X // x ∈ K }) → ℝ≥0∞) (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' Kᶜ) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν' : Measure X) : (a : Set X) → ℝ≥0∞) Kᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.map_apply (by fun_prop) hK.measurableSet.compl]

Premises used: MeasureTheory.Measure.map_apply, MeasurableSet.compl, IsCompact.measurableSet
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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∞) ((ν' : (a : Set { x : X // x ∈ K }) → ℝ≥0∞) (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' Kᶜ) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 →ᵇ ℝ
⊢ Continuous[instTopologicalSpaceSubtype, inst] (Subtype.val (p := fun (x : X) ↦ x ∈ K))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 ∂μ')
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 := ⋯ } :
          (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)

Tactic:
convert! hν' (g.compContinuous ⟨Subtype.val, by fun_prop⟩)

Premises used: ContinuousMap.mk, BoundedContinuousFunction.compContinuous, Subtype.val
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 : (a : X) → ℝ) (↑x : 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 ∂μ')

Tactic:
simp only [BoundedContinuousFunction.compContinuous_apply, ContinuousMap.coe_mk]

Premises used: ContinuousMap.coe_mk, BoundedContinuousFunction.compContinuous_apply
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 →ᵇ ℝ
⊢ AEMeasurable (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ'

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 →ᵇ ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := inst_2) (⇑g : (a : X) → ℝ)
    (Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ')

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 ∂μ)
    (@integral _ _ _ _ inst_2 (Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) μ') fun (y : X) ↦
      (g : (a : X) → ℝ) y)
⊢ Eq (α := ℝ) (∫ (x : X), (g : (a : X) → ℝ) x ∂μ) (∫ (x : (↑K : Type u_1)), (g : (a : X) → ℝ) (↑x : X) ∂μ')

Tactic:
rw [← integral_map (φ := Subtype.val) (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 (y : X) ↦
      (g : (a : X) → ℝ) y)

Tactic:
simp only [map_comap_subtype_coe hK.measurableSet, μ', Measure.restrict_eq_self_of_ae_mem h]

Premises used: MeasureTheory.Measure.restrict_eq_self_of_ae_mem, map_comap_subtype_coe, IsCompact.measurableSet
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 →ᵇ ℝ
⊢ AEMeasurable (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν'

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 →ᵇ ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := inst_2) (⇑g : (a : X) → ℝ)
    (Measure.map (Subtype.val (p := fun (x : X) ↦ x ∈ K)) ν')

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 : 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 := ⋯ } :
          (a : (↑K : Type u_1)) → ℝ)
        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 ∂ν')

Tactic:
rw [integral_map (φ := Subtype.val) (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
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 : 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 := ⋯ } :
          (a : (↑K : Type u_1)) → ℝ)
        x ∂ν')

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
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‖
⊢ ‖f‖ = ∑ x ∈ (toSimpleFunc f).range, μ.real (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) * ‖x‖

Tactic:
rw [norm_toSimpleFunc, eLpNorm_one_eq_lintegral_enorm]

Premises used: MeasureTheory.eLpNorm_one_eq_lintegral_enorm, MeasureTheory.Lp.simpleFunc.norm_toSimpleFunc
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(simpleFunc G 1 μ)
⊢ ∀ (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)
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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‖)
rw₁ :
  ∀ a ∈ (toSimpleFunc f).range,
    HMul.hMul (β := ℝ≥0∞) ‖a‖ₑ
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {a}) : ℝ≥0∞) ≠
      ∞
⊢ (∫⁻ (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‖

Tactic:
rw [SimpleFunc.lintegral_eq_lintegral, SimpleFunc.map_lintegral, ENNReal.toReal_sum]

Premises used: MeasureTheory.SimpleFunc.map_lintegral, ENNReal.toReal_sum, MeasureTheory.SimpleFunc.lintegral_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
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‖
⊢ 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:
congr
-- Module: Mathlib.MeasureTheory.Integral.SetToL1
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)
e_f :
  ∀ (x : G),
    (HMul.hMul (β := ℝ≥0∞) ‖x‖ₑ
          ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x}) : ℝ≥0∞)).toReal =
      ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := G) (⇑(toSimpleFunc f) : (a : α) → G) {x})) * ‖x‖
⊢ 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:
ext1 x