mathlib-initiative/mathlib-tactics huggingface dataset:
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
n : ℕ
v : Fin n → E
⊢ ((p.leftInv i x).comp p n) v = (id 𝕜 E x n) v

Tactic:
match n with
  | 0 =>
    simp only [comp_coeff_zero', leftInv_coeff_zero, ContinuousMultilinearMap.uncurry0_apply,
      id_apply_zero]
  | 1 =>
    simp only [leftInv_coeff_one, comp_coeff_one, h, id_apply_one, ContinuousLinearEquiv.coe_apply,
      ContinuousLinearEquiv.symm_apply_apply, continuousMultilinearCurryFin1_symm_apply]
  | n + 2 =>
    have A :
      (Finset.univ : Finset (Composition (n + 2))) =
        {c | Composition.length c < n + 2}.toFinset ∪ {Composition.ones (n + 2)} := by
      refine Subset.antisymm (fun c _ => ?_) (subset_univ _)
      by_cases! h : c.length < n + 2
      · simp [h]
      · simp [Composition.eq_ones_iff_le_length.2 h]
    have B :
      Disjoint ({c | Composition.length c < n + 2} : Set (Composition (n + 2))).toFinset
        {Composition.ones (n + 2)} := by
      simp
    have C :
      ((p.leftInv i x (Composition.ones (n + 2)).length)
          fun j : Fin (Composition.ones n.succ.succ).length =>
          p 1 fun _ => v ((Fin.castLE (Composition.length_le _)) j)) =
        p.leftInv i x (n + 2) fun j : Fin (n + 2) => p 1 fun _ => v j := by
      apply FormalMultilinearSeries.congr _ (Composition.ones_length _) fun j hj1 hj2 => ?_
      exact FormalMultilinearSeries.congr _ rfl fun k _ _ => by congr
    have D :
      (p.leftInv i x (n + 2) fun j : Fin (n + 2) => p 1 fun _ => v j) =
        -∑ c ∈ {c : Composition (n + 2) | c.length < n + 2}.toFinset,
            (p.leftInv i x c.length) (p.applyComposition c v) := by
      simp only [leftInv, _root_.neg_apply, neg_inj, _root_.sum_apply]
      convert!
        (sum_toFinset_eq_subtype (fun c : Composition (n + 2) => c.length < n + 2)
              (fun c : Composition (n + 2) =>
                (ContinuousMultilinearMap.compAlongComposition
                    (p.compContinuousLinearMap (i.symm : F →L[𝕜] E)) c (p.leftInv i x c.length))
                  fun j : Fin (n + 2) => p 1 fun _ : Fin 1 => v j)).symm.trans
          _
      simp only [compContinuousLinearMap_applyComposition,
        ContinuousMultilinearMap.compAlongComposition_apply]
      congr
      ext c
      congr
      ext k
      simp [h]
    simp [FormalMultilinearSeries.comp, A, Finset.sum_union B,
      applyComposition_ones, C, D, -Set.toFinset_ofPred, -Finset.union_singleton]

Goal state after:
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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ TendstoLocallyUniformlyOn (fun n y ↦ p.partialSum n y) (fun y ↦ f (x + y)) atTop
    ((fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r)

Tactic:
intro u hu y hy

Goal state after:
𝕜 : 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : y ∈ (fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r
⊢ ∃ t ∈ 𝓝[(fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun y ↦ f (x + y)) y, (fun n y ↦ p.partialSum n y) n y) ∈ u
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case h
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
⊢ a ∈ (fun p ↦ compPartialSumTarget 0 p.1 p.2) m → a ∈ (fun p ↦ compPartialSumTarget 0 p.1 p.2) n

Tactic:
ha

Goal state after:
case h
m n : ℕ × ℕ
hmn : m ≤ n
a : (n : ℕ) × Composition n
ha : a ∈ (fun p ↦ compPartialSumTarget 0 p.1 p.2) m
⊢ a ∈ (fun p ↦ compPartialSumTarget 0 p.1 p.2) n
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
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ TendstoLocallyUniformlyOn (fun n y ↦ p.partialSum n (y - x)) f atTop (Metric.eball x r)

Tactic:
simpa using hf.tendstoLocallyUniformlyOn'

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
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
this✝ : Tendsto (fun a ↦ 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a) (𝓝 0) (𝓝 (2 * I * C * r ^ 2 * (I + 1) ^ 2 * 0))
A : ∀ᶠ (a : ℝ) in 𝓝 0, 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a < 1
this : Tendsto (fun a ↦ r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0))
B : ∀ᶠ (a : ℝ) in 𝓝 0, r * (I + 1) * a < 1 / 2
a✝ : ℝ
⊢ a✝ ∈ Set.Ioi 0 → 0 < a✝

Tactic:
ha

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
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
this✝ : Tendsto (fun a ↦ 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a) (𝓝 0) (𝓝 (2 * I * C * r ^ 2 * (I + 1) ^ 2 * 0))
A : ∀ᶠ (a : ℝ) in 𝓝 0, 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a < 1
this : Tendsto (fun a ↦ r * (I + 1) * a) (𝓝 0) (𝓝 (r * (I + 1) * 0))
B : ∀ᶠ (a : ℝ) in 𝓝 0, r * (I + 1) * a < 1 / 2
a✝ : ℝ
ha : a✝ ∈ Set.Ioi 0
⊢ 0 < a✝
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
hp : 0 < p.radius
C r : ℝ
Cpos : 0 < C
rpos : 0 < r
ple : ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
I : ℝ := ‖↑i.symm‖
a : ℝ
apos : 0 < a
ha1 : 2 * I * C * r ^ 2 * (I + 1) ^ 2 * a ≤ 1
ha2 : r * (I + 1) * a ≤ 1 / 2
S : ℕ → ℝ := fun n ↦ ∑ k ∈ Ico 1 n, a ^ k * ‖p.rightInv i x k‖
IRec : ∀ (n : ℕ), 1 ≤ n → S n ≤ (I + 1) * a
a' : NNReal := ⟨a, ⋯⟩
n : ℕ
hn : 1 ≤ n
⊢ ‖p.rightInv i x n‖ * ↑a' ^ n ≤ (I + 1) * a

Tactic:
calc
    ‖p.rightInv i x n‖ * (a' : ℝ) ^ n = a ^ n * ‖p.rightInv i x n‖ := mul_comm _ _
    _ ≤ ∑ k ∈ Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ :=
      (haveI : ∀ k ∈ Ico 1 (n + 1), 0 ≤ a ^ k * ‖p.rightInv i x k‖ := fun k _ => by positivity
      single_le_sum this (by simp [hn]))
    _ ≤ (I + 1) * a := IRec (n + 1) (by simp)

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

Goal state before:
pp: case mp.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ EqOn f (fun y ↦ p.sum (y - x)) (insert x s ∩ eball x r)

pp: case mp.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesOnBall (fun y ↦ p.sum (y - x)) p x r

Tactic:
· intro y ⟨ys,yb⟩
      simp only [mem_eball, edist_eq_enorm_sub] at yb
      have e0 := p.hasSum (x := y - x) ?_
      · have e1 := (h.hasSum (y := y - x) ?_ ?_)
        · simp only [add_sub_cancel] at e1
          exact e1.unique e0
        · simpa only [add_sub_cancel]
        · simpa only [mem_eball, edist_zero_right]
      · simp only [mem_eball, edist_zero_right]
        exact lt_of_lt_of_le yb h.r_le

Goal state after:
case mp.refine_2
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesOnBall (fun y ↦ p.sum (y - x)) p x r
Module: Mathlib.Analysis.Analytic.Within

Goal state before:
pp: case mpr.refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
ys : y ∈ insert x s
xy : edist y x < r ∧ dist y x < e
⊢ dist y x < e

Tactic:
exact xy.2

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

Goal state before:
pp: case inl
𝕜 : 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : Fin i → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
h'c : c.length = 0
⊢ ∑ i_1, c.blocksFun i_1 < m * n

Tactic:
have : ∑ j : Fin c.length, c.blocksFun j = 0 := by
        apply Finset.sum_eq_zero (fun j hj ↦ ?_)
        have := j.2
        grind

Goal state after:
case inl
𝕜 : 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
m n : ℕ
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : HasFiniteFPowerSeriesAt g q (f x) m
hf : HasFiniteFPowerSeriesAt f p x n
hn : 0 < n
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall (g ∘ f) (q.comp p) x r
i : ℕ
c : Composition i
v : Fin i → E
hc : c.length < m
hi : ∀ (j : Fin c.length), c.blocksFun j < n
h'c : c.length = 0
this : ∑ j, c.blocksFun j = 0
⊢ ∑ i_1, c.blocksFun i_1 < m * n
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s x r
hg : HasFPowerSeriesWithinOnBall g pg s x r
⊢ HasFPowerSeriesWithinOnBall (f - g) (pf - pg) s x r

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
hg : HasFPowerSeriesOnBall g pg x r
⊢ HasFPowerSeriesOnBall (f - g) (pf - pg) x r

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f pf s x
hg : HasFPowerSeriesWithinAt g pg s x
⊢ HasFPowerSeriesWithinAt (f - g) (pf - pg) s x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f pf x
hg : HasFPowerSeriesAt g pg x
⊢ HasFPowerSeriesAt (f - g) (pf - pg) x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
hg : AnalyticWithinAt 𝕜 g s x
⊢ AnalyticWithinAt 𝕜 (f - g) s x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
x : E
hf : AnalyticAt 𝕜 f x
hg : AnalyticAt 𝕜 g x
⊢ AnalyticAt 𝕜 (f - g) x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
F : Type u_3
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
f : E →L[𝕜] F
x : E
s : Set E
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : T2Space F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑f) s x = f

Tactic:
DifferentiableAt.fderivWithin f.differentiableAt hxs

Goal state after:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
F : Type u_3
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace F
f : E →L[𝕜] F
x : E
s : Set E
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : T2Space F
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 (⇑f) x = f
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ take (take i b.blocks).sum a.blocks = take (take i b.blocks).sum (take (take (i + 1) b.blocks).sum a.blocks)

Tactic:
take_take,

Goal state after:
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ take (take i b.blocks).sum a.blocks = take (min (take i b.blocks).sum (take (i + 1) b.blocks).sum) a.blocks
Module: Mathlib.Analysis.Calculus.FDeriv.Comp

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAt f f' x
hx : f x = x
n : ℕ
⊢ HasFDerivAt f^[n] (f' ^ n) x

Tactic:
by
  refine HasFDerivAtFilter.iterate hf ?_ n
  simpa [hx] using hf.continuousAt.tendsto.prodMap (tendsto_pure_pure f x)

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

Goal state before:
pp: case zero.succ
n : ℕ
a : Composition n
b : Composition a.length
i : ℕ
IH :
  ∀ (hi : i < b.length),
    0 < b.blocksFun ⟨i, hi⟩ →
      (take (take i b.blocks).sum a.blocks).sum = (take i (List.map sum (a.blocks.splitWrtComposition b))).sum
hi : i + 1 < b.length
hj : 0 < b.blocksFun ⟨i + 1, hi⟩
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum = (take (i + 1) (List.map sum (a.blocks.splitWrtComposition b))).sum

Tactic:
have A : i < b.length := Nat.lt_of_succ_lt hi
      have B : i < List.length (map List.sum (splitWrtComposition a.blocks b)) := by simp [A]
      have C : 0 < blocksFun b ⟨i, A⟩ := Composition.blocks_pos' _ _ _
      rw [sum_take_succ _ _ B, ← IH A C]
      have :
        take (sum (take i b.blocks)) a.blocks =
          take (sum (take i b.blocks)) (take (sum (take (i + 1) b.blocks)) a.blocks) := by
        rw [take_take, min_eq_left]
        apply monotone_sum_take _ (Nat.le_succ _)
      rw [this, getElem_map, getElem_splitWrtComposition, ←
        take_append_drop (sum (take i b.blocks)) (take (sum (take (Nat.succ i) b.blocks)) a.blocks),
        sum_append]
      congr
      rw [take_append_drop]

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

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 g : E → F
f' g' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hg : HasFDerivAtFilter g g' L
⊢ HasFDerivAtFilter (f - g) (f' - g') L

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

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

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
f' : E →L[𝕜] F
x : E
s : Set E
a : E
⊢ HasFDerivWithinAt (fun x ↦ f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x)

Tactic:
by
  have : map (a + ·) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x) := by
    simp only [nhdsWithin, Filter.map_inf (add_right_injective a)]
    simp [← Set.image_vadd]
  simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS, ← this, Function.comp_def]

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✝¹² : Semiring 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✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N
⊢ (↑e.symm).compContinuousAlternatingMap ((↑e).compContinuousAlternatingMap f) = f

