awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
refine : StronglyMeasurable ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s))
refine₁ : ∀ (x : α), (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x ∈ s
refine₂ : f =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
⊢ ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g

Tactic:
refine ⟨(f' ⁻¹' s).piecewise f' (fun _ ↦ h_nonempty.some), ?meas, ?subset, ?ae_eq⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ StronglyMeasurable ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s))

Tactic:
hf'.piecewise (hf'.measurable hs) stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.StronglyMeasurable.piecewise
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ StronglyMeasurable ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s))

Tactic:
exact hf'.piecewise (hf'.measurable hs) stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.StronglyMeasurable.piecewise
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ StronglyMeasurable ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s))

Tactic:
case meas => exact hf'.piecewise (hf'.measurable hs) stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.StronglyMeasurable.piecewise
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
rw : range ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)) ⊆ s
⊢ ∀ (x : α), (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x ∈ s

Tactic:
rw [← Set.range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ range ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)) ⊆ s

Tactic:
simpa [Set.range_piecewise] using fun _ _ ↦ h_nonempty.some_mem

Premises used: Set.Nonempty.some_mem, Set.range_piecewise
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ ∀ (x : α), (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x ∈ s

Tactic:
case subset =>
    rw [← Set.range_subset_iff]
    simpa [Set.range_piecewise] using fun _ _ ↦ h_nonempty.some_mem

Premises used: Set.Nonempty.some_mem, Set.range_piecewise, Set.range_subset_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
apply : f' =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
⊢ f =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)

Tactic:
apply hff'.trans

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
h :
  ∀ (x : α) (hx : f x ∈ s) (hx' : f x = f' x),
    f' x = (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x
⊢ f' =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)

Tactic:
filter_upwards [h_mem, hff'] with x hx hx'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
x : α
hx : f x ∈ s
hx' : f x = f' x
⊢ x ∈ f' ⁻¹' s

Tactic:
simpa [hx'] using hx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
x : α
hx : f x ∈ s
hx' : f x = f' x
⊢ f' x = (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x

Tactic:
exact Eq.symm <| (f' ⁻¹' s).piecewise_eq_of_mem f' _ (by simpa [hx'] using hx)

Premises used: Set.piecewise_eq_of_mem, Set.preimage, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
case : f' =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
h :
  ∀ (x : α) (hx : f x ∈ s) (hx' : f x = f' x),
    f' x = (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x
⊢ f =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)

Tactic:
case ae_eq =>
    apply hff'.trans
    filter_upwards [h_mem, hff'] with x hx hx'
    exact Eq.symm <| (f' ⁻¹' s).piecewise_eq_of_mem f' _ (by simpa [hx'] using hx)

Premises used: Filter.EventuallyEq.trans, Set.piecewise_eq_of_mem, Set.preimage, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
refine : StronglyMeasurable ((f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s))
refine₁ : ∀ (x : α), (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x ∈ s
refine₂ : f =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
refine₃ : ∀ (x : α), (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' (fun (x : α) ↦ h_nonempty.some (s := s)) x ∈ s
refine₄ refine₅ : f =ᶠ[ae μ] (f' ⁻¹' s).piecewise (β := fun (a : α) ↦ β) f' fun (x : α) ↦ h_nonempty.some (s := s)
⊢ ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g

Tactic:
classical
  refine ⟨(f' ⁻¹' s).piecewise f' (fun _ ↦ h_nonempty.some), ?meas, ?subset, ?ae_eq⟩
  case meas => exact hf'.piecewise (hf'.measurable hs) stronglyMeasurable_const
  case subset =>
    rw [← Set.range_subset_iff]
    simpa [Set.range_piecewise] using fun _ _ ↦ h_nonempty.some_mem
  case ae_eq =>
    apply hff'.trans
    filter_upwards [h_mem, hff'] with x hx hx'
    exact Eq.symm <| (f' ⁻¹' s).piecewise_eq_of_mem f' _ (by simpa [hx'] using hx)

Premises used: MeasureTheory.stronglyMeasurable_const, Filter.EventuallyEq.trans, MeasureTheory.StronglyMeasurable.measurable, Set.Nonempty.some_mem, Set.range_piecewise, MeasureTheory.StronglyMeasurable.piecewise, Set.range_subset_iff, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ AEStronglyMeasurable (s.piecewise (β := fun (a : α) ↦ β) f g) μ

Tactic:
⟨s.piecewise (hf.mk f) (hg.mk g),
    StronglyMeasurable.piecewise hs hf.stronglyMeasurable_mk hg.stronglyMeasurable_mk, ?_⟩

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, MeasureTheory.StronglyMeasurable.piecewise, Set.piecewise, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
refine :
  s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ]
    s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg)
⊢ AEStronglyMeasurable (s.piecewise (β := fun (a : α) ↦ β) f g) μ

Tactic:
refine ⟨s.piecewise (hf.mk f) (hg.mk g),
    StronglyMeasurable.piecewise hs hf.stronglyMeasurable_mk hg.stronglyMeasurable_mk, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ]
    s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg)

