awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
l_1 : Multiset (α → M)
l : List (α → M)
hl :
  ∀ (f : α → M),
    Membership.mem (γ := Multiset (α → M)) (Quot.mk (⇑(List.isSetoid (α → M)) : List (α → M) → List (α → M) → Prop) l)
        f →
      StronglyMeasurable f
⊢ ∀ f ∈ l, StronglyMeasurable f

Tactic:
simpa using hl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
l_1 : Multiset (α → M)
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:
simpa using l.stronglyMeasurable_prod (by simpa using hl)

Premises used: List.stronglyMeasurable_prod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
s : Multiset (α → M)
hs : ∀ f ∈ s, StronglyMeasurable f
⊢ StronglyMeasurable.{u_1, u_5} (β := M) fun (x : α) ↦ Multiset.prod (Multiset.map (fun (f : α → M) ↦ f x) s)

Tactic:
simpa only [← Pi.multiset_prod_apply] using s.stronglyMeasurable_prod hs

Premises used: Pi.multiset_prod_apply, Multiset.stronglyMeasurable_prod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
ι : Type u_6
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, StronglyMeasurable (f i)
⊢ StronglyMeasurable.{u_1, u_5} (α := α) (β := M) (∏ i ∈ s, f i)

Tactic:
Finset.prod_induction _ _ (fun _a _b ha hb => ha.mul hb) (@stronglyMeasurable_one α M _ _ _) hf

Premises used: MeasureTheory.stronglyMeasurable_one, Finset.prod_induction, MeasureTheory.StronglyMeasurable.mul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
M : Type u_5
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
ι : Type u_6
f : ι → α → M
s : Finset ι
hf : ∀ i ∈ s, StronglyMeasurable (f i)
⊢ StronglyMeasurable.{u_1, u_5} (β := M) fun (a : α) ↦ ∏ i ∈ s, f i a

Tactic:
simpa only [← Finset.prod_apply] using s.stronglyMeasurable_prod hf

Premises used: Finset.stronglyMeasurable_prod, Finset.prod_apply
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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
simp : StronglyMeasurable.{u_1, u_5} (β := M) fun (a : α) ↦ ∏ c ∈ s, f c a (g a)
⊢ StronglyMeasurable.{u_1, u_5} (β := M) fun (a : α) ↦ (∏ i ∈ s, f i a) (g a)

Tactic:
simp only [Finset.prod_apply]

Premises used: Finset.prod_apply
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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
funProp : ∀ i ∈ s, i ∈ s
⊢ StronglyMeasurable.{u_1, u_5} (β := M) fun (a : α) ↦ ∏ c ∈ s, f c a (g a)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
hf : StronglyMeasurable f
⊢ 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
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 : α) → β)))
apply : range f ⊆ closure[inst] (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β))
⊢ IsSeparable (range f)

Tactic:
apply this.mono

Premises used: TopologicalSpace.IsSeparable.mono
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 : α
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 : β)
⊢ Membership.mem (γ := Set β) (closure[inst] (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)))
    (f x)

Tactic:
apply mem_closure_of_tendsto (hf.tendsto_approx x)

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx, mem_closure_of_tendsto
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 : α
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 : β)
⊢ ∀ᶠ (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:
filter_upwards with n
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 : ℕ
h :
  Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β))
    ((hf.approx n : (a : α) → β) x : β)
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β)
    (⋃ (n : ℕ), range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β)) ((hf.approx n : (a : α) → β) x : β)

Tactic:
apply mem_iUnion_of_mem n

Premises used: Set.mem_iUnion_of_mem
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 β) (range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β))
    ((hf.approx n : (a : α) → β) x : β)

Tactic:
mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 β) (range.{u_2, u_1 + 1} (ι := α) (⇑(hf.approx n) : (a : α) → β))
    ((hf.approx n : (a : α) → β) x : β)

Tactic:
exact mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
hf : StronglyMeasurable f
b : β
⊢ SeparableSpace.{u_2} (↑(range f ∪ {b}) : Type u_2)

Tactic:
letI := pseudoMetrizableSpacePseudoMetric β
  (hf.isSeparable_range.union (finite_singleton _).isSeparable).separableSpace

Premises used: MeasureTheory.StronglyMeasurable.isSeparable_range, Set.Finite.isSeparable, TopologicalSpace.IsSeparable.separableSpace, Set.finite_singleton, TopologicalSpace.IsSeparable.union
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 β
⊢ Nontrivial β

Tactic:
nontriviality β
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 β
inhabit : ∀ (inhabited_h : Inhabited β), StronglyMeasurable f
⊢ StronglyMeasurable f

Tactic:
inhabit β
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 β
inhabited_h : Inhabited β
x : α
⊢ Membership.mem (γ := Set β) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] univ) (f x)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 β
inhabited_h : Inhabited β
⊢ StronglyMeasurable f

