mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l y
hf : DifferentiableAt 𝕜 f x
hy : y = f x
⊢ deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)

Tactic:
hy

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l (f x)
hf : DifferentiableAt 𝕜 f x
hy : y = f x
⊢ deriv (l ∘ f) x = (fderiv 𝕜 l (f x)) (deriv f x)
Module: Mathlib.Analysis.Calculus.ContDiff.RCLike

Goal state before:
pp: E : Type u_4
F : Type u_5
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
s : Set E
f : E → F
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
hn : n ≠ 0
hs : Convex ℝ s
hs' : IsCompact s
⊢ ∃ K, LipschitzOnWith K f s

Tactic:
apply LocallyLipschitzOn.exists_lipschitzOnWith_of_compact hs'
  exact (hf.of_le <| ENat.one_le_iff_ne_zero_withTop.2 hn).locallyLipschitzOn hs

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

Goal state before:
pp: 𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x | (fun y ↦ HasFDerivAt f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
x' : G
H' : x' ∈ ball x ε
⊢ ‖f' x' - f' x‖ ≤ c

Tactic:
← dist_eq_norm

Goal state after:
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
f : G → H
f' : G → G →L[𝕜] H
x : G
hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y
hcont : ContinuousAt f' x
c : ℝ
hc : 0 < c
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ {x | (fun y ↦ HasFDerivAt f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c
a b : G
h : a ∈ ball x ε ∧ b ∈ ball x ε
x' : G
H' : x' ∈ ball x ε
⊢ dist (f' x') (f' x) ≤ c
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case inl
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m : ℕ∞ω
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) t
u : Set E
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
y : E
⊢ y ∈ insert x s ∩ u → ContDiffWithinAt 𝕜 ω f (insert x s ∩ u) y

Tactic:
hy

Goal state after:
case inl
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
m : ℕ∞ω
hm : m ≤ ω
h' : m = ∞ → ω = ω
t : Set E
ht : t ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p t
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) t
u : Set E
huo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
hxu : x ∈ u
hut : insert x s ∩ u ⊆ t
y : E
hy : y ∈ insert x s ∩ u
⊢ ContDiffWithinAt 𝕜 ω f (insert x s ∩ u) y
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case fderivWithin
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
k : ℕ
hk : ↑k < ↑m
y : E
⊢ y ∈ s → HasFDerivWithinAt (fun x ↦ ftaylorSeriesWithin 𝕜 f s x k) (ftaylorSeriesWithin 𝕜 f s y k.succ).curryLeft s y

Tactic:
hy

Goal state after:
case fderivWithin
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞
Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑m ≤ n
k : ℕ
hk : ↑k < ↑m
y : E
hy : y ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ftaylorSeriesWithin 𝕜 f s x k) (ftaylorSeriesWithin 𝕜 f s y k.succ).curryLeft s y
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case fderivWithin
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
k : ℕ
a✝ : ↑k < ω
y : E
⊢ y ∈ s → HasFDerivWithinAt (fun x ↦ ftaylorSeriesWithin 𝕜 f s x k) (ftaylorSeriesWithin 𝕜 f s y k.succ).curryLeft s y

Tactic:
hy

Goal state after:
case fderivWithin
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
k : ℕ
a✝ : ↑k < ω
y : E
hy : y ∈ s
⊢ HasFDerivWithinAt (fun x ↦ ftaylorSeriesWithin 𝕜 f s x k) (ftaylorSeriesWithin 𝕜 f s y k.succ).curryLeft s y
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case e'_3.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
⊢ ↑(if h : c.index 0 = c.index 0 then
          (c.emb (c.index 0)
                (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) - 1, ⋯⟩.succ)).pred
            ⋯
        else
          (c.emb (c.index 0)
                (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) - 1, ⋯⟩)).pred
            ⋯) +
      1 =
    ↑((fun m ↦ c.emb m ⟨c.partSize m - 1, ⋯⟩) (c.index 0))

