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

Goal state before:
pp: case cont
𝕜 : 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
⊢ ∀ (m_1 : ℕ), ↑m_1 ≤ ↑m → ContinuousOn (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m_1) s

Tactic:
intro k hk

Goal state after:
case cont
𝕜 : 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
⊢ ContinuousOn (fun x ↦ ftaylorSeriesWithin 𝕜 f s x k) s
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case e_3
𝕜 : 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}
x : Fin n
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
this : x = x.succ.pred ⋯
⊢ Fin.cast ⋯ ((Fin.cast A i).pred ⋯).succ = i

pp: case e_4
𝕜 : 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}
x : Fin n
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
this : x = x.succ.pred ⋯
⊢ Fin.cast ⋯ j ≍ j

Tactic:
· simp

Goal state after:
case e_4
𝕜 : 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}
x : Fin n
i : Fin c.length
j : Fin (c.partSize i)
hij : c.emb i j = x.succ
A : c.length = c.length - 1 + 1
i_ne : i ≠ 0
this : x = x.succ.pred ⋯
⊢ Fin.cast ⋯ j ≍ j
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case refine_1
𝕜 : 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 : ℕ∞ω
hs : UniqueDiffOn 𝕜 s
H : ContDiffOn 𝕜 (n + 1) f s
⊢ n = ω → AnalyticOn 𝕜 f s

Tactic:
rintro rfl
    exact H.analyticOn

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

