awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : tensorObj.{v, u} (𝒞 := inst) p f₁ ≅ pf₁
η_g₁ : tensorObj.{v, u} (𝒞 := inst) p g₁ ≅ pf₁
η_f₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ f₂ ≅ pf₁f₂
η_g₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
⊢ p ◁ (η ▷ f₂ ≪≫ g₁ ◁ θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂
have ih_η₁ : p ◁ η ▷ f₂ ≪≫ normalizeIsoComp η_g₁ η_f₂ = normalizeIsoComp η_f₁ η_f₂
Tactic: apply naturality_comp
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : tensorObj.{v, u} (𝒞 := inst) p f₁ ≅ pf₁
η_g₁ : tensorObj.{v, u} (𝒞 := inst) p g₁ ≅ pf₁
η_f₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ f₂ ≅ pf₁f₂
η_g₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
ih_η₁ : p ◁ η ▷ f₂ ≪≫ normalizeIsoComp η_g₁ η_f₂ = normalizeIsoComp η_f₁ η_f₂
⊢ p ◁ (η ▷ f₂ ≪≫ g₁ ◁ θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂
have ih_θ₁ : p ◁ g₁ ◁ θ ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_g₁ η_f₂
Tactic: apply naturality_comp
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C
η : f₁ ≅ g₁
θ : f₂ ≅ g₂
η_f₁ : tensorObj.{v, u} (𝒞 := inst) p f₁ ≅ pf₁
η_g₁ : tensorObj.{v, u} (𝒞 := inst) p g₁ ≅ pf₁
η_f₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ f₂ ≅ pf₁f₂
η_g₂ : tensorObj.{v, u} (𝒞 := inst) pf₁ g₂ ≅ pf₁f₂
ih_η : p ◁ η ≪≫ η_g₁ = η_f₁
ih_θ : pf₁ ◁ θ ≪≫ η_g₂ = η_f₂
ih_η₁ : p ◁ η ▷ f₂ ≪≫ normalizeIsoComp η_g₁ η_f₂ = normalizeIsoComp η_f₁ η_f₂
ih_θ₁ : p ◁ g₁ ◁ θ ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_g₁ η_f₂
⊢ p ◁ (η ▷ f₂ ≪≫ g₁ ◁ θ) ≪≫ normalizeIsoComp η_g₁ η_g₂ = normalizeIsoComp η_f₁ η_f₂
have η_g : tensorObj.{v, u} (𝒞 := inst) p (tensorObj.{v, u} (𝒞 := inst) g₁ f₂) ≅ pf₁f₂
Tactic: apply naturality_comp
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g pf : C
η : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_g : tensorObj.{v, u} (𝒞 := inst) p g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ η_f = η_g
have rw : p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g
Tactic: rw [← ih]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
p f g pf : C
η : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) p f ≅ pf
η_g : tensorObj.{v, u} (𝒞 := inst) p g ≅ pf
ih : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g = η_g
have w : (p ◁ η.symm ≪≫ p ◁ η ≪≫ η_g).hom = η_g.hom
Tactic: apply Iso.ext
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g f' : C
η θ : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) f ≅ f'
η_g : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) g ≅ f'
h_η : tensorUnit.{v, u} C (𝒞 := inst) ◁ η ≪≫ η_g = η_f
h_θ : tensorUnit.{v, u} C (𝒞 := inst) ◁ θ ≪≫ η_g = η_f
⊢ η = θ
have w : η.hom = θ.hom
Tactic: apply Iso.ext
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g f' : C
η θ : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) f ≅ f'
η_g : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) g ≅ f'
h_η : tensorUnit.{v, u} C (𝒞 := inst) ◁ η ≪≫ η_g = η_f
h_θ : tensorUnit.{v, u} C (𝒞 := inst) ◁ θ ≪≫ η_g = η_f
⊢ η.hom = θ.hom
have simp : η.hom = Iso.inv (λ_ f) ≫ η_f.hom ≫ η_g.inv ≫ Iso.hom (λ_ g)
Tactic: calc
    η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_η)]
    _ = θ.hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_θ)]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
f g f' : C
η θ : f ≅ g
η_f : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) f ≅ f'
η_g : tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) g ≅ f'
h_η : tensorUnit.{v, u} C (𝒞 := inst) ◁ η ≪≫ η_g = η_f
h_θ : tensorUnit.{v, u} C (𝒞 := inst) ◁ θ ≪≫ η_g = η_f
simp : η.hom = Iso.inv (λ_ f) ≫ η_f.hom ≫ η_g.inv ≫ Iso.hom (λ_ g)
⊢ η.hom = θ.hom
have simp₁ : Iso.inv (λ_ f) ≫ η_f.hom ≫ η_g.inv ≫ Iso.hom (λ_ g) = θ.hom
Tactic: calc
    η.hom = (λ_ f).inv ≫ η_f.hom ≫ η_g.inv ≫ (λ_ g).hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_η)]
    _ = θ.hom := by
      simp [← reassoc_of% (congrArg Iso.hom h_θ)]
