awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
have refine_1 : ∀ (δ : ℝ) (hδ₀ : 0 < δ)
  (hδ :
    ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ε) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 δ) (g x)),
  ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
Tactic: rcases h ε hε with ⟨δ, hδ₀, hδ⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₀ : 0 < δ
hδ : ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ε) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 δ) (g x)
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ ε * ‖g x‖
have refine_1 : ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ))
  (hδ :
    ∀ (ε_1 : ℝ≥0),
      ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 δ) (g x)),
  ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
Tactic: lift ε to ℝ≥0 using hε.le
Cleared hypotheses: ε, hε, hδ
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
δ : ℝ
hδ₀ : 0 < δ
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hδ :
  ∀ (ε_1 : ℝ≥0), ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 δ) (g x)
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
have refine_1 : ∀ (δ : ℝ≥0) (hδ₀ : 0 < (↑δ : ℝ))
  (hδ :
    ∀ (ε_1 : ℝ≥0),
      ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)),
  ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
Tactic: lift δ to ℝ≥0 using hδ₀.le
Cleared hypotheses: δ, hδ₀, hδ
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
δ : ℝ≥0
hδ₀ : 0 < (↑δ : ℝ)
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
have hε₁ : 0 < ε
Tactic: norm_cast at hε hδ₀
Cleared hypotheses: hε, hδ₀
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
δ : ℝ≥0
hδ₀ : 0 < (↑δ : ℝ)
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε₁ : 0 < ε
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
have hδ₁ : 0 < δ
Tactic: norm_cast at hε hδ₀
Cleared hypotheses: hε, hδ₀
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
have h₁ : ∀ (x : α) (hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)),
  ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
Tactic: filter_upwards [hδ (δ / ‖c‖₊) (div_pos hδ₀ hc₀).ne'] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
this : (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
⊢ ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
have this₁ : (↑(‖f x‖₊ / ε) : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_div hε.ne'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
this : (↑(‖f x‖₊ / ε) : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
⊢ ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
have rw : ‖f x‖ / (↑ε : ℝ) ≤ ‖g x‖
Tactic: rw [← div_le_iff₀' (NNReal.coe_pos.2 hε)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ ‖f x‖ ≤ (↑ε : ℝ) * ‖g x‖
have h₁ : (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
Tactic: suffices (‖f x‖₊ / ε : ℝ≥0∞) ≤ ‖g x‖₊ by
      rw [← ENNReal.coe_div hε.ne'] at this
      rw [← div_le_iff₀' (NNReal.coe_pos.2 hε)]
      exact_mod_cast this
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x) ≤
    (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞))
have h₁ : (↑(δ / ‖c‖₊) : ℝ≥0∞) ≤ (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
h₁ : (↑(δ / ‖c‖₊) : ℝ≥0∞) ≤ (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)
⊢ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x) ≤
    (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞))
have h₂ : egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x) ≤ (↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)) * (↑‖g x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) 1 1 * (↑‖g x‖₊ : ℝ≥0∞)
have bc : (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
bc : (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) ≤ 1
⊢ (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)) * (↑‖g x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) 1 1 * (↑‖g x‖₊ : ℝ≥0∞)
have bc₁ : (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
⊢ (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
have ε₁ : (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x) ≤
  (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞))
Tactic: calc
      (‖f x‖₊ / ε : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 ε) (f x) := div_le_egauge_ball 𝕜 _ _
      _ ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x) := hx
      _ ≤ (δ / ‖c‖₊) * (‖c‖₊ * ‖g x‖₊ / δ) := by
        gcongr
        exacts [ENNReal.coe_div_le, egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)]
      _ = (δ / δ) * (‖c‖₊ / ‖c‖₊) * ‖g x‖₊ := by simp only [div_eq_mul_inv]; ring
      _ ≤ 1 * 1 * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
      _ = ‖g x‖₊ := by simp
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
ε₁ :
  (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x) ≤
    (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞))
⊢ (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
have ε₂ : (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞)) =
  (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)) * (↑‖g x‖₊ : ℝ≥0∞)
Tactic: calc
      (‖f x‖₊ / ε : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 ε) (f x) := div_le_egauge_ball 𝕜 _ _
      _ ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x) := hx
      _ ≤ (δ / ‖c‖₊) * (‖c‖₊ * ‖g x‖₊ / δ) := by
        gcongr
        exacts [ENNReal.coe_div_le, egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)]
      _ = (δ / δ) * (‖c‖₊ / ‖c‖₊) * ‖g x‖₊ := by simp only [div_eq_mul_inv]; ring
      _ ≤ 1 * 1 * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
      _ = ‖g x‖₊ := by simp
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
ε₁ :
  (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x) ≤
    (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞))
ε₂ :
  (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞)) =
    (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)) * (↑‖g x‖₊ : ℝ≥0∞)
⊢ (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
have ε₃ : (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)) * (↑‖g x‖₊ : ℝ≥0∞) ≤
  HMul.hMul (α := ℝ≥0∞) 1 1 * (↑‖g x‖₊ : ℝ≥0∞)
Tactic: calc
      (‖f x‖₊ / ε : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 ε) (f x) := div_le_egauge_ball 𝕜 _ _
      _ ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x) := hx
      _ ≤ (δ / ‖c‖₊) * (‖c‖₊ * ‖g x‖₊ / δ) := by
        gcongr
        exacts [ENNReal.coe_div_le, egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)]
      _ = (δ / δ) * (‖c‖₊ / ‖c‖₊) * ‖g x‖₊ := by simp only [div_eq_mul_inv]; ring
      _ ≤ 1 * 1 * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
      _ = ‖g x‖₊ := by simp
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h :
  ∀ (i : ℝ),
    0 < i →
      ∃ (j : ℝ),
        0 < j ∧
          ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 i) (f x) ≤ (↑ε : ℝ≥0∞) * egauge 𝕜 (ball 0 j) (g x)
ε δ : ℝ≥0
hδ :
  ∀ (ε_1 : ℝ≥0),
    ε_1 ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑ε_1 : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
hε : 0 < ε
hδ₀ : 0 < δ
x : α
hx : egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x)
ε₁ :
  (↑(δ / ‖c‖₊) : ℝ≥0∞) * egauge 𝕜 (ball 0 (↑δ : ℝ)) (g x) ≤
    (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞))
ε₂ :
  (↑δ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) / (↑δ : ℝ≥0∞)) =
    (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)) * (↑‖g x‖₊ : ℝ≥0∞)
ε₃ :
  (↑δ : ℝ≥0∞) / (↑δ : ℝ≥0∞) * ((↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞)) * (↑‖g x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) 1 1 * (↑‖g x‖₊ : ℝ≥0∞)
⊢ (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤ (↑‖g x‖₊ : ℝ≥0∞)
have ε₄ : HMul.hMul (α := ℝ≥0∞) 1 1 * (↑‖g x‖₊ : ℝ≥0∞) = (↑‖g x‖₊ : ℝ≥0∞)
Tactic: calc
      (‖f x‖₊ / ε : ℝ≥0∞) ≤ egauge 𝕜 (ball 0 ε) (f x) := div_le_egauge_ball 𝕜 _ _
      _ ≤ ↑(δ / ‖c‖₊) * egauge 𝕜 (ball 0 ↑δ) (g x) := hx
      _ ≤ (δ / ‖c‖₊) * (‖c‖₊ * ‖g x‖₊ / δ) := by
        gcongr
        exacts [ENNReal.coe_div_le, egauge_ball_le_of_one_lt_norm hc (.inl <| ne_of_gt hδ₀)]
      _ = (δ / δ) * (‖c‖₊ / ‖c‖₊) * ‖g x‖₊ := by simp only [div_eq_mul_inv]; ring
      _ ≤ 1 * 1 * ‖g x‖₊ := by gcongr <;> exact ENNReal.div_self_le_one
      _ = ‖g x‖₊ := by simp
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : δ ≠ 0
x : α
⊢ ‖f x‖ ≤ ε * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * ‖g x‖ → egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
have h₁ : ∀ (hx : (↑‖f x‖₊ : ℝ) ≤ ε * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)),
  egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
Tactic: (hx : ‖f x‖₊ ≤ ε * δ / ‖c‖₊ * ‖g x‖₊)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : δ ≠ 0
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
have h₁ : ∀ (x : α) (hx : (↑‖f x‖₊ : ℝ) ≤ ε * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)),
  egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
Tactic: filter_upwards [@h ↑(ε * δ / ‖c‖₊) (by positivity)] with x (hx : ‖f x‖₊ ≤ ε * δ / ‖c‖₊ * ‖g x‖₊)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
ε : ℝ
hε : 0 < ε
δ : ℝ≥0
hδ : δ ≠ 0
x : α
hx : (↑‖f x‖₊ : ℝ) ≤ ε * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ egauge 𝕜 (ball 0 ε) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
have h₁ : ∀ (ε : ℝ≥0) (hε : 0 < (↑ε : ℝ)) (hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)),
  egauge 𝕜 (ball 0 (↑ε : ℝ)) (f x) ≤ (↑δ : ℝ≥0∞) * egauge 𝕜 (ball 0 1) (g x)
Tactic: lift ε to ℝ≥0 using hε.le
Cleared hypotheses: ε, hε, hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ (↑‖c‖₊ : ℝ≥0∞) * (↑‖f x‖₊ : ℝ≥0∞) / (↑ε : ℝ≥0∞) ≤
    (↑‖c‖₊ : ℝ≥0∞) * ((↑(ε * δ / ‖c‖₊) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)) / (↑ε : ℝ≥0∞)
have hab : (↑‖f x‖₊ : ℝ≥0∞) ≤ (↑(ε * δ / ‖c‖₊) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ (↑‖c‖₊ : ℝ≥0∞) * ((↑(ε * δ / ‖c‖₊) : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)) / (↑ε : ℝ≥0∞) =
    (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) / (↑ε : ℝ≥0∞)) * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
have simp : (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) * (↑δ : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞)⁻¹ * (↑‖g x‖₊ : ℝ≥0∞)) * (↑ε : ℝ≥0∞)⁻¹ =
  (↑‖c‖₊ : ℝ≥0∞) * (↑‖c‖₊ : ℝ≥0∞)⁻¹ * ((↑ε : ℝ≥0∞) * (↑ε : ℝ≥0∞)⁻¹) * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
Tactic: simp only [div_eq_mul_inv, ENNReal.coe_inv hc₀.ne', ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.TVS (goal)
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : NontriviallyNormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < (↑ε : ℝ)
hx : (↑‖f x‖₊ : ℝ) ≤ (↑ε : ℝ) * (↑δ : ℝ) / (↑‖c‖₊ : ℝ) * (↑‖g x‖₊ : ℝ)
⊢ (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) * ((↑ε : ℝ≥0∞) / (↑ε : ℝ≥0∞)) * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) 1 1 * (↑δ : ℝ≥0∞) * (↑‖g x‖₊ : ℝ≥0∞)
have bc : (↑‖c‖₊ : ℝ≥0∞) / (↑‖c‖₊ : ℝ≥0∞) ≤ 1
Tactic: gcongr