mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ ∃ j ∈ 𝓝 0, ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id j) (k x)

Tactic:
refine ⟨W, hW, ?_⟩

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : AddCommGroup F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : Module 𝕜 F
inst✝⁴ : AddCommGroup G
inst✝³ : TopologicalSpace G
inst✝² : Module 𝕜 G
l : Filter α
f : α → E
g : α → F
inst✝¹ : ContinuousSMul 𝕜 E
inst✝ : ContinuousSMul 𝕜 F
k : α → G
hf : f =O[𝕜; l] k
hg : g =O[𝕜; l] k
U : Set E
V : Set F
hU : (U, V).1 ∈ 𝓝 0
hUb : Balanced 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
hVb : Balanced 𝕜 (U, V).2
W : Set G
hW : W ∈ 𝓝 0
hWf : ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ egauge 𝕜 W (k x)
hWg : ∀ᶠ (x : α) in l, egauge 𝕜 V (g x) ≤ egauge 𝕜 W (k x)
⊢ ∀ᶠ (x : α) in l, egauge 𝕜 (id (U, V).1 ×ˢ id (U, V).2) (f x, g x) ≤ egauge 𝕜 (id W) (k x)
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

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 → F
x : E
s t : Set E
ht : t ∈ 𝓝 x
⊢ DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [DifferentiableWithinAt, hasFDerivWithinAt_inter ht]

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

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 → F
x : E
s t : Set E
ht : t ∈ 𝓝 x
⊢ fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x

Tactic:
simp [fderivWithin, hasFDerivWithinAt_inter ht, DifferentiableWithinAt]

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

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✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hf' : IsInducing ⇑f'
⊢ ((fun p ↦ f p.1 - f p.2) - fun p ↦ f' (p.1 - p.2)) =o[𝕜; L] fun p ↦ f' (p.1 - p.2)

Tactic:
exact hf.isLittleOTVS.trans_isBigOTVS <| f'.isThetaTVS_comp hf' |>.symm.isBigOTVS

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

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
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
hr : ↑r < p.radius
k : ℕ
⊢ Summable fun l ↦ ‖p.changeOriginSeries k l‖₊ * r ^ l

Tactic:
by
  refine NNReal.summable_of_le
    (fun n => ?_) (NNReal.summable_sigma.1 <| p.changeOriginSeries_summable_aux₂ hr k).2
  simp only [NNReal.tsum_mul_right]
  gcongr
  apply p.nnnorm_changeOriginSeries_le_tsum

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry

Goal state before:
pp: 𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
i : Fin (n + 1)
f : Ei i →L[𝕜] Ei (i.succAbove j) [×n]→L[𝕜] G
m : (i : Fin n.succ) → Ei i
⊢ ‖(f (m i)) (i.removeNth m)‖ ≤ ‖f‖ * ∏ j, ‖m j‖

Tactic:
rw [i.prod_univ_succAbove, ← mul_assoc]

Goal state after:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst✝² : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
i : Fin (n + 1)
f : Ei i →L[𝕜] Ei (i.succAbove j) [×n]→L[𝕜] G
m : (i : Fin n.succ) → Ei i
⊢ ‖(f (m i)) (i.removeNth m)‖ ≤ ‖f‖ * ‖m i‖ * ∏ i_1, ‖m (i.succAbove i_1)‖
Module: Mathlib.Analysis.Analytic.ChangeOrigin

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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
⊢ HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ↑‖y‖₊)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢
  exact hf.changeOrigin h (by simp)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ‖‖ofScalars E c x‖ * ↑r ^ x‖ = 0
n : ℕ
⊢ ‖‖ofScalars E c n‖ * ↑r ^ n‖ = 0 → 0 = ‖c n.succ‖ / ‖c n‖

Tactic:
hc'

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
hc : ∀ᶠ (x : ℕ) in atTop, ‖‖ofScalars E c x‖ * ↑r ^ x‖ = 0
n : ℕ
hc' : ‖‖ofScalars E c n‖ * ↑r ^ n‖ = 0
⊢ 0 = ‖c n.succ‖ / ‖c n‖
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ ↑r ^ n / ↑r ^ (n + 1) = ↑r⁻¹

Tactic:
rw [pow_succ, div_mul_cancel_left₀, NNReal.coe_inv]

