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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst✝³ : DivisionSemiring 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : SMulCommClass 𝕜 𝕝 F
inst✝ : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c • f y) s x = c • derivWithin f s x

pp: case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst✝³ : DivisionSemiring 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : SMulCommClass 𝕜 𝕝 F
inst✝ : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c • f y) s x = c • derivWithin f s x

Tactic:
· simp [← fderivWithin_derivWithin, ← Pi.smul_def, fderivWithin_const_smul_field c hsx]

Goal state after:
case neg
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst✝³ : DivisionSemiring 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : SMulCommClass 𝕜 𝕝 F
inst✝ : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y ↦ c • f y) s x = c • derivWithin f s x
Module: Mathlib.Analysis.Calculus.Deriv.Pow

Goal state before:
pp: 𝕜 : Type u_1
𝔸 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedCommRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
n : ℕ
⊢ HasDerivWithinAt (fun x ↦ f x ^ n) (↑n * f x ^ (n - 1) * f') s x

Tactic:
by
  simpa using h.hasFDerivWithinAt.pow n |>.hasDerivWithinAt

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 b : k
⊢ (b - a) • slope f a b = f b -ᵥ f a

Tactic:
by
  rcases eq_or_ne a b with (rfl | hne)
  · rw [sub_self, zero_smul, vsub_self]
  · rw [slope, smul_inv_smul₀ (sub_ne_zero.2 hne.symm)]

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

Goal state before:
pp: 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
s : Set k
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ 0 ≤ slope f x y

Tactic:
by
  rcases le_total x y with hxy | hxy
  · exact (slope_nonneg_iff_of_le hxy).mpr (hf hx hy hxy)
  · exact slope_comm f x y ▸ (slope_nonneg_iff_of_le hxy).mpr (hf hy hx hxy)

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

Goal state before:
pp: case zero_eq
𝕜 : 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
⊢ ∀ (x : (i : ι) → E i), (f.iteratedFDeriv 0 x).curry0 = f x

Tactic:
simp [ContinuousMultilinearMap.iteratedFDeriv]

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

Goal state before:
pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin f s x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t))

pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin f s x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t))

Tactic:
· simpa [derivWithin_zero_of_not_uniqueDiffWithinAt H] using subset_closure (zero_mem _)

Goal state after:
case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s t : Set 𝕜
h : s ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ t)
x : 𝕜
H : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin f s x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑(Submodule.span 𝕜 (f '' t))
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((p 0) fun x ↦ y) = (iteratedFDeriv 𝕜 0 f x) fun x ↦ y

Tactic:
h.iteratedFDeriv_zero_apply_diag

Goal state after:
case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
F : Type (max u v)
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ ((p 0) fun x ↦ y) = (p 0) fun x ↦ y
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst✝ : CompleteSpace F
⊢ ((p 0) fun x ↦ y) = (iteratedFDeriv 𝕜 0 f x) fun x ↦ y

Tactic:
h.iteratedFDeriv_zero_apply_diag

Goal state after:
case zero
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst✝ : CompleteSpace F
⊢ ((p 0) fun x ↦ y) = (p 0) fun x ↦ y
Module: Mathlib.Analysis.Calculus.DSlope

Goal state before:
pp: case succ
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : 𝕜
n : ℕ
ih : ∀ {f : 𝕜 → E}, (∀ k < n, (swap dslope a)^[k] f a = 0) → (b - a) ^ n • (swap dslope a)^[n] f b = f b
f : 𝕜 → E
hf : ∀ k < n + 1, (swap dslope a)^[k] f a = 0
⊢ (b - a) ^ (n + 1) • swap dslope a ((swap dslope a)^[n] f) b = f b

Tactic:
pow_succ,

Goal state after:
case succ
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : 𝕜
n : ℕ
ih : ∀ {f : 𝕜 → E}, (∀ k < n, (swap dslope a)^[k] f a = 0) → (b - a) ^ n • (swap dslope a)^[n] f b = f b
f : 𝕜 → E
hf : ∀ k < n + 1, (swap dslope a)^[k] f a = 0
⊢ ((b - a) ^ n * (b - a)) • swap dslope a ((swap dslope a)^[n] f) b = f b
Module: Mathlib.Analysis.Complex.ReImTopology

Goal state before:
pp: a : ℝ
⊢ frontier {z | a < z.im} = {z | z.im = a}

Tactic:
by
  simpa only [frontier_Ioi] using! frontier_preimage_im (Ioi a)

Goal state after:
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
⊢ LocallyLipschitzOn s f

Tactic:
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
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x
x : E
hfgx : f x = g x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ EqOn f g univ

Tactic:
exact convex_univ.eqOn_of_fderivWithin_eq hf.differentiableOn hg.differentiableOn
    uniqueDiffOn_univ (fun x _ => by simpa using hf' _) (mem_univ _) hfgx

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
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * ‖‖x - x₀‖‖ ^ (n + 1)

Tactic:
pow_succ,

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
f : E → G
s : Set E
f' : E → E →L[𝕜] G
x₀ : E
n : ℕ
hs : Convex ℝ s
hx₀s : x₀ ∈ s
hff' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
hf' : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f' x‖ ≤ c * ‖‖x - x₀‖ ^ n‖
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : E) in 𝓝[s] x₀, ‖f x - f x₀‖ ≤ c * (‖‖x - x₀‖‖ ^ n * ‖‖x - x₀‖‖)
Module: Mathlib.Analysis.Calculus.ContDiff.Comp

Goal state before:
pp: case succ
𝕜 : 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
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
hi : ↑(i + 1) ≤ n
x : E
hx : x ∈ s
m : Fin (i + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (i + 1) (fun y ↦ (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 (i + 1) c s x) m) u

Tactic:
replace hi : (i : ℕ∞ω) < n := lt_of_lt_of_le (by norm_cast; simp) hi
    have h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s :=
      (hc.clm_apply contDiffOn_const).differentiableOn_iteratedFDerivWithin hi hs
    have h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s :=
      hc.differentiableOn_iteratedFDerivWithin hi hs
    simp only [iteratedFDerivWithin_succ_apply_left]
    rw [← fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv_apply x hx)]
    rw [fderivWithin_congr' (fun x hx ↦ ih hi.le hx) hx]
    rw [fderivWithin_clm_apply (hs x hx) (h_deriv.continuousMultilinear_apply_const _ x hx)
      (differentiableWithinAt_const u)]
    rw [fderivWithin_const_apply]
    simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.comp_zero, zero_add]
    rw [fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv x hx)]

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

Goal state before:
pp: case pos
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0

pp: case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0

Tactic:
· contrapose! h
    exact hf.hasDerivWithinAt.eventually_notMem h t ht

Goal state after:
case neg
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t : Set F
ht : ¬AccPt (f x) (𝓟 t)
h : ∃ᶠ (y : 𝕜) in 𝓝[s \ {x}] x, f y ∈ t
hf : ¬DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin f s x = 0
Module: Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Goal state before:
pp: n plength : ℕ
psize : Fin plength → ℕ
partSize_pos✝¹ : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono✝¹ : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono✝¹ : StrictMono fun m ↦ pemb m ⟨psize m - 1, ⋯⟩
disjoint✝¹ : univ.PairwiseDisjoint fun m ↦ range (pemb m)
cover✝¹ : ∀ (x : Fin n), ∃ m, x ∈ range (pemb m)
qsize : Fin plength → ℕ
partSize_pos✝ : ∀ (m : Fin plength), 0 < qsize m
qemb : (m : Fin plength) → Fin (qsize m) → Fin n
emb_strictMono✝ : ∀ (m : Fin plength), StrictMono (qemb m)
parts_strictMono✝ : StrictMono fun m ↦ qemb m ⟨qsize m - 1, ⋯⟩
disjoint✝ : univ.PairwiseDisjoint fun m ↦ range (qemb m)
cover✝ : ∀ (x : Fin n), ∃ m, x ∈ range (qemb m)
hpq : plength = plength ∧ ⟨fun m ↦ ⟨psize m, ⋯⟩, fun j ↦ pemb j⟩ ≍ ⟨fun m ↦ ⟨qsize m, ⋯⟩, fun j ↦ qemb j⟩
⊢ psize ≍ qsize ∧ pemb ≍ qemb

