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

Goal state before:
pp: case fderivWithin.succ
𝕜 : 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
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
Hzero_eq : ∀ x ∈ s, (p x 0).curry0 = f x
Hfderiv_zero : ∀ x ∈ s, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft s x
Htaylor : HasFTaylorSeriesUpToOn (↑n) (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) s
x : E
hx : x ∈ s
m : ℕ
hm : ↑(m + 1) < ↑n.succ
⊢ HasFDerivWithinAt (fun x ↦ p x (m + 1)) (p x (m + 1).succ).curryLeft s x

Tactic:
have A : (m : ℕ∞ω) < n := by
          rw [Nat.cast_lt] at hm ⊢
          exact Nat.lt_of_succ_lt_succ hm
        have :
          HasFDerivWithinAt (𝕜 := 𝕜) (continuousMultilinearCurryRightEquiv' 𝕜 m E F ∘ (p · m.succ))
            ((p x).shift m.succ).curryLeft s x := Htaylor.fderivWithin _ A x hx
        rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'
            (f' := ((p x).shift m.succ).curryLeft)] at this
        convert! this
        ext y v
        change
          (p x (Nat.succ (Nat.succ m))) (cons y v) =
            (p x m.succ.succ) (snoc (cons y (init v)) (v (last _)))
        rw [← cons_snoc_eq_snoc_cons, snoc_init_self]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
f' g' : F
L : Filter (𝕜 × 𝕜)
hf : HasDerivAtFilter f f' L
hg : HasDerivAtFilter g g' L
⊢ HasDerivAtFilter (f + g) (f' + g') L

Tactic:
by
  simpa using (hf.hasFDerivAtFilter.add hg.hasFDerivAtFilter).hasDerivAtFilter

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

Goal state before:
pp: 𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
p : 𝕜[X]
x : 𝕜
⊢ HasStrictDerivAt (fun x ↦ eval x p) (eval x (derivative p)) x

Tactic:
by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simpa using! hp.add hq
  | monomial n a => simpa [mul_assoc, derivative_monomial]
                      using! (hasStrictDerivAt_pow n x).const_mul a

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_2
E : ι → Type u_3
inst✝² : (i : ι) → NormedAddCommGroup (E i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E F
n : ℕ
x v : (i : ι) → E i
m : Fin n → (i : ι) → E i
e : Fin n.succ ↪ ι
k : ι
hke : k ∈ range ⇑e
hkf : k ∉ range ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ Fin.cons v m (e.toEquivRange.symm ⟨k, ⋯⟩) k =
    Function.update ((Pi.compRightL 𝕜 E Subtype.val) x) ((Equiv.embeddingFinSucc n ι) e).snd
      (v ↑((Equiv.embeddingFinSucc n ι) e).snd) ⟨k, hkf⟩

Tactic:
· obtain rfl : k = e 0 := by
          rcases hke with ⟨j, rfl⟩
          simpa using hkf
        simp only [Function.Embedding.toEquivRange_symm_apply_self, Fin.cons_zero, Function.update,
          Pi.compRightL_apply]
        split_ifs with h
        · congr!
        · exfalso
          apply h
          simp_rw [← Equiv.embeddingFinSucc_snd e]

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

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
t : Set 𝕜
h : Dense t
⊢ range (deriv f) ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t))

Tactic:
rw [← derivWithin_univ]
  apply range_derivWithin_subset_closure_span_image
  simp [dense_iff_closure_eq.1 h]

Goal state after:
Module: Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty F
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ⇑e)
⊢ Function.Surjective (Prod.fst ∘ ⇑e)

