mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
hc : c ≠ 0
⊢ HasFDerivWithinAt (fun x ↦ f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)

Tactic:
lift c to 𝕜ˣ using IsUnit.mk0 c hc

Goal state after:
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
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : ↑c ≠ 0
⊢ HasFDerivWithinAt (fun x ↦ f (↑c • x)) (↑c • f') s x ↔ HasFDerivWithinAt f f' (↑c • s) (↑c • x)
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
hc : c ≠ 0
⊢ HasFDerivWithinAt (fun x ↦ f (c • x)) f' s x ↔ HasFDerivWithinAt (fun x ↦ c • f (c • x)) (c • f') s x

Tactic:
lift c to 𝕜ˣ using IsUnit.mk0 c hc

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
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : ↑c ≠ 0
⊢ HasFDerivWithinAt (fun x ↦ f (↑c • x)) f' s x ↔ HasFDerivWithinAt (fun x ↦ ↑c • f (↑c • x)) (↑c • f') s x
Module: Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

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
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
m : ℕ
⊢ ↑m < ↑(n + 1) → ∀ x ∈ s, HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft s x

Tactic:
(hm : (m : ℕ∞ω) < n.succ)

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
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
m : ℕ
hm : ↑m < ↑n.succ
⊢ ∀ x ∈ s, HasFDerivWithinAt (fun x ↦ p x m) (p x m.succ).curryLeft s x
Module: Mathlib.Analysis.Calculus.Deriv.Mul

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasStrictDerivAt d d' x
⊢ HasStrictDerivAt (fun y ↦ c * d y) (c * d') x

Tactic:
convert! (hasStrictDerivAt_const _ _).mul hd using 1

Goal state after:
case e'_9
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasStrictDerivAt d d' x
⊢ c * d' = 0 * d x + c * d'
Module: Mathlib.Analysis.Calculus.Deriv.Polynomial

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

Tactic:
| monomial n a =>

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a : k
⊢ slope f a a = 0

Tactic:
slope,

Goal state after:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a : k
⊢ (a - a)⁻¹ • (f a -ᵥ f a) = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
hne : a ≠ b
⊢ (b - a) • slope f a b = f b -ᵥ f a

Tactic:
slope,

Goal state after:
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
hne : a ≠ b
⊢ (b - a) • (b - a)⁻¹ • (f b -ᵥ f a) = f b -ᵥ f a
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ slope f a b = slope f b a

Tactic:
slope,

Goal state after:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (b - a)⁻¹ • (f b -ᵥ f a) = slope f b a
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (b - a)⁻¹ • (f b -ᵥ f a) = slope f b a

Tactic:
slope,

Goal state after:
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b : k
⊢ (b - a)⁻¹ • (f b -ᵥ f a) = (a - b)⁻¹ • (f a -ᵥ f b)
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case neg
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c

Tactic:
slope,

Goal state after:
case neg
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : Field k
inst✝² : AddCommGroup E
inst✝¹ : Module k E
inst✝ : AddTorsor E PE
f : k → PE
a b c : k
hab : ¬a = b
hbc : ¬b = c
⊢ ((c - b) / (c - a)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((b - a) / (c - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
Module: Mathlib.LinearAlgebra.AffineSpace.Slope

Goal state before:
pp: case neg.refine_1
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : 0 ≤ slope f x y
this : 0 ≤ (y - x) • slope f x y
⊢ f x ≤ f y

Tactic:
slope,

Goal state after:
case neg.refine_1
k : Type u_1
E : Type u_2
inst✝⁷ : Field k
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module k E
inst✝⁴ : LinearOrder k
inst✝³ : IsStrictOrderedRing k
inst✝² : PartialOrder E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : 0 ≤ slope f x y
this : 0 ≤ (y - x) • (y - x)⁻¹ • (f y -ᵥ f x)
⊢ f x ≤ f y
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: 𝕜 : 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 ⇑((Equiv.embeddingFinSucc n ι) e).fst
⊢ k ∈ range ⇑e

Tactic:
rw [Equiv.embeddingFinSucc_fst] at hke

Goal state after:
𝕜 : 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 ∘ Fin.succ)
⊢ k ∈ range ⇑e
Module: Mathlib.Analysis.Calculus.Deriv.Slope

Goal state before:
pp: 𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
g : 𝕜 → 𝕜
hg : MonotoneOn g s
⊢ 0 ≤ derivWithin g s x

Tactic:
by_cases hd : DifferentiableWithinAt 𝕜 g s x; swap
  · simp [derivWithin_zero_of_not_differentiableWithinAt hd]
  by_cases hx : AccPt x (𝓟 s); swap
  · simp [derivWithin_zero_of_not_accPt hx]
  exact hd.hasDerivWithinAt.nonneg_of_monotoneOn hx hg

Goal state after:
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
U : Set 𝕜
hf : AnalyticOnNhd 𝕜 f U
hU : IsPreconnected U
⊢ EqOn f 0 U ∨ ∀ᶠ (x : 𝕜) in codiscreteWithin U, f x ≠ 0

Tactic:
by
  simp only [or_iff_not_imp_right, ne_eq, eventually_iff, mem_codiscreteWithin,
    disjoint_principal_right, not_forall]
  rintro ⟨x, hx, hx2⟩
  refine hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hx fun nh ↦ hx2 ?_
  filter_upwards [nh] with a ha
  simp_all

Goal state after:
Module: Mathlib.Analysis.Analytic.IsolatedZeros

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁶ : NormedRing A
inst✝⁵ : IsDomain A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : IsTorsionFree A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
by_cases hU' : U = ∅
  · simp [hU']
  obtain ⟨z, hz⟩ : ∃ z, z ∈ U := nonempty_iff_ne_empty.mpr hU'
  by_cases hU'' : U = {z}
  · simpa [hU''] using hfg z hz
  apply (nontrivial_iff_ne_singleton hz).mpr at hU''
  -- Now connectedness implies that `z` is an accumulation point of `U`, so at least one of
  -- `f` and `g` must vanish frequently in a neighbourhood of `z`.
  have : ∃ᶠ w in 𝓝[≠] z, w ∈ U :=
    frequently_mem_iff_neBot.mpr <| hU.preperfect_of_nontrivial hU'' z hz
  have : ∃ᶠ w in 𝓝[≠] z, f w = 0 ∨ g w = 0 :=
    this.mp <| by filter_upwards with w hw using smul_eq_zero.mp (hfg w hw)
  cases frequently_or_distrib.mp this with
  | inl h => exact Or.inl <| hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h
  | inr h => exact Or.inr <| hg.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h

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

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
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : g x ∈ s
i : ℕ
⊢ iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
    (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x ↦ ↑g

Tactic:
induction i generalizing x with ext1 m
  | zero =>
    simp only [iteratedFDerivWithin_zero_apply, comp_apply,
      ContinuousMultilinearMap.compContinuousLinearMap_apply]
  | succ i IH =>
    simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply,
      ContinuousLinearEquiv.coe_coe, iteratedFDerivWithin_succ_apply_left]
    have : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s)) (g ⁻¹' s) x =
        fderivWithin 𝕜
          (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft _ (fun _x : Fin i => g) ∘
            (iteratedFDerivWithin 𝕜 i f s ∘ g)) (g ⁻¹' s) x :=
      fderivWithin_congr' (@IH) hx
    rw [this, ContinuousLinearEquiv.comp_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx)]
    simp only [ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe,
      ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply,
      ContinuousMultilinearMap.compContinuousLinearMap_apply]
    rw [ContinuousLinearEquiv.comp_right_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx),
      ContinuousLinearMap.comp_apply, coe_coe, tail_def, tail_def]

Goal state after:
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
hy : y ∈ insert x s ∩ u
⊢ ContDiffWithinAt 𝕜 ω f (insert x s ∩ u) y

Tactic:
refine ⟨insert x s ∩ u, ?_, p, hp.mono hut, fun i ↦ (h'p i).mono hut⟩

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
⊢ insert x s ∩ u ∈ 𝓝[insert y (insert x s ∩ u)] y
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv n f = deriv^[n] f

Tactic:
by
  ext x
  rw [← iteratedDerivWithin_univ]
  convert! iteratedDerivWithin_eq_iterate (F := F)
  simp [derivWithin_univ]

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

Goal state before:
pp: case inl
n : ℕ
c : OrderedFinpartition n
j : Fin c.length
h : range ((c.extendMiddle j).emb j) = {0}
this : (c.emb j 0).succ = 0
⊢ False

Tactic:
exact Fin.succ_ne_zero _ this

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

Goal state before:
pp: case inr
n : ℕ
c : OrderedFinpartition n
i j : Fin c.length
h : range ((c.extendMiddle i).emb j) = {0}
hij : j ≠ i
this : (c.emb j (Fin.cast ⋯ 0)).succ = 0
⊢ False

Tactic:
exact Fin.succ_ne_zero _ this

Goal state after:
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✝ : 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
h : i = 0
this : x.succ = 0
⊢ False

Tactic:
exact Fin.succ_ne_zero _ this

Goal state after:
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
n : ℕ
hs : UniqueDiffOn 𝕜 s
⊢ ContDiffOn 𝕜 (↑n) f s ↔
    (∀ m ≤ n, ContinuousOn (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s) ∧
      ∀ m < n, DifferentiableOn 𝕜 (fun x ↦ iteratedFDerivWithin 𝕜 m f s x) s

Tactic:
by
  rw [← WithTop.coe_natCast, contDiffOn_iff_continuousOn_differentiableOn hs]
  simp

Goal state after:
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
x : E
h : ContDiffAt 𝕜 1 f x
⊢ DifferentiableAt 𝕜 f x

Tactic:
by
  simpa [(le_refl 1), differentiableWithinAt_univ] using h.differentiableWithinAt

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

Goal state before:
pp: case e'_4.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 j : Fin c.length
hij : i < j
hj : j ≠ c.index 0
⊢ ↑(if h : j = c.index 0 then
          (c.emb j (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1, ⋯⟩.succ)).pred ⋯
        else (c.emb j (Fin.cast ⋯ ⟨update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) j - 1, ⋯⟩)).pred ⋯) +
      1 =
    ↑((fun m ↦ c.emb m ⟨c.partSize m - 1, ⋯⟩) j)

Tactic:
simp only [hj, ↓reduceDIte, ne_eq, not_false_eq_true, update_of_ne, cast_mk, val_pred]

Goal state after:
case e'_4.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 j : Fin c.length
hij : i < j
hj : j ≠ c.index 0
⊢ ↑(c.emb j ⟨c.partSize j - 1, ⋯⟩) - 1 + 1 = ↑(c.emb j ⟨c.partSize j - 1, ⋯⟩)
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case partSize
𝕜 : 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
o : Option (Fin c.length)
i : Fin c.length
⊢ { length := (c.extendMiddle i).length,
        partSize :=
          update (c.extendMiddle i).partSize ((c.extendMiddle i).index 0)
            ((c.extendMiddle i).partSize ((c.extendMiddle i).index 0) - 1),
        partSize_pos := ⋯,
        emb := fun i_1 j ↦
          if h : i_1 = i then ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j.succ)).pred ⋯
          else ((c.extendMiddle i).emb i_1 (Fin.cast ⋯ j)).pred ⋯,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }.partSize ≍
    c.partSize

Tactic:
simp only [heq_eq_eq, index_extendMiddle_zero]
        ext j
        rcases eq_or_ne i j with rfl | hij
        · simp [extendMiddle]
        · simp [hij.symm, extendMiddle]

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

Goal state before:
pp: 𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : IsEmpty (Algebra ℚ 𝔸)
x : 𝔸
⊢ (if h : Nonempty (Algebra ℚ 𝔸) then (expSeries ℚ 𝔸).sum x else 1) = 1

Tactic:
dif_neg (not_nonempty_iff.mpr ‹_›)

Goal state after:
𝔸 : Type u_2
inst✝³ : Ring 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : IsTopologicalRing 𝔸
inst✝ : IsEmpty (Algebra ℚ 𝔸)
x : 𝔸
⊢ 1 = 1
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: case pos.partSize
𝕜 : 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}
A : c.length - 1 + 1 = c.length
⊢ { length := c.length - 1 + 1, partSize := cons 1 fun i ↦ c.partSize (Fin.cast ⋯ i.succ), partSize_pos := ⋯,
        emb := fun i ↦
          cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
            (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i,
        emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }.partSize ≍
    c.partSize

Tactic:
refine (Fin.heq_fun_iff A).mpr (fun i ↦ ?_)

Goal state after:
case pos.partSize
𝕜 : 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}
A : c.length - 1 + 1 = c.length
i : Fin (c.length - 1 + 1)
⊢ { length := c.length - 1 + 1, partSize := cons 1 fun i ↦ c.partSize (Fin.cast ⋯ i.succ), partSize_pos := ⋯,
          emb := fun i ↦
            cases (motive := fun x ↦ Fin (cons 1 (fun i ↦ c.partSize (Fin.cast ⋯ i.succ)) x) → Fin (n + 1)) (fun x ↦ 0)
              (fun m ↦ succ ∘ fun j ↦ (c.emb (Fin.cast ⋯ m.succ) j).pred ⋯) i,
          emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }.partSize
      i =
    c.partSize ⟨↑i, ⋯⟩