Tactic:
simp_all only [Sigma.mk.inj_iff, heq_eq_eq, true_and, and_true]

Goal state after:
n plength : ℕ
psize : Fin plength → ℕ
partSize_pos✝¹ : ∀ (m : Fin plength), 0 < psize m
pemb : (m : Fin plength) → Fin (psize m) → Fin n
emb_strictMono✝¹ : ∀ (m : Fin plength), StrictMono (pemb m)
parts_strictMono✝¹ : StrictMono fun m ↦ pemb m ⟨psize m - 1, ⋯⟩
disjoint✝¹ : univ.PairwiseDisjoint fun m ↦ range (pemb m)
cover✝¹ : ∀ (x : Fin n), ∃ m, x ∈ range (pemb m)
qsize : Fin plength → ℕ
partSize_pos✝ : ∀ (m : Fin plength), 0 < qsize m
qemb : (m : Fin plength) → Fin (qsize m) → Fin n
emb_strictMono✝ : ∀ (m : Fin plength), StrictMono (qemb m)
parts_strictMono✝ : StrictMono fun m ↦ qemb m ⟨qsize m - 1, ⋯⟩
disjoint✝ : univ.PairwiseDisjoint fun m ↦ range (qemb m)
cover✝ : ∀ (x : Fin n), ∃ m, x ∈ range (qemb m)
hpq : ((fun m ↦ ⟨psize m, ⋯⟩) = fun m ↦ ⟨qsize m, ⋯⟩) ∧ (fun j ↦ pemb j) ≍ fun j ↦ qemb j
⊢ psize = qsize
Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
s : Set X
heq : EqOn (↑e) (↑e') (e'.source ∩ interior s)
hsub : e'.source ∩ interior s ⊆ e.source
⊢ e.restr (e'.source ∩ interior s) ≈ e'.restr s

Tactic:
by
  refine ⟨?_, fun z hz ↦ heq (by simpa [e'.open_source.interior_eq] using hz.2)⟩
  rw [e'.restr_source s, e.restr_source' _ (e'.open_source.inter isOpen_interior),
    inter_eq_right.mpr hsub]

Goal state after:
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
s : Set 𝕜
⊢ iteratedFDerivWithin 𝕜 n f s = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDerivWithin n f s

Tactic:
by
  rw [iteratedDerivWithin_eq_equiv_comp, ← Function.comp_assoc, LinearIsometryEquiv.self_comp_symm,
    Function.id_comp]

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

Goal state before:
pp: case refine_2.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✝ c : OrderedFinpartition n
i : Fin n
⊢ ∃ m y,
    (if h : m = c.index i then (fun i_1 ↦ cases 0 (succ ∘ c.emb (c.index i)) i_1) ∘ Fin.cast ⋯
        else succ ∘ c.emb m ∘ Fin.cast ⋯)
        y =
      i.succ

pp: case refine_2.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✝ c : OrderedFinpartition n
k : Fin c.length
i : Fin n
hi : c.index i ≠ k
⊢ ∃ m y,
    (if h : m = k then (fun i ↦ cases 0 (succ ∘ c.emb k) i) ∘ Fin.cast ⋯ else succ ∘ c.emb m ∘ Fin.cast ⋯) y = i.succ

Tactic:
· have A : update c.partSize (c.index i) (c.partSize (c.index i) + 1) (c.index i) =
          c.partSize (c.index i) + 1 := by simp
        exact ⟨c.index i, (succ (c.invEmbedding i)).cast A.symm, by simp⟩

Goal state after:
case refine_2.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✝ c : OrderedFinpartition n
k : Fin c.length
i : Fin n
hi : c.index i ≠ k
⊢ ∃ m y,
    (if h : m = k then (fun i ↦ cases 0 (succ ∘ c.emb k) i) ∘ Fin.cast ⋯ else succ ∘ c.emb m ∘ Fin.cast ⋯) y = i.succ
Module: Mathlib.Analysis.Calculus.ContDiff.Defs

Goal state before:
pp: case refine_1.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 : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
⊢ ∀ (m : ℕ), ↑m ≤ ω → ContinuousOn (fun x ↦ ftaylorSeriesWithin 𝕜 f s x m) s

Tactic:
intro k _
      exact (h k).continuousOn

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

Goal state before:
pp: case pos
𝕜 : 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
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : i = c.index 0
⊢ Fin n

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
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : ¬i = c.index 0
⊢ Fin n

Tactic:
· refine Fin.pred (c.emb i (Fin.cast ?_ (succ j))) ?_
      · rw [h]
        simpa using Nat.sub_add_cancel (c.partSize_pos (c.index 0))
      · have : 0 ≤ c.emb i 0 := Fin.zero_le _
        exact (this.trans_lt (c.emb_strictMono _ (succ_pos _))).ne'

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
c : OrderedFinpartition (n + 1)
hc : range (c.emb 0) ≠ {0}
i : Fin c.length
j : Fin (update c.partSize (c.index 0) (c.partSize (c.index 0) - 1) i)
h : ¬i = c.index 0
⊢ Fin n
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 ∈ 𝓝 x,
      (↑n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n) f' u x) →
    ∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' x

pp: case mpr
𝕜 : 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 : ℕ
⊢ (∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' x) →
    ∃ u ∈ 𝓝 x,
      (↑n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n) f' u x

Tactic:
· rintro ⟨u, H, -, f', h_fderiv, h_cont_diff⟩
    rcases mem_nhds_iff.mp H with ⟨t, htu, ht, hxt⟩
    refine ⟨f', ⟨t, ?_⟩, h_cont_diff.contDiffAt H⟩
    refine ⟨mem_nhds_iff.mpr ⟨t, Subset.rfl, ht, hxt⟩, ?_⟩
    intro y hyt
    refine (h_fderiv y (htu hyt)).hasFDerivAt ?_
    exact mem_nhds_iff.mpr ⟨t, htu, ht, hyt⟩

Goal state after:
case mpr
𝕜 : 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 : ℕ
⊢ (∃ f', (∃ u ∈ 𝓝 x, ∀ x ∈ u, HasFDerivAt f (f' x) x) ∧ ContDiffAt 𝕜 (↑n) f' x) →
    ∃ u ∈ 𝓝 x,
      (↑n = ω → AnalyticOn 𝕜 f u) ∧ ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n) f' u x
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
hij : c.emb (c.index 0) 0 = x.succ
⊢ False

Tactic:
simp only [c.emb_zero] at hij

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}
x : Fin n
hij : 0 = x.succ
⊢ False
Module: Mathlib.Analysis.Normed.Algebra.Exponential

Goal state before:
pp: case succ
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp (n • x) = exp x ^ n
⊢ exp (n • x + x) = exp x ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
case succ
𝔸 : Type u_1
inst✝² : NormedRing 𝔸
inst✝¹ : NormedAlgebra ℚ 𝔸
inst✝ : CompleteSpace 𝔸
x : 𝔸
n : ℕ
ih : exp (n • x) = exp x ^ n
⊢ exp (n • x + x) = exp x ^ n * exp x
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 (derivWithin id s) s x = if n + 1 = 0 then x else if n + 1 = 1 then 1 else 0

Tactic:
iteratedDerivWithin_congr (g := fun _ ↦ 1) _ hx

Goal state after:
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

𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
h : UniqueDiffOn 𝕜 s
n : ℕ
⊢ Set.EqOn (derivWithin id s) (fun x ↦ 1) s
Module: Mathlib.Analysis.SpecialFunctions.ExpDeriv

Goal state before:
pp: ⊢ AnalyticOnNhd ℝ rexp univ

Tactic:
by
  rw [Real.exp_eq_exp_ℝ]
  exact fun x _ ↦ NormedSpace.exp_analytic x

Goal state after: