awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
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))
⊢ StronglyMeasurable ((closure[inst] s).piecewise (β := fun (a : α) ↦ α) id fun (x : α) ↦ a)
have 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
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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 ((closure[inst] s).piecewise (β := fun (a : α) ↦ α) id fun (x : α) ↦ a)
have 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)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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 : α
⊢ AEStronglyMeasurable id μ
have refine : StronglyMeasurable ((closure[inst] s).piecewise (β := fun (a : α) ↦ α) id fun (x : α) ↦ a)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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)
⊢ AEStronglyMeasurable id μ
have 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)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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)
⊢ AEStronglyMeasurable id μ
have 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)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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)
⊢ AEStronglyMeasurable id μ
have 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)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m m₀ : MeasurableSpace α
μ : Measure α
f : α → β
m₀' : MeasurableSpace α
hm₀ : m₀' ≤ m₀
hf : AEStronglyMeasurable f (μ.trim hm₀)
⊢ AEStronglyMeasurable f μ
have obtain : ∀ (g : α → β) (hg_meas : StronglyMeasurable g) (hfg : f =ᶠ[ae (μ.trim hm₀)] g), AEStronglyMeasurable f μ
Tactic: obtain ⟨g, hg_meas, hfg⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f
have refine : s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] s.indicator f
Tactic: refine Filter.EventuallyEq.trans ?_ <|
      indicator_ae_eq_of_restrict_compl_ae_eq_zero (hm _ hs_m) hf_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] s.indicator f
have h : ∀ (x : α) (hx : f x = AEStronglyMeasurable.mk f hf x), s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x
Tactic: filter_upwards [hf.ae_eq_mk] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x
have pos : ∀ (hxs : x ∈ s), s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
pos : ∀ (hxs : x ∈ s), s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x
have neg : ∀ (hxs : x ∉ s), s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ AEStronglyMeasurable f μ
have h_ind_eq : s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f
Tactic: have h_ind_eq : s.indicator (hf.mk f) =ᵐ[μ] f := by
    refine Filter.EventuallyEq.trans ?_ <|
      indicator_ae_eq_of_restrict_compl_ae_eq_zero (hm _ hs_m) hf_zero
    filter_upwards [hf.ae_eq_mk] with x hx
    by_cases hxs : x ∈ s
    · simp [hxs, hx]
    · simp [hxs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst_1 : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
h_ind_eq : s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f
⊢ AEStronglyMeasurable f μ
have suffices : StronglyMeasurable (s.indicator (AEStronglyMeasurable.mk f hf))
Tactic: suffices StronglyMeasurable[m'] (s.indicator (hf.mk f)) from
    this.aestronglyMeasurable.congr h_ind_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEStronglyMeasurable f μ), AEStronglyMeasurable l.prod μ
hl : ∀ f_1 ∈ f :: l, AEStronglyMeasurable f_1 μ
⊢ AEStronglyMeasurable (f :: l).prod μ
have hl₁ : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ
Tactic: rw [List.forall_mem_cons] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEStronglyMeasurable f μ), AEStronglyMeasurable l.prod μ
hl : AEStronglyMeasurable f μ ∧ ∀ x ∈ l, AEStronglyMeasurable x μ
⊢ AEStronglyMeasurable (f :: l).prod μ
have cons : AEStronglyMeasurable (f * l.prod) μ
Tactic: rw [List.prod_cons]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
l : List (α → M)
hl : ∀ f ∈ l, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable l.prod μ
have nil : ∀ (hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → AEStronglyMeasurable f μ),
  AEStronglyMeasurable.{u_1, u_5} (β := M) (List.prod []) μ
Tactic: induction l with
  | nil => exact aestronglyMeasurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
l : List (α → M)
hl : ∀ f ∈ l, AEStronglyMeasurable f μ
nil :
  ∀ (hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → AEStronglyMeasurable f μ),
    AEStronglyMeasurable.{u_1, u_5} (β := M) (List.prod []) μ
⊢ AEStronglyMeasurable l.prod μ
have cons : ∀ (f : α → M) (l : List (α → M)) (ihl : ∀ (hl : ∀ f ∈ l, AEStronglyMeasurable f μ), AEStronglyMeasurable l.prod μ)
  (hl : ∀ f_1 ∈ f :: l, AEStronglyMeasurable f_1 μ), AEStronglyMeasurable (f :: l).prod μ
