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

Goal state before:
pp: 𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
y : Fin n → 𝕜
⊢ (p n) y = (∏ i, y i) • p.coeff n

Tactic:
convert! (p n).toMultilinearMap.map_smul_univ y 1

Goal state after:
case e'_2.e'_1
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
y : Fin n → 𝕜
x✝ : Fin n
⊢ y x✝ = y x✝ • 1 x✝
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalSpace E
inst✝² : Module 𝕜 E
l : Filter α
f : α → E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
x : E
h : Tendsto (fun x_1 ↦ f x_1 - x) l (𝓝 0)
U : Set E
hU₀ : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
this : ∃ c, x ∈ c • U
⊢ ↑0 < (egauge 𝕜 U x)⁻¹

Tactic:
simpa [egauge_eq_top]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 F G
u : E →ₗᵢ[𝕜] F
⊢ p.radius ≤ (p.compContinuousLinearMap u.toContinuousLinearMap).radius

Tactic:
by
  obtain (h | h) := subsingleton_or_nontrivial E
  · simp [Subsingleton.elim u.toContinuousLinearMap 0]
  · simpa [u.norm_toContinuousLinearMap]
      using div_le_radius_compContinuousLinearMap p u.toContinuousLinearMap

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

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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
⊢ ∞ ≤ p.radius

Tactic:
radius_eq_top_of_forall_image_add_eq_zero p n fun _ => hn _ (Nat.le_add_left _ _)

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
⊢ ∞ ≤ ∞
Module: Mathlib.Analysis.Analytic.CPolynomialDef

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
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
y : E
x✝ : y ∈ Metric.eball 0 ∞
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) (p.sum (0 + y))

Tactic:
rw [zero_add]

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
y : E
x✝ : y ∈ Metric.eball 0 ∞
⊢ HasSum (fun n ↦ (p n) fun x ↦ y) (p.sum y)
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: case neg.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ Summable fun n ↦ ‖‖c n‖ * ↑r' ^ n‖

Tactic:
refine summable_of_ratio_test_tendsto_lt_one hr' ?_ ?_

Goal state after:
case neg.refine_1.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ ∀ᶠ (n : ℕ) in atTop, ‖‖c n‖ * ↑r' ^ n‖ ≠ 0

case neg.refine_1.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
r : ℝ≥0
hr : r ≠ 0
hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 ↑r)
r' : ℝ≥0
hr' : r' * r < 1
hrz : ¬r' = 0
⊢ Tendsto (fun n ↦ ‖‖‖c (n + 1)‖ * ↑r' ^ (n + 1)‖‖ / ‖‖‖c n‖ * ↑r' ^ n‖‖) atTop (𝓝 ↑(r' * r))
Module: Mathlib.Analysis.Analytic.OfScalars

Goal state before:
pp: case refine_1
𝕜 : 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 : ℕ) in atTop, ‖‖ofScalars E c n‖ * ↑r ^ n‖ ≠ 0

pp: case refine_2
𝕜 : 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 : ℕ) in atTop, 2 * ‖‖ofScalars E c n‖ * ↑r ^ n‖ ≤ ‖‖ofScalars E c (n + 1)‖ * ↑r ^ (n + 1)‖

Tactic:
· contrapose! hc
    apply not_tendsto_atTop_of_tendsto_nhds (a := 0)
    apply Tendsto.congr' ?_ tendsto_const_nhds
    filter_upwards [hc] with n hc'
    rw [ofScalars_norm, norm_mul, norm_norm, mul_eq_zero] at hc'
    cases hc' <;> aesop

Goal state after:
case refine_2
𝕜 : 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 : ℕ) in atTop, 2 * ‖‖ofScalars E c n‖ * ↑r ^ n‖ ≤ ‖‖ofScalars E c (n + 1)‖ * ↑r ^ (n + 1)‖
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
s t : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
h : t ⊆ s
⊢ AnalyticWithinAt 𝕜 f t x

