awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : (↑M : Type u_2)
s : Set Ω'
hs : MeasurableSet s
a :
  Eq (α := ℝ≥0∞) (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)
a₁ : ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)
a₂ : MeasurableSet (f ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap f (↑(↑μ : FiniteMeasure Ω') : Measure Ω') : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.comap_apply _ hf.injective, image_preimage_eq_inter_range]

Premises used: MeasureTheory.Measure.comap_apply, Set.image_preimage_eq_inter_range, Topology.IsClosedEmbedding.toIsEmbedding, Topology.IsEmbedding.injective
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : (↑M : Type u_2)
s : Set Ω'
hs : MeasurableSet s
a : ∀ᵐ (x : Ω') ∂(↑(↑μ : FiniteMeasure Ω') : Measure Ω'), x ∈ range f
⊢ Eq (α := ℝ≥0∞) (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) (s ∩ range f) : ℝ≥0∞)
    (((↑(↑μ : FiniteMeasure Ω') : Measure Ω') : (a : Set Ω') → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← Measure.restrict_apply hs, Measure.restrict_eq_self_of_ae_mem]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.restrict_eq_self_of_ae_mem
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : (↑M : Type u_2)
s : Set Ω'
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0) (((↑μ : FiniteMeasure Ω') : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)

Tactic:
μ.2

Premises used: Set.Mem, setOf, Subtype.property
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : (↑M : Type u_2)
s : Set Ω'
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0) (((↑μ : FiniteMeasure Ω') : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)

Tactic:
exact μ.2

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : (↑M : Type u_2)
s : Set Ω'
hs : MeasurableSet s
⊢ ∀ᵐ (x : Ω') ∂(↑(↑μ : FiniteMeasure Ω') : Measure Ω'), x ∈ range f

Tactic:
exact (null_iff_toMeasure_null (↑μ) (range f)ᶜ).mp (by exact μ.2)

Premises used: Compl.compl, Iff.mp, Set.range, MeasureTheory.FiniteMeasure.null_iff_toMeasure_null
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : (↑M : Type u_2)
s : Set Ω'
hs : MeasurableSet s
⊢ ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht

Premises used: MeasurableEmbedding.measurableSet_image', Topology.IsClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : (↑M : Type u_2)
s : Set Ω'
hs : MeasurableSet s
⊢ ∀ (s : Set Ω), MeasurableSet s → MeasurableSet (f '' s)

Tactic:
exact fun t ht ↦ hf.measurableEmbedding.measurableSet_image' ht

Premises used: MeasurableEmbedding.measurableSet_image', Topology.IsClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : (↑M : Type u_2)
s : Set Ω'
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
hf.continuous.measurable hs

Premises used: Topology.IsClosedEmbedding.continuous, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
μ : (↑M : Type u_2)
s : Set Ω'
hs : MeasurableSet s
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
exact hf.continuous.measurable hs

Premises used: Topology.IsClosedEmbedding.continuous, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceSubtype] fun (μ : FiniteMeasure Ω) ↦
    Subtype.mk (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M) (μ.map f) ⋯

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
rw : ContinuousOn.{u_2, u_3} (Y := FiniteMeasure Ω) (fun (μ : FiniteMeasure Ω') ↦ comap f μ) M
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpace]
    (M.restrict (π := fun (μ : FiniteMeasure Ω') ↦ FiniteMeasure Ω) fun (μ : FiniteMeasure Ω') ↦ comap f μ)

Tactic:
rw [← continuousOn_iff_continuous_restrict]

Premises used: continuousOn_iff_continuous_restrict
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
⊢ ContinuousOn.{u_2, u_3} (Y := FiniteMeasure Ω) (fun (μ : FiniteMeasure Ω') ↦ comap f μ) M

Tactic:
hf.continuousOn_comap_finiteMeasure

Premises used: Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
⊢ ContinuousOn.{u_2, u_3} (Y := FiniteMeasure Ω) (fun (μ : FiniteMeasure Ω') ↦ comap f μ) M

Tactic:
exact hf.continuousOn_comap_finiteMeasure

Premises used: Topology.IsClosedEmbedding.continuousOn_comap_finiteMeasure
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
B : Homeomorph.{u_3, u_2} (FiniteMeasure Ω) (↑M : Type u_2) :=
  { toFun := fun (μ : FiniteMeasure Ω) ↦ Subtype.mk (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M) (μ.map f) ⋯,
    invFun := M.restrict (π := fun (μ : FiniteMeasure Ω') ↦ FiniteMeasure Ω) fun (μ : FiniteMeasure Ω') ↦ comap f μ,
    left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsEmbedding.{u_3, u_2} (Y := FiniteMeasure Ω') fun (μ : FiniteMeasure Ω) ↦ μ.map f

Tactic:
A.comp B.isEmbedding

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.comp, MeasureTheory.FiniteMeasure.map
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasure
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
B : Homeomorph.{u_3, u_2} (FiniteMeasure Ω) (↑M : Type u_2) :=
  { toFun := fun (μ : FiniteMeasure Ω) ↦ Subtype.mk (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M) (μ.map f) ⋯,
    invFun := M.restrict (π := fun (μ : FiniteMeasure Ω') ↦ FiniteMeasure Ω) fun (μ : FiniteMeasure Ω') ↦ comap f μ,
    left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsEmbedding.{u_3, u_2} (Y := FiniteMeasure Ω') fun (μ : FiniteMeasure Ω) ↦ μ.map f

Tactic:
exact A.comp B.isEmbedding

Premises used: Homeomorph.isEmbedding, Topology.IsEmbedding.comp
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
rw :
  Subalgebra.SeparatesPoints.{u_1, 0, 0} (α := E)
    (Subalgebra.comap (B := C(E, 𝕜)) (AlgHom.compLeftContinuous ℝ ofRealAm ⋯)
      (Subalgebra.restrictScalars ℝ (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))))
⊢ (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints

Tactic:
rw [RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict]

Premises used: RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
⊢ Subalgebra.SeparatesPoints.{u_1, 0, 0} (α := E)
    (Subalgebra.comap (B := C(E, 𝕜)) (AlgHom.compLeftContinuous ℝ ofRealAm ⋯)
      (Subalgebra.restrictScalars ℝ (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))))

Tactic:
Subalgebra.SeparatesPoints.rclike_to_real hA

Premises used: Subalgebra.SeparatesPoints.rclike_to_real
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
⊢ Subalgebra.SeparatesPoints.{u_1, 0, 0} (α := E)
    (Subalgebra.comap (B := C(E, 𝕜)) (AlgHom.compLeftContinuous ℝ ofRealAm ⋯)
      (Subalgebra.restrictScalars ℝ (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))))

Tactic:
exact Subalgebra.SeparatesPoints.rclike_to_real hA

Premises used: Subalgebra.SeparatesPoints.rclike_to_real
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
⊢ (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints

Tactic:
have hA_toReal : (A_toReal.map (toContinuousMapₐ ℝ)).SeparatesPoints := by
    rw [RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict]
    exact Subalgebra.SeparatesPoints.rclike_to_real hA
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
g : E →ᵇ ℝ
hgA_toReal : g ∈ A_toReal
rw : Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (↑((g : (a : E) → ℝ) x) : 𝕜) ∂P) (∫ (x : E), (↑((g : (a : E) → ℝ) x) : 𝕜) ∂P')
⊢ Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')

Tactic:
rw [← @ofReal_inj 𝕜, ← integral_ofReal, ← integral_ofReal]

Premises used: RCLike.ofReal_inj, integral_ofReal
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
g : E →ᵇ ℝ
hgA_toReal : g ∈ A_toReal
⊢ Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (↑((g : (a : E) → ℝ) x) : 𝕜) ∂P) (∫ (x : E), (↑((g : (a : E) → ℝ) x) : 𝕜) ∂P')

Tactic:
heq _ hgA_toReal
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
g : E →ᵇ ℝ
hgA_toReal : g ∈ A_toReal
⊢ Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (↑((g : (a : E) → ℝ) x) : 𝕜) ∂P) (∫ (x : E), (↑((g : (a : E) → ℝ) x) : 𝕜) ∂P')

Tactic:
exact heq _ hgA_toReal
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
⊢ ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')

Tactic:
have heq' : ∀ g ∈ A_toReal, ∫ x, (g : E → ℝ) x ∂P = ∫ x, (g : E → ℝ) x ∂P' := by
    intro g hgA_toReal
    rw [← @ofReal_inj 𝕜, ← integral_ofReal, ← integral_ofReal]
    exact heq _ hgA_toReal
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
h : ∀ (f : E →ᵇ ℝ), Eq (α := ℝ) (∫ (x : E), (f : (a : E) → ℝ) x ∂P) (∫ (x : E), (f : (a : E) → ℝ) x ∂P')
⊢ P = P'

Tactic:
apply ext_of_forall_integral_eq_of_IsFiniteMeasure

Premises used: MeasureTheory.ext_of_forall_integral_eq_of_IsFiniteMeasure