awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
h : g x = 0
pos :
  ∀ (this : MeasurableSet.{u_1} (α := α) {x : α | ¬g x = 0}) (h : g x = 0),
    Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ hf.approx n / (hg.approx n).restrict {x : α | g x ≠ 0}) n : (a : α) → β) x)
    atTop (𝓝 ((f / g) x))

Tactic:
simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict, Pi.div_apply, mem_setOf_eq,
      not_true_eq_false, not_false_eq_true, indicator_of_notMem, _root_.div_zero]

Premises used: not_true_eq_false, Set.mem_setOf_eq, ne_eq, Pi.div_apply, MeasureTheory.SimpleFunc.coe_restrict, MeasureTheory.SimpleFunc.coe_div, Set.indicator_of_notMem, not_false_eq_true, div_zero
-- 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}
h : g x = 0
⊢ Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- 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}
h : g x = 0
⊢ Tendsto.{0, u_2} (β := β) (fun (n : ℕ) ↦ 0) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- 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}
h : ¬g x = 0
neg :
  ∀ (this : MeasurableSet.{u_1} (α := α) {x : α | ¬g x = 0}) (h : ¬g x = 0),
    Tendsto
      (fun (n : ℕ) ↦
        HDiv.hDiv (α := β) (β := β) ((hf.approx n : (a : α) → β) x : β) ((hg.approx n : (a : α) → β) x : β))
      atTop (𝓝 (f x / 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:
simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict,
      Pi.div_apply, mem_setOf_eq, not_false_eq_true, indicator_of_mem]

Premises used: Set.mem_setOf_eq, ne_eq, Pi.div_apply, Set.indicator_of_mem, MeasureTheory.SimpleFunc.coe_restrict, MeasureTheory.SimpleFunc.coe_div, not_false_eq_true
-- 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}
h : ¬g x = 0
⊢ Tendsto
    (fun (n : ℕ) ↦ HDiv.hDiv (α := β) (β := β) ((hf.approx n : (a : α) → β) x : β) ((hg.approx n : (a : α) → β) x : β))
    atTop (𝓝 (f x / g x))

Tactic:
(hf.tendsto_approx x).div (hg.tendsto_approx x) h

Premises used: Filter.Tendsto.div, MeasureTheory.StronglyMeasurable.tendsto_approx
-- 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}
h : ¬g x = 0
⊢ Tendsto
    (fun (n : ℕ) ↦ HDiv.hDiv (α := β) (β := β) ((hf.approx n : (a : α) → β) x : β) ((hg.approx n : (a : α) → β) x : β))
    atTop (𝓝 (f x / g x))

Tactic:
exact (hf.tendsto_approx x).div (hg.tendsto_approx x) h

Premises used: Filter.Tendsto.div, MeasureTheory.StronglyMeasurable.tendsto_approx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : CommGroup β
inst_2 : IsTopologicalGroup β
hf : StronglyMeasurable f
h : StronglyMeasurable (f * g)
⊢ g = f * g * f⁻¹

Tactic:
simp only [mul_inv_cancel_comm]

Premises used: mul_inv_cancel_comm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : CommGroup β
inst_2 : IsTopologicalGroup β
hf : StronglyMeasurable f
⊢ StronglyMeasurable (g * f) ↔ StronglyMeasurable g

Tactic:
mul_comm g f ▸ mul_iff_right hf

Premises used: MeasureTheory.StronglyMeasurable.mul_iff_right, Eq.rec, mul_comm, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace β
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : SMul 𝕜 β
inst_3 : ContinuousSMul 𝕜 β
f : α → 𝕜
g : α → β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ f x • g x

Tactic:
continuous_smul.comp_stronglyMeasurable (hf.prodMk hg)

Premises used: Continuous.comp_stronglyMeasurable, MeasureTheory.StronglyMeasurable.prodMk, ContinuousSMul.continuous_smul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
𝕜 : Type u_5
inst_1 : SMul 𝕜 β
inst_2 : ContinuousConstSMul 𝕜 β
hf : StronglyMeasurable f
c : 𝕜
⊢ StronglyMeasurable (c • f)

Tactic:
⟨fun n => c • hf.approx n, fun x => (hf.tendsto_approx x).const_smul c⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, Filter.Tendsto.const_smul, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, HSMul.hSMul, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
inst : TopologicalSpace β
𝕜 : Type u_5
inst_1 : SMul 𝕜 β
inst_2 : ContinuousConstSMul 𝕜 β
hf : StronglyMeasurable f
c : 𝕜
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ c • f x

