awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
hg : g ∈ basis_begin
⊢ List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (basis_begin ++ [basis_end]) ∧
    ∀ (f : ℝ → ℝ), f ∈ basis_begin ∨ f = basis_end → Tendsto f atTop atTop

Tactic:
simp only [WellFormedBasis, List.concat_eq_append, List.mem_append, List.mem_cons,
      List.not_mem_nil, or_false] at h

Premises used: List.concat_eq_append, List.mem_append, or_false, List.mem_cons, Tactic.ComputeAsymptotics.WellFormedBasis, List.not_mem_nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
hg : g ∈ basis_begin
h :
  List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (basis_begin ++ [basis_end]) ∧
    ∀ (f : ℝ → ℝ), f ∈ basis_begin ∨ f = basis_end → Tendsto f atTop atTop
⊢ (Real.log ∘ basis_end) =o[atTop] (Real.log ∘ g)

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
hg : g ∈ basis_begin
h :
  List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (basis_begin ++ [basis_end]) ∧
    ∀ (f : ℝ → ℝ), f ∈ basis_begin ∨ f = basis_end → Tendsto f atTop atTop
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
exact h_comp.trans (by grind)

Premises used: Asymptotics.IsLittleO.trans
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
hg : g = basis_end
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g : ℝ → ℝ
h : WellFormedBasis []
h_comp : ∀ (g : ℝ → ℝ), List.head? [] = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
hg : Membership.mem (γ := Basis) [] g
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)

Tactic:
simp at hg
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h : WellFormedBasis (basis_hd :: basis_tl)
h_comp : ∀ (g : ℝ → ℝ), (basis_hd :: basis_tl).head? = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_hd :: basis_tl
⊢ (basis_hd :: basis_tl).head? = some basis_hd

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h : WellFormedBasis (basis_hd :: basis_tl)
h_comp : ∀ (g : ℝ → ℝ), (basis_hd :: basis_tl).head? = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_hd :: basis_tl
⊢ (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)

Tactic:
specialize h_comp basis_hd (by simp)
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h : WellFormedBasis (basis_hd :: basis_tl)
hg : g ∈ basis_hd :: basis_tl
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
⊢ g = basis_hd ∨ g ∈ basis_tl

Tactic:
simp only [List.mem_cons] at hg

Premises used: List.mem_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h : WellFormedBasis (basis_hd :: basis_tl)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g = basis_hd ∨ g ∈ basis_tl
cons : ∀ (hg : g = basis_hd), (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
cons₁ : ∀ (hg : g ∈ basis_tl), (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)

Tactic:
rcases hg with hg | hg
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h : WellFormedBasis (basis_hd :: basis_tl)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g = basis_hd
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)

Tactic:
simpa [hg]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h : WellFormedBasis (basis_hd :: basis_tl)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_tl
⊢ ((∀ a' ∈ basis_tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ basis_hd)) ∧
      List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) basis_tl) ∧
    Tendsto basis_hd atTop atTop ∧ ∀ a ∈ basis_tl, Tendsto a atTop atTop

Tactic:
simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h

Premises used: forall_eq_or_imp, List.pairwise_cons, List.mem_cons, Tactic.ComputeAsymptotics.WellFormedBasis
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_tl
h :
  ((∀ a' ∈ basis_tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ basis_hd)) ∧
      List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) basis_tl) ∧
    Tendsto basis_hd atTop atTop ∧ ∀ a ∈ basis_tl, Tendsto a atTop atTop
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ basis_hd)

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
f g basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_comp : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
hg : g ∈ basis_tl
h :
  ((∀ a' ∈ basis_tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ basis_hd)) ∧
      List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) basis_tl) ∧
    Tendsto basis_hd atTop atTop ∧ ∀ a ∈ basis_tl, Tendsto a atTop atTop
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)

Tactic:
exact .trans (by grind) h_comp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
f : ℝ → ℝ
h : WellFormedBasis basis
h_comp : ∀ (g : ℝ → ℝ), List.head? basis = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
g : ℝ → ℝ
hg : g ∈ basis
nil :
  ∀ (h : WellFormedBasis []) (h_comp : ∀ (g : ℝ → ℝ), List.head? [] = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f))
    (hg : Membership.mem (γ := Basis) [] g), (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
cons :
  ∀ (basis_hd : ℝ → ℝ) (basis_tl : List (ℝ → ℝ)) (h : WellFormedBasis (basis_hd :: basis_tl))
    (h_comp : ∀ (g : ℝ → ℝ), (basis_hd :: basis_tl).head? = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f))
    (hg : g ∈ basis_hd :: basis_tl), (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)