-- Lean 4 proof step from Mathlib.Tactic.CategoryTheory.Reassoc (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f g : X ⟶ Y
w : f = g
Z : C
h : Y ⟶ Z
⊢ f ≫ h = g ≫ h
have rw : g ≫ h = g ≫ h
Tactic: rw [w]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ f (c - x⁻¹)) atTop l
⊢ Tendsto f (𝓝[<] c) l
have h₁ : Eq (α := 𝕜 → α) (fun (x : 𝕜) ↦ f (c - x⁻¹)) (f ∘ (fun (x : 𝕜) ↦ c + x) ∘ Neg.neg ∘ Inv.inv)
Tactic: convert_to Tendsto (f ∘ (fun x ↦ c + x) ∘ Neg.neg ∘ Inv.inv) atTop l at h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ f (c - x⁻¹)) atTop l
h₁ : Eq (α := 𝕜 → α) (fun (x : 𝕜) ↦ f (c - x⁻¹)) (f ∘ (fun (x : 𝕜) ↦ c + x) ∘ Neg.neg ∘ Inv.inv)
⊢ Tendsto f (𝓝[<] c) l
have convert_to : ∀ (h : Tendsto (α := 𝕜) (f ∘ (fun (x : 𝕜) ↦ c + x) ∘ Neg.neg ∘ Inv.inv) atTop l), Tendsto f (𝓝[<] c) l
Tactic: convert_to Tendsto (f ∘ (fun x ↦ c + x) ∘ Neg.neg ∘ Inv.inv) atTop l at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
l : Filter α
f : 𝕜 → α
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ f (c - x⁻¹)) atTop l
⊢ Eq (α := 𝕜 → α) (fun (x : 𝕜) ↦ f (c - x⁻¹)) (f ∘ (fun (x : 𝕜) ↦ c + x) ∘ Neg.neg ∘ Inv.inv)
have h₁ : ∀ (x : 𝕜), f (c - x⁻¹) = (f ∘ (fun (x : 𝕜) ↦ c + x) ∘ Neg.neg ∘ Inv.inv) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Lemmas (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
f : 𝕜 → α
c : 𝕜
inst_5 : TopologicalSpace α
a b : α
h_neg : Tendsto (fun (x : 𝕜) ↦ f (c - x⁻¹)) atTop (𝓝 a)
h_pos : Tendsto (fun (x : 𝕜) ↦ f (c + x⁻¹)) atTop (𝓝 b)
h_eq : a = b
⊢ Tendsto f (𝓝[≠] c) (𝓝 a)
have apply : Tendsto (fun (x : 𝕜) ↦ f (c + x⁻¹)) atTop (𝓝 a)
Tactic: apply tendsto_nhdsNE_of_tendsto_atTop _ _ h_neg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
basis : Basis
f : ℝ → ℝ
h : WellFormedBasis basis
h_comp : ∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
g : ℝ → ℝ
hg : g ∈ basis
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
have inl : ∀ (h : WellFormedBasis []) (h_comp : ∀ (g : ℝ → ℝ), List.getLast? [] = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g))
  (hg : Membership.mem (γ := Basis) [] g), (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
Tactic: rcases basis.eq_nil_or_concat with rfl | ⟨basis_begin, basis_end, rfl⟩
Cleared hypotheses: basis, h, h_comp, hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
basis : Basis
f : ℝ → ℝ
h : WellFormedBasis basis
h_comp : ∀ (g : ℝ → ℝ), List.getLast? basis = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
g : ℝ → ℝ
hg : g ∈ basis
inl :
  ∀ (h : WellFormedBasis [])
    (h_comp : ∀ (g : ℝ → ℝ), List.getLast? [] = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g))
    (hg : Membership.mem (γ := Basis) [] g), (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
have inr : ∀ (basis_begin : List (ℝ → ℝ)) (basis_end : ℝ → ℝ) (h : WellFormedBasis (basis_begin.concat basis_end))
  (h_comp : ∀ (g : ℝ → ℝ), (basis_begin.concat basis_end).getLast? = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g))
  (hg : g ∈ basis_begin.concat basis_end), (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
Tactic: rcases basis.eq_nil_or_concat with rfl | ⟨basis_begin, basis_end, rfl⟩
Cleared hypotheses: basis, h, h_comp, hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (hypothesis)
Goal:
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
h_comp : ∀ (g : ℝ → ℝ), (basis_begin.concat basis_end).getLast? = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hg : g ∈ basis_begin.concat basis_end
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
have hg₁ : g ∈ basis_begin ∨ g = basis_end
Tactic: simp only [List.concat_eq_append, List.mem_append, List.mem_cons, List.not_mem_nil, or_false,
    List.getLast?_append, List.getLast?_singleton, Option.some_or, Option.some.injEq,
    forall_eq'] at hg h_comp
Cleared hypotheses: h_comp, hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (hypothesis)
Goal:
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
h_comp : ∀ (g : ℝ → ℝ), (basis_begin.concat basis_end).getLast? = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hg : g ∈ basis_begin.concat basis_end
hg₁ : g ∈ basis_begin ∨ g = basis_end
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
have h_comp₁ : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
Tactic: simp only [List.concat_eq_append, List.mem_append, List.mem_cons, List.not_mem_nil, or_false,
    List.getLast?_append, List.getLast?_singleton, Option.some_or, Option.some.injEq,
    forall_eq'] at hg h_comp
Cleared hypotheses: h_comp, hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
hg : g ∈ basis_begin ∨ g = basis_end
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
have inr : ∀ (hg : g ∈ basis_begin), (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
Tactic: rcases hg with hg | hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
hg : g ∈ basis_begin ∨ g = basis_end
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
inr : ∀ (hg : g ∈ basis_begin), (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
have inr₁ : ∀ (hg : g = basis_end), (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
Tactic: rcases hg with hg | hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (hypothesis)
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
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
have 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
Tactic: simp only [WellFormedBasis, List.concat_eq_append, List.mem_append, List.mem_cons,
      List.not_mem_nil, or_false] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (hypothesis)
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 ∘ g) =o[atTop] (Real.log ∘ f)
have h_comp₁ : (Real.log ∘ basis_hd) =o[atTop] (Real.log ∘ f)
Tactic: specialize h_comp basis_hd (by simp)
Cleared hypotheses: h_comp
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (hypothesis)
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)
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
have hg₁ : g = basis_hd ∨ g ∈ basis_tl
Tactic: simp only [List.mem_cons] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
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
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
have cons : ∀ (hg : g = basis_hd), (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
Tactic: rcases hg with hg | hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
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)
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
have cons₁ : ∀ (hg : g ∈ basis_tl), (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
Tactic: rcases hg with hg | hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (hypothesis)
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
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
have 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
Tactic: simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
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
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
have 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)
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
Cleared hypotheses: basis, h, h_comp, hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
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)
⊢ (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
have 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)
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
Cleared hypotheses: basis, h, h_comp, hg
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
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) ∧
    ∀ f ∈ left ++ right, Tendsto f atTop atTop
have left₁ : List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (left ++ right)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
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)
⊢ List.Pairwise (fun (x y : ℝ → ℝ) ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (left ++ right) ∧
    ∀ f ∈ left ++ right, Tendsto f atTop atTop
have right₁ : ∀ f ∈ left ++ right, Tendsto f atTop atTop
Tactic: constructor
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
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)
have change : WellFormedBasis ([f] ++ basis)
Tactic: change WellFormedBasis ([f] ++ basis)
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (hypothesis)
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 (left ++ f :: right)
have this : 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)
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (hypothesis)
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)
⊢ WellFormedBasis (left ++ f :: right)
have hf_comp_left₁ : ∀ g ∈ left, (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
Tactic: apply compare_left_aux (h.of_sublist (by simp)) at hf_comp_left
Cleared hypotheses: hf_comp_left
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
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)
⊢ WellFormedBasis (left ++ f :: right)
have apply : ∀ f_1 ∈ left, ∀ g ∈ f :: right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f_1)
Tactic: apply append (h.of_sublist (by simp)) this
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (hypothesis)
Goal:
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
have 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
Tactic: simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
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, ∀ f ∈ hd :: tl, 0 < f x
have cons : ∀ᶠ (x : ℝ) in atTop, 0 < hd x ∧ ∀ a ∈ tl, 0 < a x
Tactic: simp only [List.mem_cons, forall_eq_or_imp]
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
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
⊢ WellFormedBasis tl
have 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
Tactic: tauto
Cleared hypotheses: ih, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
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
⊢ WellFormedBasis tl
have 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
Tactic: tauto
Cleared hypotheses: ih, h
-- Lean 4 proof step from Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis (goal)
Goal:
basis : Basis
h : WellFormedBasis basis
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ basis, 0 < f x
have nil : ∀ (h : WellFormedBasis []), ∀ᶠ (x : ℝ) in atTop, ∀ (f : ℝ → ℝ), Membership.mem (γ := Basis) [] f → 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))
Cleared hypotheses: basis, h