awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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
⊢ 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))
have 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)
Tactic: simp only [List.forall_mem_cons, List.map_cons, List.prod_cons] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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
⊢ 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)
have 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) [])
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)
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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) [])
⊢ 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)
have 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))
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)
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
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
⊢ 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)
have 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 ι))
Tactic: obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
huv : u ~[l] v
⊢ u⁻¹ ~[l] v⁻¹
have rw : ∀ (huv : ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v), ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u⁻¹ =ᶠ[l] φ * v⁻¹
Tactic: rw [isEquivalent_iff_exists_eq_mul] at *
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
huv : ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u⁻¹ =ᶠ[l] φ * v⁻¹
have rcases : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 1)) (h : u =ᶠ[l] φ * v), ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u⁻¹ =ᶠ[l] φ * v⁻¹
Tactic: rcases huv with ⟨φ, hφ, h⟩
Cleared hypotheses: huv
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u⁻¹ =ᶠ[l] φ * v⁻¹
have rw : ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1⁻¹)), u⁻¹ =ᶠ[l] φ * v⁻¹
Tactic: rw [← inv_one]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1⁻¹)), u⁻¹ =ᶠ[l] φ * v⁻¹
have refine : u⁻¹ =ᶠ[l] (fun (x : α) ↦ (φ x)⁻¹) * v⁻¹
Tactic: refine ⟨fun x ↦ (φ x)⁻¹, Tendsto.inv₀ hφ (by simp), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
⊢ u⁻¹ =ᶠ[l] (fun (x : α) ↦ (φ x)⁻¹) * v⁻¹
have h₁ : ∀ (x : α), HMul.hMul (α := α → β) (fun (x : α) ↦ (φ x)⁻¹) v⁻¹ x = ((φ * v) x)⁻¹
Tactic: convert! h.fun_inv
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
n : ℕ
⊢ t ^ n ~[l] u ^ n
have zero : HPow.hPow (β := ℕ) t 0 ~[l] HPow.hPow (β := ℕ) u 0
Tactic: induction n with
  | zero => simpa using IsEquivalent.refl
  | succ _ ih => simpa [pow_succ] using ih.mul h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_3
inst : NormedField β
t u : α → β
l : Filter α
h : t ~[l] u
n : ℕ
zero : HPow.hPow (β := ℕ) t 0 ~[l] HPow.hPow (β := ℕ) u 0
⊢ t ^ n ~[l] u ^ n
have succ : ∀ (n : ℕ) (ih : t ^ n ~[l] u ^ n), t ^ (n + 1) ~[l] u ^ (n + 1)
Tactic: induction n with
  | zero => simpa using IsEquivalent.refl
  | succ _ ih => simpa [pow_succ] using ih.mul h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
