awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
hg : ∀ x ∈ Ioo a b, g x ≠ 0
c : (x : ℝ) → ℝ
hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this : ∀ x ∈ Ioo a b, ((fun (x' : ℝ) ↦ f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
⊢ c x ∈ Ioi a
have this₁ : a < c x ∧ c x < x
Tactic: have := cmp x hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
hg : ∀ x ∈ Ioo a b, g x ≠ 0
c : (x : ℝ) → ℝ
hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)
this_1 : ∀ x ∈ Ioo a b, ((fun (x' : ℝ) ↦ f' x' / g' x') ∘ c) x = f x / g x
cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x
x : ℝ
hx : x ∈ Ioo a b
this : a < c x ∧ c x < x
⊢ a < c x
have linarith : c x ≤ a → a - c x + (c x - a) = 0
Tactic: linarith [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have refine_1 : Tendsto f (𝓝[>] a) (𝓝 0)
Tactic: refine lhopital_zero_right_on_Ioo hab hff' hgg' hg' ?_ ?_ hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
refine_1 : Tendsto f (𝓝[>] a) (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have refine_2 : Tendsto g (𝓝[>] a) (𝓝 0)
Tactic: refine lhopital_zero_right_on_Ioo hab hff' hgg' hg' ?_ ?_ hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
⊢ Tendsto f (𝓝[>] a) (𝓝 0)
have refine_1 : Tendsto f (𝓝[Ioo a b] a) (𝓝 (f a))
Tactic: rw [← hfa, ← nhdsWithin_Ioo_eq_nhdsGT hab]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ico a b)
hcg : ContinuousOn g (Ico a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfa : f a = 0
hga : g a = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[>] a) l
⊢ Tendsto g (𝓝[>] a) (𝓝 0)
have refine_2 : Tendsto g (𝓝[Ioo a b] a) (𝓝 (g a))
Tactic: rw [← hga, ← nhdsWithin_Ioo_eq_nhdsGT hab]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l
have hdnf : ∀ x ∈ -Ioo a b, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
Tactic: have hdnf : ∀ x ∈ -Ioo a b, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x := fun x hx =>
    comp x (hff' (-x) hx) (hasDerivAt_neg x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ -Ioo a b, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l
have hdng : ∀ x ∈ -Ioo a b, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
Tactic: have hdng : ∀ x ∈ -Ioo a b, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x := fun x hx =>
    comp x (hgg' (-x) hx) (hasDerivAt_neg x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ -Ioo a b, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ -Ioo a b, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l
have hdnf₁ : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
Tactic: rw [neg_Ioo] at hdnf hdng
Cleared hypotheses: hdnf, hdng
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ -Ioo a b, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ -Ioo a b, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
hdnf₁ : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l
have hdng₁ : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
Tactic: rw [neg_Ioo] at hdnf hdng
Cleared hypotheses: hdnf, hdng
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ f' (-x) * -1 / (g' (-x) * -1)) (𝓝[>] (-b)) l
have simp : Tendsto (fun (x : ℝ) ↦ f' (-x) / g' (-x)) (𝓝[>] (-b)) l
Tactic: simp only [neg_div_neg_eq, mul_one, mul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l
have this : Tendsto (fun (x : ℝ) ↦ (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[>] (-b)) l
Tactic: have := lhopital_zero_right_on_Ioo (neg_lt_neg hab) hdnf hdng (by grind)
    (hfb.comp tendsto_neg_nhdsGT_neg) (hgb.comp tendsto_neg_nhdsGT_neg)
    (by
      simp only [neg_div_neg_eq, mul_one, mul_neg]
      exact hdiv.comp tendsto_neg_nhdsGT_neg)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : Tendsto f (𝓝[<] b) (𝓝 0)
hgb : Tendsto g (𝓝[<] b) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
hdnf : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ Ioo (-b) (-a), HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
this : Tendsto (fun (x : ℝ) ↦ (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) (𝓝[>] (-b)) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l
have this₁ : Tendsto ((fun (x : ℝ) ↦ (f ∘ Neg.neg) x / (g ∘ Neg.neg) x) ∘ Neg.neg) (𝓝[<] b) l
Tactic: have := this.comp tendsto_neg_nhdsLT
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l
have refine_1 : Tendsto f (𝓝[<] b) (𝓝 0)
Tactic: refine lhopital_zero_left_on_Ioo hab hff' hgg' hg' ?_ ?_ hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
refine_1 : Tendsto f (𝓝[<] b) (𝓝 0)
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] b) l
have refine_2 : Tendsto g (𝓝[<] b) (𝓝 0)
Tactic: refine lhopital_zero_left_on_Ioo hab hff' hgg' hg' ?_ ?_ hdiv
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
⊢ Tendsto f (𝓝[<] b) (𝓝 0)
have refine_1 : Tendsto f (𝓝[Ioo a b] b) (𝓝 (f b))
Tactic: rw [← hfb, ← nhdsWithin_Ioo_eq_nhdsLT hab]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a b : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hab : a < b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hcf : ContinuousOn f (Ioc a b)
hcg : ContinuousOn g (Ioc a b)
hg' : ∀ x ∈ Ioo a b, g' x ≠ 0
hfb : f b = 0
hgb : g b = 0
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) (𝓝[<] b) l
⊢ Tendsto g (𝓝[<] b) (𝓝 0)
have refine_2 : Tendsto g (𝓝[Ioo a b] b) (𝓝 (g b))
Tactic: rw [← hgb, ← nhdsWithin_Ioo_eq_nhdsLT hab]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have obtain : ∀ (a' : ℝ) (haa' : a < a') (ha' : 0 < a'), Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
Tactic: obtain ⟨a', haa', ha'⟩ : ∃ a', a < a' ∧ 0 < a' := ⟨1 + max a 0,
    ⟨lt_of_le_of_lt (le_max_left a 0) (lt_one_add _),
      lt_of_le_of_lt (le_max_right a 0) (lt_one_add _)⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
Tactic: have fact1 : ∀ x : ℝ, x ∈ Ioo 0 a'⁻¹ → x ≠ 0 := fun _ hx => (ne_of_lt hx.1).symm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
Tactic: have fact2 (x) (hx : x ∈ Ioo 0 a'⁻¹) : a < x⁻¹ := lt_trans haa' ((lt_inv_comm₀ ha' hx.1).mpr hx.2)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
Tactic: have hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(x ^ 2)⁻¹) x := fun x hx =>
    comp x (hff' x⁻¹ <| fact2 x hx) (hasDerivAt_inv <| fact1 x hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
Tactic: have hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(x ^ 2)⁻¹) x := fun x hx =>
    comp x (hgg' x⁻¹ <| fact2 x hx) (hasDerivAt_inv <| fact1 x hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
x : ℝ
hx : x ∈ Ioo 0 a'⁻¹
⊢ g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ ≠ 0
have refine : g' x⁻¹ ≠ 0
Tactic: refine mul_ne_zero ?_ (neg_ne_zero.mpr <| inv_ne_zero <| pow_ne_zero _ <| fact1 x hx)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
⊢ Tendsto (fun (x : ℝ) ↦ f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)) (𝓝[>] 0) l
have refine : EventuallyEq (β := ℝ) (𝓝[>] 0) ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) fun (x : ℝ) ↦
  f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
Tactic: refine (tendsto_congr' ?_).mp (hdiv.comp tendsto_inv_nhdsGT_zero)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
x : ℝ
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x →
    ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) x =
      f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
have h : ∀ (hx : 0 < x),
  ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) x =
    f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
Tactic: (hx : 0 < x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
⊢ EventuallyEq (β := ℝ) (𝓝[>] 0) ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) fun (x : ℝ) ↦
    f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
have h : ∀ (x : ℝ) (hx : 0 < x),
  ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) x =
    f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
Tactic: filter_upwards [self_mem_nhdsWithin] with x (hx : 0 < x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
x : ℝ
hx : 0 < x
⊢ ((fun (x : ℝ) ↦ f' x / g' x) ∘ fun (x : ℝ) ↦ x⁻¹) x =
    f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
have h : f' x⁻¹ / g' x⁻¹ = f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
Tactic: simp only [Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (goal)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
x : ℝ
hx : 0 < x
⊢ f' x⁻¹ / g' x⁻¹ = f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹ / (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹)
have h : -(HPow.hPow (β := ℕ) x 2)⁻¹ ≠ 0
Tactic: rw [mul_div_mul_right]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have this : Tendsto (fun (x : ℝ) ↦ (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[>] 0) l
Tactic: have := lhopital_zero_right_on_Ioo (inv_pos.mpr ha') hdnf hdng
    (by
      intro x hx
      refine mul_ne_zero ?_ (neg_ne_zero.mpr <| inv_ne_zero <| pow_ne_zero _ <| fact1 x hx)
      exact hg' _ (fact2 x hx))
    (hftop.comp tendsto_inv_nhdsGT_zero) (hgtop.comp tendsto_inv_nhdsGT_zero)
    (by
      refine (tendsto_congr' ?_).mp (hdiv.comp tendsto_inv_nhdsGT_zero)
      filter_upwards [self_mem_nhdsWithin] with x (hx : 0 < x)
      simp only [Function.comp_def]
      rw [mul_div_mul_right]
      exact neg_ne_zero.mpr (by positivity))
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Ioi a, g' x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atTop l
a' : ℝ
haa' : a < a'
ha' : 0 < a'
fact1 : ∀ x ∈ Ioo 0 a'⁻¹, x ≠ 0
fact2 : ∀ (x : ℝ) (hx : x ∈ Ioo 0 a'⁻¹), a < x⁻¹
hdnf : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (f ∘ Inv.inv) (f' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
hdng : ∀ x ∈ Ioo 0 a'⁻¹, HasDerivAt (g ∘ Inv.inv) (g' x⁻¹ * -(HPow.hPow (β := ℕ) x 2)⁻¹) x
this : Tendsto (fun (x : ℝ) ↦ (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) (𝓝[>] 0) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l
have this₁ : Tendsto (α := ℝ) ((fun (x : ℝ) ↦ (f ∘ Inv.inv) x / (g ∘ Inv.inv) x) ∘ fun (r : ℝ) ↦ r⁻¹) atTop l
Tactic: have := this.comp tendsto_inv_atTop_nhdsGT_zero
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Iio a, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
Tactic: have hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x := fun x hx =>
    comp x (hff' (-x) hx) (hasDerivAt_neg x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Iio a, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hdng : ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
Tactic: have hdng : ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x := fun x hx =>
    comp x (hgg' (-x) hx) (hasDerivAt_neg x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LHopital (hypothesis)
Goal:
a : ℝ
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
hgg' : ∀ x ∈ Iio a, HasDerivAt g (g' x) x
hg' : ∀ x ∈ Iio a, g' x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ f' x / g' x) atBot l
hdnf : ∀ x ∈ -Iio a, HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
hdng : ∀ x ∈ -Iio a, HasDerivAt (g ∘ Neg.neg) (g' (-x) * -1) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l
have hdnf₁ : ∀ x ∈ Ioi (-a), HasDerivAt (f ∘ Neg.neg) (f' (-x) * -1) x
Tactic: rw [neg_Iio] at hdnf hdng
Cleared hypotheses: hdnf, hdng