Tactic:
hf.const_smul c

Premises used: MeasureTheory.StronglyMeasurable.const_smul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
inst : TopologicalSpace β
𝕜 : Type u_5
inst_1 : TopologicalSpace 𝕜
inst_2 : SMul 𝕜 β
inst_3 : ContinuousSMul 𝕜 β
f : α → 𝕜
hf : StronglyMeasurable f
c : β
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ f x • c

Tactic:
continuous_smul.comp_stronglyMeasurable (hf.prodMk stronglyMeasurable_const)

Premises used: MeasureTheory.stronglyMeasurable_const, Continuous.comp_stronglyMeasurable, MeasureTheory.StronglyMeasurable.prodMk, ContinuousSMul.continuous_smul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
R : Type u_5
inst : MeasurableSpace α
inst_1 : Star R
inst_2 : TopologicalSpace R
inst_3 : ContinuousStar R
f : α → R
hf : StronglyMeasurable f
⊢ StronglyMeasurable (star f)

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

Premises used: MeasureTheory.StronglyMeasurable.approx, Filter.Tendsto.star, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable, Star.star
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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
rcases :
  ∀ (φ : ℕ → α →ₛ E) (hφ : ∀ (x_1 : α), Tendsto (fun (n : ℕ) ↦ (φ n : (a : α) → E) x_1) atTop (𝓝 (f x_1))),
    Measurable (g + f)
⊢ Measurable (g + f)

Tactic:
rcases hf with ⟨φ, hφ⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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))
⊢ Tendsto (fun (n : ℕ) (x_1 : α) ↦ HAdd.hAdd (β := E) (g x_1) ((φ n : (a : α) → E) x_1 : E)) atTop (𝓝 (g + f))

Tactic:
have : Tendsto (fun n x ↦ g x + φ n x) atTop (𝓝 (g + f)) :=
    tendsto_pi_nhds.2 (fun x ↦ tendsto_const_nhds.add (hφ x))
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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))
apply :
  ∀ (n : ℕ), Measurable.{u_5, u_6} (β := E) fun (x_1 : α) ↦ HAdd.hAdd (β := E) (g x_1) ((φ n : (a : α) → E) x_1 : E)
⊢ Measurable (g + f)

Tactic:
apply measurable_of_tendsto_metrizable (fun n ↦ ?_) this

Premises used: measurable_of_tendsto_metrizable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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))
n : ℕ
⊢ Measurable.{u_5, u_6} (β := E) fun (x_1 : α) ↦ HAdd.hAdd (β := E) (g x_1) ((φ n : (a : α) → E) x_1 : E)

Tactic:
hg.add_simpleFunc _

Premises used: Measurable.add_simpleFunc
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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))
n : ℕ
⊢ Measurable.{u_5, u_6} (β := E) fun (x_1 : α) ↦ HAdd.hAdd (β := E) (g x_1) ((φ n : (a : α) → E) x_1 : E)

Tactic:
exact hg.add_simpleFunc _

Premises used: Measurable.add_simpleFunc
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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
rw : Measurable (g + -f)
⊢ Measurable (g - f)

Tactic:
rw [sub_eq_add_neg]

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

Tactic:
hg.add_stronglyMeasurable hf.neg

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

Tactic:
exact hg.add_stronglyMeasurable hf.neg

Premises used: MeasureTheory.StronglyMeasurable.neg, Measurable.add_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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
rcases :
  ∀ (φ : ℕ → α →ₛ E) (hφ : ∀ (x_1 : α), Tendsto (fun (n : ℕ) ↦ (φ n : (a : α) → E) x_1) atTop (𝓝 (f x_1))),
    Measurable (f + g)
⊢ Measurable (f + g)

Tactic:
rcases hf with ⟨φ, hφ⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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))
⊢ 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)
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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))
apply :
  ∀ (n : ℕ), Measurable.{u_5, u_6} (β := E) fun (x_1 : α) ↦ HAdd.hAdd (α := E) ((φ n : (a : α) → E) x_1 : E) (g x_1)
⊢ Measurable (f + g)

Tactic:
apply measurable_of_tendsto_metrizable (fun n ↦ ?_) this

Premises used: measurable_of_tendsto_metrizable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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))
n : ℕ
⊢ Measurable.{u_5, u_6} (β := E) fun (x_1 : α) ↦ HAdd.hAdd (α := E) ((φ n : (a : α) → E) x_1 : E) (g x_1)

Tactic:
hg.simpleFunc_add _

Premises used: Measurable.simpleFunc_add
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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))
n : ℕ
⊢ Measurable.{u_5, u_6} (β := E) fun (x_1 : α) ↦ HAdd.hAdd (α := E) ((φ n : (a : α) → E) x_1 : E) (g x_1)

Tactic:
exact hg.simpleFunc_add _

Premises used: Measurable.simpleFunc_add
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
G : Type u_6
inst : TopologicalSpace β
inst_1 : Group G
inst_2 : MulAction G β
inst_3 : ContinuousConstSMul G β
m : MeasurableSpace α
c : G
h : StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ c • f x
⊢ StronglyMeasurable f

Tactic:
simpa only [inv_smul_smul] using h.const_smul' c⁻¹

Premises used: inv_smul_smul, Inv.inv, MeasureTheory.StronglyMeasurable.const_smul'
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
M : Type u_5
inst : TopologicalSpace β
inst_1 : Monoid M
inst_2 : MulAction M β
inst_3 : ContinuousConstSMul M β
x : MeasurableSpace α
c : M
hc : IsUnit c
⊢ (StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ c • f x) ↔ StronglyMeasurable f

Tactic:
let ⟨u, hu⟩ := hc
  hu ▸ stronglyMeasurable_const_smul_iff u

Premises used: Eq.rec, stronglyMeasurable_const_smul_iff, Iff, HSMul.hSMul, MeasureTheory.StronglyMeasurable, _private.0.IsUnit.stronglyMeasurable_const_smul_iff.match_1
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
G₀ : Type u_7
inst : TopologicalSpace β
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ β
inst_3 : ContinuousConstSMul G₀ β
x : MeasurableSpace α
c : G₀
hc : c ≠ 0
⊢ (StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ c • f x) ↔ StronglyMeasurable f

Tactic:
(IsUnit.mk0 _ hc).stronglyMeasurable_const_smul_iff

Premises used: IsUnit.stronglyMeasurable_const_smul_iff, IsUnit.mk0
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : Max β
inst_3 : ContinuousSup β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (f ⊔ g)

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

Premises used: MeasureTheory.StronglyMeasurable.approx, Filter.Tendsto.sup_nhds, Max.max, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : Min β
inst_3 : ContinuousInf β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (f ⊓ g)

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

Premises used: MeasureTheory.StronglyMeasurable.approx, Filter.Tendsto.inf_nhds, MeasureTheory.StronglyMeasurable.tendsto_approx, Exists.intro, MeasureTheory.StronglyMeasurable, Min.min
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → StronglyMeasurable f
⊢ StronglyMeasurable.{u_1, u_5} (α := α) (β := M) (List.prod [])

Tactic:
stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one, List.foldr, List.prod
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
M : Type u_5
inst : Monoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
m : MeasurableSpace α
hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → StronglyMeasurable f
⊢ StronglyMeasurable.{u_1, u_5} (α := α) (β := M) (List.prod [])

Tactic:
exact stronglyMeasurable_one

Premises used: MeasureTheory.stronglyMeasurable_one
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 ∧ ∀ x ∈ l, StronglyMeasurable x

Tactic:
rw [List.forall_mem_cons] at hl

Premises used: List.forall_mem_cons
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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
cons : StronglyMeasurable (f * l.prod)
⊢ StronglyMeasurable (f :: l).prod

Tactic:
rw [List.prod_cons]

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

Tactic:
hl.1.mul (ihl hl.2)

Premises used: MeasureTheory.StronglyMeasurable.mul, And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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)

Tactic:
exact hl.1.mul (ihl hl.2)

Premises used: MeasureTheory.StronglyMeasurable.mul, And.right, And.left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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 [])
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
⊢ StronglyMeasurable 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)

Premises used: MeasureTheory.stronglyMeasurable_one, List.forall_mem_cons, List.prod_cons
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
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.{u_1, u_5} (β := M) fun (x : α) ↦ List.prod (List.map (fun (f : α → M) ↦ f x) l)

Tactic:
simpa only [← Pi.list_prod_apply] using l.stronglyMeasurable_prod hl

Premises used: List.stronglyMeasurable_prod, Pi.list_prod_apply
-- 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 : Multiset (α → M)
hl : ∀ f ∈ l, StronglyMeasurable f
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))
⊢ StronglyMeasurable l.prod

Tactic:
rcases l with ⟨l⟩