⊢ Tendsto v l atBot
have h : v = Neg.neg ∘ fun (x : α) ↦ -v x
Tactic: convert! tendsto_neg_atTop_atBot.comp (huv.neg.tendsto_atTop <| tendsto_neg_atBot_atTop.comp hu)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : OrderTopology β
huv : u ~[l] v
hu : Tendsto u l atBot
⊢ v = Neg.neg ∘ fun (x : α) ↦ -v x
have h : ∀ (x : α), v x = (Neg.neg ∘ fun (x : α) ↦ -v x) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
⊢ ∃ (φ : α → β), (∀ᶠ (x : α) in l, 0 < φ x) ∧ u =ᶠ[l] φ * v
have obtain : ∀ (φ : α → β) (hφ : Tendsto φ l (𝓝 1)) (h_eq : u =ᶠ[l] φ * v), ∃ (φ : α → β), (∀ᶠ (x : α) in l, 0 < φ x) ∧ u =ᶠ[l] φ * v
Tactic: obtain ⟨φ, hφ, h_eq⟩ := h.exists_eq_mul
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, 0 ≤ v t
⊢ ∀ᶠ (x : α) in l, 0 ≤ u x
have obtain : ∀ (φ : α → β) (hφ : ∀ᶠ (x : α) in l, 0 < φ x) (h_eq : u =ᶠ[l] φ * v), ∀ᶠ (x : α) in l, 0 ≤ u x
Tactic: obtain ⟨φ, hφ, h_eq⟩ := h.exists_pos_eq_mul
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, 0 < v t
⊢ ∀ᶠ (x : α) in l, 0 < u x
have obtain : ∀ (φ : α → β) (hφ : ∀ᶠ (x : α) in l, 0 < φ x) (h_eq : u =ᶠ[l] φ * v), ∀ᶠ (x : α) in l, 0 < u x
Tactic: obtain ⟨φ, hφ, h_eq⟩ := h.exists_pos_eq_mul
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, v t ≤ 0
⊢ ∀ᶠ (x : α) in l, u x ≤ 0
have obtain : ∀ (φ : α → β) (hφ : ∀ᶠ (x : α) in l, 0 < φ x) (h_eq : u =ᶠ[l] φ * v), ∀ᶠ (x : α) in l, u x ≤ 0
Tactic: obtain ⟨φ, hφ, h_eq⟩ := h.exists_pos_eq_mul
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedField β
inst_1 : LinearOrder β
inst_2 : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst_3 : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, v t < 0
⊢ ∀ᶠ (x : α) in l, u x < 0
have obtain : ∀ (φ : α → β) (hφ : ∀ᶠ (x : α) in l, 0 < φ x) (h_eq : u =ᶠ[l] φ * v), ∀ᶠ (x : α) in l, u x < 0
Tactic: obtain ⟨φ, hφ, h_eq⟩ := h.exists_pos_eq_mul
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
⊢ u + t ~[l] v + w
have simp : (u - v + (t - w)) =o[l] (v + w)
Tactic: simp only [IsEquivalent, add_sub_add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
| IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ (u - v) x + (t - w) x) fun (x : α) ↦ v x + w x
have h : ∀ (x : α), v x + w x
Tactic: enter [3, x]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
x : α
| v x + w x
have h : |v x| + |w x|
Tactic: rw [← abs_eq_self.mpr (hu x), ← abs_eq_self.mpr (hw x)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
| IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ (u - v) x + (t - w) x) fun (x : α) ↦ v x + w x
have h : ∀ (x : α), |v x| + |w x|
Tactic: enter [3, x]; rw [← abs_eq_self.mpr (hu x), ← abs_eq_self.mpr (hw x)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.AsymptoticEquivalent (goal)
Goal:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
⊢ IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ (u - v) x + (t - w) x) fun (x : α) ↦ v x + w x
have conv : IsLittleO (E := ℝ) (F := ℝ) l (fun (x : α) ↦ (u - v) x + (t - w) x) fun (x : α) ↦ |v x| + |w x|
Tactic: conv => enter [3, x]; rw [← abs_eq_self.mpr (hu x), ← abs_eq_self.mpr (hw x)]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
⊢ IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have rw : (∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: rw [IsBigOWith_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
F : Type u_4
inst : Norm E
inst_1 : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =O[l] g ↔ ∃ (c : ℝ), IsBigOWith c l f g
have rw : (∃ (c : ℝ), IsBigOWith c l f g) ↔ ∃ (c : ℝ), IsBigOWith c l f g
Tactic: rw [IsBigO_def]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
⊢ f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have refine : ∀ (h : f =O[l] g), ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: refine ⟨fun h => ?mp, fun h => ?mpr⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
refine : ∀ (h : f =O[l] g), ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have refine₁ : ∀ (h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖), f =O[l] g
Tactic: refine ⟨fun h => ?mp, fun h => ?mpr⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (hypothesis)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : f =O[l] g
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have h₁ : ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: rw [isBigO_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have obtain : ∀ (c : ℝ) (hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖), ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: obtain ⟨c, hc⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have refine : ∀ᶠ (x : α) in l, ‖f x‖ ≤ max c 1 * ‖g x‖
Tactic: refine ⟨max c 1, zero_lt_one.trans_le (le_max_right _ _), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ max c 1 * ‖g x‖
have h : ∀ (x : α) (hx : ‖f x‖ ≤ c * ‖g x‖), ‖f x‖ ≤ max c 1 * ‖g x‖
Tactic: filter_upwards [hc] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x‖ ≤ max c 1 * ‖g x‖
have h : c * ‖g x‖ ≤ max c 1 * ‖g x‖
Tactic: apply hx.trans
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c * ‖g x‖ ≤ max c 1 * ‖g x‖
have h : c ≤ max c 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g
have rw : ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: rw [isBigO_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have obtain : ∀ c > 0, ∀ (hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖), ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: obtain ⟨c, ⟨_, hc⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g
have case : ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: case mpr =>
    rw [isBigO_iff]
    obtain ⟨c, ⟨_, hc⟩⟩ := h
    exact ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
case case₁ case₂ : ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g
have case₃ : ∀ c > 0, ∀ (hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖), ∃ (c : ℝ), ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: case mpr =>
    rw [isBigO_iff]
    obtain ⟨c, ⟨_, hc⟩⟩ := h
    exact ⟨c, hc⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
⊢ f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
have refine : ∀ (h : f =O[l] g), ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
Tactic: refine ⟨fun h => ?mp, fun h => ?mpr⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
refine : ∀ (h : f =O[l] g), ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
have refine₁ : ∀ (h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖), f =O[l] g
Tactic: refine ⟨fun h => ?mp, fun h => ?mpr⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (hypothesis)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : f =O[l] g
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
have h₁ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: rw [isBigO_iff'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
have obtain : ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖), ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
Tactic: obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
have refine : ∀ᶠ (x : α) in l, c⁻¹ * ‖f x‖ ≤ ‖g x‖
Tactic: refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∀ᶠ (x : α) in l, c⁻¹ * ‖f x‖ ≤ ‖g x‖
have h : ∀ (x : α) (hx : ‖f x‖ ≤ c * ‖g x‖), c⁻¹ * ‖f x‖ ≤ ‖g x‖
Tactic: filter_upwards [hc] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ f =O[l] g
have rw : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: rw [isBigO_iff']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have obtain : ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖), ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
have refine : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c⁻¹ * ‖g x‖
Tactic: refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c⁻¹ * ‖g x‖
have h : ∀ (x : α) (hx : c * ‖f x‖ ≤ ‖g x‖), ‖f x‖ ≤ c⁻¹ * ‖g x‖
Tactic: filter_upwards [hc] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
x : α
hx : c * ‖f x‖ ≤ ‖g x‖
⊢ ‖f x‖ ≤ c⁻¹ * ‖g x‖
have h : ∀ (hx : c⁻¹⁻¹ * ‖f x‖ ≤ ‖g x‖), ‖f x‖ ≤ c⁻¹ * ‖g x‖
Tactic: rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc_pos : c > 0
hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
x : α
hx : c * ‖f x‖ ≤ ‖g x‖
h : ∀ (hx : c⁻¹⁻¹ * ‖f x‖ ≤ ‖g x‖), ‖f x‖ ≤ c⁻¹ * ‖g x‖
⊢ ‖f x‖ ≤ c⁻¹ * ‖g x‖
have h₁ : ∀ (hx : ‖f x‖ ≤ c⁻¹ * ‖g x‖), ‖f x‖ ≤ c⁻¹ * ‖g x‖
Tactic: rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
⊢ f =O[l] g
have case : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: case mpr =>
    rw [isBigO_iff']
    obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
    refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
    filter_upwards [hc] with x hx
    rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.Defs (goal)
Goal:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst : Norm E
inst_1 : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c > 0, ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
case case₁ case₂ : ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ f =O[l] g
have case₃ : ∀ (c : ℝ) (hc_pos : c > 0) (hc : ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖), ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Tactic: case mpr =>
    rw [isBigO_iff']
    obtain ⟨c, ⟨hc_pos, hc⟩⟩ := h
    refine ⟨c⁻¹, ⟨by positivity, ?_⟩⟩
    filter_upwards [hc] with x hx
    rwa [← inv_inv c, inv_mul_le_iff₀ (by positivity)] at hx
Cleared hypotheses: h