awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
s : Set β
hs : s ∈ 𝓝 (f x)
pos :
  ∀ (n₂ : ℕ) (hn₂ : ∀ b ≥ n₂, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)),
    ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((fs b : (a : α) → β) x : β)
⊢ ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((fs b : (a : α) → β) x : β)

Tactic:
obtain ⟨n₂, hn₂⟩ := h s hs
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ b ≥ n₂, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
⊢ ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((fs b : (a : α) → β) x : β)

Tactic:
⟨max n₁ n₂, fun m hm => ?_⟩

Premises used: Max.max, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → Eq.{u_2 + 1} (α := β) ((fs m_1 : (a : α) → β) x : β) ((f_approx m_1 : (a : α) → β) x : β)
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ b ≥ n₂, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
pos : ∀ (m_1 : ℕ) (hm : m_1 ≥ max n₁ n₂), Membership.mem (α := β) s ((fs m_1 : (a : α) → β) x : β)
⊢ ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((fs b : (a : α) → β) x : β)

Tactic:
refine ⟨max n₁ n₂, fun m hm => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m_1 : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
n₁ : ℕ
hn₁ : ∀ (m : ℕ), n₁ ≤ m → Eq.{u_2 + 1} (α := β) ((fs m : (a : α) → β) x : β) ((f_approx m : (a : α) → β) x : β)
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ b ≥ n₂, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
m : ℕ
hm : m ≥ max n₁ n₂
pos : Membership.mem (α := β) s ((f_approx m : (a : α) → β) x : β)
⊢ Membership.mem (α := β) s ((fs m : (a : α) → β) x : β)

Tactic:
rw [hn₁ m ((le_max_left _ _).trans hm.le)]

Premises used: LE.le.trans, le_max_left, GE.ge.le
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m_1 : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
n₁ : ℕ
hn₁ : ∀ (m : ℕ), n₁ ≤ m → Eq.{u_2 + 1} (α := β) ((fs m : (a : α) → β) x : β) ((f_approx m : (a : α) → β) x : β)
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ b ≥ n₂, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
m : ℕ
hm : m ≥ max n₁ n₂
⊢ Membership.mem (α := β) s ((f_approx m : (a : α) → β) x : β)

Tactic:
hn₂ m ((le_max_right _ _).trans hm.le)

Premises used: le_max_right, LE.le.trans, GE.ge.le
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m_1 : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : (i : ℕ) → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : (n : ℕ) → α →ₛ β := fun (n : ℕ) ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, Eq.{u_2 + 1} (α := β) ((fs n : (a : α) → β) x : β) (0 : β)
x : α
hxt : x ∈ t
h : ∀ s ∈ 𝓝 (f x), ∃ (a : ℕ), ∀ b ≥ a, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
n₁ : ℕ
hn₁ : ∀ (m : ℕ), n₁ ≤ m → Eq.{u_2 + 1} (α := β) ((fs m : (a : α) → β) x : β) ((f_approx m : (a : α) → β) x : β)
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ b ≥ n₂, Membership.mem (α := β) s ((f_approx b : (a : α) → β) x : β)
m : ℕ
hm : m ≥ max n₁ n₂
⊢ Membership.mem (α := β) s ((f_approx m : (a : α) → β) x : β)

Tactic:
exact hn₂ m ((le_max_right _ _).trans hm.le)

Premises used: le_max_right, LE.le.trans, GE.ge.le
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m0 : MeasurableSpace α
hf : StronglyMeasurable f
μ : Measure α
inst_2 : SigmaFinite μ
⊢ ∀ (x : α), Membership.mem (γ := Set α) univᶜ x → f x = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Zero β
m0 : MeasurableSpace α
hf : StronglyMeasurable f
μ : Measure α
inst_2 rwa rwa₁ rwa₂ rwa₃ : SigmaFinite μ
⊢ SigmaFinite (μ.restrict univ)

Tactic:
rwa [Measure.restrict_univ]

Premises used: MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
hf : StronglyMeasurable f
⊢ Measurable f

Tactic:
measurable_of_tendsto_metrizable (fun n => (hf.approx n).measurable)
    (tendsto_pi_nhds.mpr hf.tendsto_approx)

Premises used: Iff.mpr, MeasureTheory.StronglyMeasurable.approx, MeasureTheory.SimpleFunc.measurable, tendsto_pi_nhds, MeasureTheory.StronglyMeasurable.tendsto_approx, measurable_of_tendsto_metrizable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
μ : Measure α
hf : StronglyMeasurable f
⊢ AEMeasurable f μ

Tactic:
hf.measurable.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.StronglyMeasurable.measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
g : β → γ
f : α → β
hg : Continuous[inst, inst_1] g
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)

