awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
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ᶜ)
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise (β := fun (a : α) ↦ β) f g x =
      s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
have h : f =ᶠ[ae (μ.restrict s)] AEStronglyMeasurable.mk f hf
Tactic: have h := hf.ae_eq_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
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 : α) ∂μ.restrict s,
    s.piecewise (β := fun (a : α) ↦ β) f g x =
      s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
have h₁ : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
Tactic: rw [Filter.EventuallyEq, ae_restrict_iff' hs] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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 : α) ∂μ.restrict s,
    s.piecewise (β := fun (a : α) ↦ β) f g x =
      s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
have 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
Tactic: rw [ae_restrict_iff' hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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 : α) ∂μ,
    x ∈ s →
      s.piecewise (β := fun (a : α) ↦ β) f g x =
        s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
have 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
Tactic: filter_upwards [h] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
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ᶜ)
⊢ ∀ᵐ (x : α) ∂μ.restrict sᶜ,
    s.piecewise (β := fun (a : α) ↦ β) f g x =
      s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
have h : g =ᶠ[ae (μ.restrict sᶜ)] AEStronglyMeasurable.mk g hg
Tactic: have h := hg.ae_eq_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
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 : α) ∂μ.restrict sᶜ,
    s.piecewise (β := fun (a : α) ↦ β) f g x =
      s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
have h₁ : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
Tactic: rw [Filter.EventuallyEq, ae_restrict_iff' hs.compl] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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 : α) ∂μ.restrict sᶜ,
    s.piecewise (β := fun (a : α) ↦ β) f g x =
      s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
have 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
Tactic: rw [ae_restrict_iff' hs.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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 : α) ∂μ,
    x ∈ sᶜ →
      s.piecewise (β := fun (a : α) ↦ β) f g x =
        s.piecewise (β := fun (a : α) ↦ β) (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x
have 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
Tactic: filter_upwards [h] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
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
have hx_mem₁ : x ∉ s
Tactic: rw [Set.mem_compl_iff] at hx_mem
Cleared hypotheses: hx_mem
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
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)
⊢ AEStronglyMeasurable f (sum μ)
have this : let this := borel β;
BorelSpace β
Tactic: borelize β
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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 μ)
have fun : ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t
Tactic: refine
    aestronglyMeasurable_iff_aemeasurable_separable.2
      ⟨AEMeasurable.sum_measure fun i => (h i).aemeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (hypothesis)
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 β
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t
have A : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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 β
A : ∀ (i : ι), ∃ (t : Set β), IsSeparable t ∧ f ⁻¹' t ∈ ae (μ i)
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t
have choose : ∀ (t : (i : ι) → Set β) (t_sep : ∀ (i : ι), IsSeparable (t i)) (ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)),
  ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t
Tactic: choose t t_sep ht using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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 β
t : (i : ι) → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂sum μ, f x ∈ t
have refine : ∀ᵐ (x : α) ∂sum μ, Membership.mem (γ := Set β) (⋃ (i : ι), t i) (f x)
Tactic: refine ⟨⋃ i, t i, .iUnion t_sep, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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 β
t : (i : ι) → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
⊢ ∀ᵐ (x : α) ∂sum μ, Membership.mem (γ := Set β) (⋃ (i : ι), t i) (f x)
have simp : ∀ (b : ι), ∀ᵐ (x : α) ∂μ b, ∃ (i : ι), f x ∈ t i
Tactic: simp only [Measure.ae_sum_eq, mem_iUnion, eventually_iSup]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
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 β
t : (i : ι) → Set β
t_sep : ∀ (i : ι), IsSeparable (t i)
ht : ∀ (i : ι), f ⁻¹' t i ∈ ae (μ i)
i : ι
⊢ ∀ᵐ (x : α) ∂μ i, ∃ (i : ι), f x ∈ t i
have h₁ : ∀ (x : α) (hx : x ∈ f ⁻¹' t i), ∃ (i : ι), f x ∈ t i
Tactic: filter_upwards [ht i] 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 α
μ : Measure α
f : α → β
inst_1 : PseudoMetrizableSpace β
ν : Measure α
⊢ AEStronglyMeasurable f (μ + ν) ↔ AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν
have rw : AEStronglyMeasurable f (bif true then μ else ν) ∧ AEStronglyMeasurable f (bif false then μ else ν) ↔
  AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν
Tactic: rw [← sum_cond, aestronglyMeasurable_sum_measure_iff, Bool.forall_bool, and_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : LinearOrder α
inst_2 : PseudoMetrizableSpace β
f : α → β
a b : α
⊢ AEStronglyMeasurable f (μ.restrict (uIoc a b)) ↔
    AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a))
