internlm/Lean-Github huggingface dataset:
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case false.pf1
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.succ i < length (x :: xs)
pf2 : Nat.succ i < length (false :: bs)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ i < length xs
Tactic:
apply Nat.lt_of_succ_lt_succ pf1
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case false.hu
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.succ i < length (x :: xs)
pf2 : Nat.succ i < length (false :: bs)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ Unique (map f xs)
Tactic:
exact hu
Proof state after:
no goals
Theorem: List.sieve_map_mem_iff_true_unique
Proof state before:
case false.hget
α : Type u_1
β : Type u_2
f : α → β
i : Nat
ih :
  ∀ {xs : List α} {bs : List Bool} (pf1 : i < length xs) (pf2 : i < length bs),
    Unique (map f xs) →
      get bs { val := i, isLt := pf2 } = true →
        get (map f xs) { val := i, isLt := (_ : i < length (map f xs)) } ∈ map f (sieve bs xs)
xs✝ : List α
bs✝ : List Bool
hu✝ : Unique (map f xs✝)
bs : List Bool
x : α
xs : List α
hnmem : ¬f x ∈ map f xs
hu : Unique (map f xs)
pf1 : Nat.succ i < length (x :: xs)
pf2 : Nat.succ i < length (false :: bs)
hget : get bs { val := i, isLt := (_ : Nat.succ i ≤ length bs) } = true
⊢ get bs { val := i, isLt := ?false.pf2 } = true
Tactic:
exact hget
Proof state after:
no goals
Theorem: uIoo_of_le
Proof state before:
α : Type u_1
inst✝ : Lattice α
x y : α
h : x ≤ y
⊢ uIoo x y = Ioo x y
Tactic:
rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]
Proof state after:
no goals
Theorem: uIoo_of_ge
Proof state before:
α : Type u_1
inst✝ : Lattice α
x y : α
h : y ≤ x
⊢ uIoo x y = Ioo y x
Tactic:
rw [uIoo, inf_eq_right.2 h, sup_eq_left.2 h]
Proof state after:
no goals
Theorem: uIoo_comm
Proof state before:
α : Type u_1
inst✝ : Lattice α
x y : α
⊢ uIoo x y = uIoo y x
Tactic:
rw [uIoo, uIoo, inf_comm, sup_comm]
Proof state after:
no goals
Theorem: taylor_mean_remainder_unordered
Proof state before:
f g g' : ℝ → ℝ
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 g (uIcc x₀ x)
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (uIcc x₀ x) x'
Tactic:
rcases Ne.lt_or_lt hx with (hx₀ | hx₀)
Proof state after:
case inl
f g g' : ℝ → ℝ
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 g (uIcc x₀ x)
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (uIcc x₀ x) x'

case inr
f g g' : ℝ → ℝ
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 g (uIcc x₀ x)
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (uIcc x₀ x) x'
Theorem: taylor_mean_remainder_unordered
Proof state before:
case inr
f g g' : ℝ → ℝ
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 g (uIcc x₀ x)
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (uIcc x₀ x) x'
Tactic:
rw [uIcc_of_ge hx₀.le] at hf hf' gcont ⊢
Proof state after:
case inr
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (uIoo x₀ x)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (Icc x x₀) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x x₀) x'
Theorem: taylor_mean_remainder_unordered
Proof state before:
case inr
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (uIoo x₀ x)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (Icc x x₀) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x x₀) x'
Tactic:
rw [uIoo_of_ge hx₀.le] at g'_ne gdiff hf' ⊢
Proof state after:
case inr
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo x x₀),
      f x - taylorWithinEval f n (Icc x x₀) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x x₀) x'
Theorem: taylor_mean_remainder_unordered
Proof state before:
case inr
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo x x₀),
      f x - taylorWithinEval f n (Icc x x₀) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x x₀) x'
Tactic:
rcases exists_ratio_hasDerivAt_eq_ratio_slope (fun t => taylorWithinEval f n (Icc x x₀) t x)
    (fun t => ((n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) t) hx₀
    (continuousOn_taylorWithinEval (uniqueDiffOn_Icc hx₀) hf)
    (fun _ hy => taylorWithinEval_hasDerivAt_Ioo x hx₀ hy hf hf') g g' gcont gdiff with
  ⟨y, hy, h⟩
Proof state after:
case inr.intro.intro
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y =
    (taylorWithinEval f n (Icc x x₀) x₀ x - taylorWithinEval f n (Icc x x₀) x x) * g' y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo x x₀),
      f x - taylorWithinEval f n (Icc x x₀) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x x₀) x'
Theorem: taylor_mean_remainder_unordered
Proof state before:
case inr.intro.intro
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y =
    (taylorWithinEval f n (Icc x x₀) x₀ x - taylorWithinEval f n (Icc x x₀) x x) * g' y
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo x x₀),
      f x - taylorWithinEval f n (Icc x x₀) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x x₀) x'
Tactic:
use y, hy
Proof state after:
case h
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y =
    (taylorWithinEval f n (Icc x x₀) x₀ x - taylorWithinEval f n (Icc x x₀) x x) * g' y
⊢ f x - taylorWithinEval f n (Icc x x₀) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x x₀) y
Theorem: taylor_mean_remainder_unordered
Proof state before:
case h
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y =
    (taylorWithinEval f n (Icc x x₀) x₀ x - taylorWithinEval f n (Icc x x₀) x x) * g' y