Tactic:
⟨fun n => SimpleFunc.map g (hf.approx n), fun x => (hg.tendsto _).comp (hf.tendsto_approx x)⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, Continuous.tendsto, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable, Filter.Tendsto.comp, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : One β
inst_1 : TopologicalSpace β
inst_2 : MetrizableSpace β
hf : StronglyMeasurable f
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : One β
inst_1 : TopologicalSpace β
inst_2 : MetrizableSpace β
hf : StronglyMeasurable f
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ MeasurableSet (mulSupport f)

Tactic:
measurableSet_mulSupport hf.measurable

Premises used: measurableSet_mulSupport, MeasureTheory.StronglyMeasurable.measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst : One β
inst_1 : TopologicalSpace β
inst_2 : MetrizableSpace β
hf : StronglyMeasurable f
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ MeasurableSet (mulSupport f)

Tactic:
exact measurableSet_mulSupport hf.measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
m m' : MeasurableSpace α
inst : TopologicalSpace β
hf : StronglyMeasurable f
h_mono : m' ≤ m
f_approx : ℕ → α →ₛ β :=
  fun (n : ℕ) ↦ { toFun := (⇑(hf.approx n) : (a : α) → β), measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

Tactic:
⟨f_approx, hf.tendsto_approx⟩

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
m m' : MeasurableSpace α
inst : TopologicalSpace β
hf : StronglyMeasurable f
h_mono : m' ≤ m
f_approx : ℕ → α →ₛ β :=
  fun (n : ℕ) ↦ { toFun := (⇑(hf.approx n) : (a : α) → β), measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

Tactic:
exact ⟨f_approx, hf.tendsto_approx⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
f : α → β × γ
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ (f x).1

Tactic:
continuous_fst.comp_stronglyMeasurable hf

Premises used: continuous_fst, Continuous.comp_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
f : α → β × γ
hf : StronglyMeasurable f
⊢ StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ (f x).2

Tactic:
continuous_snd.comp_stronglyMeasurable hf

Premises used: continuous_snd, Continuous.comp_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (β := β × γ) fun (x : α) ↦ (f x, g x)

Tactic:
⟨fun n => SimpleFunc.pair (hf.approx n) (hg.approx n), fun x => ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, Exists.intro, MeasureTheory.StronglyMeasurable, MeasureTheory.SimpleFunc.pair
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
refine :
  ∀ (x : α),
    Tendsto (β := β × γ) (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).pair (hg.approx n)) n : (a : α) → β × γ) x) atTop
      (𝓝 ((fun (x : α) ↦ (f x, g x)) x))
⊢ StronglyMeasurable (β := β × γ) fun (x : α) ↦ (f x, g x)

Tactic:
refine ⟨fun n => SimpleFunc.pair (hf.approx n) (hg.approx n), fun x => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
rw :
  Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).pair (hg.approx n)) n : (a : α) → β × γ) x) atTop
    (𝓝 (f x) ×ˢ 𝓝 (g x))
⊢ Tendsto (β := β × γ) (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).pair (hg.approx n)) n : (a : α) → β × γ) x) atTop
    (𝓝 ((fun (x : α) ↦ (f x, g x)) x))

Tactic:
rw [nhds_prod_eq]

Premises used: nhds_prod_eq
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).pair (hg.approx n)) n : (a : α) → β × γ) x) atTop
    (𝓝 (f x) ×ˢ 𝓝 (g x))

Tactic:
Tendsto.prodMk (hf.tendsto_approx x) (hg.tendsto_approx x)

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx, Filter.Tendsto.prodMk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ (hf.approx n).pair (hg.approx n)) n : (a : α) → β × γ) x) atTop
    (𝓝 (f x) ×ˢ 𝓝 (g x))

Tactic:
exact Tendsto.prodMk (hf.tendsto_approx x) (hg.tendsto_approx x)

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approx, Filter.Tendsto.prodMk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
x : MeasurableSpace α
x_1 : MeasurableSpace γ
f : α → β
g : γ → α
hf : StronglyMeasurable f
hg : Measurable g
⊢ StronglyMeasurable (f ∘ g)

Tactic:
⟨fun n => SimpleFunc.comp (hf.approx n) g hg, fun x => hf.tendsto_approx (g x)⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable, MeasureTheory.SimpleFunc.comp
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
x_1 : MeasurableSpace α
x_2 : MeasurableSpace γ
f : α → γ → β
hf : StronglyMeasurable (uncurry f)
x : α
⊢ StronglyMeasurable (f x)

