awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace β
f : α → β
inst_1 : Zero β
inst_2 : T2Space β
hf : AEFinStronglyMeasurable f μ
⊢ f =ᶠ[ae (μ.restrict hf.sigmaFiniteSetᶜ)] 0

Tactic:
hf.exists_set_sigmaFinite.choose_spec.2.1

Premises used: Exists.choose_spec, Set.Mem, setOf, MeasureTheory.AEFinStronglyMeasurable.sigmaFiniteSet, And.right, And.left, MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : Countable ι
m : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace β
f g : α → β
inst_2 : Zero β
inst_3 : T2Space β
hf : AEFinStronglyMeasurable f μ
⊢ SigmaFinite (μ.restrict hf.sigmaFiniteSet)

Tactic:
hf.exists_set_sigmaFinite.choose_spec.2.2

Premises used: Exists.choose_spec, MeasureTheory.AEFinStronglyMeasurable.sigmaFiniteSet, And.right, MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
G : Type u_5
inst : SeminormedAddCommGroup G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : SecondCountableTopology G
f : α → G
_m0 : MeasurableSpace α
μ : Measure α
inst_4 : SigmaFinite μ
simp_rw : (∃ (g : α → G), FinStronglyMeasurable g μ ∧ f =ᶠ[ae μ] g) ↔ AEMeasurable f μ
simp_rw₁ : (∃ (g : α → G), FinStronglyMeasurable g μ ∧ f =ᶠ[ae μ] g) ↔ ∃ (g : α → G), Measurable g ∧ f =ᶠ[ae μ] g
⊢ AEFinStronglyMeasurable f μ ↔ AEMeasurable f μ

Tactic:
simp_rw [AEFinStronglyMeasurable, AEMeasurable, finStronglyMeasurable_iff_measurable]

Premises used: AEMeasurable, MeasureTheory.AEFinStronglyMeasurable, MeasureTheory.finStronglyMeasurable_iff_measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
G : Type u_5
inst : SeminormedAddCommGroup G
inst_1 : MeasurableSpace G
inst_2 : BorelSpace G
inst_3 : SecondCountableTopology G
f : α → G
_m0 : MeasurableSpace α
μ : Measure α
inst_4 : SigmaFinite μ
hf : AEMeasurable f μ
⊢ AEFinStronglyMeasurable f μ

Tactic:
(aefinStronglyMeasurable_iff_aemeasurable μ).mpr hf

Premises used: Iff.mpr, MeasureTheory.aefinStronglyMeasurable_iff_aemeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : TopologicalSpace β
f : α →ₛ β
⊢ StronglyMeasurable.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
⟨fun _ => f, fun _ => tendsto_const_nhds⟩

Premises used: tendsto_const_nhds, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : Subsingleton α
⊢ StronglyMeasurable f

Tactic:
⟨fun _ => SimpleFunc.ofFinite f, fun _ => tendsto_const_nhds⟩

