awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this_1 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_2 : MeasurableSpace β := borel β
this_3 : BorelSpace β
this_4 : MeasurableSpace γ := borel γ
this_5 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
this : IsSeparable (g ⁻¹' range (g ∘ f))
⊢ IsSeparable (range f)
have refine_2 : ∀ (this : IsSeparable (g ⁻¹' g '' range f)), IsSeparable (range f)
Tactic: rwa [range_comp, hg.injective.preimage_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this_1 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_2 : MeasurableSpace β := borel β
this_3 : BorelSpace β
this_4 : MeasurableSpace γ := borel γ
this_5 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
this : IsSeparable (g ⁻¹' range (g ∘ f))
refine_2 : ∀ (this : IsSeparable (g ⁻¹' g '' range f)), IsSeparable (range f)
⊢ IsSeparable (range f)
have refine_2₁ : ∀ (this : IsSeparable (range f)), IsSeparable (range f)
Tactic: rwa [range_comp, hg.injective.preimage_image] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
⊢ StronglyMeasurable g
have this : let this := borel β;
BorelSpace β
Tactic: borelize β
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ StronglyMeasurable g
have refine_1 : Measurable g
Tactic: refine stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
refine_1 : Measurable g
⊢ StronglyMeasurable g
have refine_2 : IsSeparable (range g)
Tactic: refine stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ IsSeparable (range g)
have refine_2 : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), IsSeparable (range g)
Tactic: rcases u.exists_seq_tendsto with ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
⊢ IsSeparable (range g)
have this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
Tactic: have : IsSeparable (closure (⋃ i, range (f (v i)))) :=
      .closure <| .iUnion fun i => (hf (v i)).isSeparable_range
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
⊢ IsSeparable (range g)
have refine_2 : range g ⊆ closure[inst] (⋃ (i : ℕ), range (f (v i)))
Tactic: apply this.mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
x : α
⊢ Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), range (f (v i)))) (g x)
have refine_2 : ∀ (lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))),
  let this := borel β;
  BorelSpace β →
    ∀ (v : ℕ → ι) (hv : Tendsto v atTop u)
      (this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))) (x : α),
      Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), range (f (v i)))) (g x)
Tactic: rw [tendsto_pi_nhds] at lim
Cleared hypotheses: lim, this_1, this_2, v, hv, this, x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
x : α
⊢ Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), range (f (v i)))) (g x)
have refine_2 : ∀ᶠ (x_1 : ℕ) in atTop, Membership.mem (γ := Set β) (⋃ (i : ℕ), range (f (v i))) (((fun (i : ι) ↦ f i x) ∘ v) x_1)
Tactic: apply mem_closure_of_tendsto ((lim x).comp hv)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
x : α
⊢ ∀ᶠ (x_1 : ℕ) in atTop, Membership.mem (γ := Set β) (⋃ (i : ℕ), range (f (v i))) (((fun (i : ι) ↦ f i x) ∘ v) x_1)
have refine_2 : ∀ (n : ℕ), Membership.mem (γ := Set β) (⋃ (i : ℕ), range (f (v i))) (((fun (i : ι) ↦ f i x) ∘ v) n)
Tactic: filter_upwards with n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
x : α
n : ℕ
⊢ Membership.mem (γ := Set β) (⋃ (i : ℕ), range (f (v i))) (((fun (i : ι) ↦ f i x) ∘ v) n)
have refine_2 : ((fun (i : ι) ↦ f i x) ∘ v) n ∈ range (f (v n))
Tactic: apply mem_iUnion_of_mem n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
s : Set α
x : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (s.piecewise (β := fun (a : α) ↦ β) f g)
have refine : ∀ (x_1 : α),
  Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x_1)
    atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x_1))
Tactic: refine ⟨fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n), fun x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
s : Set α
x_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x)
    atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x))
have pos : ∀ (hx : x ∈ s),
  Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x)
    atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x))
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
s : Set α
x_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
pos :
  ∀ (hx : x ∈ s),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x)
      atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x))
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x)
    atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x))
