awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_5
E : Type u_6
x : MeasurableSpace α
inst : AddCancelMonoid E
inst_1 : TopologicalSpace E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : ContinuousAdd E
inst_5 : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x_1 : α), Tendsto (fun (n : ℕ) ↦ (φ n : (a : α) → E) x_1) atTop (𝓝 (f x_1))
this : Tendsto (fun (n : ℕ) (x_1 : α) ↦ HAdd.hAdd (β := E) (g x_1) ((φ n : (a : α) → E) x_1 : E)) atTop (𝓝 (g + f))
⊢ Measurable (g + f)
have apply : ∀ (n : ℕ), Measurable.{u_5, u_6} (β := E) fun (x_1 : α) ↦ HAdd.hAdd (β := E) (g x_1) ((φ n : (a : α) → E) x_1 : E)
Tactic: apply measurable_of_tendsto_metrizable (fun n ↦ ?_) this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_5
E : Type u_6
x : MeasurableSpace α
inst : AddGroup E
inst_1 : TopologicalSpace E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousNeg E
inst_6 : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
hf : StronglyMeasurable f
⊢ Measurable (g - f)
have rw : Measurable (g + -f)
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_5
E : Type u_6
x : MeasurableSpace α
inst : AddCancelMonoid E
inst_1 : TopologicalSpace E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : ContinuousAdd E
inst_5 : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
hf : StronglyMeasurable f
⊢ Measurable (f + g)
have rcases : ∀ (φ : ℕ → α →ₛ E) (hφ : ∀ (x_1 : α), Tendsto (fun (n : ℕ) ↦ (φ n : (a : α) → E) x_1) atTop (𝓝 (f x_1))),
  Measurable (f + g)
Tactic: rcases hf with ⟨φ, hφ⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_5
E : Type u_6
x : MeasurableSpace α
inst : AddCancelMonoid E
inst_1 : TopologicalSpace E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : ContinuousAdd E
inst_5 : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x_1 : α), Tendsto (fun (n : ℕ) ↦ (φ n : (a : α) → E) x_1) atTop (𝓝 (f x_1))
⊢ Measurable (f + g)
have this : Tendsto (fun (n : ℕ) (x_1 : α) ↦ HAdd.hAdd (α := E) ((φ n : (a : α) → E) x_1 : E) (g x_1)) atTop (𝓝 (f + g))
Tactic: have : Tendsto (fun n x ↦ φ n x + g x) atTop (𝓝 (f + g)) :=
    tendsto_pi_nhds.2 (fun x ↦ (hφ x).add tendsto_const_nhds)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_5
E : Type u_6
x : MeasurableSpace α
inst : AddCancelMonoid E
inst_1 : TopologicalSpace E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : ContinuousAdd E
inst_5 : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x_1 : α), Tendsto (fun (n : ℕ) ↦ (φ n : (a : α) → E) x_1) atTop (𝓝 (f x_1))
this : Tendsto (fun (n : ℕ) (x_1 : α) ↦ HAdd.hAdd (α := E) ((φ n : (a : α) → E) x_1 : E) (g x_1)) atTop (𝓝 (f + g))
⊢ Measurable (f + g)
have apply : ∀ (n : ℕ), Measurable.{u_5, u_6} (β := E) fun (x_1 : α) ↦ HAdd.hAdd (α := E) ((φ n : (a : α) → E) x_1 : E) (g x_1)
Tactic: apply measurable_of_tendsto_metrizable (fun n ↦ ?_) this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, StronglyMeasurable f), StronglyMeasurable l.prod
hl : ∀ f_1 ∈ f :: l, StronglyMeasurable f_1
⊢ StronglyMeasurable (f :: l).prod
have hl₁ : StronglyMeasurable f ∧ ∀ x ∈ l, StronglyMeasurable x
Tactic: rw [List.forall_mem_cons] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, StronglyMeasurable f), StronglyMeasurable l.prod
hl : StronglyMeasurable f ∧ ∀ x ∈ l, StronglyMeasurable x
⊢ StronglyMeasurable (f :: l).prod
have cons : StronglyMeasurable (f * l.prod)
Tactic: rw [List.prod_cons]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, StronglyMeasurable f
⊢ StronglyMeasurable l.prod
have nil : ∀ (hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → StronglyMeasurable f),
  StronglyMeasurable.{u_1, u_5} (α := α) (β := M) (List.prod [])