Premises used: tendsto_const_nhds, Exists.intro, MeasureTheory.SimpleFunc.ofFinite, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : Subsingleton β
refine_2 : StronglyMeasurable f
refine_1 : ∀ (x_1 : β), MeasurableSet (f ⁻¹' {x_1})
⊢ StronglyMeasurable f

Tactic:
let f_sf : α →ₛ β := ⟨f, fun x => ?_, Set.Subsingleton.finite Set.subsingleton_of_subsingleton⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : Subsingleton β
f_sf : α →ₛ β := { toFun := f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

Tactic:
⟨fun _ => f_sf, fun x => tendsto_const_nhds⟩

Premises used: tendsto_const_nhds, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : Subsingleton β
f_sf : α →ₛ β := { toFun := f, measurableSet_fiber' := ⋯, finite_range' := ⋯ }
⊢ StronglyMeasurable f

Tactic:
exact ⟨fun _ => f_sf, fun x => tendsto_const_nhds⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x_1 : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : Subsingleton β
x : β
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
simp [Set.preimage, eq_iff_true_of_subsingleton]

Premises used: Set.preimage, eq_iff_true_of_subsingleton
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : TopologicalSpace β
b : β
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ b

Tactic:
⟨fun _ => SimpleFunc.const α b, fun _ => tendsto_const_nhds⟩

Premises used: MeasureTheory.SimpleFunc.const, tendsto_const_nhds, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : One β
⊢ StronglyMeasurable.{u_1, u_2} (α := α) (β := β) 1

Tactic:
stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
hf : ∀ (x y : α), f x = f y
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
hf : ∀ (x y : α), f x = f y
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
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
hf : ∀ (x y : α), f x = f y
h : Nontrivial α
inhabited_h : Inhabited α
⊢ StronglyMeasurable.{u_1, u_2} (β := β) fun (x : α) ↦ f default

Tactic:
stronglyMeasurable_const (β := β)

Premises used: MeasureTheory.stronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
hf : ∀ (x y : α), f x = f y
h_1 : Nontrivial α
inhabited_h : Inhabited α
h : f = fun (x : α) ↦ f default
convert_3 : β
⊢ StronglyMeasurable f

Tactic:
convert! stronglyMeasurable_const (β := β) using 1

Premises used: MeasureTheory.stronglyMeasurable_const
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
hf : ∀ (x y : α), f x = f y
h : Nontrivial α
inhabited_h : Inhabited α
⊢ f = fun (x : α) ↦ f default

Tactic:
funext fun x => hf x default

Premises used: Inhabited.default, funext
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst : MeasurableSingletonClass α
⊢ (simpleFuncAux f g m.succ : (a : α) → β) (g m) = f (g m)

Tactic:
simp [simpleFuncAux]

Premises used: _private.0.MeasureTheory.simpleFuncAux
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst : MeasurableSingletonClass α
n : ℕ
hmn : m.succ.le n
inl : ∀ (hnm : g n = g m), (simpleFuncAux f g n.succ : (a : α) → β) (g m) = f (g m)
inr : ∀ (hnm : g n ≠ g m), (simpleFuncAux f g n.succ : (a : α) → β) (g m) = f (g m)
⊢ (simpleFuncAux f g n.succ : (a : α) → β) (g m) = f (g m)

Tactic:
obtain hnm | hnm := eq_or_ne (g n) (g m)

Premises used: eq_or_ne
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst : MeasurableSingletonClass α
n : ℕ
hmn : m.succ.le n
hnm : g n = g m
⊢ (simpleFuncAux f g n.succ : (a : α) → β) (g m) = f (g m)

Tactic:
simp [simpleFuncAux, Set.piecewise_eq_of_notMem, hnm.symm, simpleFuncAux_eq_of_lt _ hmn]

Premises used: Set.piecewise_eq_of_notMem, _private.0.MeasureTheory.simpleFuncAux, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst : MeasurableSingletonClass α
n : ℕ
hmn : m.succ.le n
hnm : g n ≠ g m
⊢ (simpleFuncAux f g n.succ : (a : α) → β) (g m) = f (g m)

Tactic:
simp [simpleFuncAux, Set.piecewise_eq_of_notMem, hnm.symm, simpleFuncAux_eq_of_lt _ hmn]

Premises used: Set.piecewise_eq_of_notMem, _private.0.MeasureTheory.simpleFuncAux, Ne.symm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst : MeasurableSingletonClass α
⊢ ∀ᶠ (n : ℕ) in atTop, (simpleFuncAux f g n : (a : α) → β) (g m) = f (g m)

Tactic:
eventually_atTop.2 ⟨_, simpleFuncAux_eq_of_lt⟩

Premises used: Iff.mpr, _private.0.MeasureTheory.simpleFuncAux_eq_of_lt, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : MeasurableSingletonClass α
inst_2 : Countable α
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : MeasurableSingletonClass α
inst_2 : Countable α
h : Nontrivial α
obtain : ∀ (g : ℕ → α) (hg : Surjective g), StronglyMeasurable f
⊢ StronglyMeasurable f

Tactic:
obtain ⟨g, hg⟩ := exists_surjective_nat α

Premises used: exists_surjective_nat
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : MeasurableSingletonClass α
inst_2 : Countable α
h : Nontrivial α
g : ℕ → α
hg : Surjective g
⊢ StronglyMeasurable f

Tactic:
⟨simpleFuncAux f g, hg.forall.2 fun m ↦
    tendsto_nhds_of_eventually_eq simpleFuncAux_eventuallyEq⟩

Premises used: _private.0.MeasureTheory.simpleFuncAux_eventuallyEq, Iff.mpr, Function.Surjective.forall, _private.0.MeasureTheory.simpleFuncAux, tendsto_nhds_of_eventually_eq, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
f : α → β
inst : TopologicalSpace β
inst_1 : MeasurableSingletonClass α
inst_2 : Countable α
h : Nontrivial α
g : ℕ → α
hg : Surjective g
⊢ StronglyMeasurable f

Tactic:
exact ⟨simpleFuncAux f g, hg.forall.2 fun m ↦
    tendsto_nhds_of_eventually_eq simpleFuncAux_eventuallyEq⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
x : MeasurableSpace α
hf : StronglyMeasurable f
⊢ ∀ (x_1 : α), Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x_1) atTop (𝓝 (f x_1))

Tactic:
hf.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
⊢ Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
have h_tendsto := hf.tendsto_approx x
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
simp :
  Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β))
    atTop (𝓝 (f x))
