f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
⊢ Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
⊢ Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
have L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1) := by
  have : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x))) := by
    apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
    exact ((tendsto_id.sub_const x).const_mul c).const_add 1
  simp only [_root_.sub_self, add_zero, MulZeroClass.mul_zero] at this
  apply Tendsto.congr' (Eventually.filter_mono hl _) this
  filter_upwards [self_mem_nhdsWithin] with y hy
  field_simp [sub_ne_zero.2 hy]
  ring
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 (a * 1))
⊢ Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
⊢ Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
have Z := (hf.comp h').mul L
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 (a * 1))
⊢ Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
rw [mul_one] at Z
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 *
        ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) =ᶠ[l]
    fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ Tendsto (fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)) l (𝓝 a)
apply Tendsto.congr' _ Z
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
this : ∀ᶠ (y : ℝ) in l, y + c * (y - x) ^ 2 ≠ x
⊢ (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 *
        ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) =ᶠ[l]
    fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 *
        ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) =ᶠ[l]
    fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)
have : ∀ᶠ y in l, y + c * (y - x) ^ 2 ≠ x := by apply Tendsto.mono_right h' hl self_mem_nhdsWithin
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
this : ∀ᶠ (y : ℝ) in l, y + c * (y - x) ^ 2 ≠ x
y : ℝ
hy : y + c * (y - x) ^ 2 ≠ x
⊢ ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) y * ((y + c * (y - x) ^ 2 - x) / (y - x)) =
    (f (y + c * (y - x) ^ 2) - d) / (y - x)
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
this : ∀ᶠ (y : ℝ) in l, y + c * (y - x) ^ 2 ≠ x
⊢ (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 *
        ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x))) =ᶠ[l]
    fun y => (f (y + c * (y - x) ^ 2) - d) / (y - x)
filter_upwards [this] with y hy
no goals
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
this : ∀ᶠ (y : ℝ) in l, y + c * (y - x) ^ 2 ≠ x
y : ℝ
hy : y + c * (y - x) ^ 2 ≠ x
⊢ ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) y * ((y + c * (y - x) ^ 2 - x) / (y - x)) =
    (f (y + c * (y - x) ^ 2) - d) / (y - x)
field_simp [sub_ne_zero.2 hy]
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x)))
⊢ Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
⊢ Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
have : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x))) := by
  apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
  exact ((tendsto_id.sub_const x).const_mul c).const_add 1
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
⊢ Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x)))
⊢ Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
simp only [_root_.sub_self, add_zero, MulZeroClass.mul_zero] at this
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[{x}ᶜ] x, 1 + c * (x_1 - x) = (x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
⊢ Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
apply Tendsto.congr' (Eventually.filter_mono hl _) this
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
y : ℝ
hy : y ∈ {x}ᶜ
⊢ 1 + c * (y - x) = (y + c * (y - x) ^ 2 - x) / (y - x)
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[{x}ᶜ] x, 1 + c * (x_1 - x) = (x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)
filter_upwards [self_mem_nhdsWithin] with y hy
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
y : ℝ
hy : y ∈ {x}ᶜ
⊢ (1 + c * (y - x)) * (y - x) = y + c * (y - x) ^ 2 - x
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
y : ℝ
hy : y ∈ {x}ᶜ
⊢ 1 + c * (y - x) = (y + c * (y - x) ^ 2 - x) / (y - x)
field_simp [sub_ne_zero.2 hy]
no goals
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
this : Tendsto (fun y => 1 + c * (y - x)) l (𝓝 1)
y : ℝ
hy : y ∈ {x}ᶜ
⊢ (1 + c * (y - x)) * (y - x) = y + c * (y - x) ^ 2 - x
ring
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
⊢ Tendsto (fun y => 1 + c * (y - x)) (𝓝 x) (𝓝 (1 + c * (x - x)))
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
⊢ Tendsto (fun y => 1 + c * (y - x)) l (𝓝 (1 + c * (x - x)))
apply Tendsto.mono_left _ (hl.trans nhdsWithin_le_nhds)
no goals
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
⊢ Tendsto (fun y => 1 + c * (y - x)) (𝓝 x) (𝓝 (1 + c * (x - x)))
exact ((tendsto_id.sub_const x).const_mul c).const_add 1
no goals
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[{x}ᶜ] x
hf : Tendsto (fun y => (f y - d) / (y - x)) l (𝓝 a)
h' : Tendsto (fun y => y + c * (y - x) ^ 2) l l
L : Tendsto (fun y => (y + c * (y - x) ^ 2 - x) / (y - x)) l (𝓝 1)
Z :
  Tendsto
    (fun x_1 =>
      ((fun y => (f y - d) / (y - x)) ∘ fun y => y + c * (y - x) ^ 2) x_1 * ((x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)))
    l (𝓝 a)
⊢ ∀ᶠ (y : ℝ) in l, y + c * (y - x) ^ 2 ≠ x
apply Tendsto.mono_right h' hl self_mem_nhdsWithin