mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ↑r' < r
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : C > 0
hp : ∀ (n : ℕ), ‖p n‖ * ↑r' ^ n ≤ C * a ^ n
y : E
hy : y ∈ Metric.ball 0 ↑r'
n : ℕ
ys : x + y ∈ insert x s
yr' : ‖y‖ < ↑r'
hr'0 : 0 < ↑r'
this✝ : y ∈ Metric.eball 0 r
ya : a * (‖y‖ / ↑r') ≤ a
this : ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n / (1 - a * (‖y‖ / ↑r'))
⊢ ‖p.partialSum n y - f (x + y)‖ ≤ C * (a * (‖y‖ / ↑r')) ^ n / (1 - a)

Tactic:
by
    refine this.trans ?_
    have : 0 < a := ha.1
    gcongr
    apply_rules [sub_pos.2, ha.2]

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

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
h : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
⊢ ((p.leftInv i x).comp p).comp (p.rightInv i x) = (id 𝕜 E x).comp (p.rightInv i x)

Tactic:
by rw [leftInv_comp p i _ h]

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

Goal state before:
pp: n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ k ∈ Ico 2 (n + 1), ∑ c ∈ {c | 1 < c.length}.toFinset, ∏ j, r * (a ^ c.blocksFun j * p (c.blocksFun j)) ≤
    ∑ d ∈ compPartialSumTarget 2 (n + 1) n, ∏ j, r * (a ^ d.snd.blocksFun j * p (d.snd.blocksFun j))

Tactic:
rw [sum_sigma']

Goal state after:
n : ℕ
p : ℕ → ℝ
hp : ∀ (k : ℕ), 0 ≤ p k
r a : ℝ
hr : 0 ≤ r
ha : 0 ≤ a
⊢ ∑ x ∈ (Ico 2 (n + 1)).sigma fun k ↦ {c | 1 < c.length}.toFinset,
      ∏ j, r * (a ^ x.snd.blocksFun j * p (x.snd.blocksFun j)) ≤
    ∑ d ∈ compPartialSumTarget 2 (n + 1) n, ∏ j, r * (a ^ d.snd.blocksFun j * p (d.snd.blocksFun j))
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
r : ℝ≥0∞
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
h : ∀ (i : ι), r ≤ (p i).radius
⊢ r ≤ (pi p).radius

Tactic:
by
  apply le_of_forall_nnreal_lt (fun r' hr' ↦ ?_)
  have I i : ∃ C > 0, ∀ n, ‖p i n‖ * (r' : ℝ) ^ n ≤ C :=
    norm_mul_pow_le_of_lt_radius _ (hr'.trans_le (h i))
  choose C C_pos hC using I
  obtain ⟨D, D_nonneg, hD⟩ : ∃ D ≥ 0, ∀ i, C i ≤ D :=
    ⟨∑ i, C i, Finset.sum_nonneg (fun i _ ↦ (C_pos i).le),
      fun i ↦ Finset.single_le_sum (fun j _ ↦ (C_pos j).le) (Finset.mem_univ _)⟩
  apply le_radius_of_bound _ D (fun n ↦ ?_)
  rcases le_or_gt ((r' : ℝ) ^ n) 0 with hr' | hr'
  · exact le_trans (mul_nonpos_of_nonneg_of_nonpos (by positivity) hr') D_nonneg
  · simp only [pi]
    rw [← le_div_iff₀ hr', ContinuousMultilinearMap.opNorm_pi,
      pi_norm_le_iff_of_nonneg (by positivity)]
    intro i
    exact (le_div_iff₀ hr').2 ((hC i n).trans (hD i))

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

Goal state before:
pp: case e'_3
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
n✝ n : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
this : List.map sum (ofFn fun i ↦ (d i).blocks) = c.blocks
e_2✝ :
  ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.gather
        { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ }).length =
    c.length
⊢ (fun i ↦
      ({ blocks := (ofFn fun j ↦ (d j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ }.sigmaCompositionAux
          { blocks := ofFn fun j ↦ (d j).length, blocks_pos := ⋯, blocks_sum := ⋯ } i).blocks) ≍
    fun i ↦ (d i).blocks

Tactic:
· rw [Fin.heq_fun_iff]
      · intro i
        dsimp [Composition.sigmaCompositionAux]
        rw [getElem_of_eq (splitWrtComposition_flatten _ _ _)]
        · simp only [List.getElem_ofFn]
        · simp only [map_ofFn, Function.comp_def]
      · congr

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c ↦ (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c ↦ (r c.fst.length) fun i ↦ (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
⊢ ∑ c, f c = ∑ i, g ((sigmaEquivSigmaPi n) i)

Tactic:
apply Finset.sum_congr rfl

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H := ⋯
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H := ⋯
⊢ ∀ x ∈ Finset.univ, f x = g ((sigmaEquivSigmaPi n) x)
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case insert
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_9
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
s : Set E
a : α
B : Finset α
aB : a ∉ B
hB : (∀ n ∈ B, AnalyticWithinAt 𝕜 (f n) s c) → AnalyticWithinAt 𝕜 (fun z ↦ ∏ n ∈ B, f n z) s c
h : ∀ n ∈ insert a B, AnalyticWithinAt 𝕜 (f n) s c
⊢ AnalyticWithinAt 𝕜 (fun z ↦ ∏ n ∈ insert a B, f n z) s c

Tactic:
simp_rw [Finset.prod_insert aB]
    simp only [Finset.mem_insert] at h
    exact (h a (Or.inl rfl)).mul (hB fun b m ↦ h b (Or.inr m))

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
ι : Type u_6
inst✝¹⁶ : CommSemiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M'
inst✝¹¹ : Module R M'
inst✝¹⁰ : TopologicalSpace M'
inst✝⁹ : AddCommMonoid N
inst✝⁸ : Module R N
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ContinuousAdd N
inst✝⁵ : ContinuousConstSMul R N
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R N'
inst✝² : TopologicalSpace N'
inst✝¹ : ContinuousAdd N'
inst✝ : ContinuousConstSMul R N'
f : N →L[R] N'
g₁ g₂ : M [⋀^ι]→L[R] N
⊢ f.compContinuousAlternatingMap (g₁ + g₂) = f.compContinuousAlternatingMap g₁ + f.compContinuousAlternatingMap g₂

Tactic:
by ext1; apply f.map_add

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Alternating.Basic

Goal state before:
pp: 𝕜 : Type u
n : ℕ
E : Type wE
F : Type wF
G : Type wG
ι : Type v
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G
C : ℝ
H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖
x : F
⊢ ‖{ toFun := fun x ↦ (f x).mkContinuous (C * ‖x‖) ⋯, map_add' := ⋯, map_smul' := ⋯ } x‖ ≤ max C 0 * ‖x‖

Tactic:
rw [LinearMap.coe_mk, AddHom.coe_mk]
      exact (mkContinuous_norm_le' _ _).trans_eq <| by
        rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_6
F' : ι → Type u_7
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
i : ι
f : (i : ι) → F' i
s' : Set ((i : ι) → F' i)
⊢ DifferentiableWithinAt 𝕜 (fun f ↦ f i) s' f

Tactic:
by
  apply HasFDerivWithinAt.differentiableWithinAt
  fun_prop

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

Goal state before:
pp: case mpr.cont.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
m : ℕ
hm : ↑(m + 1) ≤ ↑n.succ
⊢ ContinuousOn (fun x ↦ p x (m + 1)) s

Tactic:
· refine (continuousMultilinearCurryRightEquiv' 𝕜 m E F).comp_continuousOn_iff.mp ?_
        refine Htaylor.cont _ ?_
        rw [Nat.cast_le] at hm ⊢
        exact Nat.lt_succ_iff.mp hm

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

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
⊢ ftaylorSeriesWithin 𝕜 f univ = ftaylorSeries 𝕜 f

Tactic:
by
  ext1 x; ext1 n
  change iteratedFDerivWithin 𝕜 n f univ x = iteratedFDeriv 𝕜 n f x
  rw [iteratedFDerivWithin_univ]

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

Goal state before:
pp: 𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕝 : Type u_3
inst✝³ : DivisionSemiring 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : SMulCommClass 𝕜 𝕝 F
inst✝ : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
⊢ deriv (c • f) x = c • deriv f x

Tactic:
simp only [← derivWithin_univ, derivWithin_const_smul_field]

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
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
⊢ HasSum (fun m ↦ z ^ m • a m) 0

Tactic:
by simpa [ha 0 hn, h] using hasSum_at_zero a

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

Goal state before:
pp: a b R : ℝ
c : ℂ
h_R : R ≠ 0
x✝ : b - a ≤ 2 * π
⊢ Set.InjOn (circleMap c R) (Set.Ico a b)

Tactic:
by
  rintro _ ⟨_, _⟩ _ ⟨_, _⟩ h
  apply eq_of_circleMap_eq h_R _ h
  rw [abs_lt]
  constructor <;> linarith

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

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m ↦ z ^ m • a (m + n)) t

pp: case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m ↦ z ^ m • a (m + n)) t

Tactic:
· have : s = 0 := hs.unique (by simpa [ha 0 hn, h] using hasSum_at_zero a)
    exact ⟨a n, by simp [h, hn.ne', this], by simpa [h] using hasSum_at_zero fun m => a (m + n)⟩

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : E
n : ℕ
z : 𝕜
a : ℕ → E
hs : HasSum (fun m ↦ z ^ m • a m) s
ha : ∀ k < n, a k = 0
hn : n > 0
h : ¬z = 0
⊢ ∃ t, z ^ n • t = s ∧ HasSum (fun m ↦ z ^ m • a (m + n)) t
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter (𝕜' × 𝕜')
hh₂ : HasDerivAtFilter h₂ h₂' L'
hh : HasDerivAtFilter h h' L
hL : Tendsto (Prod.map h h) L L'
⊢ HasDerivAtFilter (h₂ ∘ h) (h₂' * h') L

Tactic:
rw [mul_comm]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
L' : Filter (𝕜' × 𝕜')
hh₂ : HasDerivAtFilter h₂ h₂' L'
hh : HasDerivAtFilter h h' L
hL : Tendsto (Prod.map h h) L L'
⊢ HasDerivAtFilter (h₂ ∘ h) (h' * h₂') L
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
⊢ HasDerivWithinAt (h₂ ∘ h) (h₂' * h') s x

Tactic:
rw [mul_comm]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
s' : Set 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasDerivWithinAt h₂ h₂' s' (h x)
hh : HasDerivWithinAt h h' s x
hst : MapsTo h s s'
⊢ HasDerivWithinAt (h₂ ∘ h) (h' * h₂') s x
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' (h x)
hh : HasStrictDerivAt h h' x
⊢ HasStrictDerivAt (h₂ ∘ h) (h₂' * h') x

Tactic:
rw [mul_comm]

Goal state after:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h : 𝕜 → 𝕜'
h₂ : 𝕜' → 𝕜'
h' h₂' : 𝕜'
hh₂ : HasStrictDerivAt h₂ h₂' (h x)
hh : HasStrictDerivAt h h' x
⊢ HasStrictDerivAt (h₂ ∘ h) (h' * h₂') x
Module: Mathlib.Analysis.Calculus.Deriv.Comp

Goal state before:
pp: 𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x)) (derivWithin f s x)

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
  · exact (hl.hasFDerivWithinAt.comp_hasDerivWithinAt x hf.hasDerivWithinAt hs).derivWithin hsx
  · simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

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
x : E
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
this : ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x

Tactic:
rcases this with ⟨u, hu, 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
n : ℕ∞ω
h : ContDiffWithinAt 𝕜 n f s x
u : Set E
hu : u ∈ 𝓝[insert x s] x
p : E → FormalMultilinearSeries 𝕜 E F
H : HasFTaylorSeriesUpToOn 0 f p u
⊢ ContinuousWithinAt f s x
Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
⊢ (e.restr (e.source ∩ s)).source = (e.restr s).source

Tactic:
simp [e.open_source.interior_eq, ← inter_assoc]

Goal state after:
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✝ c : OrderedFinpartition n
k i : Fin c.length
hi : i ∈ univ
j : Fin c.length
hj✝ : j ∈ univ
hij : i ≠ j
h : i ≠ k
hj : j ≠ k
⊢ (Disjoint on fun m ↦
      range
        (if h : m = k then
          have this := ⋯;
          (fun i ↦ cases 0 (succ ∘ c.emb k) i) ∘ Fin.cast this
        else
          have this := ⋯;
          succ ∘ c.emb m ∘ Fin.cast this))
    i j

Tactic:
· simp only [onFun, h, ↓reduceDIte, hj]
      apply Set.disjoint_iff_forall_ne.2
      simp only [mem_range, comp_apply, ne_eq, forall_exists_index, forall_apply_eq_imp_iff,
        succ_inj]
      intro a b
      apply c.emb_ne_emb_of_ne hij

Goal state after:
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 : ℕ∞ω
h : ∀ (m : ℕ), AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
x : E
hx : x ∈ s
⊢ HasFTaylorSeriesUpToOn ω f (ftaylorSeriesWithin 𝕜 f s) (insert x s)

Tactic:
rw [insert_eq_of_mem hx]
    constructor
    · intro y _
      simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply,
        iteratedFDerivWithin_zero_apply]
    · intro k _ y hy
      exact ((h k).differentiableOn y hy).hasFDerivWithinAt
    · intro k _
      exact (h k).continuousOn

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

Goal state before:
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 ⟨f', ⟨u, H, h_fderiv⟩, h_cont_diff⟩
    refine ⟨u, H, by simp, f', fun x hxu ↦ ?_, h_cont_diff.contDiffWithinAt⟩
    exact (h_fderiv x hxu).hasFDerivWithinAt

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

Goal state before:
pp: 𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : DivisionRing 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ ((expSeries 𝕂 𝔸 n) fun x_1 ↦ x) = x ^ n / ↑n !

Tactic:
by
  rw [div_eq_mul_inv, ← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq, ← smul_eq_mul,
    expSeries_apply_eq, inv_natCast_smul_eq 𝕂 𝔸]

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

Tactic:
have A : c.length - 1 + 1 = c.length := Nat.sub_add_cancel (c.length_pos (Nat.zero_lt_succ n))
      dsimp only
      rw [dif_pos h]
      simp only [extend, extendLeft, eraseLeft]
      ext
      · exact A
      · refine (Fin.heq_fun_iff A).mpr (fun i ↦ ?_)
        induction i using Fin.induction with
        | zero => change 1 = c.partSize 0; simp [c.partSize_eq_one_of_range_emb_eq_singleton h]
        | succ i => simp only [cons_succ, val_succ]; rfl
      · refine hfunext (congrArg Fin A) ?_
        simp only
        intro i i' h'
        have : i' = Fin.cast A i := eq_of_val_eq (by apply val_eq_val_of_heq h'.symm)
        subst this
        refine (Fin.heq_fun_iff ?_).mpr ?_
        · induction i using Fin.induction with
          | zero => simp [c.partSize_eq_one_of_range_emb_eq_singleton h]
          | succ i => simp
        · intro j
          induction i using Fin.induction with
          | zero =>
            simp only [cases_zero, cast_zero, val_eq_zero]
            exact (apply_eq_of_range_eq_singleton h _).symm
          | succ i => simp

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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
m : Fin c.length
v : Fin n → E
q : E [×c.partSize m]→L[𝕜] F
⊢ c.applyOrderedFinpartition (update p m q) v = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m))

Tactic:
ext d

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
n : ℕ
c : OrderedFinpartition n
p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F
m : Fin c.length
v : Fin n → E
q : E [×c.partSize m]→L[𝕜] F
d : Fin c.length
⊢ c.applyOrderedFinpartition (update p m q) v d = update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m)) d
Module: Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
f g : 𝕜 → F
s t : Set 𝕜
h : f =ᶠ[𝓝[s] x] g
ht : t ⊆ s
n : ℕ
⊢ iteratedDerivWithin n f t =ᶠ[𝓝[s] x] iteratedDerivWithin n g t

Tactic:
unfold iteratedDerivWithin
  exact h.iteratedFDerivWithin' ht n |>.fun_comp (fun a ↦ a fun _ ↦ 1)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
s : Set 𝕜
f : 𝕜 → F
c : 𝕜
⊢ iteratedDerivWithin n (fun z ↦ f (z + c)) s = fun x ↦ iteratedDerivWithin n f (c +ᵥ s) (x + c)

Tactic:
ext x
  simp [iteratedDerivWithin, ← iteratedFDerivWithin_comp_add_right n c x]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
a : 𝕜
⊢ iteratedDeriv n (fun x ↦ -f x) a = -iteratedDeriv n f a

Tactic:
simpa only [← iteratedDerivWithin_univ] using! iteratedDerivWithin_neg f

Goal state after: