awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ I, f i) s x) (∑ i ∈ I, iteratedDerivWithin n (f i) s x)
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
  Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ ∅, f i) s x) (∑ i ∈ ∅, iteratedDerivWithin n (f i) s x)
Tactic: induction I using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    rw [forall_mem_insert] at hf
    simp only [sum_insert hi, sum_fn] at IH ⊢
    rw [iteratedDerivWithin_add hx hs hf.1 (.sum hf.2), IH hf.2]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ ∅, f i) s x) (∑ i ∈ ∅, iteratedDerivWithin n (f i) s x)
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ I, f i) s x) (∑ i ∈ I, iteratedDerivWithin n (f i) s x)
have insert : ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
  (IH :
    ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
      Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ t, f i) s x) (∑ i ∈ t, iteratedDerivWithin n (f i) s x))
  (hf : ∀ i_1 ∈ insert i t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i_1) s x),
  Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ insert i t, f i) s x)
    (∑ i ∈ insert i t, iteratedDerivWithin n (f i) s x)
Tactic: induction I using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    rw [forall_mem_insert] at hf
    simp only [sum_insert hi, sum_fn] at IH ⊢
    rw [iteratedDerivWithin_add hx hs hf.1 (.sum hf.2), IH hf.2]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ I, f i) s x) (∑ i ∈ I, iteratedDerivWithin n (f i) s x)
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
  Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ ∅, f i) s x) (∑ i ∈ ∅, iteratedDerivWithin n (f i) s x)
Tactic: classical
  induction I using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    rw [forall_mem_insert] at hf
    simp only [sum_insert hi, sum_fn] at IH ⊢
    rw [iteratedDerivWithin_add hx hs hf.1 (.sum hf.2), IH hf.2]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_2
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
ι : Type u_7
n : ℕ
x : 𝕜
f : ι → 𝕜 → F
I : Finset ι
s : Set 𝕜
hx : x ∈ s
hs : UniqueDiffOn 𝕜 s
hf : ∀ i ∈ I, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
    Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ ∅, f i) s x) (∑ i ∈ ∅, iteratedDerivWithin n (f i) s x)
⊢ Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ I, f i) s x) (∑ i ∈ I, iteratedDerivWithin n (f i) s x)
have insert : ∀ (i : ι) (t : Finset ι) (hi : i ∉ t)
  (IH :
    ∀ (hf : ∀ i ∈ t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i) s x),
      Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ t, f i) s x) (∑ i ∈ t, iteratedDerivWithin n (f i) s x))
  (hf : ∀ i_1 ∈ insert i t, ContDiffWithinAt 𝕜 (↑n : WithTop ℕ∞) (f i_1) s x),
  Eq.{u_2 + 1} (α := F) (iteratedDerivWithin n (∑ i ∈ insert i t, f i) s x)
    (∑ i ∈ insert i t, iteratedDerivWithin n (f i) s x)
Tactic: classical
  induction I using Finset.induction_on with
  | empty => simp
  | insert i t hi IH =>
    rw [forall_mem_insert] at hf
    simp only [sum_insert hi, sum_fn] at IH ⊢
    rw [iteratedDerivWithin_add hx hs hf.1 (.sum hf.2), IH hf.2]
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
m : ℤ
k : ℕ
hs : IsOpen s
⊢ Set.EqOn (β := 𝕜) (iteratedDerivWithin k (fun (y : 𝕜) ↦ y ^ m) s)
    (fun (y : 𝕜) ↦ (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * y ^ (m - (↑k : ℤ))) s
have apply : Set.EqOn (β := 𝕜) (deriv^[k] fun (y : 𝕜) ↦ y ^ m)
  (fun (y : 𝕜) ↦ (∏ i ∈ Finset.range k, HSub.hSub (α := 𝕜) (↑m : 𝕜) (↑i : 𝕜)) * y ^ (m - (↑k : ℤ))) s
Tactic: apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen_eq_iterate hs)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
k : ℕ
hs : IsOpen s
⊢ Set.EqOn (β := 𝕜) (iteratedDerivWithin k (fun (y : 𝕜) ↦ 1 / y) s)
    (fun (y : 𝕜) ↦ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * y ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) s
have apply : Set.EqOn (β := 𝕜) (deriv^[k] fun (y : 𝕜) ↦ 1 / y)
  (fun (y : 𝕜) ↦ HPow.hPow (α := 𝕜) (-1) k * (↑k ! : 𝕜) * y ^ HSub.hSub (α := ℤ) (-1) (↑k : ℤ)) s
Tactic: apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen_eq_iterate hs)
-- 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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b
Tactic: have sub : ∀ x ∈ Ioo a b, Ioo a x ⊆ Ioo a b := fun x hx =>
    Ioo_subset_Ioo (le_refl a) (le_of_lt hx.2)