Tactic: induction l with
  | nil => exact stronglyMeasurable_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.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, StronglyMeasurable f
nil :
  ∀ (hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → StronglyMeasurable f),
    StronglyMeasurable.{u_1, u_5} (α := α) (β := M) (List.prod [])
⊢ StronglyMeasurable l.prod
have cons : ∀ (f : α → M) (l : List (α → M)) (ihl : ∀ (hl : ∀ f ∈ l, StronglyMeasurable f), StronglyMeasurable l.prod)
  (hl : ∀ f_1 ∈ f :: l, StronglyMeasurable f_1), StronglyMeasurable (f :: l).prod
Tactic: induction l with
  | nil => exact stronglyMeasurable_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.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
l : Multiset (α → M)
hl : ∀ f ∈ l, StronglyMeasurable f
⊢ StronglyMeasurable 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 →
        StronglyMeasurable f),
  StronglyMeasurable (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.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
n : MeasurableSpace β
ι : Type u_6
f : ι → α → β → M
g : α → β
s : Finset ι
hf : ∀ i ∈ s, StronglyMeasurable ↿(f i)
hg : Measurable g
⊢ StronglyMeasurable.{u_1, u_5} (β := M) fun (a : α) ↦ (∏ i ∈ s, f i a) (g a)
have simp : StronglyMeasurable.{u_1, u_5} (β := M) fun (a : α) ↦ ∏ c ∈ s, f c a (g a)
Tactic: simp only [Finset.prod_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
n : MeasurableSpace β
ι : Type u_6
f : ι → α → β → M
g : α → β
s : Finset ι
hf : ∀ i ∈ s, StronglyMeasurable ↿(f i)
hg : Measurable g
⊢ StronglyMeasurable.{u_1, u_5} (β := M) fun (a : α) ↦ ∏ c ∈ s, f c a (g a)
have funProp : ∀ i ∈ s, i ∈ s
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
hf : StronglyMeasurable f
⊢ IsSeparable (range f)
have this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)))
Tactic: have : IsSeparable (closure (⋃ n, range (hf.approx n))) :=
    .closure <| .iUnion fun n => (hf.approx n).finite_range.isSeparable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
hf : StronglyMeasurable f
this :
  IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)))
⊢ IsSeparable (range f)
have apply : range f ⊆ closure[inst] (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β))
Tactic: apply this.mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
hf : StronglyMeasurable f
this :
  IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)))
x : α
⊢ Membership.mem (γ := Set β) (closure[inst] (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)))
    (f x)
have apply : ∀ᶠ (x_1 : ℕ) in atTop,
  Membership.mem.{u_2, u_2} (α := β) (γ := Set β)
    (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)) ((hf.approx x_1 : (a : α) → β) x : β)
Tactic: apply mem_closure_of_tendsto (hf.tendsto_approx x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
hf : StronglyMeasurable f
this :
  IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)))
x : α
⊢ ∀ᶠ (x_1 : ℕ) in atTop,
    Membership.mem.{u_2, u_2} (α := β) (γ := Set β)
      (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)) ((hf.approx x_1 : (a : α) → β) x : β)
have h : ∀ (n : ℕ),
  Membership.mem.{u_2, u_2} (α := β) (γ := Set β)
    (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)) ((hf.approx n : (a : α) → β) x : β)
Tactic: filter_upwards with n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
hf : StronglyMeasurable f
this :
  IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)))
x : α
n : ℕ
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β)
    (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)) ((hf.approx n : (a : α) → β) x : β)
have h : Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β))
  ((hf.approx n : (a : α) → β) x : β)