Tactic:
exact Prod.fst_surjective.comp e.surjective

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
t : Set 𝕜'
x : E
hh : HasDerivWithinAt h₂ h₂' t (f x)
hf : HasFDerivWithinAt f f' s x
hst : MapsTo f s t
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
exact hh.comp_hasFDerivWithinAt x hf hst

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
ε : ℝ
ε0 : ε > 0
hε : ball x ε ∩ s ⊆ {y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Tactic:
rw [inter_comm] at hε

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
x : E
f' : E → E →L[𝕜] G
hs : Convex ℝ s
f : E → G
hder : ∀ᶠ (y : E) in 𝓝[s] x, HasFDerivWithinAt f (f' y) s y
hcont : ContinuousWithinAt f' s x
K : ℝ≥0
hK : ‖f' x‖₊ < K
ε : ℝ
ε0 : ε > 0
hε : s ∩ ball x ε ⊆ {y | HasFDerivWithinAt f (f' y) s y ∧ ‖f' y‖₊ < K}
⊢ ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
Module: Mathlib.Analysis.Calculus.ContDiff.Basic

Goal state before:
pp: case cont
𝕜 : 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
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) → (E [×m]→L[𝕜] F) → G [×m]→L[𝕜] F := fun m h ↦ h.compContinuousLinearMap fun x ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
m : ℕ
hm : ↑m ≤ n
⊢ ContinuousOn (fun x ↦ (p (g x) m).compContinuousLinearMap fun x ↦ g.contLinear) (⇑g ⁻¹' s)

Tactic:
exact (hA m).continuous.comp_continuousOn <| (hf.cont m hm).comp g.continuous.continuousOn <|
      Subset.refl _

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

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 : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
this : AnalyticOn 𝕜 (fun y ↦ (continuousMultilinearCurryFin0 𝕜 E F).symm (f y)) w
⊢ AnalyticOn 𝕜 f w

Tactic:
have : AnalyticOn 𝕜 (fun y ↦ (continuousMultilinearCurryFin0 𝕜 E F)
            ((continuousMultilinearCurryFin0 𝕜 E F).symm (f y))) w :=
          AnalyticOnNhd.comp_analyticOn (LinearIsometryEquiv.analyticOnNhd _ _) this
          (mapsTo_univ _ _)

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 : ℕ∞ω
s : Set E
t : Set F
g : F → G
f : E → F
x : E
st : MapsTo f s t
hf : ContDiffWithinAt 𝕜 ω f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
v : Set F
hv : v ∈ 𝓝[insert (f x) t] f x
q : F → FormalMultilinearSeries 𝕜 F G
hq : HasFTaylorSeriesUpToOn ω g q v
h'q : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ q x i) v
w : Set E := insert x s ∩ (u ∩ f ⁻¹' v)
wv : w ⊆ f ⁻¹' v
wu : w ⊆ u
this✝ : AnalyticOn 𝕜 (fun y ↦ (continuousMultilinearCurryFin0 𝕜 E F).symm (f y)) w
this :
  AnalyticOn 𝕜 (fun y ↦ (continuousMultilinearCurryFin0 𝕜 E F) ((continuousMultilinearCurryFin0 𝕜 E F).symm (f y))) w
⊢ AnalyticOn 𝕜 f w
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
h : ContDiffWithinAt 𝕜 ω f s x
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u

Tactic:
obtain ⟨u, hu, p, hp, h'p⟩ := h

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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn ω f p u
h'p : ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
⊢ ∃ u ∈ 𝓝[insert x s] x, AnalyticOn 𝕜 f u
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 f₁ : E → F
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
h₁ : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
⊢ ContDiffWithinAt 𝕜 n f₁ s x

Tactic:
by
  match n with
  | ω =>
    obtain ⟨u, hu, p, H, H'⟩ := h
    exact ⟨{x ∈ u | f₁ x = f x}, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right,
      fun i ↦ (H' i).mono (sep_subset _ _)⟩
  | (n : ℕ∞) =>
    intro m hm
    let ⟨u, hu, p, H⟩ := h m hm
    exact ⟨{ x ∈ u | f₁ x = f x }, Filter.inter_mem hu (mem_nhdsWithin_insert.2 ⟨hx, h₁⟩), p,
      (H.mono (sep_subset _ _)).congr fun _ ↦ And.right⟩

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

Goal state before:
pp: case mp.refine_2.refine_2
𝕜 : 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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : ω ≠ ∞
h'n : ω + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (ω + 1) f s x
Hp :
  (∀ x ∈ u, (p x 0).curry0 = f x) ∧
    (∀ x ∈ u, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft u x) ∧
      HasFTaylorSeriesUpToOn ω (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) u
H'p : ω + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ (continuousMultilinearCurryRightEquiv' 𝕜 i E F) (p x (i + 1))) u

Tactic:
apply (LinearIsometryEquiv.analyticOnNhd _ _).comp_analyticOn
        ?_ (Set.mapsTo_univ _ _)

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
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
hn : ω ≠ ∞
h'n : ω + 1 ≠ ∞
h : ContDiffWithinAt 𝕜 (ω + 1) f s x
Hp :
  (∀ x ∈ u, (p x 0).curry0 = f x) ∧
    (∀ x ∈ u, HasFDerivWithinAt (fun y ↦ p y 0) (p x 1).curryLeft u x) ∧
      HasFTaylorSeriesUpToOn ω (fun x ↦ (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x ↦ (p x).shift) u
H'p : ω + 1 = ω → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x ↦ p x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x ↦ p x (i + 1)) u
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

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
s : Set E
x₀ : E
m n : ℕ∞ω
f : E → F → G
g : E → F
t : Set F
hf : ContDiffWithinAt 𝕜 n (uncurry f) (insert x₀ s ×ˢ t) (x₀, g x₀)
ht : ∀ᶠ (x : E) in 𝓝[insert x₀ s] x₀, UniqueDiffWithinAt 𝕜 t (g x)
hgt : t ∈ 𝓝[g '' s] g x₀
hg : ContDiffWithinAt 𝕜 ∞ g s x₀
hmn : ∞ + 1 ≤ n
this : ∀ (k : ℕ), ↑k ≤ ∞ → ContDiffWithinAt 𝕜 (↑k) (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀
⊢ ContDiffWithinAt 𝕜 ∞ (fun x ↦ fderivWithin 𝕜 (f x) t (g x)) s x₀

Tactic:
rw [contDiffWithinAt_infty]
    exact fun k ↦ this k (by exact_mod_cast le_top)

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

Goal state before:
pp: case inr
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 ≤ Nat.card ↑(range (c.emb (c.index 0)))

Tactic:
convert! Nat.card_mono Subtype.finite this

Goal state after:
case e'_3
n : ℕ
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
this✝ : c.partSize (c.index 0) = Nat.card ↑(range (c.emb (c.index 0)))
h : c.index 0 ≠ 0
this : {0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩} ⊆ range (c.emb (c.index 0))
⊢ 2 = Nat.card ↑{0, c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1, ⋯⟩}
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
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
n : ℕ
c✝ c : OrderedFinpartition n
m : Fin c.length
this : ∀ (a' b' : Fin (c.partSize m + 1)), a' < b' → cases 0 (succ ∘ c.emb m) a' < cases 0 (succ ∘ c.emb m) b'
a b : Fin (update c.partSize m (c.partSize m + 1) m)
⊢ a < b → ((fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast ⋯) a < ((fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast ⋯) b

Tactic:
hab

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✝ c : OrderedFinpartition n
m : Fin c.length
this : ∀ (a' b' : Fin (c.partSize m + 1)), a' < b' → cases 0 (succ ∘ c.emb m) a' < cases 0 (succ ∘ c.emb m) b'
a b : Fin (update c.partSize m (c.partSize m + 1) m)
hab : a < b
⊢ ((fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast ⋯) a < ((fun i ↦ cases 0 (succ ∘ c.emb m) i) ∘ Fin.cast ⋯) b
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
A : 1 < c.partSize (c.index 0)
⊢ ↑(c.emb (c.index 0) 0) < ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩)

Tactic:
rw [← lt_def]

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
A : 1 < c.partSize (c.index 0)
⊢ c.emb (c.index 0) 0 < c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 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
A : 1 < c.partSize (c.index 0)
⊢ ↑(c.emb (c.index 0) 0) < ↑(c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩)

Tactic:
rw [← lt_def]

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
A : 1 < c.partSize (c.index 0)
⊢ c.emb (c.index 0) 0 < c.emb (c.index 0) ⟨c.partSize (c.index 0) - 1 - 1 + 1, ⋯⟩
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
n : ℕ∞ω
⊢ ContDiffOn 𝕜 ω f univ → ContDiff 𝕜 ω f

Tactic:
intro H
      use ftaylorSeriesWithin 𝕜 f univ
      rw [← hasFTaylorSeriesUpToOn_univ_iff]
      refine ⟨H.ftaylorSeriesWithin uniqueDiffOn_univ, fun i ↦ ?_⟩
      rw [← analyticOn_univ]
      exact H.analyticOn.iteratedFDerivWithin uniqueDiffOn_univ _

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 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n) fun x_1 ↦ x) = (↑n !)⁻¹ • x ^ n

Tactic:
by simp [expSeries]

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
s : Set E
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i) f s x
hg : ContDiffWithinAt 𝕜 (↑i) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h : t ∩ insert x s ⊆ {x | (fun x ↦ ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x) x}
hft : ContDiffOn 𝕜 (↑i) f (s ∩ t)
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x

Tactic:
have hgt : ContDiffOn 𝕜 i g (s ∩ t) := fun a ha ↦ (h (by simp_all)).2.mono inter_subset_left

Goal state after:
𝕜 : 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
x : E
i : ℕ
f g : E → F
hf : ContDiffWithinAt 𝕜 (↑i) f s x
hg : ContDiffWithinAt 𝕜 (↑i) g s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
this : ∀ᶠ (x : E) in 𝓝[insert x s] x, ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hxt : x ∈ t
h : t ∩ insert x s ⊆ {x | (fun x ↦ ContDiffWithinAt 𝕜 (↑i) f s x ∧ ContDiffWithinAt 𝕜 (↑i) g s x) x}
hft : ContDiffOn 𝕜 (↑i) f (s ∩ t)
hgt : ContDiffOn 𝕜 (↑i) g (s ∩ t)
⊢ iteratedFDerivWithin 𝕜 i (f + g) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x
Module: Mathlib.Analysis.Calculus.LocalExtr.Basic

Goal state before:
pp: s : Set ℝ
a : ℝ
⊢ 1 ∈ posTangentConeAt s a ↔ a ∈ closure (Ioi a ∩ s)

Tactic:
constructor
  · intro h
    rcases exists_fun_of_mem_tangentConeAt h with ⟨ι, l, hl, c, d, hd₀, hd, hcd⟩
    have : Tendsto (a + d ·) l (𝓝 a) := by
      simpa only [add_zero] using tendsto_const_nhds.add hd₀
    apply mem_closure_of_tendsto this
    filter_upwards [hcd.eventually_const_lt one_pos, hd] with n hcdn hdn
    refine ⟨?_, hdn⟩
    simpa using pos_of_mul_pos_right hcdn
  · intro h
    apply mem_posTangentConeAt_of_frequently_mem
    rw [mem_closure_iff_frequently, ← map_add_left_nhds_zero, frequently_map] at h
    simpa [nhdsWithin, frequently_inf_principal] using h

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t ↦ (AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t
hMVT : ∃ t ∈ Ioo 0 1, (f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)

Tactic:
rcases hMVT with ⟨t, Ht, hMVT'⟩

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
x y : E
f' : E → StrongDual ℝ E
hf : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hs : Convex ℝ s
xs : x ∈ s
ys : y ∈ s
g : ℝ → E := fun t ↦ (AffineMap.lineMap x y) t
I : Set ℝ := Icc 0 1
hsub : Ioo 0 1 ⊆ I
hmaps : MapsTo g I s
hfg : ∀ t ∈ I, HasDerivWithinAt (f ∘ g) ((f' (g t)) (y - x)) I t
t : ℝ
Ht : t ∈ Ioo 0 1
hMVT' : (f' (g t)) (y - x) = (f (g 1) - f (g 0)) / (1 - 0)
⊢ ∃ z ∈ segment ℝ x y, f y - f x = (f' z) (y - x)
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid O
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
c : R
hc : 0 < c
x : M
hx : x ∈ ⇑f ⁻¹' ↑C
⊢ c • x ∈ ⇑f ⁻¹' ↑C

Tactic:
mem_preimage,

Goal state after:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid O
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
c : R
hc : 0 < c
x : M
hx : x ∈ ⇑f ⁻¹' ↑C
⊢ f (c • x) ∈ ↑C
Module: Mathlib.Geometry.Convex.Cone.Basic

Goal state before:
pp: 𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid O
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
x : M
hx : x ∈ ⇑f ⁻¹' ↑C
y : M
hy : y ∈ ⇑f ⁻¹' ↑C
⊢ x + y ∈ ⇑f ⁻¹' ↑C

Tactic:
mem_preimage,

Goal state after:
𝕜 : Type u_1
R : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid O
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R O
f : M →ₗ[R] N
C : ConvexCone R N
x : M
hx : x ∈ ⇑f ⁻¹' ↑C
y : M
hy : y ∈ ⇑f ⁻¹' ↑C
⊢ f (x + y) ∈ ↑C