Tactic:
obtain ⟨p, hp⟩ := hf

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
s t : Set E
x : E
h : t ⊆ s
p : FormalMultilinearSeries 𝕜 E F
hp : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt 𝕜 f t x
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousConstSMul 𝕜 E
H : Type u_6
inst✝⁴ : CommRing H
inst✝³ : Algebra 𝕜 H
inst✝² : TopologicalSpace H
inst✝¹ : IsTopologicalRing H
inst✝ : ContinuousConstSMul 𝕜 H
p : FormalMultilinearSeries 𝕜 E H
n : ℕ
c : Composition n
v : Fin n → E
⊢ ∏ i, p.applyComposition c v i = ∏ i, (p (c.blocksFun i)) (v ∘ ⇑(c.embedding i))

Tactic:
by
  rfl

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
ι : Type u_5
Em : ι → Type u_6
inst✝² : (i : ι) → NormedAddCommGroup (Em i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (Em i)
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em F
x : (i : ι) → Em i
⊢ x ∈ Metric.eball 0 ∞

Tactic:
by simp only [Metric.eball_top, Set.mem_univ]

Goal state after:
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
x : G × ((i : ι) → Em i)
⊢ x ∈ Metric.eball 0 ∞

Tactic:
by simp only [Metric.eball_top, Set.mem_univ]

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 = id 𝕜 E x

Tactic:
by
  ext n v
  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.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
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
this✝ : insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x
this : insert (f x) t ∩ Metric.eball (f x) rg ∈ Filter.map f (𝓝[insert x s] x)
⊢ ∃ δ, 0 < δ ∧ ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg

Tactic:
rcases EMetric.mem_nhdsWithin_iff.1 this with ⟨δ, δpos, Hδ⟩

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
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i ↦ ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
this✝ : insert (f x) t ∩ Metric.eball (f x) rg ∈ 𝓝[insert (f x) t] f x
this : insert (f x) t ∩ Metric.eball (f x) rg ∈ Filter.map f (𝓝[insert x s] x)
δ : ℝ≥0∞
δpos : δ > 0
Hδ : Metric.eball x δ ∩ insert x s ⊆ f ⁻¹' (insert (f x) t ∩ Metric.eball (f x) rg)
⊢ ∃ δ, 0 < δ ∧ ∀ {z : E}, z ∈ insert x s ∩ Metric.eball x δ → f z ∈ insert (f x) t ∩ Metric.eball (f x) rg
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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
y✝ : E
hy : y✝ ∈ Metric.eball 0 p.radius
⊢ HasSum (fun n ↦ (p n) fun x ↦ y✝) (p.sum (0 + y✝))

Tactic:
rw [zero_add]

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
inst✝ : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
y✝ : E
hy : y✝ ∈ Metric.eball 0 p.radius
⊢ HasSum (fun n ↦ (p n) fun x ↦ y✝) (p.sum y✝)
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
g : F → G
f : E → F
y : F
x : E
t : Set F
s : Set E
hg : AnalyticWithinAt 𝕜 g t (f x)
hf : AnalyticWithinAt 𝕜 f s x
h : Set.MapsTo f s t
hy : f x = y
⊢ AnalyticWithinAt 𝕜 (g ∘ f) s x

Tactic:
exact hg.comp hf h

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
G : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s (u x) r
⊢ r / ‖u‖ₑ ≤ (pf.compContinuousLinearMap u).radius

Tactic:
by
    calc
      _ ≤ pf.radius / ‖u‖ₑ := by
        gcongr
        exact hf.r_le
      _ ≤ _ := pf.div_le_radius_compContinuousLinearMap _

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
⊢ ∀
    (i :
      Fin
        ({ 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),
    ({ 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 =
      (d ⟨↑i, ⋯⟩).blocks

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

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

Goal state before:
pp: 𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
⊢ HasFPowerSeriesOnBall (fun x ↦ (1 + x)⁻¹) (alternatingGeometricSeries 𝕜 𝕝) 0 1

Tactic:
convert! hasFPowerSeriesOnBall_inverse_one_add 𝕜 𝕝

Goal state after:
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
x✝ : 𝕝
⊢ Inv.inv = Ring.inverse
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 : G → E
x : G
f' : G →L[𝕜] F
⊢ HasFDerivWithinAt (⇑iso ∘ f) f' univ x ↔ HasFDerivWithinAt f (↑iso.symm ∘SL f') univ x

Tactic:
iso.comp_hasFDerivWithinAt_iff'

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
x : E
s : Set E
h : DifferentiableWithinAt 𝕜 (fun y ↦ -f y) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
simpa only [neg_neg] using h.fun_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
x : E
h : DifferentiableAt 𝕜 (fun y ↦ -f y) x
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa only [neg_neg] using h.fun_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
s : Set E
h : DifferentiableOn 𝕜 (fun y ↦ -f y) s
⊢ DifferentiableOn 𝕜 f s

Tactic:
simpa only [neg_neg] using h.fun_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
h : Differentiable 𝕜 fun y ↦ -f y
⊢ Differentiable 𝕜 f

Tactic:
simpa only [neg_neg] using h.fun_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 g : E → F
s : Set E
hg : DifferentiableOn 𝕜 g s
⊢ DifferentiableOn 𝕜 (f - g) s ↔ DifferentiableOn 𝕜 f s

Tactic:
simp only [sub_eq_add_neg, differentiableOn_neg_iff, hg, add_iff_left]

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
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
x : E
s : Set E
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (⇑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) s x =
    ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderivWithin 𝕜 f s x

Tactic:
ContinuousLinearEquiv.comp_fderivWithin _ hs

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
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
x : E
s : Set E
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
hs : UniqueDiffWithinAt 𝕜 s x
⊢ ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderivWithin 𝕜 f s x =
    ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderivWithin 𝕜 f s x
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: case inr.hs
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
hs : UniqueDiffWithinAt 𝕜 s x
hc : c ≠ 0
⊢ UniqueDiffWithinAt 𝕜 (c • s) (c • x)

Tactic:
exact hs.smul hc

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 ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ‖f fun j ↦ (Function.update (fun x ↦ g) i dg j) (v j)‖ ≤ ‖g‖ ^ (Fintype.card ι - 1) * (‖f‖ * (‖dg‖ * ∏ i, ‖v i‖))

Tactic:
le_opNorm

Goal state after:
𝕜 : 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 ι
inst✝ : DecidableEq ι
g : E →L[𝕜] F
f : F [⋀^ι]→L[𝕜] G
dg : E →L[𝕜] F
v : ι → E
i : ι
⊢ ‖f‖ * ∏ i_1, ‖(Function.update (fun x ↦ g) i dg i_1) (v i_1)‖ ≤
    ‖g‖ ^ (Fintype.card ι - 1) * (‖f‖ * (‖dg‖ * ∏ i, ‖v i‖))
Module: Mathlib.Analysis.Calculus.FDeriv.Analytic

Goal state before:
pp: case e'_13
𝕜 : 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
inst✝ : DecidableEq ι
⊢ x = 0 + x

Tactic:
rw [zero_add]

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

Goal state before:
pp: n : ℕ
R θ : ℝ
⊢ circleMap 0 R θ ^ n = circleMap 0 (R ^ n) (↑n * θ)

Tactic:
by
  simp [circleMap_zero, mul_pow, ← Complex.exp_nat_mul, ← mul_assoc]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
f : ι → E → 𝔸
f' : ι → E →L[𝕜] 𝔸
l : List ι
x : E
h : ∀ i ∈ l, HasFDerivWithinAt (fun x ↦ f i x) (f' i) s x
⊢ HasFDerivWithinAt (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) l).prod)
    (∑ i,
      (List.map (fun x_1 ↦ f x_1 x) (List.take (↑i) l)).prod •>
        (f' l[i] <• (List.map (fun x_1 ↦ f x_1 x) (List.drop (↑i).succ l)).prod))
    s x

Tactic:
by
  simp_rw [Fin.getElem_fin, ← l.get_eq_getElem, ← List.map_get_finRange l, List.map_map]
  refine .congr_fderiv (hasFDerivAt_list_prod_finRange'.comp_hasFDerivWithinAt x
    (hasFDerivWithinAt_pi.mpr fun i ↦ h (l.get i) (l.get_mem i)) :) ?_
  ext m
  simp_rw [List.map_take, List.map_drop, List.map_map, comp_apply, sum_apply, smul_apply,
    proj_apply, pi_apply, Function.comp_def]

Goal state after: