mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
a✝ : m ∈ Finset.univ
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
⊢ ↑(n.choose ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(↑p).countPerms * ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(↑(Sym.fill i m p)).countPerms *
      (‖iteratedFDerivWithin 𝕜 (Multiset.count i ↑(Sym.fill i m p)) (f i) s x‖ *
        ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)

Tactic:
]

Goal state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
a✝ : m ∈ Finset.univ
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
⊢ ↑(n.choose ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(↑p).countPerms * ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(↑(Sym.fill i m p)).countPerms *
      (‖iteratedFDerivWithin 𝕜 (Multiset.count i ↑(Sym.fill i m p)) (f i) s x‖ *
        ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
a✝ : m ∈ Finset.univ
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
⊢ ↑(n.choose ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(↑p).countPerms * ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(n.choose ↑m * (↑p).countPerms) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)

Tactic:
]

Goal state after:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
a✝ : m ∈ Finset.univ
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
⊢ ↑(n.choose ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(↑p).countPerms * ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑p) (f x_1) s x‖) =
    ↑(n.choose ↑m * (↑p).countPerms) *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
a✝ : m ∈ Finset.univ
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
this :
  ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
⊢ ↑(n.choose ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖) =
    ↑(n.choose ↑m) * ↑(↑p).countPerms *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
a✝ : m ∈ Finset.univ
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
this :
  ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ =
    ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖
⊢ ↑(n.choose ↑m) * ‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
      (↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑(Sym.fill i m p)) (f j) s x‖) =
    ↑(n.choose ↑m) * ↑(↑p).countPerms *
      (‖iteratedFDerivWithin 𝕜 (↑m) (f i) s x‖ *
        ∏ x_1 ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count x_1 ↑(Sym.fill i m p)) (f x_1) s x‖)
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
s : Set E
ι : Type u_2
A' : Type u_4
inst✝³ : NormedCommRing A'
inst✝² : NormedAlgebra 𝕜 A'
inst✝¹ : DecidableEq ι
inst✝ : NormOneClass A'
f : ι → E → A'
N : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
i : ι
u : Finset ι
hi : i ∉ u
n : ℕ
hn : ↑n ≤ N
hf : ContDiffOn 𝕜 N (f i) s ∧ ∀ a ∈ u, ContDiffOn 𝕜 N (f a) s
m : Fin (n + 1)
IH :
  ‖iteratedFDerivWithin 𝕜 (n - ↑m) (fun x ↦ ∏ j ∈ u, f j x) s x‖ ≤
    ∑ p ∈ u.sym (n - ↑m), ↑(↑p).countPerms * ∏ j ∈ u, ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖
a✝ : m ∈ Finset.univ
p : Sym ι (n - ↑m)
hp : ∀ a ∈ p, a ∈ u
hip : i ∉ p
j : ι
hj : j ∈ u
hji : j ≠ i
⊢ ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖ = ‖iteratedFDerivWithin 𝕜 (Multiset.count j ↑p) (f j) s x‖

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
n : ℕ
IH : μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
⊢ μ (s \ ⋃ p ∈ F (u n), closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)

Tactic:
]

Goal state after:
α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
n : ℕ
IH : μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
⊢ μ (s \ ⋃ p ∈ F (u n), closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: f : ℝ → ℝ
a : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioi a)
⊢ ContinuousOn f (Ioi a ∪ {a})

Tactic:
]

Goal state after:
f : ℝ → ℝ
a : ℝ
h : ContinuousAt f a
hd₀ : DifferentiableOn ℝ f (Ioi a)
⊢ ContinuousOn f (Ioi a ∪ {a})
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁵ : MetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : HasBesicovitchCovering α
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → Set ℝ
s : Set α
hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
P : Finset (α × ℝ) → Prop :=
  fun t ↦ ((↑t).PairwiseDisjoint fun p ↦ closedBall p.1 p.2) ∧ (∀ p ∈ t, p.1 ∈ s) ∧ ∀ p ∈ t, p.2 ∈ f p.1
F : Finset (α × ℝ) → Finset (α × ℝ)
hF :
  ∀ (t : Finset (α × ℝ)),
    P t →
      t ⊆ F t ∧ P (F t) ∧ μ (s \ ⋃ p ∈ F t, closedBall p.1 p.2) ≤ ↑N / (↑N + 1) * μ (s \ ⋃ p ∈ t, closedBall p.1 p.2)
u : ℕ → Finset (α × ℝ) := fun n ↦ F^[n] ∅
u_succ : ∀ (n : ℕ), u n.succ = F (u n)
Pu : ∀ (n : ℕ), P (u n)
A : ∀ (n : ℕ), μ (s \ ⋃ p ∈ ⋃ n, ↑(u n), closedBall p.1 p.2) ≤ μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2)
n : ℕ
IH : μ (s \ ⋃ p ∈ u n, closedBall p.1 p.2) ≤ (↑N / (↑N + 1)) ^ n * μ s
⊢ ↑N / (↑N + 1) * ((↑N / (↑N + 1)) ^ n * μ s) ≤ ↑N / (↑N + 1) * ((↑N / (↑N + 1)) ^ n * μ s)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: case hg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
i : ℕ
hi : i ≤ n
⊢ ↑n + 1 ≤ ↑n + 1

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
i : ℕ
hi : i ≤ n
j : ℕ
hj : j ≤ i
⊢ ‖iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)‖ =
    ‖iteratedFDerivWithin 𝕜 j (fun y ↦ fderivWithin 𝕜 g t y) t (f x)‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: case hC
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
i : ℕ
hi : i ≤ n
j : ℕ
hj : j ≤ i
this : ‖iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)‖ = ‖iteratedFDerivWithin 𝕜 (j + 1) g t (f x)‖
⊢ ‖iteratedFDerivWithin 𝕜 (j + 1) g t (f x)‖ ≤ C

Tactic:
]

Goal state after:
case hC
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
i : ℕ
hi : i ≤ n
j : ℕ
hj : j ≤ i
this : ‖iteratedFDerivWithin 𝕜 j (fderivWithin 𝕜 g t) t (f x)‖ = ‖iteratedFDerivWithin 𝕜 (j + 1) g t (f x)‖
⊢ ‖iteratedFDerivWithin 𝕜 (j + 1) g t (f x)‖ ≤ C
Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
⊢ ‖∑ i, (-1) ^ ↑i • (f (v i)) (i.removeNth v)‖ ≤ ∑ i, ‖f‖ * ∏ i, ‖v i‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
⊢ ‖∑ i, (-1) ^ ↑i • (f (v i)) (i.removeNth v)‖ ≤ ∑ i, ‖f‖ * ∏ i, ‖v i‖
Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
i : Fin (n + 1)
hi : i ∈ Finset.univ
⊢ ‖(f (v i)) (i.removeNth v)‖ ≤ ‖f‖ * ‖v i‖ * ∏ i_1, ‖v (i.succAbove i_1)‖

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
i : Fin (n + 1)
hi : i ∈ Finset.univ
⊢ ‖(f (v i)) (i.removeNth v)‖ ≤ ‖f‖ * ‖v i‖ * ∏ i_1, ‖v (i.succAbove i_1)‖
Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
⊢ ‖AlternatingMap.mkContinuousLinear alternatizeUncurryFinCLM.aux (↑n + 1) ⋯‖ ≤ ↑n + 1

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
⊢ ‖AlternatingMap.mkContinuousLinear alternatizeUncurryFinCLM.aux (↑n + 1) ⋯‖ ≤ ↑n + 1
Module: Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
⊢ ((AlternatingMap.mkContinuousLinear alternatizeUncurryFinCLM.aux (↑n + 1) ⋯) f) v =
    ∑ i, (-1) ^ ↑i • (f (v i)) (i.removeNth v)

Tactic:
]

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F
v : Fin (n + 1) → E
⊢ ((AlternatingMap.mkContinuousLinear alternatizeUncurryFinCLM.aux (↑n + 1) ⋯) f) v =
    ∑ i, (-1) ^ ↑i • (f (v i)) (i.removeNth v)
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
Fu : Type u
inst✝³ : NormedAddCommGroup Fu
inst✝² : NormedSpace 𝕜 Fu
f : E → Fu
s : Set E
t : Set Fu
x : E
ht : UniqueDiffOn 𝕜 t
hs : UniqueDiffOn 𝕜 s
hst : MapsTo f s t
hx : x ∈ s
C D : ℝ
n : ℕ
IH :
  ∀ m ≤ n,
    ∀ {Gu : Type u} [inst : NormedAddCommGroup Gu] [inst_1 : NormedSpace 𝕜 Gu] {g : Fu → Gu},
      ContDiffOn 𝕜 (↑m) g t →
        ContDiffOn 𝕜 (↑m) f s →
          (∀ i ≤ m, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
            (∀ (i : ℕ), 1 ≤ i → i ≤ m → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
              ‖iteratedFDerivWithin 𝕜 m (g ∘ f) s x‖ ≤ ↑m ! * C * D ^ m
Gu : Type u
inst✝¹ : NormedAddCommGroup Gu
inst✝ : NormedSpace 𝕜 Gu
g : Fu → Gu
hg : ContDiffOn 𝕜 (↑(n + 1)) g t
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hC : ∀ i ≤ n + 1, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C
hD : ∀ (i : ℕ), 1 ≤ i → i ≤ n + 1 → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i
M : ↑n < ↑n.succ
Cnonneg : 0 ≤ C
Dnonneg : 0 ≤ D
I : ∀ i ∈ Finset.range (n + 1), ‖iteratedFDerivWithin 𝕜 i (fderivWithin 𝕜 g t ∘ f) s x‖ ≤ ↑i ! * C * D ^ i
J : ∀ (i : ℕ), ‖iteratedFDerivWithin 𝕜 (n - i) (fderivWithin 𝕜 f s) s x‖ ≤ D ^ (n - i + 1)
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 (g ∘ f) s y) s x‖ =
    ‖iteratedFDerivWithin 𝕜 n (fun y ↦ fderivWithin 𝕜 (g ∘ f) s y) s x‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.DerivativeTest

Goal state before:
pp: f : ℝ → ℝ
b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ IsMinOn f univ b

Tactic:
refine isMinOn_univ_of_anti_mono ?_ ?_

Goal state after:
case refine_1
f : ℝ → ℝ
b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ AntitoneOn f (Iic b)

case refine_2
f : ℝ → ℝ
b : ℝ
hb : ContinuousAt f b
hd₀ : DifferentiableOn ℝ f (Iio b)
hd₁ : DifferentiableOn ℝ f (Ioi b)
h₀ : ∀ x ∈ Iio b, deriv f x ≤ 0
h₁ : ∀ x ∈ Ioi b, 0 ≤ deriv f x
⊢ MonotoneOn f (Ici b)