awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[s \ {a}] a) l
x : ℝ
h : s \ {a} ∈ 𝓝 x
refine_2 : deriv f x / deriv g x = deriv f x / derivWithin g (s \ {a}) x
⊢ deriv f x / deriv g x = derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x

Tactic:
rw [derivWithin_of_mem_nhds ‹_›]

Premises used: derivWithin_of_mem_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[s \ {a}] a) l
x : ℝ
h : s \ {a} ∈ 𝓝 x
refine_2 refine_2₁ : deriv f x / deriv g x = deriv f x / deriv g x
⊢ deriv f x / deriv g x = deriv f x / derivWithin g (s \ {a}) x

Tactic:
rw [derivWithin_of_mem_nhds ‹_›]

Premises used: derivWithin_of_mem_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
s : Set ℝ
hs : Convex ℝ s
hdf : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[s \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[s \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[s \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[s \ {a}] a) l
x : ℝ
h : s \ {a} ∈ 𝓝 x
refine_2 refine_2₁ refine_2₂ refine_2₃ : deriv f x / deriv g x = deriv f x / derivWithin g (s \ {a}) x
⊢ deriv f x / deriv g x = derivWithin f (s \ {a}) x / derivWithin g (s \ {a}) x

Tactic:
iterate 2 rw [derivWithin_of_mem_nhds ‹_›]

Premises used: derivWithin_of_mem_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[>] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[>] a) l
rw :
  ∀ (hdf : ∀ᶠ (x : ℝ) in 𝓝[Ici a \ {a}] a, DifferentiableAt ℝ f x) (hg' : ∀ᶠ (x : ℝ) in 𝓝[Ici a \ {a}] a, deriv g x ≠ 0)
    (hfa : Tendsto f (𝓝[Ici a \ {a}] a) (𝓝 0)) (hga : Tendsto g (𝓝[Ici a \ {a}] a) (𝓝 0))
    (hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[Ici a \ {a}] a) l),
    Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[Ici a \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l

Tactic:
rw [← Ici_diff_left] at *

Premises used: Set.Ici_diff_left
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Ici a \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Ici a \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Ici a \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[Ici a \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[Ici a \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[Ici a \ {a}] a) l

Tactic:
lhopital_zero_nhdsWithin_convex (convex_Ici a) hdf hg' hfa hga hdiv

Premises used: deriv.lhopital_zero_nhdsWithin_convex, convex_Ici
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Ici a \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Ici a \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Ici a \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[Ici a \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[Ici a \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[Ici a \ {a}] a) l

Tactic:
exact lhopital_zero_nhdsWithin_convex (convex_Ici a) hdf hg' hfa hga hdiv

Premises used: deriv.lhopital_zero_nhdsWithin_convex, convex_Ici
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[<] a) l
rw :
  ∀ (hdf : ∀ᶠ (x : ℝ) in 𝓝[Iic a \ {a}] a, DifferentiableAt ℝ f x) (hg' : ∀ᶠ (x : ℝ) in 𝓝[Iic a \ {a}] a, deriv g x ≠ 0)
    (hfa : Tendsto f (𝓝[Iic a \ {a}] a) (𝓝 0)) (hga : Tendsto g (𝓝[Iic a \ {a}] a) (𝓝 0))
    (hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[Iic a \ {a}] a) l),
    Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[Iic a \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[<] a) l

Tactic:
rw [← Iic_diff_right] at *

Premises used: Set.Iic_diff_right
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Iic a \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Iic a \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Iic a \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[Iic a \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[Iic a \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[Iic a \ {a}] a) l

Tactic:
lhopital_zero_nhdsWithin_convex (convex_Iic a) hdf hg' hfa hga hdiv

Premises used: convex_Iic, deriv.lhopital_zero_nhdsWithin_convex
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[Iic a \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[Iic a \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[Iic a \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[Iic a \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[Iic a \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[Iic a \ {a}] a) l

Tactic:
exact lhopital_zero_nhdsWithin_convex (convex_Iic a) hdf hg' hfa hga hdiv

Premises used: convex_Iic, deriv.lhopital_zero_nhdsWithin_convex
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[≠] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[≠] a) (𝓝 0)
hga : Tendsto g (𝓝[≠] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[≠] a) l
rw :
  ∀ (hdf : ∀ᶠ (x : ℝ) in 𝓝[univ \ {a}] a, DifferentiableAt ℝ f x) (hg' : ∀ᶠ (x : ℝ) in 𝓝[univ \ {a}] a, deriv g x ≠ 0)
    (hfa : Tendsto f (𝓝[univ \ {a}] a) (𝓝 0)) (hga : Tendsto g (𝓝[univ \ {a}] a) (𝓝 0))
    (hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[univ \ {a}] a) l),
    Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[univ \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l

Tactic:
rw [compl_eq_univ_diff] at *

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[univ \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[univ \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[univ \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[univ \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[univ \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[univ \ {a}] a) l

Tactic:
lhopital_zero_nhdsWithin_convex convex_univ hdf hg' hfa hga hdiv

Premises used: deriv.lhopital_zero_nhdsWithin_convex, convex_univ
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[univ \ {a}] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[univ \ {a}] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[univ \ {a}] a) (𝓝 0)
hga : Tendsto g (𝓝[univ \ {a}] a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[univ \ {a}] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[univ \ {a}] a) l

Tactic:
exact lhopital_zero_nhdsWithin_convex convex_univ hdf hg' hfa hga hdiv

Premises used: deriv.lhopital_zero_nhdsWithin_convex, convex_univ
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
hdf₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, DifferentiableAt ℝ f x
hg'₁ : ∀ᶠ (x : ℝ) in 𝓝[≠] a, deriv g x ≠ 0
hfa₁ : Tendsto f (𝓝[≠] a) (𝓝 0)
hga₁ : Tendsto g (𝓝[≠] a) (𝓝 0)
hdiv₁ : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[≠] a) l
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[≠] a) l

Tactic:
apply lhopital_zero_nhdsNE

Premises used: deriv.lhopital_zero_nhdsNE
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
hdf₁ : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, DifferentiableAt ℝ f x

Tactic:
apply eventually_nhdsWithin_of_eventually_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
hdf₁ : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, DifferentiableAt ℝ f x

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds, tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
hg'₁ : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, deriv g x ≠ 0

Tactic:
apply eventually_nhdsWithin_of_eventually_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
hg'₁ : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
⊢ ∀ᶠ (x : ℝ) in 𝓝[≠] a, deriv g x ≠ 0

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds, tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
hfa₁ : Tendsto f (𝓝 a) (𝓝 0)
⊢ Tendsto f (𝓝[≠] a) (𝓝 0)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
hfa₁ : Tendsto f (𝓝 a) (𝓝 0)
⊢ Tendsto f (𝓝[≠] a) (𝓝 0)

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds, tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
hga₁ : Tendsto g (𝓝 a) (𝓝 0)
⊢ Tendsto g (𝓝[≠] a) (𝓝 0)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
hga₁ : Tendsto g (𝓝 a) (𝓝 0)
⊢ Tendsto g (𝓝[≠] a) (𝓝 0)

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds, tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv hdiv₁ : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[≠] a) l

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv hdiv₁ : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝[≠] a) l

Tactic:
first | apply eventually_nhdsWithin_of_eventually_nhds |
      apply tendsto_nhdsWithin_of_tendsto_nhds

Premises used: eventually_nhdsWithin_of_eventually_nhds, tendsto_nhdsWithin_of_tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto f (𝓝 a) (𝓝 0)

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto g (𝓝 a) (𝓝 0)

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝 a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝 a, deriv g x ≠ 0
hfa : Tendsto f (𝓝 a) (𝓝 0)
hga : Tendsto g (𝓝 a) (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l
⊢ Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) (𝓝 a) l

Tactic:
assumption
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atTop l
⊢ ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x

Tactic:
have hdg : ∀ᶠ x in atTop, DifferentiableAt ℝ g x := hg'.mp
    (Eventually.of_forall fun _ hg' =>
      by_contradiction fun h => hg' (deriv_zero_of_not_differentiableAt h))
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atTop l
hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x
⊢ ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (deriv f x) x

Tactic:
have hdf' : ∀ᶠ x in atTop, HasDerivAt f (deriv f x) x :=
    hdf.mono fun _ => DifferentiableAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atTop l
hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (deriv f x) x
⊢ ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (deriv g x) x

Tactic:
have hdg' : ∀ᶠ x in atTop, HasDerivAt g (deriv g x) x :=
    hdg.mono fun _ => DifferentiableAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atTop l
hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (deriv f x) x
hdg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (deriv g x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l

Tactic:
HasDerivAt.lhopital_zero_atTop hdf' hdg' hg' hftop hgtop hdiv

Premises used: HasDerivAt.lhopital_zero_atTop
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atTop, deriv g x ≠ 0
hftop : Tendsto f atTop (𝓝 0)
hgtop : Tendsto g atTop (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atTop l
hdg : ∀ᶠ (x : ℝ) in atTop, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt f (deriv f x) x
hdg' : ∀ᶠ (x : ℝ) in atTop, HasDerivAt g (deriv g x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atTop l

Tactic:
exact HasDerivAt.lhopital_zero_atTop hdf' hdg' hg' hftop hgtop hdiv

Premises used: HasDerivAt.lhopital_zero_atTop
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atBot l
⊢ ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x

Tactic:
have hdg : ∀ᶠ x in atBot, DifferentiableAt ℝ g x :=
    hg'.mono fun _ hg' => by_contradiction fun h => hg' (deriv_zero_of_not_differentiableAt h)
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atBot l
hdg : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x
⊢ ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (deriv f x) x

Tactic:
have hdf' : ∀ᶠ x in atBot, HasDerivAt f (deriv f x) x :=
    hdf.mono fun _ => DifferentiableAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atBot l
hdg : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (deriv f x) x
⊢ ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (deriv g x) x

Tactic:
have hdg' : ∀ᶠ x in atBot, HasDerivAt g (deriv g x) x :=
    hdg.mono fun _ => DifferentiableAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atBot l
hdg : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (deriv f x) x
hdg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (deriv g x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l

Tactic:
HasDerivAt.lhopital_zero_atBot hdf' hdg' hg' hfbot hgbot hdiv

Premises used: HasDerivAt.lhopital_zero_atBot
-- Module: Mathlib.Analysis.Calculus.LHopital
Goal:
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in atBot, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun (x : ℝ) ↦ deriv f x / deriv g x) atBot l
hdg : ∀ᶠ (x : ℝ) in atBot, DifferentiableAt ℝ g x
hdf' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt f (deriv f x) x
hdg' : ∀ᶠ (x : ℝ) in atBot, HasDerivAt g (deriv g x) x
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) atBot l

Tactic:
exact HasDerivAt.lhopital_zero_atBot hdf' hdg' hg' hfbot hgbot hdiv

Premises used: HasDerivAt.lhopital_zero_atBot
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range = ⊤
fφ : (x : E) → F × ℝ := fun (x : E) ↦ (f x, φ x)
change : map (Prod.snd ∘ fφ) (𝓝[fφ ⁻¹' {p : F × ℝ | p.1 = f x₀}] x₀) = 𝓝 (φ x₀)
⊢ map φ (𝓝[f ⁻¹' {f x₀}] x₀) = 𝓝 (φ x₀)

Tactic:
change map (Prod.snd ∘ fφ) (𝓝[fφ ⁻¹' {p | p.1 = f x₀}] x₀) = 𝓝 (φ x₀)

Premises used: Filter.map, nhdsWithin, setOf, Function.comp, nhds, Prod.fst, Set.preimage, Eq, Prod.snd
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range = ⊤
fφ : (x : E) → F × ℝ := fun (x : E) ↦ (f x, φ x)
rw : map Prod.snd (𝓝 (f x₀, φ x₀) ⊓ 𝓟 {p : F × ℝ | p.1 = f x₀}) = 𝓝 (φ x₀)
⊢ map (Prod.snd ∘ fφ) (𝓝[fφ ⁻¹' {p : F × ℝ | p.1 = f x₀}] x₀) = 𝓝 (φ x₀)

Tactic:
rw [← map_map, nhdsWithin, map_inf_principal_preimage,
      (hf'.prodMk hφ').map_nhds_eq_of_surj htop]

Premises used: nhdsWithin, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.map_nhds_eq_of_surj, Filter.map_map, Filter.map_inf_principal_preimage
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range = ⊤
fφ : (x : E) → F × ℝ := fun (x : E) ↦ (f x, φ x)
⊢ map Prod.snd (𝓝 (f x₀, φ x₀) ⊓ 𝓟 {p : F × ℝ | p.1 = f x₀}) = 𝓝 (φ x₀)

Tactic:
map_snd_nhdsWithin _

Premises used: Set.Mem, nhdsWithin, setOf, map_snd_nhdsWithin, Set.preimage, Set.singleton
-- Module: Mathlib.Analysis.Calculus.LagrangeMultipliers
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
f : E → F
φ : E → ℝ
x₀ : E
f' : E →L[ℝ] F
φ' : StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | f x = f x₀} x₀
hf' : HasStrictFDerivAt f f' x₀
hφ' : HasStrictFDerivAt φ φ' x₀
htop : (↑(f'.prod φ') : E →ₗ[ℝ] F × ℝ).range = ⊤
fφ : (x : E) → F × ℝ := fun (x : E) ↦ (f x, φ x)
⊢ map Prod.snd (𝓝 (f x₀, φ x₀) ⊓ 𝓟 {p : F × ℝ | p.1 = f x₀}) = 𝓝 (φ x₀)

Tactic:
exact map_snd_nhdsWithin _

Premises used: map_snd_nhdsWithin