Theorem: taylor_mean_remainder_lagrange_unordered (ExponentialRamsey/Prereq/Mathlib/Analysis/Calculus/Taylor.lean)

State before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        iteratedDerivWithin (n + 1) f (uIcc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
have gcont : ContinuousOn (fun t : ℝ => (x - t) ^ (n + 1)) (uIcc x₀ x) := by
  refine' Continuous.continuousOn _
  sorry
State after:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        iteratedDerivWithin (n + 1) f (uIcc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!

State before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        iteratedDerivWithin (n + 1) f (uIcc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
have hg' : ∀ y : ℝ, y ∈ uIoo x₀ x → -(↑n + 1) * (x - y) ^ n ≠ 0 := fun y hy =>
  mul_ne_zero (neg_ne_zero.mpr (Nat.cast_add_one_ne_zero n)) (xy_ne y hy)
State after:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        iteratedDerivWithin (n + 1) f (uIcc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!

State before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        iteratedDerivWithin (n + 1) f (uIcc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
rcases taylor_mean_remainder_unordered hx hf hf' gcont (fun y _ => monomial_has_deriv_aux y x _)
    hg' with
  ⟨y, hy, h⟩
State after:
case intro.intro
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        iteratedDerivWithin (n + 1) f (uIcc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!

State before:
case intro.intro
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        iteratedDerivWithin (n + 1) f (uIcc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
use y, hy
State after:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!

State before:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    ((x - y) ^ n / ↑n ! * ((x - x) ^ (n + 1) - (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
simp only [sub_self, zero_pow', Ne.def, Nat.succ_ne_zero, not_false_iff, zero_sub, mul_neg] at h
State after:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!

State before:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
rw [h, neg_div, ← div_neg, neg_mul, neg_neg]
State after:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ ((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1) / ((↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f (uIcc x₀ x) y =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!

State before:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ ((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1) / ((↑n + 1) * (x - y) ^ n)) • iteratedDerivWithin (n + 1) f (uIcc x₀ x) y =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) / ↑(n + 1)!
Tactic:
field_simp [n.cast_add_one_ne_zero, n.factorial_ne_zero, xy_ne y hy]
State after:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ (x - y) ^ n * (x - x₀) ^ (n + 1) * iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * ↑(n + 1)! =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) * (↑n ! * ((↑n + 1) * (x - y) ^ n))

State before:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ (x - y) ^ n * (x - x₀) ^ (n + 1) * iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * ↑(n + 1)! =
    iteratedDerivWithin (n + 1) f (uIcc x₀ x) y * (x - x₀) ^ (n + 1) * (↑n ! * ((↑n + 1) * (x - y) ^ n))
Tactic:
ring_nf
State after:
case h
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
xy_ne : ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
hg' : ∀ y ∈ uIoo x₀ x, -(↑n + 1) * (x - y) ^ n ≠ 0
y : ℝ
hy : y ∈ uIoo x₀ x
h :
  f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
    (-((x - y) ^ n / ↑n ! * (x - x₀) ^ (n + 1)) / (-(↑n + 1) * (x - y) ^ n)) •
      iteratedDerivWithin (n + 1) f (uIcc x₀ x) y
⊢ x * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑(1 + n)! * (x - y) ^ n * (x - x₀) ^ n -
      x₀ * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑(1 + n)! * (x - y) ^ n * (x - x₀) ^ n =
    x * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑n ! * ↑n * (x - y) ^ n * (x - x₀) ^ n +
        x * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑n ! * (x - y) ^ n * (x - x₀) ^ n +
      (-(x₀ * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑n ! * ↑n * (x - y) ^ n * (x - x₀) ^ n) -
        x₀ * iteratedDerivWithin (1 + n) f (uIcc x₀ x) y * ↑n ! * (x - y) ^ n * (x - x₀) ^ n)

State before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
⊢ ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
Tactic:
refine' Continuous.continuousOn _
State after:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
⊢ Continuous fun t => (x - t) ^ (n + 1)

State before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
⊢ Continuous fun t => (x - t) ^ (n + 1)
Tactic:
sorry
State after:
no goals

State before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
⊢ ∀ y ∈ uIoo x₀ x, (x - y) ^ n ≠ 0
Tactic:
intro y hy
State after:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ (x - y) ^ n ≠ 0

State before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ (x - y) ^ n ≠ 0
Tactic:
refine' pow_ne_zero _ _
State after:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ x - y ≠ 0

State before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ x - y ≠ 0
Tactic:
rw [sub_ne_zero]
State after:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ x ≠ y

State before:
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
⊢ x ≠ y
Tactic:
cases' le_total x₀ x with h h
State after:
case inl
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
h : x₀ ≤ x
⊢ x ≠ y

case inr
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
h : x ≤ x₀
⊢ x ≠ y

State before:
case inl
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
h : x₀ ≤ x
⊢ x ≠ y
Tactic:
rw [uIoo_of_le h] at hy
State after:
case inl
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ Ioo x₀ x
h : x₀ ≤ x
⊢ x ≠ y

State before:
case inl
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ Ioo x₀ x
h : x₀ ≤ x
⊢ x ≠ y
Tactic:
exact hy.2.ne'
State after:
no goals

State before:
case inr
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ uIoo x₀ x
h : x ≤ x₀
⊢ x ≠ y
Tactic:
rw [uIoo_of_ge h] at hy
State after:
case inr
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ Ioo x x₀
h : x ≤ x₀
⊢ x ≠ y

State before:
case inr
f : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (uIcc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (uIcc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn (fun t => (x - t) ^ (n + 1)) (uIcc x₀ x)
y : ℝ
hy : y ∈ Ioo x x₀
h : x ≤ x₀
⊢ x ≠ y
Tactic:
exact hy.1.ne
State after:
no goals