mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝²¹ : CommSemiring A
R✝ : Type u_3
inst✝²⁰ : CommRing R✝
inst✝¹⁹ : Algebra A R✝
τ : Type u_4
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R✝ S
inst✝¹⁵ : IsScalarTower A R✝ S
a✝¹ a✝ : σ → MvPowerSeries τ S
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : IsUniformAddGroup T✝
inst✝⁹ : IsTopologicalRing T✝
inst✝⁸ : IsLinearTopology T✝ T✝
inst✝⁷ : Algebra R✝ T✝
ε : MvPowerSeries τ S →ₐ[R✝] T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R✝ S T✝
υ : Type u_7
T : Type u_8
inst✝⁴ : CommRing T
inst✝³ : Algebra R✝ T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R✝ S T
b : τ → MvPowerSeries υ T
R : Type u_9
inst✝ : CommSemiring R
a : σ → R
f g : MvPowerSeries σ R
⊢ (fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) (f * g)) =
    (fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) f) * fun n ↦ (n.prod fun s m ↦ a s ^ m) * (coeff n) g

Tactic:
by
    ext n
    classical
    rw [coeff_apply, coeff_mul, coeff_mul, Finset.mul_sum]
    apply Finset.sum_congr rfl
    intro x hx
    simp only [Finset.mem_antidiagonal] at hx
    rw [← hx]
    simp only [coeff_apply]
    rw [Finsupp.prod_of_support_subset _ Finsupp.support_add,
      Finsupp.prod_of_support_subset x.1 Finset.subset_union_left,
      Finsupp.prod_of_support_subset x.2 Finset.subset_union_right]
    · simp only [← mul_assoc]
      congr 1
      rw [mul_assoc, mul_comm (f x.1), ← mul_assoc]
      congr 1
      rw [← Finset.prod_mul_distrib]
      apply Finset.prod_congr rfl
      simp [pow_add]
    all_goals {simp}

Goal state after:
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
U V : Set E
hU : Balanced 𝕜 U
hV : Balanced 𝕜 V
a b : E
⊢ egauge 𝕜 ((fun x ↦ x.1 + x.2) '' U ×ˢ V) (a + b) ≤ egauge 𝕜 (U ×ˢ V) (a, b)

Tactic:
exact MapsTo.egauge_le 𝕜 (LinearMap.fst 𝕜 E E + LinearMap.snd 𝕜 E E) (mapsTo_image _ _) (a, b)

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : ∀ i ∈ u \ t, i ∈ s
hv : ∀ i ∈ v \ t, i ∈ s
i : ι
w : Finset ι
hi : i ∉ w
hw' : (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k
hw : ∀ i_1 ∈ insert i w, i_1 ∈ s
k : ℕ
hk : k ≤ n
⊢ ∑ x ∈ k.divisorsAntidiagonal, (f i) x.1 * (∏ x ∈ w, f x) x.2 = ∑ x ∈ k.divisorsAntidiagonal, 1 x.1 * 1 x.2

Tactic:
refine Finset.sum_congr rfl fun j hj ↦ ?_

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
f : ι → ArithmeticFunction R
this✝ : UniformSpace R := ⊥
this : IsUniformInducing DFunLike.coe
n : ℕ
s : Set ι
hs : s ∈ cofinite
hs' : ∀ y ∈ s, ∀ i ∈ Set.Iic n, (f y) i = 1 i
t : Finset ι := ⋯.toFinset
u v : Finset ι
hu : ∀ i ∈ u \ t, i ∈ s
hv : ∀ i ∈ v \ t, i ∈ s
i : ι
w : Finset ι
hi : i ∉ w
hw' : (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k
hw : ∀ i_1 ∈ insert i w, i_1 ∈ s
k : ℕ
hk : k ≤ n
j : ℕ × ℕ
hj : j ∈ k.divisorsAntidiagonal
⊢ (f i) j.1 * (∏ x ∈ w, f x) j.2 = 1 j.1 * 1 j.2
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ≥0
hc : 1 < ‖c‖
h₀ : r ≠ 0 ∨ ‖x‖ ≠ 0
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝², non_trivial := ⋯ }
hr : 0 < r
hx : ‖x‖ ≠ 0
⊢ egauge 𝕜 (ball 0 ↑r) x ≤ ‖c‖ₑ * ‖x‖ₑ / ↑r

