awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 (𝓝 (f x))
have hfx0₁ : f x = 0
Tactic: rw [norm_eq_zero] at hfx0
Cleared hypotheses: hfx0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 (𝓝 (f x))
have 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)
Tactic: rw [hfx0] at h_tendsto ⊢
Cleared hypotheses: h_tendsto, hfx0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)
have h : 0 = norm.{u_5} (E := β) 0
Tactic: convert! h_tendsto.norm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ 0 = norm.{u_5} (E := β) 0
have h : Eq (α := ℝ) 0 0
Tactic: rw [norm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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.{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)
have h_tendsto_norm : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)
have 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 : β)
Tactic: refine squeeze_zero_norm (fun n => ?_) h_tendsto_norm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    norm (E := ℝ) 1 * norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
have hbc : ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ ≤ norm (E := ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : β))‖ ≤ norm (E := ℝ) 1
have hbc : min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) ≤ 1
Tactic: rw [norm_one, Real.norm_of_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ ≤ norm (E := ℝ) 1
have hbc₁ : 0 ≤ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))
Tactic: rw [norm_one, Real.norm_of_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : ℕ
⊢ norm (E := ℝ) 1 * norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) =
    norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
have rw : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : β)
⊢ norm (E := ℝ) 1 * norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) =
    norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
have rw₁ : norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) = norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
Tactic: rw [norm_one, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : β)‖ ≤
    norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
have 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 : β)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : β)
⊢ ‖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 : β)
have n₂ : norm (E := ℝ) 1 * norm.{u_5} (E := β) ((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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 (𝓝 (f x))
have 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)))
Tactic: rw [← one_smul ℝ (f x)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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)))
have neg : Tendsto (β := ℝ) (fun (n : ℕ) ↦ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))) atTop (𝓝 1)
Tactic: refine Tendsto.smul ?_ h_tendsto
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (hypothesis)
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 : ℕ) ↦ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))) atTop (𝓝 1)
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 (𝓝 1)
have neg : Tendsto (fun (n : ℕ) ↦ min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))) atTop
  (𝓝 (min 1 (c / ‖f x‖)))
Tactic: nth_rw 2 [this.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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‖)))
have neg : Tendsto (fun (n : ℕ) ↦ c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)) atTop (𝓝 (c / ‖f x‖))
Tactic: refine Tendsto.min tendsto_const_nhds ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : α) ∂μ, Tendsto (fun (n : ℕ) ↦ (hf.approxBounded c n : (a : α) → β) x) atTop (𝓝 (f x))
have 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
Tactic: filter_upwards [hf_bound] with x hfx using tendsto_approxBounded_of_norm_le hf hfx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ (hf.approxBounded c n : (a : α) → β) x) atTop (𝓝 (f x))
have h₁ : ∀ (a : α), ‖f a‖ ≤ c → Tendsto (fun (n : ℕ) ↦ (hf.approxBounded c n : (a : α) → β) a) atTop (𝓝 (f a))
Tactic: filter_upwards [hf_bound] with x hfx using tendsto_approxBounded_of_norm_le hf hfx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
⊢ norm.{u_5} (E := β) ((hf.approxBounded c n : (a : α) → β) x : β) ≤ c
have simp : ‖HSMul.hSMul (β := β) (min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)))
      ((hf.approx n : (a : α) → β) x : β)‖ ≤
  c
Tactic: simp only [StronglyMeasurable.approxBounded, SimpleFunc.coe_map, Function.comp_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
have refine : ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
    norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
  c
Tactic: refine (norm_smul_le _ _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
Goal:
α : Type u_1
β : Type u_5
f : α → β
inst : SeminormedAddCommGroup β
inst_1 : NormedSpace ℝ β
m : MeasurableSpace α
c : ℝ
hf : StronglyMeasurable f
hc : 0 ≤ c
n : ℕ
x : α
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have 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
Tactic: by_cases h0 : ‖hf.approx n x‖ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have 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
Tactic: by_cases h0 : ‖hf.approx n x‖ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have 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
Tactic: rcases le_total ‖hf.approx n x‖ c with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have 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
Tactic: rcases le_total ‖hf.approx n x‖ c with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg : norm (E := ℝ) 1 * norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤ c
Tactic: rw [min_eq_left _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have rw : 1 ≤ c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β)
Tactic: rw [min_eq_left _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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 : β)
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have neg : ‖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 _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic (goal)
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
⊢ ‖min 1 (c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β))‖ *
      norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤
    c
have rw : c / norm.{u_5} (E := β) ((hf.approx n : (a : α) → β) x : β) ≤ 1
Tactic: rw [min_eq_right _]