have rw : AEStronglyMeasurable f (μ.restrict (Ioc a b ∪ Ioc b a)) ↔
  AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a))
Tactic: rw [uIoc_eq_union, aestronglyMeasurable_union_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : LinearOrder α
inst_2 : PseudoMetrizableSpace β
f : α → β
a b : α
rw :
  AEStronglyMeasurable f (μ.restrict (Ioc a b ∪ Ioc b a)) ↔
    AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a))
⊢ AEStronglyMeasurable f (μ.restrict (uIoc a b)) ↔
    AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a))
have rw₁ : AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a)) ↔
  AEStronglyMeasurable f (μ.restrict (Ioc a b)) ∧ AEStronglyMeasurable f (μ.restrict (Ioc b a))
Tactic: rw [uIoc_eq_union, aestronglyMeasurable_union_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
hf : AEFinStronglyMeasurable f μ
⊢ ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)
have rcases : ∀ (g : α → β) (hg : FinStronglyMeasurable g μ) (hfg : f =ᶠ[ae μ] g),
  ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)
Tactic: rcases hf with ⟨g, hg, hfg⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
⊢ ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)
have obtain : ∀ (t : Set α) (ht : MeasurableSet t) (hgt_zero : ∀ x ∈ tᶜ, g x = 0) (htμ : SigmaFinite (μ.restrict t)),
  ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)