⊢ Tendsto (fun (n : ℕ) ↦ (hf.approxBounded c n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
simp only [StronglyMeasurable.approxBounded, SimpleFunc.coe_map, Function.comp_apply]

Premises used: MeasureTheory.SimpleFunc.coe_map, Function.comp_apply, MeasureTheory.StronglyMeasurable.approxBounded
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
pos :
  ∀ (hfx0 : ‖f x‖ = 0),
    Tendsto
      (fun (n : ℕ) ↦
        HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
          ((hf.approx n : (a : α) → β) x : β))
      atTop (𝓝 (f x))
neg :
  ∀ (hfx0 : ¬‖f x‖ = 0),
    Tendsto
      (fun (n : ℕ) ↦
        HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
          ((hf.approx n : (a : α) → β) x : β))
      atTop (𝓝 (f x))
⊢ Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β))
    atTop (𝓝 (f x))

Tactic:
by_cases hfx0 : ‖f x‖ = 0
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
hfx0 : ‖f x‖ = 0
⊢ f x = 0

Tactic:
rw [norm_eq_zero] at hfx0

Premises used: norm_eq_zero
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
hfx0 : f x = 0
pos :
  ∀ (h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)) (hfx0 : f x = 0),
    Tendsto.{0, u_5} (β := β)
      (fun (n : ℕ) ↦
        HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
          ((hf.approx n : (a : α) → β) x : β))
      atTop (𝓝 0)
⊢ Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β))
    atTop (𝓝 (f x))

Tactic:
rw [hfx0] at h_tendsto ⊢
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
⊢ Tendsto (fun (x_1 : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx x_1 : (a : α) → β) x : β)) atTop (𝓝 (norm.{u_5} (E := β) 0))

Tactic:
h_tendsto.norm

Premises used: Filter.Tendsto.norm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
h : 0 = norm.{u_5} (E := β) 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 0)

Tactic:
convert! h_tendsto.norm

Premises used: Filter.Tendsto.norm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
h h₁ : Eq (α := ℝ) 0 0
⊢ 0 = norm.{u_5} (E := β) 0

Tactic:
rw [norm_zero]

Premises used: norm_zero
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 0)

Tactic:
have h_tendsto_norm : Tendsto (fun n => ‖hf.approx n x‖) atTop (𝓝 0) := by
      convert! h_tendsto.norm
      rw [norm_zero]
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 0)
⊢ Tendsto.{0, u_5} (β := β)
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β))
    atTop (𝓝 0)

Tactic:
squeeze_zero_norm (fun n => ?_) h_tendsto_norm

Premises used: squeeze_zero_norm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 0)
pos :
  ∀ (n : ℕ),
    ‖HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
          ((hf.approx n : (a : α) → β) x : β)‖ ≤
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
⊢ Tendsto.{0, u_5} (β := β)
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β))
    atTop (𝓝 0)

Tactic:
refine squeeze_zero_norm (fun n => ?_) h_tendsto_norm

Premises used: squeeze_zero_norm
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 0)
n : ℕ
⊢ ‖HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β)‖ =
    ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)

Tactic:
norm_smul _ _

Premises used: norm_smul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 0)
n : ℕ
hbc : ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ ≤ norm (E := ℝ) 1
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    norm (E := ℝ) 1 * norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 0)
n : ℕ
hbc : min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤ 1
hbc₁ : 0 ≤ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ ≤ norm (E := ℝ) 1

Tactic:
rw [norm_one, Real.norm_of_nonneg]

Premises used: NormOneClass.norm_one, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 0)
n : ℕ
⊢ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤ 1

Tactic:
min_le_left _ _

Premises used: min_le_left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 0)
n : ℕ
⊢ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤ 1

Tactic:
exact min_le_left _ _

Premises used: min_le_left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 0)
n : ℕ
⊢ 0 ≤ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))

Tactic:
le_min zero_le_one (div_nonneg ((norm_nonneg _).trans hfx) (norm_nonneg _))

Premises used: zero_le_one, le_min, div_nonneg, LE.le.trans, norm_nonneg
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
hf : StronglyMeasurable f
c : ℝ
x : α
hfx : ‖f x‖ ≤ c
h_tendsto : Tendsto.{0, u_5} (β := β) (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 0)
hfx0 : f x = 0
h_tendsto_norm : Tendsto (β := ℝ) (fun (n : ℕ) ↦ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 0)
n : ℕ
⊢ 0 ≤ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))

Tactic:
exact le_min zero_le_one (div_nonneg ((norm_nonneg _).trans hfx) (norm_nonneg _))

Premises used: zero_le_one, le_min, div_nonneg, LE.le.trans, norm_nonneg