Tactic: apply mem_iUnion_of_mem n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : SecondCountableTopology β
inst_4 : OpensMeasurableSpace β
hf : Measurable f
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ 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
f : α → β
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : SecondCountableTopology β
inst_4 : OpensMeasurableSpace β
hf : Measurable f
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
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
f : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
⊢ StronglyMeasurable f ↔ Measurable f ∧ IsSeparable (range f)
have refine : Measurable f ∧ IsSeparable (range f) → ∀ (Hm : Measurable f) (Hsep : IsSeparable (range f)), StronglyMeasurable f
Tactic: refine ⟨fun H ↦ ⟨H.measurable, H.isSeparable_range⟩, fun ⟨Hm, Hsep⟩  ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
h : Measurable f ∧ IsSeparable (range f)
Hm : Measurable f
Hsep : IsSeparable (range f)
⊢ StronglyMeasurable f
have this : SecondCountableTopology.{u_2} (↑(range f) : Type u_2)
Tactic: have := Hsep.secondCountableTopology
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
h : Measurable f ∧ IsSeparable (range f)
Hm : Measurable f
Hsep : IsSeparable (range f)
this : SecondCountableTopology.{u_2} (↑(range f) : Type u_2)
⊢ StronglyMeasurable f
have Hm' : StronglyMeasurable (rangeFactorization f)
Tactic: have Hm' : StronglyMeasurable (rangeFactorization f) := Hm.subtype_mk.stronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst_1, inst_3] f
⊢ StronglyMeasurable f
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
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst_1, inst_3] f
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ StronglyMeasurable f
have inl : SecondCountableTopology α → StronglyMeasurable f
Tactic: cases h.out
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst_1, inst_3] f
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
inl : SecondCountableTopology α → StronglyMeasurable f
⊢ StronglyMeasurable f
have inr : SecondCountableTopology β → StronglyMeasurable f
Tactic: cases h.out
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst_1, inst_3] f
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_1 : SecondCountableTopology α
⊢ StronglyMeasurable f
have inl : Measurable f ∧ IsSeparable (range f)
Tactic: rw [stronglyMeasurable_iff_measurable_separable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
hf : Continuous[inst_1, inst_3] f
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
h_1 : SecondCountableTopology α
⊢ Measurable f ∧ IsSeparable (range f)
have inl : IsSeparable (range f)
Tactic: refine ⟨hf.measurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
inst_5 : One β
f : α → β
hf : Continuous[inst_1, inst_3] f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
⊢ StronglyMeasurable f
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
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : PseudoMetrizableSpace β
inst_5 : One β
f : α → β
hf : Continuous[inst_1, inst_3] f
k : Set α
hk : IsCompact k
h'f : mulSupport f ⊆ k
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ StronglyMeasurable f
have rw : Measurable f ∧ IsSeparable (range f)
Tactic: rw [stronglyMeasurable_iff_measurable_separable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
Goal:
α : Type u_1
X : Type u_5
Y : Type u_6
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
⊢ StronglyMeasurable f
have this : let this := borel α;
BorelSpace α
Tactic: borelize α
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
X : Type u_5
Y : Type u_6
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
⊢ StronglyMeasurable f
have apply : IsSeparable (range f)
Tactic: apply stronglyMeasurable_iff_measurable_separable.2 ⟨h'f.measurable_of_prod hf, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ (StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)) ↔ StronglyMeasurable f
have this₁ : let this := borel β;
BorelSpace β
Tactic: borelize β γ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this₁ :
  let this := borel β;
  BorelSpace β
⊢ (StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)) ↔ StronglyMeasurable f
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_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
⊢ (StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)) ↔ StronglyMeasurable f
have refine_1 : ∀ (H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)), Measurable f
Tactic: refine
    ⟨fun H => stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩, fun H =>
      hg.continuous.comp_stronglyMeasurable H⟩
-- 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 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
refine_1 : ∀ (H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)), Measurable f
⊢ (StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)) ↔ StronglyMeasurable f
have refine_2 : ∀ (H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)), IsSeparable (range f)
Tactic: refine
    ⟨fun H => stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩, fun H =>
      hg.continuous.comp_stronglyMeasurable H⟩
-- 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 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
G : β → (↑(range g) : Type u_3) := rangeFactorization g
⊢ IsClosed[instTopologicalSpaceSubtype] (range G)
have rw : IsClosed[instTopologicalSpaceSubtype] univ
Tactic: rw [rangeFactorization_surjective.range_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
G : β → (↑(range g) : Type u_3) := rangeFactorization g
⊢ Measurable f
have hG : IsClosedEmbedding G
Tactic: have hG : IsClosedEmbedding G :=
      { hg.codRestrict _ _ with
        isClosed_range := by
          rw [rangeFactorization_surjective.range_eq]
          exact isClosed_univ }
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
G : β → (↑(range g) : Type u_3) := rangeFactorization g
hG : IsClosedEmbedding G
⊢ Measurable f
have this₁ : Measurable (G ∘ f)
Tactic: have : Measurable (G ∘ f) := Measurable.subtype_mk H.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
⊢ IsSeparable (range f)
have this₁ : IsSeparable (g ⁻¹' range (g ∘ f))
Tactic: have : IsSeparable (g ⁻¹' range (g ∘ f)) := hg.isSeparable_preimage H.isSeparable_range