-- 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
inl :
  ∀ (ih : ¬WellFormedBasis 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) → WellFormedBasis tl
inr :
  ∀ (ih : ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x),
    (∀ 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) → WellFormedBasis tl
inl₁ :
  ∀ (ih : ¬WellFormedBasis 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) → WellFormedBasis tl
inr₁ :
  ∀ (ih : ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x),
    (∀ 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) → WellFormedBasis tl
inl₂ :
  ∀ (ih : ¬WellFormedBasis 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) → WellFormedBasis tl
inr₂ :
  ∀ (ih : ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x),
    (∀ 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) → WellFormedBasis tl
inl₃ inl₄ inl₅ :
  ∀ (ih : ¬WellFormedBasis 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) → WellFormedBasis tl
inr₃ inr₄ inr₅ :
  ∀ (ih : ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x),
    (∀ 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) → WellFormedBasis tl
inl₆ inl₇ :
  ∀ (ih : ¬WellFormedBasis 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) → WellFormedBasis tl
inr₆ inr₇ :
  ∀ (ih : ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x),
    (∀ 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) → WellFormedBasis tl
⊢ WellFormedBasis tl

Tactic:
tauto