a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → HasDerivAt f (f' y) y
hgg' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → HasDerivAt g (g' y) y
hg' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → g' y ≠ 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
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (f' x) x
hgg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (g' x) x
hg' : ∀ᶠ (x : ℝ) in atTop, 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
rw [eventually_iff_exists_mem] at *
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → HasDerivAt g (g' y) y
hg' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → g' y ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
⊢ Tendsto (fun x => f x / g x) atTop l
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hff' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → HasDerivAt f (f' y) y
hgg' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → HasDerivAt g (g' y) y
hg' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → g' y ≠ 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
rcases hff' with ⟨s₁, hs₁, hff'⟩
case intro.intro.intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hg' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → g' y ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
⊢ Tendsto (fun x => f x / g x) atTop l
case intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hgg' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → HasDerivAt g (g' y) y
hg' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → g' y ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
⊢ Tendsto (fun x => f x / g x) atTop l
rcases hgg' with ⟨s₂, hs₂, hgg'⟩
case intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
⊢ Tendsto (fun x => f x / g x) atTop l
case intro.intro.intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hg' : ∃ v, v ∈ atTop ∧ ∀ (y : ℝ), y ∈ v → g' y ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
⊢ Tendsto (fun x => f x / g x) atTop l
rcases hg' with ⟨s₃, hs₃, hg'⟩
case intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
⊢ Tendsto (fun x => f x / g x) atTop l
case intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
⊢ Tendsto (fun x => f x / g x) atTop l
let s := s₁ ∩ s₂ ∩ s₃
case intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
hs : s ∈ atTop
⊢ Tendsto (fun x => f x / g x) atTop l
case intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
⊢ Tendsto (fun x => f x / g x) atTop l
have hs : s ∈ atTop := inter_mem (inter_mem hs₁ hs₂) hs₃
case intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
hs : ∃ a, ∀ (b : ℝ), b ≥ a → b ∈ s
⊢ Tendsto (fun x => f x / g x) atTop l
case intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
hs : s ∈ atTop
⊢ Tendsto (fun x => f x / g x) atTop l
rw [mem_atTop_sets] at hs
case intro.intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l✝ : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l✝
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ (b : ℝ), b ≥ l → b ∈ s
⊢ Tendsto (fun x => f x / g x) atTop l✝
case intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
hs : ∃ a, ∀ (b : ℝ), b ≥ a → b ∈ s
⊢ Tendsto (fun x => f x / g x) atTop l
rcases hs with ⟨l, hl⟩
case intro.intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l✝ : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l✝
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ (b : ℝ), b ≥ l → b ∈ s
hl' : Ioi l ⊆ s
⊢ Tendsto (fun x => f x / g x) atTop l✝
case intro.intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l✝ : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l✝
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ (b : ℝ), b ≥ l → b ∈ s
⊢ Tendsto (fun x => f x / g x) atTop l✝
have hl' : Ioi l ⊆ s := fun x hx => hl x (le_of_lt hx)
no goals
case intro.intro.intro.intro.intro.intro.intro
a b : ℝ
hab : a < b
l✝ : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l✝
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ (b : ℝ), b ≥ l → b ∈ s
hl' : Ioi l ⊆ s
⊢ Tendsto (fun x => f x / g x) atTop l✝
refine' lhopital_zero_atTop_on_Ioi _ _ (fun x hx => hg' x <| (hl' hx).2) hftop hgtop hdiv <;>
  intro x hx <;> apply_assumption <;> first | exact (hl' hx).1.1| exact (hl' hx).1.2
case intro.intro.intro.intro.intro.intro.intro.refine'_2.a
a b : ℝ
hab : a < b
l✝ : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l✝
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ (b : ℝ), b ≥ l → b ∈ s
hl' : Ioi l ⊆ s
x : ℝ
hx : x ∈ Ioi l
⊢ x ∈ s₂
case intro.intro.intro.intro.intro.intro.intro.refine'_2.a
a b : ℝ
hab : a < b
l✝ : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l✝
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ (b : ℝ), b ≥ l → b ∈ s
hl' : Ioi l ⊆ s
x : ℝ
hx : x ∈ Ioi l
⊢ x ∈ s₂
exact (hl' hx).1.1
no goals
case intro.intro.intro.intro.intro.intro.intro.refine'_2.a
a b : ℝ
hab : a < b
l✝ : Filter ℝ
f f' g g' : ℝ → ℝ
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun x => f' x / g' x) atTop l✝
s₁ : Set ℝ
hs₁ : s₁ ∈ atTop
hff' : ∀ (y : ℝ), y ∈ s₁ → HasDerivAt f (f' y) y
s₂ : Set ℝ
hs₂ : s₂ ∈ atTop
hgg' : ∀ (y : ℝ), y ∈ s₂ → HasDerivAt g (g' y) y
s₃ : Set ℝ
hs₃ : s₃ ∈ atTop
hg' : ∀ (y : ℝ), y ∈ s₃ → g' y ≠ 0
s : Set ℝ := s₁ ∩ s₂ ∩ s₃
l : ℝ
hl : ∀ (b : ℝ), b ≥ l → b ∈ s
hl' : Ioi l ⊆ s
x : ℝ
hx : x ∈ Ioi l
⊢ x ∈ s₂
exact (hl' hx).1.2