Tactic:
simp only [↓reduceDIte, update_self, succ_mk, cast_mk, val_pred]

Goal state after:
case e'_3.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
j : Fin c.length
hij : c.index 0 < j
⊢ ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩) - 1 + 1 =
    ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case e'_4.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
hij : i < c.index 0
⊢ ↑(if h : c.index 0 = c.index 0 then
          (c.emb (c.index 0)
                (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) - 1, ⋯⟩.succ)).pred
            ⋯
        else
          (c.emb (c.index 0)
                (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) (c.index 0) - 1, ⋯⟩)).pred
            ⋯) +
      1 =
    ↑((fun m ↦ c.emb m ⟨c.partSize m - 1, ⋯⟩) (c.index 0))

Tactic:
simp only [↓reduceDIte, update_self, succ_mk, cast_mk, val_pred]

Goal state after:
case e'_4.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ : OrderedFinpartition n
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
hij : i < c.index 0
⊢ ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩) - 1 + 1 =
    ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩)
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hx : s ∈ 𝓝 x
⊢ ContDiffWithinAt 𝕜 n f (univ ∩ s) x

Tactic:
univ_inter

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
hx : s ∈ 𝓝 x
⊢ ContDiffWithinAt 𝕜 n f s x
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f univ) univ ∧
    ∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun x ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ

Tactic:
refine ⟨H.ftaylorSeriesWithin uniqueDiffOn_univ, fun i ↦ ?_⟩

Goal state after:
case h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
H : ContDiffOn 𝕜 ω f univ
i : ℕ
⊢ AnalyticOnNhd 𝕜 (fun x ↦ ftaylorSeriesWithin 𝕜 f univ x i) univ
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ∞ω
⊢ ContDiff 𝕜 n f ↔ ∀ (x : E), ContDiffAt 𝕜 n f x

Tactic:
simp [← contDiffOn_univ, ContDiffOn, ContDiffAt]

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ ∀ (n : ℕ), True

Tactic:
implies_true

Goal state after:
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ ‖f j - f N‖ < ε

Tactic:
← dist_eq_norm

Goal state after:
β : Type v
inst✝ : NormedField β
f : ℕ → β
hf : CauchySeq f
hf1 : (map f atTop).NeBot
hf2 : ∀ s ∈ uniformity β, ∃ t ∈ map f atTop, t ×ˢ t ⊆ s
ε : ℝ
hε : ε > 0
t : Set β
htsub : t ×ˢ t ⊆ {x | dist x.1 x.2 < ε}
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f b ∈ t
j : ℕ
hj : j ≥ N
⊢ dist (f j) (f N) < ε
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set 𝕜
h : UniqueDiffOn 𝕜 s
f : 𝕜 → F
c : 𝕜
hs : Set.MapsTo (fun x ↦ c * x) s s
n : ℕ
ih :
  ∀ {x : 𝕜},
    x ∈ s →
      ContDiffOn 𝕜 (↑n) f s → iteratedDerivWithin n (fun x ↦ f (c * x)) s x = c ^ n • iteratedDerivWithin n f s (c * x)
x : 𝕜
hx : x ∈ s
hf : ContDiffOn 𝕜 (↑(n + 1)) f s
hcx : c * x ∈ s
h₀ : Set.EqOn (iteratedDerivWithin n (fun x ↦ f (c * x)) s) (fun x ↦ c ^ n • iteratedDerivWithin n f s (c * x)) s
h₁ : DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x)
⊢ DifferentiableWithinAt 𝕜 (iteratedDerivWithin n f s) s (c * x)

Tactic:
exact hf.differentiableOn_iteratedDerivWithin (Nat.cast_lt.mpr n.lt_succ_self) h _ hcx

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
n : ℕ∞ω
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
⊢ ContDiff 𝕜 n Φ ↔ ∀ (i : ι), ContDiff 𝕜 n fun x ↦ Φ x i