Tactic:
cases basis with
  | nil => simp at hg
  | cons basis_hd basis_tl =>
    specialize h_comp basis_hd (by simp)
    simp only [List.mem_cons] at hg
    rcases hg with hg | hg
    · simpa [hg]
    · simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h
      exact .trans (by grind) h_comp

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis.nil, forall_eq_or_imp, List.pairwise_cons, List.mem_cons, Tactic.ComputeAsymptotics.WellFormedBasis
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
h_left :
  List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) left ∧ ∀ f ∈ left, Tendsto f atTop atTop
h_right :
  List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) right ∧ ∀ f ∈ right, Tendsto f atTop atTop
h : ∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
left₁ : List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (left ++ right)
right₁ : ∀ f ∈ left ++ right, Tendsto f atTop atTop
⊢ List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (left ++ right) ∧
    ∀ f ∈ left ++ right, Tendsto f atTop atTop

Tactic:
constructor
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
h_left :
  List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) left ∧ ∀ f ∈ left, Tendsto f atTop atTop
h_right :
  List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) right ∧ ∀ f ∈ right, Tendsto f atTop atTop
h : ∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (left ++ right)

Tactic:
simpa [List.pairwise_append, h_left, h_right] using h

Premises used: List.pairwise_append
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
h_left :
  List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) left ∧ ∀ f ∈ left, Tendsto f atTop atTop
h_right :
  List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) right ∧ ∀ f ∈ right, Tendsto f atTop atTop
h : ∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ ∀ f ∈ left ++ right, Tendsto f atTop atTop

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
f : ℝ → ℝ
h_basis : WellFormedBasis basis
hf_tendsto : Tendsto f atTop atTop
hf : ∀ g ∈ basis, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
change : WellFormedBasis ([f] ++ basis)
⊢ WellFormedBasis (f :: basis)

Tactic:
change WellFormedBasis ([f] ++ basis)

Premises used: List.cons, Tactic.ComputeAsymptotics.WellFormedBasis, HAppend.hAppend, List.nil
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
f : ℝ → ℝ
h_basis : WellFormedBasis basis
hf_tendsto : Tendsto f atTop atTop
hf : ∀ g ∈ basis, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ WellFormedBasis [f]

Tactic:
simpa [WellFormedBasis]

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
f : ℝ → ℝ
h_basis : WellFormedBasis basis
hf_tendsto : Tendsto f atTop atTop
hf : ∀ g ∈ basis, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ ∀ f_1 ∈ [f], ∀ g ∈ basis, (Real.log ∘ g) =o[atTop] (Real.log ∘ f_1)

Tactic:
simpa
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
f : ℝ → ℝ
h_basis : WellFormedBasis basis
hf_tendsto : Tendsto f atTop atTop
hf : ∀ g ∈ basis, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ WellFormedBasis ([f] ++ basis)

Tactic:
exact append (by simpa [WellFormedBasis]) h_basis (by simpa)

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis.append
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ List.Sublist right (left ++ right)

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ WellFormedBasis (f :: right)

Tactic:
have : WellFormedBasis (f :: right) := cons (h.of_sublist (by simp)) hf_tendsto
    (compare_right_aux (h.of_sublist (by simp)) hf_comp_right)
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
⊢ List.Sublist left (left ++ right)

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
⊢ ∀ g ∈ left, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
apply compare_left_aux (h.of_sublist (by simp)) at hf_comp_left

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis.compare_left_aux, Tactic.ComputeAsymptotics.WellFormedBasis.of_sublist
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
hf_comp_left : ∀ g ∈ left, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ List.Sublist left (left ++ right)

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
hf_comp_left : ∀ g ∈ left, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
apply : ∀ f_1 ∈ left, ∀ g ∈ f :: right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f_1)
⊢ WellFormedBasis (left ++ f :: right)

Tactic:
apply append (h.of_sublist (by simp)) this

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis.append, Tactic.ComputeAsymptotics.WellFormedBasis.of_sublist
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
hf_comp_left : ∀ g ∈ left, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
g : ℝ → ℝ
hg : g ∈ left
⊢ ∀ (g_1 : ℝ → ℝ), (f :: right).head? = some g_1 → (Real.log ∘ g_1) =o[atTop] (Real.log ∘ g)

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
hf_comp_left : ∀ g ∈ left, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ ∀ f_1 ∈ left, ∀ g ∈ f :: right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f_1)

Tactic:
exact fun g hg ↦ compare_right_aux this (by grind)

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis.compare_right_aux
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
f : ℝ → ℝ
h : WellFormedBasis basis
hf_tendsto : Tendsto f atTop atTop
hf_comp : ∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ WellFormedBasis (basis ++ [])

