awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
a : α
this : SecondCountableTopology.{u_1} (↑(closure[inst] s) : Type u_1)
⊢ StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))

Tactic:
continuous_subtype_val.stronglyMeasurable

Premises used: continuous_subtype_val, Continuous.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
a : α
this : SecondCountableTopology.{u_1} (↑(closure[inst] s) : Type u_1)
⊢ StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))

Tactic:
exact continuous_subtype_val.stronglyMeasurable

Premises used: continuous_subtype_val, Continuous.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
a : α
⊢ StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))

Tactic:
have h : StronglyMeasurable ((↑) : closure s → α) := by
    have := h1.closure.secondCountableTopology
    exact continuous_subtype_val.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Nontrivial α
a : α
h :
  StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
h₁ :
  ∀ (x : α),
    (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
      Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x
⊢ ((closure[inst] s).piecewise (β := fun (i : α) ↦ α) id fun (x : α) ↦ a) =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Nontrivial α
a : α
h :
  StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
x : α
pos :
  ∀ (hx : x ∈ closure[inst] s),
    (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
      Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x
neg :
  ∀ (hx : x ∉ closure[inst] s),
    (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
      Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x
⊢ (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x

Tactic:
by_cases hx : x ∈ closure s

Premises used: closure
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Nontrivial α
a : α
h :
  StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
x : α
hx : x ∈ closure[inst] s
⊢ (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x

Tactic:
simp [Function.extend_val_apply, hx]

Premises used: Function.extend_val_apply
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Nontrivial α
a : α
h :
  StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
x : α
hx : x ∉ closure[inst] s
⊢ (closure[inst] s).piecewise (β := fun (i : α) ↦ α) id (fun (x : α) ↦ a) x =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) (fun (x : α) ↦ a) x

Tactic:
simp [hx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Nontrivial α
a : α
h :
  StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
⊢ ((closure[inst] s).piecewise (β := fun (i : α) ↦ α) id fun (x : α) ↦ a) =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a

Tactic:
have : (closure s).piecewise id (fun _ ↦ a) =
      ((↑) : closure s → α).extend ((↑) : closure s → α) (fun _ ↦ a) := by
    ext x
    by_cases hx : x ∈ closure s
    · simp [Function.extend_val_apply, hx]
    · simp [hx]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Nontrivial α
a : α
h :
  StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
this :
  ((closure[inst] s).piecewise (β := fun (i : α) ↦ α) id fun (x : α) ↦ a) =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a
rw :
  StronglyMeasurable.{u_1, u_1} (α := α)
    (Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a)
⊢ StronglyMeasurable ((closure[inst] s).piecewise (β := fun (a : α) ↦ α) id fun (x : α) ↦ a)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Nontrivial α
a : α
h :
  StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
this :
  ((closure[inst] s).piecewise (β := fun (i : α) ↦ α) id fun (x : α) ↦ a) =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a
⊢ StronglyMeasurable.{u_1, u_1} (α := α)
    (Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a)

Tactic:
(MeasurableEmbedding.subtype_coe isClosed_closure.measurableSet).stronglyMeasurable_extend
    h stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const, IsClosed.measurableSet, MeasurableEmbedding.stronglyMeasurable_extend, isClosed_closure, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h_1 : Nontrivial α
a : α
h :
  StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
    (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
this :
  ((closure[inst] s).piecewise (β := fun (i : α) ↦ α) id fun (x : α) ↦ a) =
    Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a
⊢ StronglyMeasurable.{u_1, u_1} (α := α)
    (Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a)

Tactic:
exact (MeasurableEmbedding.subtype_coe isClosed_closure.measurableSet).stronglyMeasurable_extend
    h stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const, IsClosed.measurableSet, MeasurableEmbedding.stronglyMeasurable_extend, isClosed_closure, MeasurableEmbedding.subtype_coe
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
s : Set α
h1 : IsSeparable s
h2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : Nontrivial α
a : α
refine : StronglyMeasurable ((closure[inst] s).piecewise (β := fun (a : α) ↦ α) id fun (x : α) ↦ a)
refine₁ :
  ∀
    (h :
      StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
        (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))),
    StronglyMeasurable ((closure[inst] s).piecewise (β := fun (a : α) ↦ α) id fun (x : α) ↦ a)
refine₂ :
  ∀
    (h :
      StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
        (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)))
    (this :
      ((closure[inst] s).piecewise (β := fun (i : α) ↦ α) id fun (x : α) ↦ a) =
        Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
          (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a),
    StronglyMeasurable ((closure[inst] s).piecewise (β := fun (a : α) ↦ α) id fun (x : α) ↦ a)
refine₃ :
  ∀
    (h :
      StronglyMeasurable.{u_1, u_1} (α := { x : α // x ∈ closure[inst] s })
        (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)))
    (this :
      ((closure[inst] s).piecewise (β := fun (i : α) ↦ α) id fun (x : α) ↦ a) =
        Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
          (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a),
    StronglyMeasurable.{u_1, u_1} (α := α)
      (Function.extend (α := { x : α // x ∈ closure[inst] s }) (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s))
        (Subtype.val (p := fun (x : α) ↦ x ∈ closure[inst] s)) fun (x : α) ↦ a)
⊢ AEStronglyMeasurable id μ

Tactic:
classical
  refine ⟨(closure s).piecewise id (fun _ ↦ a), ?_,
    Filter.mem_of_superset h2 (fun x hx ↦ by simp [subset_closure hx])⟩
  have h : StronglyMeasurable ((↑) : closure s → α) := by
    have := h1.closure.secondCountableTopology
    exact continuous_subtype_val.stronglyMeasurable
  have : (closure s).piecewise id (fun _ ↦ a) =
      ((↑) : closure s → α).extend ((↑) : closure s → α) (fun _ ↦ a) := by
    ext x
    by_cases hx : x ∈ closure s
    · simp [Function.extend_val_apply, hx]
    · simp [hx]
  rw [this]
  exact (MeasurableEmbedding.subtype_coe isClosed_closure.measurableSet).stronglyMeasurable_extend
    h stronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Countable α
inst_2 : MeasurableSingletonClass α
⊢ AEStronglyMeasurable f μ

Tactic:
StronglyMeasurable.of_discrete.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.StronglyMeasurable.of_discrete
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
⊢ StronglyMeasurable (AEStronglyMeasurable.mk f hf)

Tactic:
hf.choose_spec.1

Premises used: Exists.choose_spec, MeasureTheory.AEStronglyMeasurable.mk, And.left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
hf : AEStronglyMeasurable f μ
⊢ Measurable (AEStronglyMeasurable.mk f hf)

Tactic:
hf.stronglyMeasurable_mk.measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
⊢ f =ᶠ[ae μ] AEStronglyMeasurable.mk f hf

Tactic:
hf.choose_spec.2

Premises used: Exists.choose_spec, MeasureTheory.AEStronglyMeasurable.mk, And.right
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : BorelSpace β
f : α → β
hf : AEStronglyMeasurable f μ
⊢ AEMeasurable f μ

Tactic:
⟨hf.mk f, hf.stronglyMeasurable_mk.measurable, hf.ae_eq_mk⟩

Premises used: AEMeasurable, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
hf : AEStronglyMeasurable f μ
h : f =ᶠ[ae μ] g
⊢ AEStronglyMeasurable g μ

Tactic:
⟨hf.mk f, hf.stronglyMeasurable_mk, h.symm.trans hf.ae_eq_mk⟩

Premises used: Filter.EventuallyEq.trans, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
h : f =ᶠ[ae μ] g
⊢ AEStronglyMeasurable f μ ↔ AEStronglyMeasurable g μ

Tactic:
⟨fun hf => hf.congr h, fun hg => hg.congr h.symm⟩

Premises used: MeasureTheory.AEStronglyMeasurable.congr, Iff.intro, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
ν : Measure α
hf : AEStronglyMeasurable f μ
h : ν ≤ μ
⊢ AEStronglyMeasurable f ν

Tactic:
⟨hf.mk f, hf.stronglyMeasurable_mk, Eventually.filter_mono (ae_mono h) hf.ae_eq_mk⟩

Premises used: Filter.Eventually.filter_mono, MeasureTheory.ae_mono, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ ν : Measure α
f : α → β
h : ν ≪ μ
hμ : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f ν

Tactic:
let ⟨g, hg, hg'⟩ := hμ; ⟨g, hg, h.ae_eq hg'⟩

Premises used: _private.0.MeasureTheory.AEStronglyMeasurable.mono_ac.match_1, And.intro, Exists.intro, MeasureTheory.Measure.AbsolutelyContinuous.ae_eq, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
s t : Set α
h : s ⊆ t
ht : AEStronglyMeasurable f (μ.restrict t)
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
ht.mono_measure (restrict_mono h le_rfl)

Premises used: le_rfl, MeasureTheory.Measure.restrict_mono, MeasureTheory.AEStronglyMeasurable.mono_measure
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
m' : MeasurableSpace α
hm : m ≤ m'
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f μ

Tactic:
let ⟨f', hf'_meas, hff'⟩ := hf; ⟨f', hf'_meas.mono hm, hff'⟩

Premises used: _private.0.MeasureTheory.AEStronglyMeasurable.mono_ac.match_1, MeasureTheory.StronglyMeasurable.mono, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
m₀' : MeasurableSpace α
hm₀ : m₀' ≤ m₀
hf : AEStronglyMeasurable f (μ.trim hm₀)
obtain : ∀ (g : α → β) (hg_meas : StronglyMeasurable g) (hfg : f =ᶠ[ae (μ.trim hm₀)] g), AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f μ

Tactic:
obtain ⟨g, hg_meas, hfg⟩ := hf
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
m₀' : MeasurableSpace α
hm₀ : m₀' ≤ m₀
g : α → β
hg_meas : StronglyMeasurable g
hfg : f =ᶠ[ae (μ.trim hm₀)] g
⊢ AEStronglyMeasurable f μ

Tactic:
⟨g, hg_meas, ae_eq_of_ae_eq_trim hfg⟩

Premises used: MeasureTheory.ae_eq_of_ae_eq_trim, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
m₀' : MeasurableSpace α
hm₀ : m₀' ≤ m₀
g : α → β
hg_meas : StronglyMeasurable g
hfg : f =ᶠ[ae (μ.trim hm₀)] g
⊢ AEStronglyMeasurable f μ

Tactic:
exact ⟨g, hg_meas, ae_eq_of_ae_eq_trim hfg⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hfm : AEStronglyMeasurable f μ
s : Set α
⊢ AEStronglyMeasurable f (μ.restrict s)

Tactic:
hfm.mono_measure Measure.restrict_le_self

Premises used: MeasureTheory.AEStronglyMeasurable.mono_measure, MeasureTheory.Measure.restrict_le_self
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
s : Set α
h : AEStronglyMeasurable f (μ.restrict s)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f h x

Tactic:
ae_imp_of_ae_restrict h.ae_eq_mk

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.ae_imp_of_ae_restrict
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m m₀ : MeasurableSpace α
μ : Measure α
g : β → γ
f : α → β
hg : Continuous[inst, inst_1] g
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ

Tactic:
⟨_, hg.comp_stronglyMeasurable hf.stronglyMeasurable_mk, EventuallyEq.fun_comp hf.ae_eq_mk g⟩

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Continuous.comp_stronglyMeasurable, And.intro, Exists.intro, Filter.EventuallyEq.fun_comp, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : PseudoMetrizableSpace β
inst_4 : SecondCountableTopologyEither α β
hf : Continuous[inst_1, inst] f
⊢ AEStronglyMeasurable f μ

Tactic:
hf.stronglyMeasurable.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, Continuous.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β × γ
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := β) (fun (x : α) ↦ (f x).1) μ

Tactic:
continuous_fst.comp_aestronglyMeasurable hf

Premises used: Continuous.comp_aestronglyMeasurable, continuous_fst
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β × γ
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ (f x).2) μ

Tactic:
continuous_snd.comp_aestronglyMeasurable hf

Premises used: Continuous.comp_aestronglyMeasurable, continuous_snd
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
g : α → γ
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable (β := β × γ) (fun (x : α) ↦ (f x, g x)) μ

Tactic:
⟨fun x => (hf.mk f x, hg.mk g x), hf.stronglyMeasurable_mk.prodMk hg.stronglyMeasurable_mk,
    hf.ae_eq_mk.prodMk hg.ae_eq_mk⟩

Premises used: Prod.mk, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, MeasureTheory.StronglyMeasurable.prodMk, Exists.intro, Filter.EventuallyEq.prodMk, MeasureTheory.AEStronglyMeasurable