Tactic: obtain ⟨t, ht, hgt_zero, htμ⟩ := hg.exists_set_sigmaFinite
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ ∃ (t : Set α), MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)
have refine : f =ᶠ[ae (μ.restrict tᶜ)] 0
Tactic: refine ⟨t, ht, ?_, htμ⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ f =ᶠ[ae (μ.restrict tᶜ)] 0
have refine : g =ᶠ[ae (μ.restrict tᶜ)] 0
Tactic: refine EventuallyEq.trans (ae_restrict_of_ae hfg) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ g =ᶠ[ae (μ.restrict tᶜ)] 0
have rw : ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → g x = 0 x
Tactic: rw [EventuallyEq, ae_restrict_iff' ht.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
G : Type u_5
inst : SeminormedAddCommGroup G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : SecondCountableTopology G
f : α → G
_m0 : MeasurableSpace α
μ : Measure α
inst_4 : SigmaFinite μ
⊢ AEFinStronglyMeasurable f μ ↔ AEMeasurable f μ
have simp_rw : (∃ (g : α → G), FinStronglyMeasurable g μ ∧ f =ᶠ[ae μ] g) ↔ AEMeasurable f μ
Tactic: simp_rw [AEFinStronglyMeasurable, AEMeasurable, finStronglyMeasurable_iff_measurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable (goal)
Goal:
α : Type u_1
G : Type u_5
inst : SeminormedAddCommGroup G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : SecondCountableTopology G
f : α → G
_m0 : MeasurableSpace α
μ : Measure α
inst_4 : SigmaFinite μ
simp_rw : (∃ (g : α → G), FinStronglyMeasurable g μ ∧ f =ᶠ[ae μ] g) ↔ AEMeasurable f μ
⊢ AEFinStronglyMeasurable f μ ↔ AEMeasurable f μ
have simp_rw₁ : (∃ (g : α → G), FinStronglyMeasurable g μ ∧ f =ᶠ[ae μ] g) ↔ ∃ (g : α → G), Measurable g ∧ f =ᶠ[ae μ] g
Tactic: simp_rw [AEFinStronglyMeasurable, AEMeasurable, finStronglyMeasurable_iff_measurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : Subsingleton β
refine_2 : StronglyMeasurable f
⊢ StronglyMeasurable f
have refine_1 : ∀ (x_1 : β), MeasurableSet (f ⁻¹' {x_1})
Tactic: let f_sf : α →ₛ β := ⟨f, fun x => ?_, Set.Subsingleton.finite Set.subsingleton_of_subsingleton⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
hf : ∀ (x y : α), f x = f y
⊢ StronglyMeasurable f
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
hf : ∀ (x y : α), f x = f y
h : Nontrivial α
⊢ StronglyMeasurable f
have inhabit : ∀ (inhabited_h : Inhabited α), StronglyMeasurable f
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
hf : ∀ (x y : α), f x = f y
h : Nontrivial α
inhabited_h : Inhabited α
⊢ StronglyMeasurable f
have h : f = fun (x : α) ↦ f default
Tactic: convert! stronglyMeasurable_const (β := β) using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
hf : ∀ (x y : α), f x = f y
h_1 : Nontrivial α
inhabited_h : Inhabited α
h : f = fun (x : α) ↦ f default
⊢ StronglyMeasurable f
have convert_3 : β
Tactic: convert! stronglyMeasurable_const (β := β) using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst : MeasurableSingletonClass α
n : ℕ
hmn : m.succ.le n
⊢ (simpleFuncAux f g n.succ : (a : α) → β) (g m) = f (g m)
have inl : ∀ (hnm : g n = g m), (simpleFuncAux f g n.succ : (a : α) → β) (g m) = f (g m)
Tactic: obtain hnm | hnm := eq_or_ne (g n) (g m)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst : MeasurableSingletonClass α
n : ℕ
hmn : m.succ.le n
inl : ∀ (hnm : g n = g m), (simpleFuncAux f g n.succ : (a : α) → β) (g m) = f (g m)
⊢ (simpleFuncAux f g n.succ : (a : α) → β) (g m) = f (g m)
have inr : ∀ (hnm : g n ≠ g m), (simpleFuncAux f g n.succ : (a : α) → β) (g m) = f (g m)
Tactic: obtain hnm | hnm := eq_or_ne (g n) (g m)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : MeasurableSingletonClass α
inst_2 : Countable α
⊢ StronglyMeasurable f
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : MeasurableSingletonClass α
inst_2 : Countable α
h : Nontrivial α
⊢ StronglyMeasurable f
have obtain : ∀ (g : ℕ → α) (hg : Surjective g), StronglyMeasurable f
Tactic: obtain ⟨g, hg⟩ := exists_surjective_nat α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
⊢ Tendsto (fun (n : ℕ) ↦ (hf.approxBounded c n : (a : α) → β) x) atTop (𝓝 (f x))
have h_tendsto : Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
Tactic: have h_tendsto := hf.tendsto_approx x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ Tendsto (fun (n : ℕ) ↦ (hf.approxBounded c n : (a : α) → β) x) atTop (𝓝 (f x))
have simp : Tendsto
  (fun (n : ℕ) ↦
    HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
      ((hf.approx n : (a : α) → β) x : β))
  atTop (𝓝 (f x))
Tactic: simp only [StronglyMeasurable.approxBounded, SimpleFunc.coe_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β))
    atTop (𝓝 (f x))
have pos : ∀ (hfx0 : ‖f x‖ = 0),
  Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β))
    atTop (𝓝 (f x))
Tactic: by_cases hfx0 : ‖f x‖ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
pos :
  ∀ (hfx0 : ‖f x‖ = 0),
    Tendsto
      (fun (n : ℕ) ↦
        HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
          ((hf.approx n : (a : α) → β) x : β))
      atTop (𝓝 (f x))
⊢ Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β))
    atTop (𝓝 (f x))
have neg : ∀ (hfx0 : ¬‖f x‖ = 0),
  Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β))
    atTop (𝓝 (f x))
Tactic: by_cases hfx0 : ‖f x‖ = 0