Tactic:
simp [h]
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
f : ℝ → ℝ
h : WellFormedBasis basis
hf_tendsto : Tendsto f atTop atTop
hf_comp : ∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ ∀ (g : ℝ → ℝ), List.head? [] = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
h : WellFormedBasis basis
f : ℝ → ℝ
hf : f ∈ basis
⊢ Tendsto f atTop atTop

Tactic:
h.right f hf

Premises used: And.right
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
h : WellFormedBasis []
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ (f : ℝ → ℝ), Membership.mem (γ := Basis) [] f → 0 < f x

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
hd : ℝ → ℝ
tl : List (ℝ → ℝ)
ih : ∀ (h : WellFormedBasis tl), ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x
h : WellFormedBasis (hd :: tl)
⊢ ((∀ a' ∈ tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ hd)) ∧
      List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) tl) ∧
    Tendsto hd atTop atTop ∧ ∀ a ∈ tl, Tendsto a atTop atTop

Tactic:
simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h

Premises used: forall_eq_or_imp, List.pairwise_cons, List.mem_cons, Tactic.ComputeAsymptotics.WellFormedBasis
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
hd : ℝ → ℝ
tl : List (ℝ → ℝ)
ih : ∀ (h : WellFormedBasis tl), ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x
h :
  ((∀ a' ∈ tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ hd)) ∧
      List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) tl) ∧
    Tendsto hd atTop atTop ∧ ∀ a ∈ tl, Tendsto a atTop atTop
cons : ∀ᶠ (x : ℝ) in atTop, 0 < hd x ∧ ∀ a ∈ tl, 0 < a x
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ hd :: tl, 0 < f x

Tactic:
simp only [List.mem_cons, forall_eq_or_imp]

Premises used: forall_eq_or_imp, List.mem_cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
hd : ℝ → ℝ
tl : List (ℝ → ℝ)
ih : ∀ (h : WellFormedBasis tl), ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x
h :
  ((∀ a' ∈ tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ hd)) ∧
      List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) tl) ∧
    Tendsto hd atTop atTop ∧ ∀ a ∈ tl, Tendsto a atTop atTop
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < hd x ∧ ∀ a ∈ tl, 0 < a x

Tactic:
exact (h.right.left.eventually <| eventually_gt_atTop 0).and (ih (by tauto))

Premises used: Filter.Eventually.and, And.right, And.left, Filter.Tendsto.eventually, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
h : WellFormedBasis basis
nil : ∀ (h : WellFormedBasis []), ∀ᶠ (x : ℝ) in atTop, ∀ (f : ℝ → ℝ), Membership.mem (γ := Basis) [] f → 0 < f x
cons :
  ∀ (hd : ℝ → ℝ) (tl : List (ℝ → ℝ)) (ih : ∀ (h : WellFormedBasis tl), ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x)
    (h : WellFormedBasis (hd :: tl)), ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ hd :: tl, 0 < f x
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ basis, 0 < f x

Tactic:
induction basis with
  | nil => simp
  | cons hd tl ih =>
    simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h
    simp only [List.mem_cons, forall_eq_or_imp]
    exact (h.right.left.eventually <| eventually_gt_atTop 0).and (ih (by tauto))

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis.nil, forall_eq_or_imp, List.pairwise_cons, Tactic.ComputeAsymptotics.WellFormedBasis.cons, List.mem_cons, Tactic.ComputeAsymptotics.WellFormedBasis
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
h : WellFormedBasis (basis_hd :: basis_tl)
⊢ ∀ (x : ℝ), (basis_hd ∈ basis_hd :: basis_tl → 0 < basis_hd x) → 0 < basis_hd x

Tactic:
grind
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
hd : ℝ → ℝ
tl : Basis
h : WellFormedBasis (hd :: tl)
f : ℝ → ℝ
hf : f ∈ tl
rw :
  ∀
    (h :
      ((∀ a' ∈ tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ hd)) ∧
          List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) tl) ∧
        ∀ f ∈ hd :: tl, Tendsto f atTop atTop)
    {f : ℝ → ℝ} (hf : f ∈ tl), (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

Tactic:
rw [WellFormedBasis, List.pairwise_cons] at h

Premises used: List.pairwise_cons, Tactic.ComputeAsymptotics.WellFormedBasis
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
hd : ℝ → ℝ
tl : Basis
h :
  ((∀ a' ∈ tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ hd)) ∧
      List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) tl) ∧
    ∀ f ∈ hd :: tl, Tendsto f atTop atTop
f : ℝ → ℝ
hf : f ∈ tl
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

Tactic:
h.left.left _ hf

Premises used: And.left
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
hd : ℝ → ℝ
tl : Basis
h :
  ((∀ a' ∈ tl, (Real.log ∘ a') =o[atTop] (Real.log ∘ hd)) ∧
      List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) tl) ∧
    ∀ f ∈ hd :: tl, Tendsto f atTop atTop