Tactic:
ext; simp [(· ∘ ·)]

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✝¹² : Semiring 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✝² : AddCommMonoid N'
inst✝¹ : Module R N'
inst✝ : TopologicalSpace N'
n : ℕ
f✝ g : M [⋀^ι]→L[R] N
e : N ≃L[R] N'
f : M [⋀^ι]→L[R] N'
⊢ (↑e).compContinuousAlternatingMap ((↑e.symm).compContinuousAlternatingMap f) = f

Tactic:
ext; simp [(· ∘ ·)]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
ι : Type u_5
inst✝¹⁴ : NormedField 𝕜
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : ContinuousSMul 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜 F
inst✝⁷ : TopologicalSpace F
inst✝⁶ : IsTopologicalAddGroup F
inst✝⁵ : ContinuousConstSMul 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : Module 𝕜 G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : ContinuousConstSMul 𝕜 G
⊢ Continuous[topologicalSpace, topologicalSpace] fun g ↦
    let __LinearMap := (compContinuousAlternatingMapₗ 𝕜 E F G) g;
    { toLinearMap := __LinearMap, cont := ⋯ }

Tactic:
rw [ContinuousLinearMap.isEmbedding_postcomp
      (ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜)
      ContinuousAlternatingMap.isEmbedding_toContinuousMultilinearMap |>.continuous_iff]
    exact map_continuous <|
      (precomp (ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) G)
        ((ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 : (E [⋀^ι]→L[𝕜] F) →L[𝕜] _))) ∘L
        (compContinuousMultilinearMapL 𝕜 (fun _ : ι ↦ E) F G)

