awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
rw :
  1 * norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
rw₁ rw₂ :
  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 : β) =
    norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)

Tactic:
rw [norm_one, one_mul]

Premises used: NormOneClass.norm_one, one_mul
-- 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 : ℕ
n₁ :
  ‖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 : β)
n₂ :
  norm (E := ℝ) 1 * norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) =
    norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
⊢ ‖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 : β)

Tactic:
calc
      ‖min 1 (c / ‖hf.approx n x‖) • hf.approx n x‖ =
          ‖min 1 (c / ‖hf.approx n x‖)‖ * ‖hf.approx n x‖ :=
        norm_smul _ _
      _ ≤ ‖(1 : ℝ)‖ * ‖hf.approx n x‖ := by
        gcongr
        rw [norm_one, Real.norm_of_nonneg]
        · exact min_le_left _ _
        · exact le_min zero_le_one (div_nonneg ((norm_nonneg _).trans hfx) (norm_nonneg _))
      _ = ‖hf.approx n x‖ := by rw [norm_one, one_mul]

Premises used: Norm.norm, MeasureTheory.StronglyMeasurable.approx, norm_smul, HDiv.hDiv, OfNat.ofNat, DFunLike.coe, Min.min
-- 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
neg :
  Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β))
    atTop (𝓝 (HSMul.hSMul (α := ℝ) 1 (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:
rw [← one_smul ℝ (f x)]

Premises used: Real, one_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 (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
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 (𝓝 (HSMul.hSMul (α := ℝ) 1 (f x)))

Tactic:
Tendsto.smul ?_ h_tendsto

Premises used: Filter.Tendsto.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 (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
neg : Tendsto (β := ℝ) (fun (n : ℕ) ↦ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))) atTop (𝓝 1)
⊢ Tendsto
    (fun (n : ℕ) ↦
      HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β))
    atTop (𝓝 (HSMul.hSMul (α := ℝ) 1 (f x)))

Tactic:
refine Tendsto.smul ?_ h_tendsto

Premises used: Filter.Tendsto.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 (fun (n : ℕ) ↦ (hf.approx n : (a : α) → β) x) atTop (𝓝 (f x))
hfx0 : ¬‖f x‖ = 0
rw : ‖f x‖ ≤ c
⊢ min 1 (c / ‖f x‖) = 1

Tactic:
rw [min_eq_left_iff, one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm hfx0))]

Premises used: Ne.symm, min_eq_left_iff, one_le_div, norm_nonneg, lt_of_le_of_ne
-- 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‖ ≤ c

Tactic:
hfx
-- 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‖ ≤ c

Tactic:
exact hfx
-- 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
⊢ min 1 (c / ‖f x‖) = 1

Tactic:
have : min 1 (c / ‖f x‖) = 1 := by
    rw [min_eq_left_iff, one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm hfx0))]
    exact hfx
-- 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
this : min 1 (c / ‖f x‖) = 1
neg :
  Tendsto (fun (n : ℕ) ↦ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))) atTop
    (𝓝 (min 1 (c / ‖f x‖)))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))) atTop (𝓝 1)

Tactic:
nth_rw 2 [this.symm]

Premises used: Eq.symm
-- 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
this : min 1 (c / ‖f x‖) = 1
⊢ Tendsto (fun (n : ℕ) ↦ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))) atTop
    (𝓝 (min 1 (c / ‖f x‖)))

Tactic:
Tendsto.min tendsto_const_nhds ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.min
-- 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
this : min 1 (c / ‖f x‖) = 1
neg : Tendsto (fun (n : ℕ) ↦ c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 (c / ‖f x‖))
⊢ Tendsto (fun (n : ℕ) ↦ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))) atTop
    (𝓝 (min 1 (c / ‖f x‖)))

Tactic:
refine Tendsto.min tendsto_const_nhds ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.min
-- 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
this : min 1 (c / ‖f x‖) = 1
⊢ Tendsto (fun (n : ℕ) ↦ c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 (c / ‖f x‖))

Tactic:
Tendsto.div tendsto_const_nhds h_tendsto.norm hfx0

Premises used: tendsto_const_nhds, Filter.Tendsto.norm, Filter.Tendsto.div
-- 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
this : min 1 (c / ‖f x‖) = 1
⊢ Tendsto (fun (n : ℕ) ↦ c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 (c / ‖f x‖))

Tactic:
exact Tendsto.div tendsto_const_nhds h_tendsto.norm hfx0

Premises used: tendsto_const_nhds, Filter.Tendsto.norm, Filter.Tendsto.div
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m m0 : MeasurableSpace α
μ : Measure α
hf : StronglyMeasurable f
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
x : α
hfx : ‖f x‖ ≤ c
⊢ Tendsto (fun (n : ℕ) ↦ (hf.approxBounded c n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
tendsto_approxBounded_of_norm_le hf hfx

Premises used: MeasureTheory.StronglyMeasurable.tendsto_approxBounded_of_norm_le
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : NormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m m0 : MeasurableSpace α
μ : Measure α
hf : StronglyMeasurable f
c : ℝ
hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ‖f x‖ ≤ c) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ Tendsto (fun (n : ℕ) ↦ (hf.approxBounded c n : (a : α) → β) x) atTop (𝓝 (f x))) x}
            x}
      a