Goal state after:
case ha
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
inst✝ : NormOneClass E
hc✝ : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop atTop
r : ℝ≥0
hr : ↑r < (ofScalars E c).radius
this : 0 < r
n : ℕ
hc : 2 * ↑r⁻¹ ≤ ‖c n.succ‖ / ‖c n‖
hn : n ≠ 0
⊢ ↑r ^ n ≠ 0
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: case e_f
𝕜 : 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A✝ : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
k : ℕ
hk : ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4
A : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
w : E
hw : ‖w‖₊ < r'
i : ℕ
⊢ ((p (k + i)) fun x ↦ w) = (p (i + k)) fun x ↦ w

Tactic:
add_comm k

Goal state after:
case e_f
𝕜 : 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : y ∈ Metric.eball 0 r
h'y : x + y ∈ insert x s
A✝ : Tendsto (fun z ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : ↑r' < r
yr'_2 : ‖y‖ < ↑r'
S : Summable fun n ↦ ‖p n‖ * ↑r' ^ n
k : ℕ
hk : ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4
A : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, dist (p.partialSum k z.2) (p.partialSum k y) < ε / 4
B : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, ‖z.2‖₊ < r'
C : ∀ᶠ (z : ℕ × E) in atTop ×ˢ 𝓝 y, k ≤ z.1
n : ℕ
z : E
h'z : ‖(n, z).2‖₊ < r'
hkn : k ≤ (n, z).1
hz : ‖p.partialSum k z - p.partialSum k y‖ < ε / 4
w : E
hw : ‖w‖₊ < r'
i : ℕ
⊢ ((p (i + k)) fun x ↦ w) = (p (i + k)) fun x ↦ w
Module: Mathlib.Analysis.Analytic.CPolynomial

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F
⊢ HasFiniteFPowerSeriesOnBall (fun p ↦ (f p.1) p.2) f.toFormalMultilinearSeriesOfMultilinear 0
    (Fintype.card (Option ι) + 1) ∞

Tactic:
by
  apply HasFiniteFPowerSeriesOnBall.mk' ?_ ENNReal.zero_lt_top ?_
  · intro m hm
    apply dif_neg
    exact Nat.ne_of_lt hm
  · intro y _
    rw [Finset.sum_eq_single_of_mem _ (Finset.self_mem_range_succ _), zero_add]
    · rw [toFormalMultilinearSeriesOfMultilinear, dif_pos rfl]; rfl
    · intro m _ ne; rw [toFormalMultilinearSeriesOfMultilinear, dif_neg ne.symm]; rfl

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
n : ℕ
⊢ p.removeZero.leftInv i x n = p.leftInv i x n

Tactic:
induction n using Nat.strong_induction_on with

Goal state after:
case h
𝕜 : 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
n : ℕ
IH : ∀ m < n, p.removeZero.leftInv i x m = p.leftInv i x m
⊢ p.removeZero.leftInv i x n = p.leftInv i x n
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
n : ℕ
⊢ p.removeZero.rightInv i x n = p.rightInv i x n

Tactic:
induction n using Nat.strong_induction_on with

Goal state after:
case h
𝕜 : 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
n : ℕ
IH : ∀ m < n, p.removeZero.rightInv i x m = p.rightInv i x m
⊢ p.removeZero.rightInv i x n = p.rightInv i x n
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: ⊢ Tendsto (fun p ↦ compPartialSumTarget 0 p.1 p.2) atTop atTop

Tactic:
apply Monotone.tendsto_atTop_finset

Goal state after:
case h
⊢ Monotone fun p ↦ compPartialSumTarget 0 p.1 p.2

case h'
⊢ ∀ (x : (n : ℕ) × Composition n), ∃ n, x ∈ compPartialSumTarget 0 n.1 n.2
Module: Mathlib.Analysis.Analytic.Composition

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
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
⊢ HasFiniteFPowerSeriesAt (g ∘ f) (q.comp p) x (m * n)

Tactic:
refine ⟨r, hr, fun i hi ↦ ?_⟩

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
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 : ℕ
hi : m * n ≤ i
⊢ q.comp p i = 0
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
L : Filter (E × E)
x : E × E
⊢ 0 x = f x.1 - f x.2 - f (x.1 - x.2)

Tactic:
by
    simp only [f.map_sub, sub_self, Pi.zero_apply]

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⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum = (take (i + 1) (List.map sum (a.blocks.splitWrtComposition b))).sum

Tactic:
sum_take_succ _ _ B,

Goal state after:
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⟩
A : i < b.length
B : i < (List.map sum (a.blocks.splitWrtComposition b)).length
C : 0 < b.blocksFun ⟨i, A⟩
⊢ (take (take (i + 1) b.blocks).sum a.blocks).sum =
    (take i (List.map sum (a.blocks.splitWrtComposition b))).sum + (List.map sum (a.blocks.splitWrtComposition b))[i]
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: case e_x
𝕜 : 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
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := min r0 ↑r1
this : Metric.eball 0 r ∈ 𝓝 0
y : E
hy : y ∈ Metric.eball 0 r
hy0 : y ∈ Metric.eball 0 r0
A : HasSum (fun i ↦ (q.compAlongComposition p i.snd) fun _j ↦ y) (f (x + y))
B :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n.1 n.2, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (f (x + y)))
C : Tendsto (fun n ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a) fun _b ↦ y)) atTop (𝓝 (f (x + y)))
fst✝ n : ℕ
hn : 1 ≤ n
⊢ (∑ a ∈ Ico 1 (fst✝, n).2, (p a) fun _b ↦ y) = p.partialSum (fst✝, n).2 y - (p 0) fun x ↦ 0