Tactic:
· rcases rescale_to_shell_semi_normed hc hr hx with ⟨a, ha₀, har, -, hainv⟩
      calc
        egauge 𝕜 (ball 0 r) x ≤ ↑(‖a‖₊⁻¹) :=
          egauge_le_of_smul_mem_of_ne (mem_ball_zero_iff.2 har) ha₀
        _ ≤ ↑(‖c‖₊ * ‖x‖₊ / r) := by rwa [ENNReal.coe_le_coe, div_eq_inv_mul, ← mul_assoc]
        _ ≤ ‖c‖ₑ * ‖x‖ₑ / r := ENNReal.coe_div_le.trans <| by simp [ENNReal.coe_mul, enorm]

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

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
x : ℝ
H : DifferentiableWithinAt ℝ f (Ioi x) x
A : HasDerivWithinAt f (derivWithin f (Ioi x) x) (Ici x) x
B : HasDerivWithinAt f (derivWithin f (Ici x) x) (Ici x) x
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
simpa using (uniqueDiffOn_Ici x).eq self_mem_Ici A B

Goal state after:
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✝ : ContinuousSMul 𝕜 E
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : ↑ε * ↑‖c‖₊ / ↑r < 1
x : α
hx : egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
⊢ f x ∈ id U

Tactic:
refine mem_of_egauge_lt_one hUb (hx.trans_lt ?_)

Goal state after:
α : 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✝ : ContinuousSMul 𝕜 E
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
U : Set E
hU : U ∈ 𝓝 0
hUb : Balanced 𝕜 U
r : ℝ≥0
hr : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
hr₀ : 0 < r
c : 𝕜
hc : 1 < ‖c‖
ε : ℝ≥0
hε₀ : 0 < ε
hε : ↑ε * ↑‖c‖₊ / ↑r < 1
x : α
hx : egauge 𝕜 (id U) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x)
⊢ ↑ε * egauge 𝕜 (ball 0 ↑r) (1 x) < 1
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
ι : Type u_4
s : ι → Set E
hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
hs : ∀ (i : ι), IsOpen[inst✝³] (s i)
hs' : ⋃ i, s i = univ
⊢ DifferentiableOn 𝕜 f univ

Tactic:
← hs'

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 → F
ι : Type u_4
s : ι → Set E
hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
hs : ∀ (i : ι), IsOpen[inst✝³] (s i)
hs' : ⋃ i, s i = univ
⊢ DifferentiableOn 𝕜 f (⋃ i, s i)
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: case mp
α : 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✝ : ContinuousSMul 𝕜 E
⊢ f =o[𝕜; l] 1 → Tendsto f l (𝓝 0)