Tactic:
exact ⟨SimpleFunc.approxOn f hf Set.univ default (Set.mem_univ _), fun x ↦
    SimpleFunc.tendsto_approxOn hf (Set.mem_univ _) (by simp)⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst : MeasurableSpace β
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : BorelSpace β
inst_4 : SecondCountableTopology β
⊢ StronglyMeasurable f ↔ Measurable f

Tactic:
⟨fun h => h.measurable, fun h => Measurable.stronglyMeasurable h⟩

Premises used: Measurable.stronglyMeasurable, MeasureTheory.StronglyMeasurable.measurable, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
inst : TopologicalSpace α
inst_1 : PseudoMetrizableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : SecondCountableTopology α
⊢ StronglyMeasurable.{u_1, u_1} (α := α) id

Tactic:
measurable_id.stronglyMeasurable

Premises used: measurable_id, Measurable.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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)

Tactic:
⟨fun H ↦ ⟨H.measurable, H.isSeparable_range⟩, fun ⟨Hm, Hsep⟩  ↦ ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.isSeparable_range, MeasureTheory.StronglyMeasurable.measurable, _private.0.stronglyMeasurable_iff_measurable_separable.match_1, And.intro, Iff.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
refine :
  Measurable f ∧ IsSeparable (range f) → ∀ (Hm : Measurable f) (Hsep : IsSeparable (range f)), StronglyMeasurable f
⊢ StronglyMeasurable f ↔ Measurable f ∧ IsSeparable (range f)

Tactic:
refine ⟨fun H ↦ ⟨H.measurable, H.isSeparable_range⟩, fun ⟨Hm, Hsep⟩  ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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)
⊢ SecondCountableTopology.{u_2} (↑(range f) : Type u_2)

Tactic:
have := Hsep.secondCountableTopology
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 (rangeFactorization f)

Tactic:
have Hm' : StronglyMeasurable (rangeFactorization f) := Hm.subtype_mk.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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)
Hm' : StronglyMeasurable (rangeFactorization f)
⊢ StronglyMeasurable f

Tactic:
continuous_subtype_val.comp_stronglyMeasurable Hm'

Premises used: continuous_subtype_val, Continuous.comp_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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)
Hm' : StronglyMeasurable (rangeFactorization f)
⊢ StronglyMeasurable f

Tactic:
exact continuous_subtype_val.comp_stronglyMeasurable Hm'

Premises used: continuous_subtype_val, Continuous.comp_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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
inr : SecondCountableTopology β → StronglyMeasurable f
⊢ StronglyMeasurable f

Tactic:
cases h.out

Premises used: SecondCountableTopologyEither.out
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 α
inl : Measurable f ∧ IsSeparable (range f)
⊢ StronglyMeasurable f

Tactic:
rw [stronglyMeasurable_iff_measurable_separable]

Premises used: stronglyMeasurable_iff_measurable_separable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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)

Tactic:
⟨hf.measurable, ?_⟩

Premises used: And.intro, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 α
inl : IsSeparable (range f)
⊢ Measurable f ∧ IsSeparable (range f)

Tactic:
refine ⟨hf.measurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 α
⊢ IsSeparable (range f)

Tactic:
isSeparable_range hf

Premises used: TopologicalSpace.isSeparable_range
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 α
⊢ IsSeparable (range f)

Tactic:
exact isSeparable_range hf

Premises used: TopologicalSpace.isSeparable_range
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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

Tactic:
hf.measurable.stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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

Tactic:
exact hf.measurable.stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 β
rw : Measurable f ∧ IsSeparable (range f)
⊢ StronglyMeasurable f

Tactic:
rw [stronglyMeasurable_iff_measurable_separable]

Premises used: stronglyMeasurable_iff_measurable_separable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 β
⊢ Measurable f ∧ IsSeparable (range f)

Tactic:
⟨hf.measurable, (isCompact_range_of_mulSupport_subset_isCompact hf hk h'f).isSeparable⟩

Premises used: IsCompact.isSeparable, And.intro, Continuous.measurable, isCompact_range_of_mulSupport_subset_isCompact
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 β
⊢ Measurable f ∧ IsSeparable (range f)

Tactic:
exact ⟨hf.measurable, (isCompact_range_of_mulSupport_subset_isCompact hf hk h'f).isSeparable⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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
h'f : HasCompactMulSupport f
⊢ StronglyMeasurable f

Tactic:
hf.stronglyMeasurable_of_mulSupport_subset_isCompact h'f (subset_mulTSupport f)

Premises used: subset_mulTSupport, Continuous.stronglyMeasurable_of_mulSupport_subset_isCompact
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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
⊢ let this := borel α;
  BorelSpace α

Tactic:
borelize α
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 α
apply : IsSeparable (range f)
⊢ StronglyMeasurable f

Tactic:
apply stronglyMeasurable_iff_measurable_separable.2 ⟨h'f.measurable_of_prod hf, ?_⟩

Premises used: Iff.mpr, HasCompactSupport.measurable_of_prod, stronglyMeasurable_iff_measurable_separable, And.intro