h₁ h₂ : ∀ (x : α) (hfx : ‖f x‖ ≤ c), Tendsto (fun (n : ℕ) ↦ (hf.approxBounded c n : (a : α) → β) x) atTop (𝓝 (f x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ (hf.approxBounded c n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
filter_upwards [hf_bound] with x hfx using tendsto_approxBounded_of_norm_le hf hfx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
simp :
  ‖HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β)‖ ≤
    c
⊢ norm.{u_5} (E := β) ((hf.approxBounded c n : (a : α) → β) x : β) ≤ c

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 : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
⊢ ‖HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β)‖ ≤
    c

Tactic:
(norm_smul_le _ _).trans ?_

Premises used: norm_smul_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
refine :
  ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
⊢ ‖HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
        ((hf.approx n : (a : α) → β) x : β)‖ ≤
    c

Tactic:
refine (norm_smul_le _ _).trans ?_

Premises used: norm_smul_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
pos :
  ∀ (h0 : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0),
    ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
        norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
      c
neg :
  ∀ (h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0),
    ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
        norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
      c
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c

Tactic:
by_cases h0 : ‖hf.approx n x‖ = 0

Premises used: MeasureTheory.StronglyMeasurable.approx, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
pos : 0 ≤ c
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c

Tactic:
simp only [h0, _root_.div_zero, min_eq_right, zero_le_one, norm_zero, mul_zero]

Premises used: norm_zero, MulZeroClass.mul_zero, zero_le_one, min_eq_right, div_zero
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
⊢ 0 ≤ c

Tactic:
hc
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
⊢ 0 ≤ c

Tactic:
exact hc
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
neg :
  ∀ (h : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤ c),
    ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
        norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
      c
neg₁ :
  ∀ (h : c ≤ norm.{u_5} (E := β) ((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 : β) ≤
      c
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c

Tactic:
rcases le_total ‖hf.approx n x‖ c with h | h

Premises used: Norm.norm, MeasureTheory.StronglyMeasurable.approx, le_total, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤ c
neg : norm (E := ℝ) 1 * norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤ c
rw : 1 ≤ c / norm.{u_5} (E := β) ((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 : β) ≤
    c

Tactic:
rw [min_eq_left _]

Premises used: min_eq_left
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤ c
⊢ norm (E := ℝ) 1 * norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤ c

Tactic:
simpa only [norm_one, one_mul] using h

Premises used: NormOneClass.norm_one, one_mul
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤ c
rwa rwa₁ rwa₂ rwa₃ : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤ c
⊢ 1 ≤ c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)

Tactic:
rwa [one_le_div (lt_of_le_of_ne (norm_nonneg _) (Ne.symm h0))]

Premises used: Ne.symm, one_le_div, norm_nonneg, lt_of_le_of_ne
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
neg :
  ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
rw : c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤ 1
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c

Tactic:
rw [min_eq_right _]

Premises used: min_eq_right
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
neg :
  ‖c‖ / ‖norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₁ :
  ‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₂ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      (‖c‖ / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤
    c
neg₃ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ /
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
neg₄ :
  norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖ *
      (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ ≤
    c
neg₅ :
  (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ *
      (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) * ‖c‖) ≤
    c
neg₆ :
  (norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))⁻¹ *
        norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) *
      ‖c‖ ≤
    c
neg₇ : 1 * ‖c‖ ≤ c
neg₈ : ‖c‖ ≤ c
neg₉ neg₁₀ : c ≤ c
⊢ ‖c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c

Tactic:
rw [norm_div, norm_norm, mul_comm, mul_div, div_eq_mul_inv, mul_comm, ← mul_assoc,
        inv_mul_cancel₀ h0, one_mul, Real.norm_of_nonneg hc]

Premises used: mul_div, mul_assoc, norm_norm, div_eq_mul_inv, norm_div, mul_comm, inv_mul_cancel₀, one_mul, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
h0 : ¬norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = 0
h : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
rwa rwa₁ rwa₂ rwa₃ : c ≤ norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
⊢ c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤ 1

Tactic:
rwa [div_le_one (lt_of_le_of_ne (norm_nonneg _) (Ne.symm h0))]

Premises used: Ne.symm, div_le_one, norm_nonneg, lt_of_le_of_ne
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
inl : ∀ (hα : IsEmpty α), StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c
inr : ∀ (hα : Nonempty α), StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c
⊢ StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c

Tactic:
rcases isEmpty_or_nonempty α with hα | hα

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : IsEmpty α
⊢ StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
⊢ StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c

Tactic:
⟨fun hf => ?_, fun hf_eq => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
inr : ∀ (hf : StronglyMeasurable f), ∃ (c : β), f = fun (x : α) ↦ c
inr₁ : ∀ (hf_eq : ∃ (c : β), f = fun (x : α) ↦ c), StronglyMeasurable f
⊢ StronglyMeasurable f ↔ ∃ (c : β), f = fun (x : α) ↦ c

Tactic:
refine ⟨fun hf => ?_, fun hf_eq => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
⊢ ∃ (c : β), f = fun (x : α) ↦ c

Tactic:
⟨f hα.some, ?_⟩

Premises used: Nonempty.some, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
inr : f = fun (x : α) ↦ f hα.some
⊢ ∃ (c : β), f = fun (x : α) ↦ c

Tactic:
refine ⟨f hα.some, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : TopologicalSpace β
inst_1 : Nonempty β
inst_2 : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
⊢ ∀ (x : α), Tendsto (fun (n : ℕ) ↦ (fs n : (a : α) → β) x) atTop (𝓝 (f x))

Tactic:
have h_fs_tendsto : ∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x)) := hf.tendsto_approx