Tactic:
rw [partialSum, eq_sub_iff_add_eq', Finset.range_eq_Ico,
        Finset.sum_eq_sum_Ico_succ_bot hn]

Goal state after:
case e_x
𝕜 : 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
f : E → G
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
hq : 0 < q.radius
hp : 0 < p.radius
r0 : ℝ≥0∞
h0 : HasFPowerSeriesOnBall f (q.comp p) x r0
r1 : NNReal
r1_pos : 0 < r1
hr1 : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r1 ^ i.fst
r : ℝ≥0∞ := min r0 ↑r1
this : Metric.eball 0 r ∈ 𝓝 0
y : E
hy : y ∈ Metric.eball 0 r
hy0 : y ∈ Metric.eball 0 r0
A : HasSum (fun i ↦ (q.compAlongComposition p i.snd) fun _j ↦ y) (f (x + y))
B :
  Tendsto (fun n ↦ ∑ i ∈ compPartialSumTarget 0 n.1 n.2, (q.compAlongComposition p i.snd) fun _j ↦ y) atTop
    (𝓝 (f (x + y)))
C : Tendsto (fun n ↦ q.partialSum n.1 (∑ a ∈ Ico 1 n.2, (p a) fun _b ↦ y)) atTop (𝓝 (f (x + y)))
fst✝ n : ℕ
hn : 1 ≤ n
⊢ (((p 0) fun x ↦ 0) + ∑ a ∈ Ico 1 (fst✝, n).2, (p a) fun _b ↦ y) =
    ((p 0) fun x ↦ y) + ∑ k ∈ Ico (0 + 1) n, (p k) fun x ↦ y
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_7
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
n : ℕ
⊢ AnalyticWithinAt 𝕜 (f ^ n) s z

Tactic:
induction n with
  | zero =>
    simp only [pow_zero]
    apply analyticWithinAt_const
  | succ m hm =>
    simp only [pow_succ]
    exact hm.mul hf

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
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
this : HasFPowerSeriesAt (⇑(ContinuousLinearMap.id 𝕜 E)) ((p.leftInv i a).comp p) a
x : E
hx : x ∈ f.source
⊢ (ContinuousLinearMap.id 𝕜 E) x = (↑f.symm ∘ ↑f) x

Tactic:
simp [hx]

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
A : Type u_7
inst✝² : NormedRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : HasSummableGeomSeries A
z : Aˣ
⊢ AnalyticAt 𝕜 Ring.inverse ↑z

Tactic:
by
  rcases subsingleton_or_nontrivial A with hA | hA
  · convert! analyticAt_const (v := (0 : A))
  · let f1 : A → A := fun a ↦ a * z.inv
    let f2 : A → A := fun b ↦ (1 - b)⁻¹ʳ
    let f3 : A → A := fun c ↦ 1 - z.inv * c
    have feq : ∀ᶠ y in 𝓝 (z : A), (f1 ∘ f2 ∘ f3) y = y⁻¹ʳ := by
      have : Metric.ball (z : A) (‖(↑z⁻¹ : A)‖⁻¹) ∈ 𝓝 (z : A) := by
        apply Metric.ball_mem_nhds
        simp
      filter_upwards [this] with y hy
      simp only [Metric.mem_ball, dist_eq_norm] at hy
      have : y = Units.ofNearby z y hy := rfl
      rw [this, Eq.comm]
      simp only [Ring.inverse_unit, Function.comp_apply]
      simp only [Units.ofNearby, Units.add, mul_sub, Units.inv_mul, neg_sub, add_sub_cancel,
        mul_inv_rev, Units.val_mul, Units.val_inv_copy, Units.inv_eq_val_inv, Units.val_copy,
        _root_.sub_sub_cancel, Units.mul_left_inj, f1, f2, f3]
      rw [← Ring.inverse_unit]
      congr
      simp
    apply AnalyticAt.congr _ feq
    apply (analyticAt_id.mul analyticAt_const).comp
    apply AnalyticAt.comp
    · simp only [Units.inv_eq_val_inv, Units.inv_mul, sub_self, f2, f3]
      exact analyticAt_inverse_one_sub 𝕜 A
    · exact analyticAt_const.sub (analyticAt_const.mul analyticAt_id)