Goal state after:
Module: Mathlib.Topology.MetricSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : Completion α
⊢ dist x y = dist y x

Tactic:
by
  refine induction_on₂ x y ?_ ?_
  · exact isClosed_eq (Completion.continuous_dist continuous_fst continuous_snd)
        (Completion.continuous_dist continuous_snd continuous_fst)
  · intro a b
    rw [Completion.dist_eq, Completion.dist_eq, dist_comm]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter (E × E)
⊢ HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x)) φ' l ↔
    HasFDerivAtFilter φ (proj 0 ∘SL φ') l ∧ HasFDerivAtFilter φs (Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l

Tactic:
rw [hasFDerivAtFilter_pi', Fin.forall_fin_succ, hasFDerivAtFilter_pi']

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
n : ℕ
F' : Fin n.succ → Type u_6
inst✝¹ : (i : Fin n.succ) → NormedAddCommGroup (F' i)
inst✝ : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)
φ : E → F' 0
φs : E → (i : Fin n) → F' i.succ
φ' : E →L[𝕜] (i : Fin n.succ) → F' i
l : Filter (E × E)
⊢ (HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x) 0) (proj 0 ∘SL φ') l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x ↦ Fin.cons (φ x) (φs x) i.succ) (proj i.succ ∘SL φ') l) ↔
    HasFDerivAtFilter φ (proj 0 ∘SL φ') l ∧
      ∀ (i : Fin n), HasFDerivAtFilter (fun x ↦ φs x i) (proj i ∘SL Pi.compRightL 𝕜 F' Fin.succ ∘SL φ') l