Tactic:
ae_of_ae_restrict_of_ae_restrict_compl s ?_ ?_

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
refine_1 :
  ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise (β := fun (a : α) ↦ β) f g x =
      s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
refine_2 :
  ∀ᵐ (x : α) ∂μ.restrict sᶜ,
    s.piecewise (β := fun (a : α) ↦ β) f g x =
      s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
⊢ s.piecewise (β := fun (a : α) ↦ β) f g =ᶠ[ae μ]
    s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg)

Tactic:
refine ae_of_ae_restrict_of_ae_restrict_compl s ?_ ?_

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ f =ᶠ[ae (μ.restrict s)] AEStronglyMeasurable.mk f hf

Tactic:
have h := hf.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : f =ᶠ[ae (μ.restrict s)] AEStronglyMeasurable.mk f hf
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs] at h

Premises used: Filter.EventuallyEq, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
refine_1 :
  ∀ᵐ (x : α) ∂μ,
    x ∈ s →
      s.piecewise (β := fun (a : α) ↦ β) f g x =
        s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise (β := fun (a : α) ↦ β) f g x =
      s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
rw [ae_restrict_iff' hs]

Premises used: MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
h₁ :
  ∀ (x : α) (hx : x ∈ s → f x = AEStronglyMeasurable.mk f hf x),
    x ∈ s →
      s.piecewise (β := fun (a : α) ↦ β) f g x =
        s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
⊢ ∀ᵐ (x : α) ∂μ,
    x ∈ s →
      s.piecewise (β := fun (a : α) ↦ β) f g x =
        s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
x : α
hx : x ∈ s → f x = AEStronglyMeasurable.mk f hf x
hx_mem : x ∈ s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x =
    s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
simp only [hx_mem, Set.piecewise_eq_of_mem, hx hx_mem]

Premises used: Set.piecewise_eq_of_mem
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ g =ᶠ[ae (μ.restrict sᶜ)] AEStronglyMeasurable.mk g hg

Tactic:
have h := hg.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : g =ᶠ[ae (μ.restrict sᶜ)] AEStronglyMeasurable.mk g hg
⊢ ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs.compl] at h

Premises used: Filter.EventuallyEq, MeasurableSet.compl, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
refine_2 :
  ∀ᵐ (x : α) ∂μ,
    x ∈ sᶜ →
      s.piecewise (β := fun (a : α) ↦ β) f g x =
        s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
⊢ ∀ᵐ (x : α) ∂μ.restrict sᶜ,
    s.piecewise (β := fun (a : α) ↦ β) f g x =
      s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
rw [ae_restrict_iff' hs.compl]

Premises used: MeasurableSet.compl, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
h₁ :
  ∀ (x : α) (hx : x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x),
    x ∈ sᶜ →
      s.piecewise (β := fun (a : α) ↦ β) f g x =
        s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
⊢ ∀ᵐ (x : α) ∂μ,
    x ∈ sᶜ →
      s.piecewise (β := fun (a : α) ↦ β) f g x =
        s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
filter_upwards [h] with x hx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
x : α
hx : x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
hx_mem : x ∈ sᶜ
⊢ x ∉ s

Tactic:
rw [Set.mem_compl_iff] at hx_mem

Premises used: Set.mem_compl_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
x : α
hx : x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
hx_mem : x ∉ s
⊢ s.piecewise (β := fun (a : α) ↦ β) f g x =
    s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
simp only [hx_mem, not_false_eq_true, Set.piecewise_eq_of_notMem, hx hx_mem]

Premises used: Set.piecewise_eq_of_notMem, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ AEStronglyMeasurable f (sum μ)

Tactic:
aestronglyMeasurable_iff_aemeasurable_separable.2
      ⟨AEMeasurable.sum_measure fun i => (h i).aemeasurable, ?_⟩

Premises used: Iff.mpr, MeasureTheory.AEStronglyMeasurable.aemeasurable, aestronglyMeasurable_iff_aemeasurable_separable, AEMeasurable.sum_measure, And.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
fun : ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t
⊢ AEStronglyMeasurable f (sum μ)

Tactic:
refine
    aestronglyMeasurable_iff_aemeasurable_separable.2
      ⟨AEMeasurable.sum_measure fun i => (h i).aemeasurable, ?_⟩

Premises used: Iff.mpr, MeasureTheory.AEStronglyMeasurable.aemeasurable, aestronglyMeasurable_iff_aemeasurable_separable, AEMeasurable.sum_measure, And.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : Countable ι
inst_1 : TopologicalSpace β
f : α → β
inst_2 : PseudoMetrizableSpace β
m : MeasurableSpace α
μ : ι → Measure α
h : ∀ (i : ι), AEStronglyMeasurable f (μ i)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ ∀ (i : ι), ∃ (t : Set β), IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i)

Tactic:
have A : ∀ i : ι, ∃ t : Set β, IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i) := fun i =>
    (aestronglyMeasurable_iff_aemeasurable_separable.1 (h i)).2