Tactic:
simp only [← contDiffOn_univ, contDiffOn_pi]

Goal state after:
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: case mp
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 1)
⊢ a ∈ closure (Ioi a ∩ s)

Tactic:
have : Tendsto (a + d ·) l (𝓝 a) := by
      simpa only [add_zero] using tendsto_const_nhds.add hd₀

Goal state after:
case mp
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (fun n ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun x ↦ a + d x) l (𝓝 a)
⊢ a ∈ closure (Ioi a ∩ s)
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
ι : Type u_3
f : ι → E → F
u : Finset ι
i : ℕ
x : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : ∀ j ∈ u, ContDiffWithinAt 𝕜 (↑i) (f j) s x
x✝ : E
⊢ ∑ j ∈ u, f j x✝ = (∑ j ∈ u, f j) x✝

Tactic:
rw [Finset.sum_apply]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
ι : Type u_3
f : ι → E → F
u : Finset ι
n : ℕ
x : E
h : ∀ j ∈ u, ContDiffAt 𝕜 (↑n) (f j) x
x✝ : E
⊢ ∑ j ∈ u, f j x✝ = (∑ j ∈ u, f j) x✝

Tactic:
rw [Finset.sum_apply]

Goal state after:
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
⊢ y ∈ D → x < y → C * (y - x) < f y - f x

Tactic:
hy

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_gt : ∀ x ∈ interior D, C < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ x < y → C * (y - x) < f y - f x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
⊢ y ∈ D → x ≤ y → C * (y - x) ≤ f y - f x

Tactic:
hy

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
C : ℝ
hf'_ge : ∀ x ∈ interior D, C ≤ deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ x ≤ y → C * (y - x) ≤ f y - f x
Module: Mathlib.Analysis.Calculus.Deriv.MeanValue

Goal state before:
pp: D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
⊢ y ∈ D → x < y → f x < f y

Tactic:
hy

Goal state after:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, 0 < deriv f x
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
⊢ x < y → f x < f y
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
B : ball x' s ⊆ ball x r'
y : E
⊢ y ∈ ball x' s → ∀ z ∈ ball x' s, ‖f z - f y - L (z - y)‖ < ε * r