have neg : ∀ (hx : x ∉ s),
  Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x)
    atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x))
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
⊢ StronglyMeasurable (Function.extend g f g')
have refine : ∀ (x : γ),
  Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
    (𝓝 (Function.extend g f g' x))
Tactic: refine ⟨fun n => SimpleFunc.extend (hf.approx n) g hg (hg'.approx n), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
    (𝓝 (Function.extend g f g' x))
have pos : ∀ (hx : ∃ (y : α), g y = x),
  Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
    (𝓝 (Function.extend g f g' x))
Tactic: by_cases hx : ∃ y, g y = x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
pos :
  ∀ (hx : ∃ (y : α), g y = x),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
      (𝓝 (Function.extend g f g' x))
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
    (𝓝 (Function.extend g f g' x))
have neg : ∀ (hx : ¬∃ (y : α), g y = x),
  Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
    (𝓝 (Function.extend g f g' x))
Tactic: by_cases hx : ∃ y, g y = x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ∃ (y : α), g y = x
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) x) atTop
    (𝓝 (Function.extend g f g' x))
have pos : ∀ (y : α),
  Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).extend g hg (hg'.approx n)) n : (a : γ) → β) (g y)) atTop
    (𝓝 (Function.extend g f g' (g y)))
Tactic: rcases hx with ⟨y, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
⊢ 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
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : 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
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
⊢ StronglyMeasurable f
have suffices : Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
    (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
      default) =
  f
Tactic: suffices Function.extend Subtype.val (fun x : s ↦ f x)
      (Function.extend (↑) (fun x : t ↦ f x) fun _ ↦ default) = f from
    this ▸ (MeasurableEmbedding.subtype_coe hs).stronglyMeasurable_extend hc <|
      (MeasurableEmbedding.subtype_coe ht).stronglyMeasurable_extend hd stronglyMeasurable_const
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default) =
    f
have h₁ : ∀ (x : α),
  Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      x =
    f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : α
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      x =
    f x
have pos : ∀ (hxs : x ∈ s),
  Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      x =
    f x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : α
pos :
  ∀ (hxs : x ∈ s),
    Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
        (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
          default)
        x =
      f x
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      x =
    f x
have neg : ∀ (hxs : x ∉ s),
  Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      x =
    f x
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : α
hxs : x ∈ s
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      x =
    f x
have pos : ∀ (x : { x : α // x ∈ s }),
  Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      (↑x : α) =
    f (↑x : α)
Tactic: lift x to s using hxs
Cleared hypotheses: x, hxs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : α
hxs : x ∉ s
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      x =
    f x
have neg : ∀ (x : { x : α // x ∈ t }) (hxs : (↑x : α) ∉ s),
  Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      (↑x : α) =
    f (↑x : α)
Tactic: lift x to t using (h trivial).resolve_left hxs
Cleared hypotheses: x, hxs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : TopologicalSpace β
f : α → β
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hc : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑s : Type u_1)) ↦ f (↑a : α)
hd : StronglyMeasurable.{u_1, u_2} (β := β) fun (a : (↑t : Type u_1)) ↦ f (↑a : α)
h_1 : Nontrivial β
inhabited_h : Inhabited β
x : { x : α // x ∈ t }
hxs : (↑x : α) ∉ s
⊢ Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (fun (x : (↑s : Type u_1)) ↦ f (↑x : α))
      (Function.extend (Subtype.val (p := fun (x : α) ↦ x ∈ t)) (fun (x : (↑t : Type u_1)) ↦ f (↑x : α)) fun (x : α) ↦
        default)
      (↑x : α) =
    f (↑x : α)
have neg : ¬∃ (a : { x : α // x ∈ s }), (↑a : α) = (↑x : α)
Tactic: rw [extend_apply', Subtype.coe_injective.extend_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : AddZeroClass β
inst_2 : TopologicalSpace β
P : (f : α → β) → StronglyMeasurable f → Prop
ind : ∀ (c : β) ⦃s : Set α⦄ (hs : MeasurableSet s), P (s.indicator fun (x : α) ↦ c) ⋯
add :
  ∀ ⦃f g : α → β⦄ (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) (hfg : StronglyMeasurable (f + g)),
    Disjoint (support f) (support g) → P f hf → P g hg → P (f + g) hfg
lim :
  ∀ ⦃f : ℕ → α → β⦄ ⦃g : α → β⦄ (hf : ∀ (n : ℕ), StronglyMeasurable (f n)) (hg : StronglyMeasurable g),
    (∀ (n : ℕ), P (f n) ⋯) → (∀ (x : α), Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g x))) → P g hg
f : α → β
hf : StronglyMeasurable f
s : ℕ → α →ₛ β := hf.approx
⊢ P f hf
have refine : ∀ (n : ℕ), P (⇑(s n) : (a : α) → β) sorry
Tactic: refine lim (fun n ↦ (s n).stronglyMeasurable) hf (fun n ↦ ?_) hf.tendsto_approx