f : ℝ → ℝ
hf : f ∈ tl
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

Tactic:
exact h.left.left _ hf

Premises used: And.left
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ basis_hd :: basis_tl ≠ []

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
hf_tendsto : Tendsto (Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) atTop atTop
hf_comp :
  ∀ (g : ℝ → ℝ),
    (basis_hd :: basis_tl).getLast? = some g →
      (Real.log ∘ Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) =o[atTop] (Real.log ∘ g)
⊢ WellFormedBasis (basis_hd :: basis_tl ++ [Real.log ∘ (basis_hd :: basis_tl).getLast ⋯])

Tactic:
apply h_basis.push

Premises used: Tactic.ComputeAsymptotics.WellFormedBasis.push
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ Tendsto (Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) atTop atTop

Tactic:
simp [Real.tendsto_log_atTop.comp, h_basis.right]

Premises used: And.right, Real.tendsto_log_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis_hd : ℝ → ℝ
basis_tl : Basis
h_basis : WellFormedBasis (basis_hd :: basis_tl)
g : ℝ → ℝ
hg : (basis_hd :: basis_tl).getLast? = some g
⊢ (Real.log ∘ Real.log ∘ (basis_hd :: basis_tl).getLast ⋯) =o[atTop] (Real.log ∘ g)

Tactic:
simpa [List.getLast_of_getLast?_eq_some hg] using Real.isLittleO_log_id_atTop.comp_tendsto <|
      Real.tendsto_log_atTop.comp <| h_basis.tendsto_atTop <| List.mem_of_getLast? hg

Premises used: Real.isLittleO_log_id_atTop, List.mem_of_getLast?, Tactic.ComputeAsymptotics.WellFormedBasis.tendsto_atTop, Asymptotics.IsLittleO.comp_tendsto, Real.tendsto_log_atTop, Filter.Tendsto.comp, List.getLast_of_getLast?_eq_some
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
⊢ List.Sublist [] nil.getBasis

Tactic:
simp
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
basis_hd : ℝ → ℝ
basis_tl : Basis
ex : BasisExtension basis_tl
ih : List.Sublist basis_tl ex.getBasis
⊢ (basis_hd :: basis_tl).Sublist (keep basis_hd ex).getBasis

Tactic:
simpa [getBasis] using ih

Premises used: Tactic.ComputeAsymptotics.BasisExtension.getBasis
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis basis_1 : Basis
f : ℝ → ℝ
ex : BasisExtension basis_1
ih : List.Sublist basis_1 ex.getBasis
⊢ List.Sublist basis_1 (insert f ex).getBasis

Tactic:
List.Sublist.cons _ ih

Premises used: Tactic.ComputeAsymptotics.BasisExtension.getBasis, List.Sublist.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis basis_1 : Basis
f : ℝ → ℝ
ex : BasisExtension basis_1
ih : List.Sublist basis_1 ex.getBasis
⊢ List.Sublist basis_1 (insert f ex).getBasis

Tactic:
exact List.Sublist.cons _ ih

Premises used: List.Sublist.cons
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
ex : BasisExtension basis
nil : List.Sublist [] BasisExtension.nil.getBasis
keep :
  ∀ (basis_hd : ℝ → ℝ) {basis_tl : Basis} (ex : BasisExtension basis_tl) (ih : List.Sublist basis_tl ex.getBasis),
    (basis_hd :: basis_tl).Sublist (BasisExtension.keep basis_hd ex).getBasis
insert :
  ∀ {basis : Basis} (f : ℝ → ℝ) (ex : BasisExtension basis) (ih : List.Sublist basis ex.getBasis),
    List.Sublist basis (BasisExtension.insert f ex).getBasis
⊢ List.Sublist basis ex.getBasis

Tactic:
induction ex with
  | nil => simp
  | keep _ ex ih => simpa [getBasis] using ih
  | insert _ ex ih => exact List.Sublist.cons _ ih

Premises used: Tactic.ComputeAsymptotics.BasisExtension.keep, Tactic.ComputeAsymptotics.BasisExtension.getBasis, Tactic.ComputeAsymptotics.BasisExtension.nil, Tactic.ComputeAsymptotics.BasisExtension.insert
-- Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Goal:
basis : Basis
f : ℝ → ℝ
ex_tl : BasisExtension basis
h_basis : WellFormedBasis (insert f ex_tl).getBasis
⊢ List.Sublist ex_tl.getBasis (insert f ex_tl).getBasis

Tactic:
simp [getBasis]

Premises used: Tactic.ComputeAsymptotics.BasisExtension.getBasis