⊢ f x - taylorWithinEval f n (Icc x x₀) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x x₀) y
Tactic:
simp only [taylorWithinEval_self] at h
Proof state after:
case h
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y =
    (taylorWithinEval f n (Icc x x₀) x₀ x - f x) * g' y
⊢ f x - taylorWithinEval f n (Icc x x₀) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x x₀) y
Theorem: taylor_mean_remainder_unordered
Proof state before:
case h
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  (g x₀ - g x) * ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y =
    (taylorWithinEval f n (Icc x x₀) x₀ x - f x) * g' y
⊢ f x - taylorWithinEval f n (Icc x x₀) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x x₀) y
Tactic:
rw [mul_comm, ← div_left_inj' (g'_ne y hy), mul_div_cancel _ (g'_ne y hy)] at h
Proof state after:
case h
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) / g' y =
    taylorWithinEval f n (Icc x x₀) x₀ x - f x
⊢ f x - taylorWithinEval f n (Icc x x₀) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x x₀) y
Theorem: taylor_mean_remainder_unordered
Proof state before:
case h
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) / g' y =
    taylorWithinEval f n (Icc x x₀) x₀ x - f x
⊢ f x - taylorWithinEval f n (Icc x x₀) x₀ x =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x x₀) y
Tactic:
rw [← neg_sub, ← h]
Proof state after:
case h
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) / g' y =
    taylorWithinEval f n (Icc x x₀) x₀ x - f x
⊢ -(((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) / g' y) =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x x₀) y
Theorem: taylor_mean_remainder_unordered
Proof state before:
case h
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) / g' y =
    taylorWithinEval f n (Icc x x₀) x₀ x - f x
⊢ -(((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) / g' y) =
    ((x - y) ^ n / ↑n ! * (g x - g x₀) / g' y) • iteratedDerivWithin (n + 1) f (Icc x x₀) y
Tactic:
field_simp [g'_ne y hy, n.factorial_ne_zero]
Proof state after:
case h
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) / g' y =
    taylorWithinEval f n (Icc x x₀) x₀ x - f x
⊢ -((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) * (↑n ! * g' y)) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc x x₀) y * (↑n ! * g' y)
Theorem: taylor_mean_remainder_unordered
Proof state before:
case h
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x x₀)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x x₀)) (Ioo x x₀)
gcont : ContinuousOn g (Icc x x₀)
gdiff : ∀ x_1 ∈ Ioo x x₀, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x x₀, g' x_1 ≠ 0
hx₀ : x < x₀
y : ℝ
hy : y ∈ Ioo x x₀
h :
  ((↑n !)⁻¹ * (x - y) ^ n) • iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) / g' y =
    taylorWithinEval f n (Icc x x₀) x₀ x - f x
⊢ -((x - y) ^ n * iteratedDerivWithin (n + 1) f (Icc x x₀) y * (g x₀ - g x) * (↑n ! * g' y)) =
    (x - y) ^ n * (g x - g x₀) * iteratedDerivWithin (n + 1) f (Icc x x₀) y * (↑n ! * g' y)
Tactic:
ring
Proof state after:
no goals
Theorem: taylor_mean_remainder_unordered
Proof state before:
case inl
f g g' : ℝ → ℝ
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 g (uIcc x₀ x)
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (uIcc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (uIcc x₀ x) x'
Tactic:
rw [uIcc_of_le hx₀.le] at hf hf' gcont ⊢
Proof state after:
case inl
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x'
Theorem: taylor_mean_remainder_unordered
Proof state before:
case inl
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (uIoo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ uIoo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ uIoo x₀ x, g' x_1 ≠ 0
hx₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ uIoo x₀ x),
      f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x'
Tactic:
rw [uIoo_of_le hx₀.le] at g'_ne gdiff hf' ⊢
Proof state after:
case inl
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
hx₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo x₀ x),
      f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x'
Theorem: taylor_mean_remainder_unordered
Proof state before:
case inl
f g g' : ℝ → ℝ
x x₀ : ℝ
n : ℕ
hx : x₀ ≠ x
hf : ContDiffOn ℝ (↑n) f (Icc x₀ x)
hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc x₀ x)) (Ioo x₀ x)
gcont : ContinuousOn g (Icc x₀ x)
gdiff : ∀ x_1 ∈ Ioo x₀ x, HasDerivAt g (g' x_1) x_1
g'_ne : ∀ x_1 ∈ Ioo x₀ x, g' x_1 ≠ 0
hx₀ : x₀ < x
⊢ ∃ x',
    ∃ (_ : x' ∈ Ioo x₀ x),
      f x - taylorWithinEval f n (Icc x₀ x) x₀ x =
        ((x - x') ^ n / ↑n ! * (g x - g x₀) / g' x') • iteratedDerivWithin (n + 1) f (Icc x₀ x) x'
Tactic:
exact taylor_mean_remainder hx₀ hf hf' gcont gdiff g'_ne
Proof state after:
no goals
Theorem: taylor_mean_remainder_lagrange_unordered
Proof 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
Proof 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)!
Theorem: taylor_mean_remainder_lagrange_unordered
Proof 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)
Proof 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)!
Theorem: taylor_mean_remainder_lagrange_unordered
Proof 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⟩
Proof 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)!
Theorem: taylor_mean_remainder_lagrange_unordered
Proof 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
Proof 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)!