Tactic:
hy

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε : ℝ
x : E
r' : ℝ
r'_mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
s : ℝ
s_gt : r / 2 < s
s_lt : s < r'
this : s ∈ Ioc (r / 2) r
x' : E
hx' : x' ∈ ball x (r' - s)
B : ball x' s ⊆ ball x r'
y : E
hy : y ∈ ball x' s
⊢ ∀ z ∈ ball x' s, ‖f z - f y - L (z - y)‖ < ε * r
Module: Mathlib.Analysis.Calculus.FDeriv.Measurable

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
L : E →L[𝕜] F
r ε δ : ℝ
h : ε ≤ δ
⊢ A f L r ε ⊆ A f L r δ

Tactic:
by
  rintro x ⟨r', r'r, hr'⟩
  refine ⟨r', r'r, fun y hy z hz => (hr' y hy z hz).trans_le (mul_le_mul_of_nonneg_right h ?_)⟩
  linarith [mem_ball.1 hy, r'r.2, @dist_nonneg _ _ y x]

Goal state after:
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: case inl
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
r : R
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
hr : r < 0
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)

pp: case inr.inl
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = 0 • (y - z)

pp: case inr.inr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
r : R
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
hr : 0 < r
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)

Tactic:
· -- r < 0: use (-r) • z - (-r) • y = r • (y - z)
        refine ⟨(-r) • z, C.smul_mem (neg_pos.mpr hr) hz,
               (-r) • y, C.smul_mem (neg_pos.mpr hr) hy, ?_⟩
        rw [neg_smul, neg_smul, neg_sub_neg, smul_sub]

Goal state after:
case inr.inl
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = 0 • (y - z)

case inr.inr
R : Type u_7
M : Type u_8
inst✝⁵ : Ring R
inst✝⁴ : LinearOrder R
inst✝³ : AddLeftStrictMono R
inst✝² : AddCommGroup M
inst✝¹ : Nontrivial M
inst✝ : Module R M
C : ConvexCone R M
h : Submodule.span R ↑C = ⊤
x : M
hne : (↑C).Nonempty
r : R
y : M
hy : y ∈ ↑C
z : M
hz : z ∈ ↑C
hr : 0 < r
⊢ ∃ x ∈ C, ∃ y_1 ∈ C, x - y_1 = r • (y - z)
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)
F' : ℝ → ℝ := fun y ↦ (y ^ 2) ^ n / (1 - y ^ 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
y : ℝ
⊢ y ∈ Set.Ioo (-1) 1 → HasDerivAt F (F' y) y

Tactic:
hy

Goal state after:
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)
F' : ℝ → ℝ := fun y ↦ (y ^ 2) ^ n / (1 - y ^ 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
y : ℝ
hy : y ∈ Set.Ioo (-1) 1
⊢ HasDerivAt F (F' y) y
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)
F' : ℝ → ℝ := fun y ↦ (y ^ 2) ^ n / (1 - y ^ 2)
y : ℝ
⊢ y ∈ Set.Icc 0 x → HasDerivAt F (F' y) y

Tactic:
hy

Goal state after:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)
F' : ℝ → ℝ := fun y ↦ (y ^ 2) ^ n / (1 - y ^ 2)
y : ℝ
hy : y ∈ Set.Icc 0 x
⊢ HasDerivAt F (F' y) y
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

Goal state before:
pp: x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)
F' : ℝ → ℝ := fun y ↦ (y ^ 2) ^ n / (1 - y ^ 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
⊢ y ∈ interior (Set.Icc 0 x) → 0 ≤ F' y

Tactic:
hy

Goal state after:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ 1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1)
F' : ℝ → ℝ := fun y ↦ (y ^ 2) ^ n / (1 - y ^ 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ interior (Set.Icc 0 x)
⊢ 0 ≤ F' y
Module: Mathlib.Analysis.Convex.Cone.Extension

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
⊢ y ∈ c → ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
hy

Goal state after:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : PointedCone ℝ E
p : E →ₗ.[ℝ] ℝ
hp_nonneg : ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x
hp_dense : ∀ (y : E), ∃ x, ↑x + y ∈ s
S : Set (E →ₗ.[ℝ] ℝ) := {p | ∀ (x : ↥p.domain), ↑x ∈ s → 0 ≤ ↑p x}
c : Set (E →ₗ.[ℝ] ℝ)
hcs : c ⊆ S
c_chain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : E →ₗ.[ℝ] ℝ
hy : y ∈ c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
x : E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : ε • s ∩ -(ε • s) ∈ 𝓝 0
y : E
⊢ y ∈ ε • s ∩ -(ε • s) → gauge s (x + y) ∈ Icc (gauge s x - ε) (gauge s x + ε)

Tactic:
hy

Goal state after:
E : Type u_2
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
s : Set E
x : E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : s ∈ 𝓝 0
ha : Absorbent ℝ s
ε : ℝ
hε₀ : 0 < ε
this : ε • s ∩ -(ε • s) ∈ 𝓝 0
y : E
hy : y ∈ ε • s ∩ -(ε • s)
⊢ gauge s (x + y) ∈ Icc (gauge s x - ε) (gauge s x + ε)
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
hpx : 0 < p x
hpx₂ : 0 < 2 * p x
⊢ (2 * p x)⁻¹ * p x < 1

Tactic:
inv_mul_lt_iff₀ hpx₂,

Goal state after:
case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
hpx : 0 < p x
hpx₂ : 0 < 2 * p x
⊢ p x < 2 * p x * 1