Goal state after:
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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
H : DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s)
y : F
hy : y ∈ s
⊢ DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) (iso.symm y)

Tactic:
apply H

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
iso : E ≃L[𝕜] F
f : F → G
s : Set F
H : DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s)
y : F
hy : y ∈ s
⊢ iso.symm y ∈ ⇑iso ⁻¹' s
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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
⊢ HasFDerivWithinAt (f ∘ ⇑iso) (f' ∘SL ↑iso) (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f f' s (iso x)

Tactic:
refine ⟨fun H => ?_, fun H => H.comp x iso.hasFDerivWithinAt (mapsTo_preimage _ s)⟩
  rw [← iso.symm_apply_apply x] at H
  have A : f = (f ∘ iso) ∘ iso.symm := by
    rw [Function.comp_assoc, iso.self_comp_symm]
    rfl
  have B : f' = (f'.comp (iso : E →L[𝕜] F)).comp (iso.symm : F →L[𝕜] E) := by
    rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id]
  rw [A, B]
  apply H.comp (iso x) iso.symm.hasFDerivWithinAt
  intro y hy
  simpa only [mem_preimage, apply_symm_apply] using hy

Goal state after:
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
f' : E →L[𝕜] F
x : E
s : Set E
c : F
h : HasFDerivWithinAt f f' s x
hf' : ∃ C, AntilipschitzWith C ⇑f'
⊢ ∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ≠ c

Tactic:
rw [← eventually_map (m := f) (P := fun z ↦ z ≠ c)]
  apply Eventually.filter_mono (h.tendsto_nhdsWithin_nhdsNE hf')
  rcases eq_or_ne (f x) c with rfl | hc
  · exact eventually_mem_nhdsWithin
  · exact eventually_ne_nhdsWithin hc

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Completion

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
x y : Completion E
⊢ dist x y = ‖-x + y‖

Tactic:
induction x, y using Completion.induction_on₂

Goal state after:
case hp
E : Type u_1
inst✝ : SeminormedAddCommGroup E
⊢ IsClosed {x | dist x.1 x.2 = ‖-x.1 + x.2‖}

case ih
E : Type u_1
inst✝ : SeminormedAddCommGroup E
a✝ b✝ : E
⊢ dist ↑a✝ ↑b✝ = ‖-↑a✝ + ↑b✝‖
Module: Mathlib.Analysis.Normed.Group.Completion

Goal state before:
pp: case ih
E : Type u_1
inst✝ : SeminormedAddCommGroup E
a✝ b✝ : E
⊢ dist ↑a✝ ↑b✝ = ‖↑(-a✝ + b✝)‖

Tactic:
norm_coe,

Goal state after:
case ih
E : Type u_1
inst✝ : SeminormedAddCommGroup E
a✝ b✝ : E
⊢ dist ↑a✝ ↑b✝ = ‖-a✝ + b✝‖
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 : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
m : ℕ
hm : ↑m < ↑n
x : E
hx : x ∈ s
A : ↑m.succ < ↑n.succ
⊢ HasFDerivWithinAt (fun x ↦ (p x).shift m) ((p x).shift m.succ).curryLeft s x

Tactic:
change HasFDerivWithinAt (continuousMultilinearCurryRightEquiv' 𝕜 m E F ∘ (p · m.succ))
      (p x m.succ.succ).curryRight.curryLeft s x

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 : ℕ
H : HasFTaylorSeriesUpToOn (↑(n + 1)) f p s
m : ℕ
hm : ↑m < ↑n
x : E
hx : x ∈ s
A : ↑m.succ < ↑n.succ
⊢ HasFDerivWithinAt (⇑(continuousMultilinearCurryRightEquiv' 𝕜 m E F) ∘ fun x ↦ p x m.succ)
    (p x m.succ.succ).curryRight.curryLeft s x