Tactic:
intro hf
    rw [(basis_sets _).isLittleOTVS_iff nhds_basis_ball] at hf
    rw [(nhds_basis_balanced 𝕜 E).tendsto_right_iff]
    rintro U ⟨hU, hUb⟩
    rcases hf U hU with ⟨r, hr₀, hr⟩
    lift r to ℝ≥0 using hr₀.le
    norm_cast at hr₀
    rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩
    obtain ⟨ε, hε₀, hε⟩ : ∃ ε : ℝ≥0, 0 < ε ∧ (ε * ‖c‖₊ / r : ℝ≥0∞) < 1 := by
      apply Eventually.exists_gt
      refine Continuous.tendsto' ?_ _ _ (by simp) |>.eventually_lt_const zero_lt_one
      fun_prop (disch := intros; first | apply ENNReal.coe_ne_top | positivity)
    filter_upwards [hr ε hε₀.ne'] with x hx
    refine mem_of_egauge_lt_one hUb (hx.trans_lt ?_)
    calc
      (ε : ℝ≥0∞) * egauge 𝕜 (ball (0 : 𝕜) r) 1 ≤ (ε * ‖c‖₊ / r : ℝ≥0∞) := by
        rw [mul_div_assoc]
        gcongr
        simpa using! egauge_ball_le_of_one_lt_norm (r := r) (x := (1 : 𝕜)) hc (by simp)
      _ < 1 := ‹_›

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
this :
  (∃ a ∈ Ioo 0 1, (fun n ↦ ‖p n‖ * ↑r ^ n) =o[atTop] fun x ↦ a ^ x) ↔
    ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
⊢ ∃ a ∈ Ioo 0 1, (fun n ↦ ‖p n‖ * ↑r ^ n) =o[atTop] fun x ↦ a ^ x

Tactic:
rw [this]

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
this :
  (∃ a ∈ Ioo 0 1, (fun n ↦ ‖p n‖ * ↑r ^ n) =o[atTop] fun x ↦ a ^ x) ↔
    ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
⊢ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
Module: Mathlib.Analysis.Analytic.ConvergenceRadius

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < p.radius
⊢ ∃ C r, ∃ (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n

Tactic:
have rpos : 0 < (r : ℝ) := by simp [ENNReal.coe_pos.1 r0]

Goal state after:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
r : ℝ≥0
r0 : 0 < ↑r
rlt : ↑r < p.radius
rpos : 0 < ↑r
⊢ ∃ C r, ∃ (_ : 0 < C) (_ : 0 < r), ∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: case hy
𝕜 : 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
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : ‖y‖ₑ + ‖z‖ₑ < r
⊢ y + z ∈ Metric.eball 0 r

Tactic:
exact mem_eball_zero_iff.2 (lt_of_le_of_lt (enorm_add_le _ _) hz)

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
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : z ∈ Metric.eball 0 (r - ‖y‖ₑ)
this : f (x + y + z) = (p.changeOrigin y).sum z
⊢ HasSum (fun n ↦ (p.changeOrigin y n) fun x ↦ z) (f (x + y + z))

Tactic:
rw [this]

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
h : ‖y‖ₑ < r
hy : x + y ∈ insert x s
z : E
h'z : x + y + z ∈ insert (x + y) s
hz : z ∈ Metric.eball 0 (r - ‖y‖ₑ)
this : f (x + y + z) = (p.changeOrigin y).sum z
⊢ HasSum (fun n ↦ (p.changeOrigin y n) fun x ↦ z) ((p.changeOrigin y).sum z)
Module: Mathlib.Analysis.Analytic.Basic

Goal state before:
pp: case inr
𝕜 : 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
h'y : y ∈ Metric.eball 0 r
hy : x + y ∈ s
⊢ g (x + y) = f (x + y)

Tactic:
· apply h'
    refine ⟨hy, ?_⟩
    simpa [edist_eq_enorm_sub] using h'y

Goal state after:
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 : ℕ → 𝕜
hc : ∀ᶠ (n : ℕ) in atTop, c n ≠ 0
hc' : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 0)
r' : ℝ≥0
hrz : ¬r' = 0
⊢ Summable fun n ↦ ‖‖c n‖ * ↑r' ^ n‖

Tactic:
apply summable_of_ratio_test_tendsto_lt_one zero_lt_one (hc.mp (Eventually.of_forall ?_))
      · simp only [norm_norm]
        exact mul_zero (_ : ℝ) ▸ tendsto_succ_norm_div_norm _ hrz (NNReal.coe_zero ▸ hc')
      · simp_all

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

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

Tactic:
· filter_upwards [eventually_cofinite_ne 0] with n hn
      simp only [norm_mul, norm_norm, norm_pow, NNReal.norm_eq]
      gcongr
      exact ofScalars_norm_le E c n (Nat.pos_iff_ne_zero.mpr hn)

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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ Metric.eball 0 (r - ↑‖y‖₊)
this : f (x + y + z) = (p.changeOrigin y).sum z
⊢ HasSum (fun n ↦ (p.changeOrigin y n) fun x ↦ z) (f (x + y + z))

Tactic:
rw [this]

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
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ Metric.eball 0 (r - ↑‖y‖₊)
this : f (x + y + z) = (p.changeOrigin y).sum z
⊢ HasSum (fun n ↦ (p.changeOrigin y n) fun x ↦ z) ((p.changeOrigin y).sum z)
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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
n : ℕ
x y : E
hf : HasFiniteFPowerSeriesOnBall f p x n r
h : ↑‖y‖₊ < r
z : E
hz : z ∈ Metric.eball 0 (r - ↑‖y‖₊)
⊢ HasSum (fun n ↦ (p.changeOrigin y n) fun x ↦ z) (f (x + y + z))

Tactic:
by
    have : f (x + y + z) =
        FormalMultilinearSeries.sum (FormalMultilinearSeries.changeOrigin p y) z := by
      rw [mem_eball_zero_iff, lt_tsub_iff_right, add_comm] at hz
      rw [p.changeOrigin_eval_of_finite hf.finite, add_assoc, hf.sum]
      exact mem_eball_zero_iff.2 ((enorm_add_le _ _).trans_lt hz)
    rw [this]
    apply (p.changeOrigin y).hasSum_of_finite fun _ => p.changeOrigin_finite_of_finite hf.finite

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∞
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
this : Metric.ball 0 ↑r' ∈ 𝓝 y
⊢ ∀ᶠ (z : E) in 𝓝 y, ‖z‖₊ < r'

Tactic:
filter_upwards [this] with a ha using by simpa [← coe_nnnorm] using ha

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
A : ContinuousOn (fun y ↦ y - x) (insert x s ∩ Metric.eball x r)
z : E
⊢ z ∈ insert x s ∩ Metric.eball x r → (fun y ↦ y - x) z ∈ (fun x_1 ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r

Tactic:
simp [edist_eq_enorm_sub]

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
this : ∑ j, c.blocksFun j = 0
⊢ ∑ i_1, c.blocksFun i_1 < m * n

Tactic:
rw [this]

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
⊢ 0 < m * n
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i ↦ (b i).blocks) = ofFn fun i ↦ (b' i).blocks
this : ofFn (sum ∘ fun i ↦ (b i).blocks) = ofFn (sum ∘ fun i ↦ (b' i).blocks)
⊢ a.blocks = a'.blocks

Tactic:
change
      (ofFn fun i : Fin (Composition.length a) => (b i).blocks.sum) =
        ofFn fun i : Fin (Composition.length a') => (b' i).blocks.sum at this

Goal state after:
n : ℕ
a : Composition n
b : (i : Fin a.length) → Composition (a.blocksFun i)
a' : Composition n
b' : (i : Fin a'.length) → Composition (a'.blocksFun i)
H : (ofFn fun i ↦ (b i).blocks) = ofFn fun i ↦ (b' i).blocks
this : (ofFn fun i ↦ (b i).blocks.sum) = ofFn fun i ↦ (b' i).blocks.sum
⊢ a.blocks = a'.blocks
Module: Mathlib.Analysis.Calculus.FDeriv.Comp

Goal state before:
pp: case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
⊢ HasFDerivAtFilter f^[n + 1] (f' ^ (n + 1)) L

Tactic:
rw [Function.iterate_succ, pow_succ]

Goal state after:
case succ
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
L : Filter (E × E)
f : E → E
f' : E →L[𝕜] E
hf : HasFDerivAtFilter f f' L
hL : Tendsto (Prod.map f f) L L
n : ℕ
ihn : HasFDerivAtFilter f^[n] (f' ^ n) L
⊢ HasFDerivAtFilter (f^[n] ∘ f) (f' ^ n * f') L
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
n✝ n : ℕ
i : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i))
⊢ ∀ {i_1 : ℕ}, i_1 ∈ (ofFn fun j ↦ (i.snd j).blocks).flatten → 0 < i_1

Tactic:
by
          simp only [and_imp, List.mem_flatten, exists_imp, forall_mem_ofFn_iff]
          exact fun {i} j hj => Composition.blocks_pos _ hj

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

Goal state before:
pp: case right.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 : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
i : Fin (a.gather b).length
⊢ { blocks := (a.blocks.splitWrtComposition b)[↑i], blocks_pos := ⋯, blocks_sum := ⋯ }.length = b.blocks[↑⟨↑i, ⋯⟩]

Tactic:
Composition.length,

Goal state after:
case right.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 : ℕ
a : Composition n
b : Composition a.length
B : (a.gather b).length = b.blocks.length
i : Fin (a.gather b).length
⊢ { blocks := (a.blocks.splitWrtComposition b)[↑i], blocks_pos := ⋯, blocks_sum := ⋯ }.blocks.length =
    b.blocks[↑⟨↑i, ⋯⟩]
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
n✝ n : ℕ
⊢ Function.RightInverse
    (fun i ↦
      ⟨{ blocks := (ofFn fun j ↦ (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ },
        { blocks := ofFn fun j ↦ (i.snd j).length, blocks_pos := ⋯, blocks_sum := ⋯ }⟩)
    fun i ↦ ⟨i.fst.gather i.snd, i.fst.sigmaCompositionAux i.snd⟩

Tactic:
rintro ⟨c, d⟩

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
n✝ n : ℕ
c : Composition n
d : (i : Fin c.length) → Composition (c.blocksFun i)
⊢ (fun i ↦ ⟨i.fst.gather i.snd, i.fst.sigmaCompositionAux i.snd⟩)
      ((fun i ↦
          ⟨{ blocks := (ofFn fun j ↦ (i.snd j).blocks).flatten, blocks_pos := ⋯, blocks_sum := ⋯ },
            { blocks := ofFn fun j ↦ (i.snd j).length, blocks_pos := ⋯, blocks_sum := ⋯ }⟩)
        ⟨c, d⟩) =
    ⟨c, d⟩