Goal state before:
pp: case mp
𝕜 : 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
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
⊢ t ∈ 𝓝 x ∧ ∀ x ∈ t, HasFDerivAt f (f' x) x

Tactic:
refine ⟨mem_nhds_iff.mpr ⟨t, Subset.rfl, ht, hxt⟩, ?_⟩

Goal state after:
case mp
𝕜 : 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
x : E
n : ℕ
u : Set E
H : u ∈ 𝓝 x
f' : E → E →L[𝕜] F
h_fderiv : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x
h_cont_diff : ContDiffWithinAt 𝕜 (↑n) f' u x
t : Set E
htu : t ⊆ u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
⊢ ∀ x ∈ t, HasFDerivAt f (f' x) x
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case inr
𝕜 : 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
x✝¹ : i ∈ univ
j : Fin c.length
x✝ : j ∈ univ
hij : i ≠ j
this :
  ∀ i ∈ univ,
    ∀ j ∈ univ,
      i ≠ j →
        i ≠ c.index 0 →
          (Disjoint on fun m ↦
              range fun j ↦
                if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
            i j
h : ¬i ≠ c.index 0
⊢ (Disjoint on fun m ↦
      range fun j ↦ if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
    i j

Tactic:
apply Disjoint.symm
        (this j (mem_univ j) i (mem_univ i) hij.symm ?_)

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
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
x✝¹ : i ∈ univ
j : Fin c.length
x✝ : j ∈ univ
hij : i ≠ j
this :
  ∀ i ∈ univ,
    ∀ j ∈ univ,
      i ≠ j →
        i ≠ c.index 0 →
          (Disjoint on fun m ↦
              range fun j ↦
                if h : m = c.index 0 then (c.emb m (Fin.cast ⋯ j.succ)).pred ⋯ else (c.emb m (Fin.cast ⋯ j)).pred ⋯)
            i j
h : ¬i ≠ c.index 0
⊢ j ≠ c.index 0
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 𝔸
inst✝ : CharZero 𝕂
x : 𝔸
⊢ (expSeries 𝕂 𝔸).sum x = ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n

Tactic:
exact expSeries_sum_eq x

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

Goal state before:
pp: case zero
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
⊢ (↑0!)⁻¹ • 0 ^ 0 = Pi.single 0 1 0

pp: case succ
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
⊢ (↑(n + 1)!)⁻¹ • 0 ^ (n + 1) = Pi.single 0 1 (n + 1)

Tactic:
· simp

Goal state after:
case succ
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
n : ℕ
⊢ (↑(n + 1)!)⁻¹ • 0 ^ (n + 1) = Pi.single 0 1 (n + 1)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case inl
𝔸 : Type u_2
inst✝⁵ : Ring 𝔸
inst✝⁴ : TopologicalSpace 𝔸
inst✝³ : IsTopologicalRing 𝔸
inst✝² : T2Space 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h✝ : IsEmpty (Algebra ℚ 𝔸)
⊢ star (exp x) = exp (star x)

pp: case inr
𝔸 : Type u_2
inst✝⁵ : Ring 𝔸
inst✝⁴ : TopologicalSpace 𝔸
inst✝³ : IsTopologicalRing 𝔸
inst✝² : T2Space 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
val✝ : Algebra ℚ 𝔸
⊢ star (exp x) = exp (star x)

Tactic:
· simp

Goal state after:
case inr
𝔸 : Type u_2
inst✝⁵ : Ring 𝔸
inst✝⁴ : TopologicalSpace 𝔸
inst✝³ : IsTopologicalRing 𝔸
inst✝² : T2Space 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
val✝ : Algebra ℚ 𝔸
⊢ star (exp x) = exp (star x)
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case inl
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
h✝ : IsEmpty (Algebra ℚ 𝔸)
⊢ Commute x (exp y)

pp: case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
val✝ : Algebra ℚ 𝔸
⊢ Commute x (exp y)

Tactic:
· simp

Goal state after:
case inr
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
val✝ : Algebra ℚ 𝔸
⊢ Commute x (exp y)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case neg
𝕜 : 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✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (c.emb 0) = {0}
⊢ (if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩).fst.extend
      (if h : range (c.emb 0) = {0} then ⟨c.eraseLeft h, none⟩ else ⟨c.eraseMiddle h, some (c.index 0)⟩).snd =
    c

Tactic:
rw [dif_neg h]

Goal state after:
case neg
𝕜 : 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✝
n : ℕ
c : OrderedFinpartition (n + 1)
h : ¬range (c.emb 0) = {0}
⊢ ⟨c.eraseMiddle h, some (c.index 0)⟩.fst.extend ⟨c.eraseMiddle h, some (c.index 0)⟩.snd = c
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : CharZero 𝕂
inst✝² : ContinuousSMul ℚ 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ Tendsto (fun n ↦ ‖1‖ * ‖(↑(n + 1))⁻¹‖) atTop (𝓝 0)

Tactic:
norm_one,

Goal state after:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : CharZero 𝕂
inst✝² : ContinuousSMul ℚ 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ Tendsto (fun n ↦ 1 * ‖(↑(n + 1))⁻¹‖) atTop (𝓝 0)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos.e_6
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ update v j z ∘ c.emb (c.index j) = update v (c.emb (c.index j) (c.invEmbedding j)) z ∘ c.emb (c.index j)

pp: case pos.e_6.hf
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ Injective (c.emb (c.index j))

Tactic:
· simp

Goal state after:
case pos.e_6.hf
𝕜 : 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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
j : Fin n
v : Fin n → E
z : E
m : Fin c.length
h : m = c.index j
⊢ Injective (c.emb (c.index j))
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
⊢ iteratedDerivWithin 0 id s x = if 0 = 0 then x else if 0 = 1 then 1 else 0

pp: case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ iteratedDerivWithin (n + 1) id s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0

Tactic:
· simp

Goal state after:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ iteratedDerivWithin (n + 1) id s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

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
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
α : Type u_5
H : Type u_6
inst✝ : NormedAddCommGroup H
l : Filter α
p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G
q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F
f : α → H
n : ℕ
hp_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖p₁ x k‖
hpf : ∀ k ≤ n, (fun a ↦ p₁ a k - p₂ a k) =o[l] f
hq₁_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₁ x k‖
hq₂_bdd : ∀ k ≤ n, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖q₂ x k‖
hqf : ∀ k ≤ n, (fun a ↦ q₁ a k - q₂ a k) =o[l] f
k : Fin (n + 1)
⊢ ↑k ≤ n

Tactic:
by grind

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
x : E
n : ℕ∞ω
f : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt 𝕜 n (fun x ↦ -f x) univ x

Tactic:
exact hf.neg

Goal state after:
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: case succ.zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
⊢ iteratedDerivWithin 0 (fun x ↦ x ^ (i + 1)) s x = ↑((i + 1).descFactorial 0) * x ^ (i + 1 - 0)

pp: case succ.succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
⊢ iteratedDerivWithin (k + 1) (fun x ↦ x ^ (i + 1)) s x = ↑((i + 1).descFactorial (k + 1)) * x ^ (i + 1 - (k + 1))

Tactic:
· simp

Goal state after:
case succ.succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
i : ℕ
IH : ∀ (k : ℕ), iteratedDerivWithin k (fun x ↦ x ^ i) s x = ↑(i.descFactorial k) * x ^ (i - k)
k : ℕ
⊢ iteratedDerivWithin (k + 1) (fun x ↦ x ^ (i + 1)) s x = ↑((i + 1).descFactorial (k + 1)) * x ^ (i + 1 - (k + 1))
Module: Mathlib.Analysis.Calculus.ContDiff.Operations

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
i✝ : ℕ
a : 𝕜
i : ℕ
hi : ContDiff 𝕜 (↑i) f → (iteratedFDeriv 𝕜 i fun z ↦ f (a • z)) = fun x ↦ a ^ i • iteratedFDeriv 𝕜 i f (a • x)
hf : ContDiff 𝕜 (↑(i + 1)) f
v : E
x✝ : Fin (i + 1) → E
⊢ ((a ^ (i + 1) • fderiv 𝕜 (iteratedFDeriv 𝕜 i f) (a • v)) (x✝ 0)) (tail x✝) =
    a ^ (i + 1) • ((fderiv 𝕜 (iteratedFDeriv 𝕜 i f) (a • v)) (x✝ 0)) (tail x✝)

pp: case succ.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
i✝ : ℕ
a : 𝕜
i : ℕ
hi : ContDiff 𝕜 (↑i) f → (iteratedFDeriv 𝕜 i fun z ↦ f (a • z)) = fun x ↦ a ^ i • iteratedFDeriv 𝕜 i f (a • x)
hf : ContDiff 𝕜 (↑(i + 1)) f
v : E
x✝ : Fin (i + 1) → E
⊢ DifferentiableAt 𝕜 (fun x ↦ iteratedFDeriv 𝕜 i f (a • x)) v

Tactic:
· simp

Goal state after:
case succ.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
i✝ : ℕ
a : 𝕜
i : ℕ
hi : ContDiff 𝕜 (↑i) f → (iteratedFDeriv 𝕜 i fun z ↦ f (a • z)) = fun x ↦ a ^ i • iteratedFDeriv 𝕜 i f (a • x)
hf : ContDiff 𝕜 (↑(i + 1)) f
v : E
x✝ : Fin (i + 1) → E
⊢ DifferentiableAt 𝕜 (fun x ↦ iteratedFDeriv 𝕜 i f (a • x)) v
Module: Mathlib.Topology.Order.Rolle

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
hab : a ≠ b
hfc : ContinuousOn f (uIcc a b)
hfI : f a = f b
⊢ f (min a b) = f (max a b)

Tactic:
by grind

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

Goal state before:
pp: R : Type u_2
G : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : AddCommGroup G
inst✝ : SMul R G
C : ConvexCone R G
x : G
hx : x ∈ C
left✝ : x ≠ 0
hxneg : -x ∈ C
⊢ x + -x ∈ C

Tactic:
exact add_mem hx hxneg

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (fun x ↦ (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε

Tactic:
have int_f_ne_top : (∫⁻ a : α, f a ∂μ) ≠ ∞ :=
    (hasFiniteIntegral_iff_ofNNReal.1 fint.hasFiniteIntegral).ne

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : μ.WeaklyRegular
inst✝ : SigmaFinite μ
f : α → ℝ≥0
fint : Integrable (fun x ↦ ↑(f x)) μ
fmeas : AEMeasurable f μ
ε : ℝ≥0
εpos : 0 < ↑ε
δ : ℝ≥0
δpos : 0 < δ
hδε : δ < ε
int_f_ne_top : ∫⁻ (a : α), ↑(f a) ∂μ ≠ ∞
⊢ ∃ g,
    (∀ (x : α), ↑(f x) < g x) ∧
      LowerSemicontinuous g ∧
        (∀ᵐ (x : α) ∂μ, g x < ∞) ∧
          Integrable (fun x ↦ (g x).toReal) μ ∧ ∫ (x : α), (g x).toReal ∂μ < ∫ (x : α), ↑(f x) ∂μ + ↑ε
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: R : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : PartialOrder R
G : Type u_7
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module R G
inst✝ : PosSMulMono R G
x : G
hx_nonneg : x ∈ positive R G
hx_ne_zero : x ≠ 0
hx_nonpos : -x ∈ positive R G
⊢ 0 < 0

Tactic:
by
    simpa using add_pos_of_nonneg_of_pos hx_nonpos <| hx_nonneg.lt_of_ne' hx_ne_zero

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

Goal state before:
pp: 𝕜 : Type u_1
M : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : AddCommGroup M
inst✝ : Module 𝕜 M
s : Set M
hs : Convex 𝕜 s
x : M
⊢ x ∈ toCone s hs ↔ ∃ c, 0 < c ∧ c • x ∈ s

Tactic:
refine hs.mem_toCone.trans ⟨?_, ?_⟩
  · rintro ⟨c, hc, y, hy, rfl⟩
    exact ⟨c⁻¹, inv_pos.2 hc, by rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]⟩
  · rintro ⟨c, hc, hcx⟩
    exact ⟨c⁻¹, inv_pos.2 hc, _, hcx, by rw [smul_smul, inv_mul_cancel₀ hc.ne', one_smul]⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv

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

pp: case refine_3
x : ℝ
h : |x| < 1
n : ℕ
F : ℝ → ℝ := fun x ↦ ∑ i ∈ Finset.range n, x ^ (i + 1) / (↑i + 1) + log (1 - x)
F' : ℝ → ℝ := fun x ↦ -x ^ n / (1 - x)
A : ∀ y ∈ Set.Ioo (-1) 1, HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, |F' y| ≤ |x| ^ n / (1 - |x|)
⊢ x ∈ Set.Icc (-|x|) |x|

Tactic:
· simp

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

Goal state before:
pp: y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
⊢ 1 - y ≠ 0

Tactic:
by grind

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : E
s : Set E
⊢ x ∈ hull R s ↔ ∃ c, ↑c.support ⊆ s ∧ (∀ (y : E), 0 ≤ c y) ∧ (c.sum fun m r ↦ r • m) = x

Tactic:
rw [mem_span_set]
  constructor
  · rintro ⟨c, hc, rfl⟩
    exact ⟨⟨c.support, Subtype.val ∘ c, by simp [← Subtype.val_inj]⟩, hc, fun y ↦ (c y).2, rfl⟩
  · rintro ⟨c, hc, hc₀, rfl⟩
    exact ⟨⟨c.support, fun y ↦ ⟨c y, hc₀ _⟩, by simp⟩, hc, rfl⟩

Goal state after:
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 : ℝ
hy : y ∈ Set.Ioo (-1) 1
⊢ -1 < y

Tactic:
by grind

Goal state after:
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 : ℝ
hy : y ∈ Set.Ioo (-1) 1
⊢ y < 1

Tactic:
by grind

Goal state after:
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 : ℝ
hy : y ∈ Set.Icc 0 x
⊢ -1 < y

Tactic:
by grind

Goal state after:
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 : ℝ
hy : y ∈ Set.Icc 0 x
⊢ y < 1

Tactic:
by grind

Goal state after:
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : s ⊆ 0
⊢ gauge s = 0

Tactic:
obtain rfl | rfl := subset_singleton_iff_eq.1 h

Goal state after:
case inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
h : ∅ ⊆ 0
⊢ gauge ∅ = 0

case inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
h : {0} ⊆ 0
⊢ gauge {0} = 0
Module: Mathlib.Analysis.Convex.Gauge

Goal state before:
pp: E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
hs₀ : StarConvex ℝ 0 s
hs₂ : Absorbs ℝ s {x}
hx : x ∉ a • s
⊢ a ≤ gauge s x

Tactic:
rw [starConvex_zero_iff] at hs₀
  obtain ⟨r, hr, h⟩ := hs₂.exists_pos
  refine le_csInf ⟨r, hr, singleton_subset_iff.1 <| h _ (Real.norm_of_nonneg hr.le).ge⟩ ?_
  rintro b ⟨hb, x, hx', rfl⟩
  refine not_lt.1 fun hba => hx ?_
  have ha := hb.trans hba
  refine ⟨(a⁻¹ * b) • x, hs₀ hx' (by positivity) ?_, ?_⟩
  · rw [← div_eq_inv_mul]
    exact div_le_one_of_le₀ hba.le ha.le
  · dsimp only
    rw [← mul_smul, mul_inv_cancel_left₀ ha.ne']

Goal state after: