-- Mathlib/Analysis/Calculus/Monotone.lean
theorem tendsto_apply_add_mul_sq_div_sub {f : ℝ → ℝ} {x a c d : ℝ} {l : Filter ℝ} (hl : l ≤ 𝓝[≠] 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)

Proof state:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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)

Tactic:
simp only [_root_.sub_self, add_zero, mul_zero] at this

Result:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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)

Proof state:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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, 1 + c * (x_1 - x) = (x_1 + c * (x_1 - x) ^ 2 - x) / (x_1 - x)

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy

Result:
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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)

Proof state:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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)))

Tactic:
exact ((tendsto_id.sub_const x).const_mul c).const_add 1

Result:
no goals

Proof state:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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)

Tactic:
apply Tendsto.congr' _ Z

Result:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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)

Proof state:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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)

Tactic:
rw [mul_one] at Z

Result:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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)

Proof state:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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)

Tactic:
have : ∀ᶠ y in l, y + c * (y - x) ^ 2 ≠ x := by apply Tendsto.mono_right h' hl self_mem_nhdsWithin

Result:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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)

Proof state:
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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)

Tactic:
field_simp [sub_ne_zero.2 hy]

Result:
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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

Proof state:
case h
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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

Tactic:
ring

Result:
no goals

Proof state:
f : ℝ → ℝ
x a c d : ℝ
l : Filter ℝ
hl : l ≤ 𝓝[≠] 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

Tactic:
apply Tendsto.mono_right h' hl self_mem_nhdsWithin

Result:
no goals