-- 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
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
⊢ Tendsto g (𝓝[<] x) (𝓝 0)
have rw : Tendsto g (𝓝[Ioo a x] x) (𝓝 (g x))
Tactic: rw [← h, ← nhdsWithin_Ioo_eq_nhdsLT hx.1]
-- 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
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
⊢ False
have this : Tendsto g (𝓝[<] x) (𝓝 0)
Tactic: have : Tendsto g (𝓝[<] x) (𝓝 0) := by
      rw [← h, ← nhdsWithin_Ioo_eq_nhdsLT hx.1]
      exact ((hgg' x hx).continuousAt.continuousWithinAt.mono <| sub x hx).tendsto
-- 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
x : ℝ
hx : x ∈ Ioo a b
h : g x = 0
this : Tendsto g (𝓝[<] x) (𝓝 0)
⊢ False
have obtain : ∀ (y : ℝ) (hyx : y ∈ Ioo a x) (hy : g' y = 0), False
Tactic: obtain ⟨y, hyx, hy⟩ : ∃ c ∈ Ioo a x, g' c = 0 :=
      exists_hasDerivAt_eq_zero' hx.1 hga this fun y hy => hgg' y <| sub x hx hy
-- 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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have hg : ∀ x ∈ Ioo a b, g x ≠ 0
Tactic: have hg : ∀ x ∈ Ioo a b, g x ≠ 0 := by
    intro x hx h
    have : Tendsto g (𝓝[<] x) (𝓝 0) := by
      rw [← h, ← nhdsWithin_Ioo_eq_nhdsLT hx.1]
      exact ((hgg' x hx).continuousAt.continuousWithinAt.mono <| sub x hx).tendsto
    obtain ⟨y, hyx, hy⟩ : ∃ c ∈ Ioo a x, g' c = 0 :=
      exists_hasDerivAt_eq_zero' hx.1 hga this fun y hy => hgg' y <| sub x hx hy
    exact hg' y (sub x hx hyx) hy
-- 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
x : ℝ
hx : x ∈ Ioo a b
⊢ ∃ c ∈ Ioo a x, f x * g' c = g x * f' c
have rw : ∃ c ∈ Ioo a x, (f x - 0) * g' c = (g x - 0) * f' c
Tactic: rw [← sub_zero (f x), ← sub_zero (g 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
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have this : ∀ x ∈ Ioo a b, ∃ c ∈ Ioo a x, f x * g' c = g x * f' c
Tactic: have : ∀ x ∈ Ioo a b, ∃ c ∈ Ioo a x, f x * g' c = g x * f' c := by
    intro x hx
    rw [← sub_zero (f x), ← sub_zero (g x)]
    exact exists_ratio_hasDerivAt_eq_ratio_slope' g g' hx.1 f f' (fun y hy => hgg' y <| sub x hx hy)
      (fun y hy => hff' y <| sub x hx hy) hga hfa
      (tendsto_nhdsWithin_of_tendsto_nhds (hgg' x hx).continuousAt.tendsto)
      (tendsto_nhdsWithin_of_tendsto_nhds (hff' x hx).continuousAt.tendsto)
-- 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
this : ∀ x ∈ Ioo a b, ∃ c ∈ Ioo a x, f x * g' c = g x * f' c
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have choose! : ∀ (c : (x : ℝ) → ℝ) (hc : ∀ x ∈ Ioo a b, c x ∈ Ioo a x ∧ f x * g' (c x) = g x * f' (c x)),
  Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
Tactic: choose! c hc using this
Cleared hypotheses: this
-- 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)
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have this : ∀ x ∈ Ioo a b, ((fun (x' : ℝ) ↦ f' x' / g' x') ∘ c) x = f x / g x
Tactic: have : ∀ x ∈ Ioo a b, ((fun x' => f' x' / g' x') ∘ c) x = f x / g x := by grind
-- 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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x
Tactic: have cmp : ∀ x ∈ Ioo a b, a < c x ∧ c x < x := fun x hx ↦ (hc x hx).1
-- 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 : ∀ 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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[>] a) l
have rw : Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[Ioo a b] a) l
Tactic: rw [← 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
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
⊢ Tendsto (fun (x : ℝ) ↦ f x / g x) (𝓝[Ioo a b] a) l
have apply : Tendsto ((fun (x' : ℝ) ↦ f' x' / g' x') ∘ c) (𝓝[Ioo a b] a) l
Tactic: apply tendsto_nhdsWithin_congr 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
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
⊢ Tendsto ((fun (x' : ℝ) ↦ f' x' / g' x') ∘ c) (𝓝[Ioo a b] a) l
have apply : Tendsto c (𝓝[Ioo a b] a) (𝓝[>] a)
Tactic: apply hdiv.comp
-- 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 : ∀ 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
⊢ Tendsto c (𝓝[Ioo a b] a) (𝓝[>] a)
have refine_1 : ∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, a ≤ c b
Tactic: refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
    (tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds
      (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id) ?_ ?_) ?_
-- 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 : ∀ 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
refine_1 : ∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, a ≤ c b
⊢ Tendsto c (𝓝[Ioo a b] a) (𝓝[>] a)
have refine_2 : ∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, c b ≤ id b
Tactic: refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
    (tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds
      (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id) ?_ ?_) ?_
-- 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 : ∀ 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
refine_1 : ∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, a ≤ c b
refine_2 : ∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, c b ≤ id b
⊢ Tendsto c (𝓝[Ioo a b] a) (𝓝[>] a)
have refine_3 : ∀ᶠ (x : ℝ) in 𝓝[Ioo a b] a, c x ∈ Ioi a
Tactic: refine tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
    (tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds
      (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id) ?_ ?_) ?_
-- 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 : ∀ 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
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, a ≤ c b
have refine_1 : ∀ x ∈ Ioo a b, a ≤ c x
Tactic: apply eventually_nhdsWithin_of_forall
-- 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
⊢ a ≤ c x
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
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
⊢ ∀ᶠ (b : ℝ) in 𝓝[Ioo a b] a, c b ≤ id b
have refine_2 : ∀ x ∈ Ioo a b, c x ≤ id x
Tactic: apply eventually_nhdsWithin_of_forall
-- 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 ≤ id x
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
⊢ c x ≤ id x
have refine_2 : c x ≤ x
Tactic: simp
-- 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
⊢ c x ≤ x
have linarith : x < c x → c x - x + (x - c x) = 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
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 : ℝ) in 𝓝[Ioo a b] a, c x ∈ Ioi a
have refine_3 : ∀ x ∈ Ioo a b, c x ∈ Ioi a
Tactic: apply eventually_nhdsWithin_of_forall