Module: Mathlib.Topology.MetricSpace.CauSeqFilter

Goal state before:
pp: β : Type v
inst✝¹ : NormedRing β
hn : IsAbsoluteValue norm
f : CauSeq β norm
inst✝ : IsComplete β norm
⊢ ∀ (s : Set β), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → f.lim ∈ s → ↑f ⁻¹' s ∈ atTop

Tactic:
intro s os lfs
      suffices ∃ a : ℕ, ∀ b : ℕ, b ≥ a → f b ∈ s by simpa using this
      rcases Metric.isOpen_iff.1 os _ lfs with ⟨ε, ⟨hε, hεs⟩⟩
      obtain ⟨N, hN⟩ := Setoid.symm (CauSeq.equiv_lim f) _ hε
      exists N
      intro b hb
      apply hεs
      dsimp [Metric.ball]
      rw [dist_comm, dist_eq_norm]
      solve_by_elim

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

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

Tactic:
simp [iteratedDerivWithin_const]

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

Goal state before:
pp: case zero.zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
⊢ iteratedDerivWithin 0 (fun x ↦ x ^ 0) s x = ↑(Nat.descFactorial 0 0) * x ^ (0 - 0)

Tactic:
simp [iteratedDerivWithin_const]

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

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

Tactic:
simp [iteratedDerivWithin_const]

Goal state after: