awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
⊢ (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
have h : Eq (α := α → E) (fun (x : α) ↦ b x • (φ x • u x - v x)) fun (i : α) ↦ (φ * b) i • u i - b i • v i
Tactic: convert!
      (habφ.comp₂ (· • ·) <| EventuallyEq.refl _ u).fun_sub
        (EventuallyEq.refl _ fun x ↦ b x • v x) using 1
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
⊢ Eq (α := α → E) (fun (x : α) ↦ b x • (φ x • u x - v x)) fun (i : α) ↦ (φ * b) i • u i - b i • v i
have h : ∀ (x : α), b x • (φ x • u x - v x) = (φ * b) x • u x - b x • v x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
x : α
⊢ b x • (φ x • u x - v x) = (φ * b) x • u x - b x • v x
have h : b x • (φ x • u x - v x) = (φ x * b x) • u x - b x • v x
Tactic: rw [Pi.mul_apply, mul_comm, mul_smul, ← smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
x : α
h : b x • (φ x • u x - v x) = (φ x * b x) • u x - b x • v x
⊢ b x • (φ x • u x - v x) = (φ * b) x • u x - b x • v x
have h₁ : b x • (φ x • u x - v x) = (b x * φ x) • u x - b x • v x
Tactic: rw [Pi.mul_apply, mul_comm, mul_smul, ← smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
x : α
h : b x • (φ x • u x - v x) = (φ x * b x) • u x - b x • v x
h₁ : b x • (φ x • u x - v x) = (b x * φ x) • u x - b x • v x
⊢ b x • (φ x • u x - v x) = (φ * b) x • u x - b x • v x
have h₂ : b x • (φ x • u x - v x) = b x • φ x • u x - b x • v x
Tactic: rw [Pi.mul_apply, mul_comm, mul_smul, ← smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
x : α
h : b x • (φ x • u x - v x) = (φ x * b x) • u x - b x • v x
h₁ : b x • (φ x • u x - v x) = (b x * φ x) • u x - b x • v x
h₂ : b x • (φ x • u x - v x) = b x • φ x • u x - b x • v x
⊢ b x • (φ x • u x - v x) = (φ * b) x • u x - b x • v x
have h₃ : b x • (φ x • u x - v x) = b x • (φ x • u x - v x)
Tactic: rw [Pi.mul_apply, mul_comm, mul_smul, ← smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
⊢ IsEquivalent.{u_1, u_2} (E' := E) l (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x
have this : (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
  b x • (φ x • u x - v x)
Tactic: have : ((fun x ↦ a x • u x) - (fun x ↦ b x • v x)) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x) := by
    convert!
      (habφ.comp₂ (· • ·) <| EventuallyEq.refl _ u).fun_sub
        (EventuallyEq.refl _ fun x ↦ b x • v x) using 1
    ext
    rw [Pi.mul_apply, mul_comm, mul_smul, ← smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
⊢ IsEquivalent.{u_1, u_2} (E' := E) l (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x
have refine : IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v
Tactic: refine (isLittleO_congr this.symm <| EventuallyEq.rfl).mp ((isBigO_refl b l).smul_isLittleO ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
⊢ IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v
have rcases : ∀ (C : ℝ) (hC : C > 0) (hCuv : IsBigOWith C l u v), IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v
Tactic: rcases huv.isBigO.exists_pos with ⟨C, hC, hCuv⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : IsBigOWith C l u v
⊢ IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v
have rw : ∀ (hab : (a - b) =o[l] b) (huv : (u - v) =o[l] v) (φ : α → 𝕜) (hφ : Tendsto φ l (𝓝 1)) (habφ : a =ᶠ[l] φ * b)
  (this :
    (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
      b x • (φ x • u x - v x))
  (C : ℝ) (hC : C > 0) (hCuv : IsBigOWith C l u v), IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v
Tactic: rw [IsEquivalent] at *
Cleared hypotheses: hab, huv, φ, hφ, habφ, this, C, hC, hCuv
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : (a - b) =o[l] b
huv : (u - v) =o[l] v
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : IsBigOWith C l u v
⊢ IsLittleO (E := E) l (fun (x : α) ↦ φ x • u x - v x) v
have rw : ∀ (hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖)
  (huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖) (φ : α → 𝕜) (hφ : Tendsto φ l (𝓝 1))
  (habφ : a =ᶠ[l] φ * b)
  (this :
    (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
      b x • (φ x • u x - v x))
  (C : ℝ) (hC : C > 0) (hCuv : IsBigOWith C l u v) ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
Tactic: rw [isLittleO_iff] at *
Cleared hypotheses: hab, huv, φ, hφ, habφ, this, C, hC, hCuv
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : IsBigOWith C l u v
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
have hCuv₁ : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
Tactic: rw [IsBigOWith] at hCuv
Cleared hypotheses: hCuv
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
have hφ₁ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x - 1‖ < ε
Tactic: simp only [Metric.tendsto_nhds, dist_eq_norm] at hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
hφ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖φ x - 1‖ < ε
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
have hφ₁ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
Tactic: specialize hφ (c / 2 / C) (div_pos (div_pos hc zero_lt_two) hC)
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
⊢ ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
have huv₁ : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
Tactic: specialize huv (div_pos hc zero_lt_two)
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
⊢ ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
have refine : ∀ (x : α) (hCuvx : ‖u x‖ ≤ C * ‖v x‖) (huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖) (hφx : ‖φ x - 1‖ < c / 2 / C),
  ‖φ x • u x - v x‖ ≤ c * ‖v x‖
Tactic: refine hφ.mp (huv.mp <| hCuv.mono fun x hCuvx huvx hφx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 / C * ‖u x‖
have ha : 0 ≤ ‖u x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ c / 2 / C * ‖u x‖ ≤ c / 2 / C * (C * ‖v x‖)
have ha : 0 ≤ c / 2 / C
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (hypothesis)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ ‖φ x • u x - v x‖ ≤ c * ‖v x‖
have key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
Tactic: have key :=
    calc
      ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 / C * ‖u x‖ := by gcongr
      _ ≤ c / 2 / C * (C * ‖v x‖) := by gcongr
      _ = c / 2 * ‖v x‖ := by field
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖
have rw : ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖
Tactic: rw [norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ c / 2 * ‖v x‖ + ‖u x - v x‖ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖
have bc : ‖u x - v x‖ ≤ c / 2 * ‖v x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖φ x • u x - v x‖ ≤ c * ‖v x‖
have x₁ : ‖HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ φ x • u x) v x‖ = ‖(φ x - 1) • u x + (u x - v x)‖
Tactic: calc
    ‖((fun x : α ↦ φ x • u x) - v) x‖ = ‖(φ x - 1) • u x + (u x - v x)‖ := by
      simp [sub_smul, sub_add]
    _ ≤ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ := norm_add_le _ _
    _ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ := by rw [norm_smul]
    _ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖ := by gcongr
    _ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖ := by gcongr; exact huvx
    _ = c * ‖v x‖ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
x₁ : ‖HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ φ x • u x) v x‖ = ‖(φ x - 1) • u x + (u x - v x)‖
⊢ ‖φ x • u x - v x‖ ≤ c * ‖v x‖
have x₂ : ‖(φ x - 1) • u x‖ + ‖u x - v x‖ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖
Tactic: calc
    ‖((fun x : α ↦ φ x • u x) - v) x‖ = ‖(φ x - 1) • u x + (u x - v x)‖ := by
      simp [sub_smul, sub_add]
    _ ≤ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ := norm_add_le _ _
    _ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ := by rw [norm_smul]
    _ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖ := by gcongr
    _ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖ := by gcongr; exact huvx
    _ = c * ‖v x‖ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
x₁ : ‖HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ φ x • u x) v x‖ = ‖(φ x - 1) • u x + (u x - v x)‖
x₂ : ‖(φ x - 1) • u x‖ + ‖u x - v x‖ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖
⊢ ‖φ x • u x - v x‖ ≤ c * ‖v x‖
have x₃ : ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖
Tactic: calc
    ‖((fun x : α ↦ φ x • u x) - v) x‖ = ‖(φ x - 1) • u x + (u x - v x)‖ := by
      simp [sub_smul, sub_add]
    _ ≤ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ := norm_add_le _ _
    _ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ := by rw [norm_smul]
    _ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖ := by gcongr
    _ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖ := by gcongr; exact huvx
    _ = c * ‖v x‖ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
x₁ : ‖HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ φ x • u x) v x‖ = ‖(φ x - 1) • u x + (u x - v x)‖
x₂ : ‖(φ x - 1) • u x‖ + ‖u x - v x‖ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖
x₃ : ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖
⊢ ‖φ x • u x - v x‖ ≤ c * ‖v x‖
have x₄ : c / 2 * ‖v x‖ + ‖u x - v x‖ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖
Tactic: calc
    ‖((fun x : α ↦ φ x • u x) - v) x‖ = ‖(φ x - 1) • u x + (u x - v x)‖ := by
      simp [sub_smul, sub_add]
    _ ≤ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ := norm_add_le _ _
    _ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ := by rw [norm_smul]
    _ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖ := by gcongr
    _ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖ := by gcongr; exact huvx
    _ = c * ‖v x‖ := by ring
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this :
  (HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ a x • u x) fun (x : α) ↦ b x • v x) =ᶠ[l] fun (x : α) ↦
    b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
hc : 0 < c
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
x₁ : ‖HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ φ x • u x) v x‖ = ‖(φ x - 1) • u x + (u x - v x)‖
x₂ : ‖(φ x - 1) • u x‖ + ‖u x - v x‖ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖
x₃ : ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖
x₄ : c / 2 * ‖v x‖ + ‖u x - v x‖ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖
⊢ ‖φ x • u x - v x‖ ≤ c * ‖v x‖
have x₅ : c / 2 * ‖v x‖ + c / 2 * ‖v x‖ = c * ‖v x‖
Tactic: calc
    ‖((fun x : α ↦ φ x • u x) - v) x‖ = ‖(φ x - 1) • u x + (u x - v x)‖ := by
      simp [sub_smul, sub_add]
    _ ≤ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ := norm_add_le _ _
    _ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ := by rw [norm_smul]
    _ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖ := by gcongr
    _ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖ := by gcongr; exact huvx
    _ = c * ‖v x‖ := by ring