Tactic:
hf.comp_measurable measurable_prodMk_left

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
x : MeasurableSpace α
x_1 : MeasurableSpace γ
f : α → γ → β
hf : StronglyMeasurable (uncurry f)
y : γ
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ f x y

Tactic:
hf.comp_measurable measurable_prodMk_right

Premises used: measurable_prodMk_right, MeasureTheory.StronglyMeasurable.comp_measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : MeasurableSpace α
x_1 : MeasurableSpace β
inst : TopologicalSpace γ
f : β × α → γ
hf : StronglyMeasurable f
⊢ StronglyMeasurable (β := γ) fun (z : α × β) ↦ f z.swap

Tactic:
hf.comp_measurable measurable_swap

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable, measurable_swap
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
x : MeasurableSpace α
mβ : MeasurableSpace β
inst : TopologicalSpace γ
f : α → γ
hf : StronglyMeasurable f
⊢ StronglyMeasurable (β := γ) fun (z : α × β) ↦ f z.1

Tactic:
hf.comp_measurable measurable_fst

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable, measurable_fst
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
x : MeasurableSpace β
inst : TopologicalSpace γ
f : β → γ
hf : StronglyMeasurable f
⊢ StronglyMeasurable (β := γ) fun (z : α × β) ↦ f z.2

Tactic:
hf.comp_measurable measurable_snd

Premises used: MeasureTheory.StronglyMeasurable.comp_measurable, measurable_snd
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Mul β
inst_2 : ContinuousMul β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (f * g)

Tactic:
⟨fun n => hf.approx n * hg.approx n, fun x => (hf.tendsto_approx x).mul (hg.tendsto_approx x)⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, HMul.hMul, Filter.Tendsto.mul, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Mul β
inst_2 : ContinuousMul β
hf : StronglyMeasurable f
c : β
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ f x * c

Tactic:
hf.mul stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.mul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Mul β
inst_2 : ContinuousMul β
hf : StronglyMeasurable f
c : β
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ c * f x

Tactic:
stronglyMeasurable_const.mul hf

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.mul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Monoid β
inst_2 : ContinuousMul β
hf : StronglyMeasurable f
n : ℕ
⊢ StronglyMeasurable (f ^ n)

Tactic:
⟨fun k => hf.approx k ^ n, fun x => (hf.tendsto_approx x).pow n⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, Filter.Tendsto.pow, HPow.hPow, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Inv β
inst_2 : ContinuousInv β
hf : StronglyMeasurable f
⊢ StronglyMeasurable f⁻¹

Tactic:
⟨fun n => (hf.approx n)⁻¹, fun x => (hf.tendsto_approx x).inv⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, Filter.Tendsto.inv, Inv.inv, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : Div β
inst_2 : ContinuousDiv β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (f / g)

Tactic:
⟨fun n => hf.approx n / hg.approx n, fun x => (hf.tendsto_approx x).div' (hg.tendsto_approx x)⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, HDiv.hDiv, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable, Filter.Tendsto.div'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
h₀ : ∀ (x : α), g x ≠ 0
⊢ StronglyMeasurable (f / g)

Tactic:
⟨fun n => hf.approx n / hg.approx n,
    fun x => (hf.tendsto_approx x).div (hg.tendsto_approx x) (h₀ x)⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, HDiv.hDiv, Filter.Tendsto.div, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
inst_4 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSingletonClass β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (f / g)

Tactic:
⟨fun n => hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}, fun x => ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, setOf, HDiv.hDiv, Ne, MeasureTheory.SimpleFunc.restrict, Exists.intro, MeasureTheory.StronglyMeasurable, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
inst_4 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSingletonClass β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
refine :
  ∀ (x : α),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
      atTop (𝓝 ((f / g) x))
⊢ StronglyMeasurable (f / g)

Tactic:
refine ⟨fun n => hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}, fun x => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
inst_4 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSingletonClass β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ MeasurableSet.{u_1} (α := α) {x : α | g x ≠ 0}

Tactic:
have : MeasurableSet {x | g x ≠ 0} := ((MeasurableSet.singleton 0).preimage hg.measurable).compl
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : GroupWithZero β
inst_2 : ContinuousMul β
inst_3 : ContinuousInv₀ β
inst_4 : PseudoMetrizableSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
inst_7 : MeasurableSingletonClass β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
this : MeasurableSet.{u_1} (α := α) {x : α | g x ≠ 0}
pos :
  ∀ (h : g x = 0),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
      atTop (𝓝 ((f / g) x))
neg :
  ∀ (h : ¬g x = 0),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
      atTop (𝓝 ((f / g) x))
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
    atTop (𝓝 ((f / g) x))

Tactic:
by_cases h : g x = 0