Tactic: induction l with
  | nil => exact aestronglyMeasurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
l : Multiset (α → M)
hl : ∀ f ∈ l, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable l.prod μ
have mk : ∀ (l : List (α → M))
  (hl :
    ∀ (f : α → M),
      Membership.mem (γ := Multiset (α → M)) (Quot.mk (⇑(List.isSetoid (α → M)) : List (α → M) → List (α → M) → Prop) l)
          f →
        AEStronglyMeasurable f μ),
  AEStronglyMeasurable (Multiset.prod (Quot.mk (⇑(List.isSetoid (α → M)) : List (α → M) → List (α → M) → Prop) l)) μ
Tactic: rcases l with ⟨l⟩
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEStronglyMeasurable (s.indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)
have mp : AEStronglyMeasurable (s.indicator f) μ → AEStronglyMeasurable f (μ.restrict s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
mp : AEStronglyMeasurable (s.indicator f) μ → AEStronglyMeasurable f (μ.restrict s)
⊢ AEStronglyMeasurable (s.indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)
have mpr : AEStronglyMeasurable f (μ.restrict s) → AEStronglyMeasurable (s.indicator f) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
⊢ AEStronglyMeasurable (s.indicator f) μ
have mpr : s.indicator f =ᶠ[ae μ] s.indicator (AEStronglyMeasurable.mk f h)
Tactic: refine ⟨indicator s (h.mk f), h.stronglyMeasurable_mk.indicator hs, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEStronglyMeasurable.mk f h)
have A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEStronglyMeasurable.mk f h)
Tactic: have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (h.mk f) :=
      (indicator_ae_eq_restrict hs).trans (h.ae_eq_mk.trans <| (indicator_ae_eq_restrict hs).symm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEStronglyMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEStronglyMeasurable.mk f h)
have B : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] s.indicator (AEStronglyMeasurable.mk f h)
Tactic: have B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (h.mk f) :=
      (indicator_ae_eq_restrict_compl hs).trans (indicator_ae_eq_restrict_compl hs).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : NullMeasurableSet s μ
⊢ AEStronglyMeasurable (s.indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)
have rw : AEStronglyMeasurable ((toMeasurable μ s).indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)
Tactic: rw [← aestronglyMeasurable_congr (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    aestronglyMeasurable_indicator_iff (measurableSet_toMeasurable ..),
    restrict_congr_set hs.toMeasurable_ae_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : NullMeasurableSet s μ
rw : AEStronglyMeasurable ((toMeasurable μ s).indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)
⊢ AEStronglyMeasurable (s.indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)
have rw₁ : AEStronglyMeasurable f (μ.restrict (toMeasurable μ s)) ↔ AEStronglyMeasurable f (μ.restrict s)
Tactic: rw [← aestronglyMeasurable_congr (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    aestronglyMeasurable_indicator_iff (measurableSet_toMeasurable ..),
    restrict_congr_set hs.toMeasurable_ae_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst_1 : Zero β
s : Set α
hs : NullMeasurableSet s μ
rw : AEStronglyMeasurable ((toMeasurable μ s).indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)
rw₁ : AEStronglyMeasurable f (μ.restrict (toMeasurable μ s)) ↔ AEStronglyMeasurable f (μ.restrict s)
⊢ AEStronglyMeasurable (s.indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)
have rw₂ : AEStronglyMeasurable f (μ.restrict s) ↔ AEStronglyMeasurable f (μ.restrict s)
Tactic: rw [← aestronglyMeasurable_congr (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    aestronglyMeasurable_indicator_iff (measurableSet_toMeasurable ..),
    restrict_congr_set hs.toMeasurable_ae_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ NullMeasurableSet {x : α | f x = g x} μ
have this : {a : α | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {x : α | f x = g x}
Tactic: apply
    (hf.stronglyMeasurable_mk.measurableSet_eq_fun
          hg.stronglyMeasurable_mk).nullMeasurableSet.congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : TopologicalSpace E
inst_1 : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a : α | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} =ᶠ[ae μ] {x : α | f x = g x}
have h : ∀ (x : α) (hfx : f x = AEStronglyMeasurable.mk f hf x) (hgx : g x = AEStronglyMeasurable.mk g hg x),
  {a : α | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} x = {x : α | f x = g x} x
Tactic: filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx