awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖

Tactic:
specialize huv (div_pos hc zero_lt_two)

Premises used: div_pos, zero_lt_two
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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‖

Tactic:
hφ.mp (huv.mp <| hCuv.mono fun x hCuvx huvx hφx ↦ ?_)

Premises used: Filter.Eventually.mono, Filter.Eventually.mp
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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‖
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‖
⊢ ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖

Tactic:
refine hφ.mp (huv.mp <| hCuv.mono fun x hCuvx huvx hφx ↦ ?_)

Premises used: Filter.Eventually.mono, Filter.Eventually.mp
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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
ha : 0 ≤ ‖u x‖
⊢ ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 / C * ‖u x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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
ha : 0 ≤ c / 2 / C
⊢ c / 2 / C * ‖u x‖ ≤ c / 2 / C * (C * ‖v x‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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 * (C * ‖v x‖) = c / 2 * ‖v x‖

Tactic:
field
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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 * ‖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
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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‖
⊢ ‖HSub.hSub (α := (x : α) → E) (fun (x : α) ↦ φ x • u x) v x‖ = ‖(φ x - 1) • u x + (u x - v x)‖

Tactic:
simp [sub_smul, sub_add]

Premises used: sub_add, sub_smul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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‖

Tactic:
norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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‖
rw rw₁ : ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖
⊢ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖

Tactic:
rw [norm_smul]

Premises used: norm_smul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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‖ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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‖
bc : ‖u x - v x‖ ≤ c / 2 * ‖v x‖
⊢ c / 2 * ‖v x‖ + ‖u x - v x‖ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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‖
⊢ ‖u x - v x‖ ≤ c / 2 * ‖v x‖

Tactic:
huvx
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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‖
⊢ ‖u x - v x‖ ≤ c / 2 * ‖v x‖

Tactic:
exact huvx
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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‖ + c / 2 * ‖v x‖ = c * ‖v x‖

Tactic:
ring
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
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₅ : c / 2 * ‖v x‖ + c / 2 * ‖v x‖ = c * ‖v x‖
⊢ ‖φ x • u x - 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

Premises used: HSub.hSub, norm_add_le, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
t u v w : α → β
l : Filter α
htu : t ~[l] u
hvw : v ~[l] w
⊢ t * v ~[l] u * w

Tactic:
htu.smul hvw

Premises used: Asymptotics.IsEquivalent.smul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : NormedField β
l : Filter α
f g : ι → α → β
h : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i ~[l] g i
⊢ IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) [])) fun (x : α) ↦
    List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) [])

Tactic:
simp [IsEquivalent.refl]

Premises used: Asymptotics.IsEquivalent.refl
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : NormedField β
l : Filter α
f g : ι → α → β
i : ι
L : List ι
ihL :
  ∀ (h : ∀ i ∈ L, f i ~[l] g i),
    IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
      List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
h : ∀ i_1 ∈ i :: L, f i_1 ~[l] g i_1
cons :
  ∀ (h : f i ~[l] g i ∧ ∀ x ∈ L, f x ~[l] g x),
    IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
      fun (x : α) ↦ g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
⊢ IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (i :: L)))
    fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) (i :: L))

Tactic:
simp only [List.forall_mem_cons, List.map_cons, List.prod_cons] at h ⊢

Premises used: List.map_cons, List.forall_mem_cons, List.prod_cons
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : NormedField β
l : Filter α
f g : ι → α → β
i : ι
L : List ι
ihL :
  ∀ (h : ∀ i ∈ L, f i ~[l] g i),
    IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
      List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
h : f i ~[l] g i ∧ ∀ x ∈ L, f x ~[l] g x
⊢ IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
    fun (x : α) ↦ g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
h.1.mul (ihL h.2)

Premises used: Asymptotics.IsEquivalent.mul, And.right, And.left
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : NormedField β
l : Filter α
f g : ι → α → β
i : ι
L : List ι
ihL :
  ∀ (h : ∀ i ∈ L, f i ~[l] g i),
    IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
      List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)
h : f i ~[l] g i ∧ ∀ x ∈ L, f x ~[l] g x
⊢ IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ f i x * List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
    fun (x : α) ↦ g i x * List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
exact h.1.mul (ihL h.2)

Premises used: Asymptotics.IsEquivalent.mul, And.right, And.left
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : NormedField β
l : Filter α
L : List ι
f g : ι → α → β
h : ∀ i ∈ L, f i ~[l] g i
nil :
  ∀ (h : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i ~[l] g i),
    IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) [])) fun (x : α) ↦
      List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) [])
cons :
  ∀ (i : ι) (L : List ι)
    (ihL :
      ∀ (h : ∀ i ∈ L, f i ~[l] g i),
        IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L))
          fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L))
    (h : ∀ i_1 ∈ i :: L, f i_1 ~[l] g i_1),
    IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) (i :: L)))
      fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) (i :: L))
⊢ IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ List.prod (List.map (fun (x_1 : ι) ↦ f x_1 x) L)) fun (x : α) ↦
    List.prod (List.map (fun (x_1 : ι) ↦ g x_1 x) L)

Tactic:
induction L with
  | nil => simp [IsEquivalent.refl]
  | cons i L ihL =>
    simp only [List.forall_mem_cons, List.map_cons, List.prod_cons] at h ⊢
    exact h.1.mul (ihL h.2)

Premises used: List.map_cons, Asymptotics.IsEquivalent.refl, List.forall_mem_cons, List.prod_cons
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : NormedField β
l : Filter α
s : Multiset ι
f g : ι → α → β
h : ∀ i ∈ s, f i ~[l] g i
⊢ ∃ (l : List ι), (↑l : Multiset ι) = s

Tactic:
Quotient.mk_surjective s

Premises used: Multiset, Multiset.ofList, Quotient.mk_surjective
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : NormedField β
l : Filter α
s : Multiset ι
f g : ι → α → β
h : ∀ i ∈ s, f i ~[l] g i
obtain :
  ∀ (l_1 : List ι) (h : ∀ i ∈ (↑l_1 : Multiset ι), f i ~[l] g i),
    IsEquivalent.{u_1, u_3} (E' := β) l
      (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) (↑l_1 : Multiset ι))) fun (x : α) ↦
      Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (↑l_1 : Multiset ι))
⊢ IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) s))
    fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) s)

Tactic:
obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s

Premises used: List, Quotient.mk_surjective, rfl
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : NormedField β
l_1 : Filter α
f g : ι → α → β
l : List ι
h : ∀ i ∈ (↑l : Multiset ι), f i ~[l_1] g i
⊢ IsEquivalent.{u_1, u_3} (E' := β) l_1
    (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) (↑l : Multiset ι))) fun (x : α) ↦
    Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (↑l : Multiset ι))

Tactic:
listProd h

Premises used: Multiset.foldr, Multiset.prod, Asymptotics.IsEquivalent.listProd, List.prod
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : NormedField β
l_1 : Filter α
f g : ι → α → β
l : List ι
h : ∀ i ∈ (↑l : Multiset ι), f i ~[l_1] g i
⊢ IsEquivalent.{u_1, u_3} (E' := β) l_1
    (fun (x : α) ↦ Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ f x_1 x) (↑l : Multiset ι))) fun (x : α) ↦
    Multiset.prod (Multiset.map (fun (x_1 : ι) ↦ g x_1 x) (↑l : Multiset ι))

Tactic:
exact listProd h

Premises used: Asymptotics.IsEquivalent.listProd
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
ι : Type u_2
β : Type u_3
inst : NormedField β
l : Filter α
s : Finset ι
f g : ι → α → β
h : ∀ i ∈ s, f i ~[l] g i
⊢ IsEquivalent.{u_1, u_3} (E' := β) l (fun (x : α) ↦ ∏ i ∈ s, f i x) fun (x : α) ↦ ∏ i ∈ s, g i x

Tactic:
multisetProd h

Premises used: Asymptotics.IsEquivalent.multisetProd, Finset.prod
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
huv : u ~[l] v
rw :
  ∀ (huv : ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v),
    ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u⁻¹ =ᶠ[l] φ * v⁻¹
⊢ u⁻¹ ~[l] v⁻¹

Tactic:
rw [isEquivalent_iff_exists_eq_mul] at *

Premises used: Asymptotics.isEquivalent_iff_exists_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
huv : ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
rcases :
  ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 1)) (h : u =ᶠ[l] φ * v), ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u⁻¹ =ᶠ[l] φ * v⁻¹
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u⁻¹ =ᶠ[l] φ * v⁻¹

Tactic:
rcases huv with ⟨φ, hφ, h⟩
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
rw : ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1⁻¹)), u⁻¹ =ᶠ[l] φ * v⁻¹
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u⁻¹ =ᶠ[l] φ * v⁻¹

Tactic:
rw [← inv_one]

Premises used: inv_one
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ Ne.{u_3 + 1} (α := β) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
refine : u⁻¹ =ᶠ[l] (fun (x : α) ↦ (φ x)⁻¹) * v⁻¹
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1⁻¹)), u⁻¹ =ᶠ[l] φ * v⁻¹

Tactic:
refine ⟨fun x ↦ (φ x)⁻¹, Tendsto.inv₀ hφ (by simp), ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ EventuallyEq.{u_1, u_3} (β := β) l (fun (i : α) ↦ (u i)⁻¹) fun (i : α) ↦ ((φ * v) i)⁻¹

Tactic:
h.fun_inv

Premises used: Filter.EventuallyEq.fun_inv
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
h₁ : ∀ (x : α), HMul.hMul (α := α → β) (fun (x : α) ↦ (φ x)⁻¹) v⁻¹ x = ((φ * v) x)⁻¹
⊢ u⁻¹ =ᶠ[l] (fun (x : α) ↦ (φ x)⁻¹) * v⁻¹

Tactic:
convert! h.fun_inv

Premises used: Filter.EventuallyEq.fun_inv
-- Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x : α
⊢ HMul.hMul (α := α → β) (fun (x : α) ↦ (φ x)⁻¹) v⁻¹ x = ((φ * v) x)⁻¹

Tactic:
simp [mul_comm]

Premises used: mul_comm