mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ∃ i, q ^ i = a
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ i, q ^ i = a
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0

Tactic:
· by_cases hb : ∃ j, q ^ j = b
          · obtain ⟨i, rfl⟩ := ha
            obtain ⟨j, rfl⟩ := hb
            rw [← pow_add] at hab
            exact (hn ⟨i + j, hab⟩).elim
          · rwa [mul_comm, Function.extend_apply', Pi.zero_apply, zero_mul]

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : 1 < q
hn : ¬∃ a, q ^ a = n
a b : ℕ
hk : (a, b) ∈ n.divisorsAntidiagonal
hab : (a, b).1 * (a, b).2 = n
ha : ¬∃ i, q ^ i = a
⊢ Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) f) 0 (a, b).1 *
      Function.extend (fun x ↦ q ^ x) (fun x ↦ (PowerSeries.coeff x) g) 0 (a, b).2 =
    0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Finsupp.degree d = 1
f : R⟦X⟧
⊢ MvPowerSeries.constantCoeff p = 0

Tactic:
← MvPowerSeries.coeff_zero_eq_constantCoeff_apply,

Goal state after:
R : Type u_2
inst✝ : CommRing R
a : R
σ : Type u_7
p : MvPowerSeries σ R
hp_lin : ∀ d ∈ Function.support p, Finsupp.degree d = 1
f : R⟦X⟧
⊢ (MvPowerSeries.coeff 0) p = 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommRing R
a : σ → R
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ n ∉ ⋯.toFinset → (coeff n) f * (coeff n) (n.prod fun s e ↦ (a s • X s) ^ e) = 0

Tactic:
intro hn
    simpa using hn

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff d) f * (MvPowerSeries.coeff e) ↑((MvPolynomial.X 0 + MvPolynomial.X 1) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff (e 0 + e 1)) f

Tactic:
MvPolynomial.coeff_coe

Goal state after:
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ),
      (MvPowerSeries.coeff d) f * MvPolynomial.coeff e ((MvPolynomial.X 0 + MvPolynomial.X 1) ^ d PUnit.unit) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff (e 0 + e 1)) f
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
he : (single 0 (e 0), single 1 (e 1)) ∉ antidiagonal e
i : Fin 2
⊢ (single 0 (e 0) + single 1 (e 1)) i = e i

Tactic:
fin_cases i <;> simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Semiring 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
s t : Set E
x : E
h : UniqueDiffWithinAt 𝕜 s x
st : s ⊆ t
⊢ UniqueDiffWithinAt 𝕜 t x

Tactic:
rw [uniqueDiffWithinAt_iff] at *
  grw [← st]
  exact h

Goal state after:
Module: Mathlib.Analysis.Calculus.TangentCone.Real

Goal state before:
pp: E : Type u_1
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
inst✝ : IsTopologicalAddGroup E
conv : Convex ℝ s
hs : (interior s).Nonempty
x : E
hx : x ∈ closure[inst✝²] s
⊢ UniqueDiffWithinAt ℝ s x

Tactic:
by
  simp [uniqueDiffWithinAt_iff, conv.span_tangentConeAt hs hx, hx]

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

Goal state before:
pp: case hc
𝕜 : 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
x : E
s : Set E
c : F
⊢ HasFDerivWithinAt (fun x ↦ c) 0 s x

Tactic:
apply hasFDerivWithinAt_const

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
h : f =o[𝕜; l] g
U : Set E
hU : U ∈ 𝓝 0
⊢ ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)

Tactic:
rcases h.1 U hU with ⟨V, hV₀, hV⟩

Goal state after:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
h : f =o[𝕜; l] g
U : Set E
hU : U ∈ 𝓝 0
V : Set F
hV₀ : V ∈ 𝓝 0
hV : ∀ (ε : ℝ≥0), ε ≠ 0 → (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ ↑ε * egauge 𝕜 V (g x)
⊢ ∃ V ∈ 𝓝 0, (fun x ↦ egauge 𝕜 U (f x)) ≤ᶠ[l] fun x ↦ egauge 𝕜 V (g x)
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
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x

Tactic:
have A := H.hasDerivWithinAt.Ici_of_Ioi

Goal state after:
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
⊢ derivWithin f (Ioi x) x = derivWithin f (Ici x) x
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
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
⊢ Tendsto f l (𝓝 0)

Tactic:
(nhds_basis_balanced 𝕜 E).tendsto_right_iff

Goal state after:
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
hf :
  ∀ i ∈ 𝓝 0, ∃ j, 0 < j ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 (id i) (f x) ≤ ↑ε * egauge 𝕜 (ball 0 j) (1 x)
⊢ ∀ (i : Set E), i ∈ 𝓝 0 ∧ Balanced 𝕜 i → ∀ᶠ (x : α) in l, f x ∈ id i
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
f' : E →L[𝕜] F
x : E
inst✝⁴ : ContinuousAdd E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : T2Space F
h : HasFDerivAt f f' x
⊢ fderiv 𝕜 f x = f'

Tactic:
rw [h.unique h.differentiableAt.hasFDerivAt]

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) ~[L] fun p ↦ f' (p.1 - p.2)

Tactic:
rw [IsEquivalent, ← isLittleOTVS_iff_isLittleO (𝕜 := 𝕜)]

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✝¹ : 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)
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

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
n : ℕ
h : f =O[𝓝[s] x₀] fun x ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
⊢ (fun x' ↦ f x') =o[𝓝[s] x₀] fun x' ↦ x' - x₀

Tactic:
h.trans_isLittleO ((isLittleO_pow_sub_sub x₀ hn).mono nhdsWithin_le_nhds)

Goal state after:
Module: Mathlib.Analysis.Calculus.FormalMultilinearSeries

Goal state before:
pp: 𝕜 : Type u
E : Type v
F : Type w
inst✝¹¹ : Semiring 𝕜
inst✝¹⁰ : AddCommMonoid E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : ContinuousAdd E
inst✝⁶ : ContinuousConstSMul 𝕜 E
inst✝⁵ : AddCommMonoid F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst✝ : DecidablePred fun n ↦ p n ≠ 0
hp : ∃ n, p n ≠ 0
⊢ p.order = Nat.find hp

Tactic:
convert! Nat.sInf_def hp

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < ↑ε
hx : ↑‖f x‖₊ ≤ ↑ε * ↑δ / ↑‖c‖₊ * ↑‖g x‖₊
⊢ ↑‖c‖₊ * ↑‖f x‖₊ / ↑ε ≤ ↑‖c‖₊ * (↑(ε * δ / ‖c‖₊) * ↑‖g x‖₊) / ↑ε

Tactic:
gcongr; exact_mod_cast hx

Goal state after:
Module: Mathlib.Analysis.Asymptotics.TVS

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
f : α → E
g : α → F
l : Filter α
c : 𝕜
hc : 1 < ‖c‖₊
hc₀ : 0 < ‖c‖₊
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
δ : ℝ≥0
hδ : δ ≠ 0
x : α
ε : ℝ≥0
hε : 0 < ↑ε
hx : ↑‖f x‖₊ ≤ ↑ε * ↑δ / ↑‖c‖₊ * ↑‖g x‖₊
⊢ ↑‖c‖₊ * (↑(ε * δ / ‖c‖₊) * ↑‖g x‖₊) / ↑ε = ↑‖c‖₊ / ↑‖c‖₊ * (↑ε / ↑ε) * ↑δ * ↑‖g x‖₊

Tactic:
simp only [div_eq_mul_inv, ENNReal.coe_inv hc₀.ne', ENNReal.coe_mul]; ring

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
x : E
r : ℝ≥0∞
hf : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
n : ℕ
⊢ p (n + 0) = 0

Tactic:
by rw [add_zero]; exact hp n

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c c' : ℕ → 𝕜
n✝ : ℕ
x✝ : Fin n✝ → E
⊢ (ofScalars E (c - c') n✝) x✝ = ((ofScalars E c - ofScalars E c') n✝) x✝

Tactic:
simp [ofScalars, sub_smul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
f : E →L[𝕜] E
| (ofScalars E c).compContinuousLinearMap (-f)

Tactic:
rw [← ContinuousLinearMap.id_comp f, ← ContinuousLinearMap.neg_comp]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
f : E →L[𝕜] E
| (ofScalars E c).compContinuousLinearMap ((-ContinuousLinearMap.id 𝕜 E) ∘SL f)
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
y z : E
hz2 : z ∈ Metric.eball 0 r
hz1 : z = 0 ∨ x + y + z + -y ∈ s
⊢ z = 0 ∨ x + z ∈ s

Tactic:
abel_nf at hz1

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
y z : E
hz2 : z ∈ Metric.eball 0 r
hz1 : z = 0 ∨ x + z ∈ s
⊢ z = 0 ∨ x + z ∈ s
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case pos
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : CommRing 𝕜
inst✝⁹ : AddCommGroup E
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousConstSMul 𝕜 E
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
c : Composition n
j : Fin n
v : Fin n → E
z : E
k : Fin c.length
h : k = c.index j
⊢ p.applyComposition c (Function.update v j z) k =
    Function.update (p.applyComposition c v) (c.index j)
      ((p (c.blocksFun (c.index j))) (Function.update (v ∘ ⇑(c.embedding (c.index j))) (c.invEmbedding j) z)) k

Tactic:
rw [h]
    let r : Fin (c.blocksFun (c.index j)) → Fin n := c.embedding (c.index j)
    simp only [Function.update_self]
    change p (c.blocksFun (c.index j)) (Function.update v j z ∘ r) = _
    let j' := c.invEmbedding j
    suffices B : Function.update v j z ∘ r = Function.update (v ∘ r) j' z by rw [B]
    suffices C : Function.update v (r j') z ∘ r = Function.update (v ∘ r) j' z by
      convert! C; exact (c.embedding_comp_inv j).symm
    exact Function.update_comp_eq_of_injective _ (c.embedding _).injective _ _

Goal state after:
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 : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
hL : ∀ y ∈ Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s, ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y
⊢ L =O[𝓟 (Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s)] fun y ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
simp_rw [L, mul_right_comm _ (_ * _)]

Goal state after:
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 : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r' : ℝ≥0
hr : ↑r' < r
hr'0 : 0 < r'
a : ℝ
ha : a ∈ Ioo 0 1
C : ℝ
hC : 0 < C
hp : ∀ (n : ℕ), ‖p n‖ ≤ C * a ^ n / ↑r' ^ n
L : E × E → ℝ := fun y ↦ C * (a / ↑r') ^ 2 * (‖y - (x, x)‖ * ‖y.1 - y.2‖) * (a / (1 - a) ^ 2 + 2 / (1 - a))
hL : ∀ y ∈ Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s, ‖f y.1 - f y.2 - (p 1) fun x ↦ y.1 - y.2‖ ≤ L y
⊢ (fun y ↦
      C * (a / ↑r') ^ 2 * (a / (1 - a) ^ 2 + 2 / (1 - a)) *
        (‖y - (x, x)‖ * ‖y.1 - y.2‖)) =O[𝓟 (Metric.eball (x, x) ↑r' ∩ insert x s ×ˢ insert x s)]
    fun y ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: case hi
α : Type u_6
inst✝ : AddCommMonoid α
m M N : ℕ
f : (n : ℕ) × (Fin n → ℕ) → α
g : (n : ℕ) × Composition n → α
h : ∀ (e : (n : ℕ) × (Fin n → ℕ)) (he : e ∈ compPartialSumSource m M N), f e = g (compChangeOfVariables m M N e he)
k : ℕ
blocks_fun : Fin k → ℕ
H✝ : ⟨k, blocks_fun⟩ ∈ compPartialSumSource m M N
H :
  (m ≤ ⟨k, blocks_fun⟩.fst ∧ ⟨k, blocks_fun⟩.fst < M) ∧
    ∀ (a : Fin ⟨k, blocks_fun⟩.fst), 1 ≤ ⟨k, blocks_fun⟩.snd a ∧ ⟨k, blocks_fun⟩.snd a < N
j : Fin (ofFn fun a ↦ blocks_fun a).length
⊢ { blocks := ofFn fun a ↦ blocks_fun a, blocks_pos := ⋯, blocks_sum := ⋯ }.blocksFun j < N

Tactic:
simp only [Composition.blocksFun, (H.right _).right, List.get_ofFn]

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
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ TendstoLocallyUniformlyOn (fun n y ↦ p.partialSum n y) (fun y ↦ f (x + y)) atTop (Metric.eball 0 r)

Tactic:
simpa using hf.tendstoLocallyUniformlyOn

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

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun n ↦ y ^ n • p.coeff n) (f (z₀ + y))
⊢ Tendsto (fun n ↦ ‖p n‖ * ↑‖z‖₊ ^ n) atTop (𝓝 ?l)

pp: case l
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun n ↦ y ^ n • p.coeff n) (f (z₀ + y))
⊢ ℝ

Tactic:
convert! tendsto_norm.comp (h le_z).summable.tendsto_atTop_zero

Goal state after:
case e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun n ↦ y ^ n • p.coeff n) (f (z₀ + y))
x✝ : ℕ
⊢ ‖p x✝‖ * ↑‖z‖₊ ^ x✝ = ((fun a ↦ ‖a‖) ∘ fun n ↦ z ^ n • p.coeff n) x✝
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:
rw [take_take, min_eq_left]

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 i b.blocks).sum ≤ (take (i + 1) b.blocks).sum
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
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
⊢ ∀ {y : E},
    e + y ∈ insert e t → y ∈ Metric.eball 0 (min r s) → HasSum (fun n ↦ (p.prod q n) fun x ↦ y) (f (e + y), g (e + y))

Tactic:
intro y h'y hy

Goal state after:
𝕜 : 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
e : E
f : E → F
g : E → G
r s : ℝ≥0∞
t : Set E
p : FormalMultilinearSeries 𝕜 E F
q : FormalMultilinearSeries 𝕜 E G
hf : HasFPowerSeriesWithinOnBall f p t e r
hg : HasFPowerSeriesWithinOnBall g q t e s
y : E
h'y : e + y ∈ insert e t
hy : y ∈ Metric.eball 0 (min r s)
⊢ HasSum (fun n ↦ (p.prod q n) fun x ↦ y) (f (e + y), g (e + 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
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e
⊢ HasFPowerSeriesAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) e

Tactic:
simp_rw [← hasFPowerSeriesWithinAt_univ] at hf ⊢

Goal state after:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hf : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e
⊢ HasFPowerSeriesWithinAt (fun x x_1 ↦ f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e
Module: Mathlib.Analysis.Analytic.Constructions

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

Tactic:
convert! analyticAt_const (v := (0 : A))

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
n : ℕ
f : M [⋀^Fin (n + 1)]→L[R] N
x y : M
v : Fin n → M
⊢ f (Fin.cons (x - y) v) = f (vecCons x v) - f (vecCons y v)

Tactic:
← Fin.update_cons_zero 0,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : TopologicalSpace N
n : ℕ
f : M [⋀^Fin (n + 1)]→L[R] N
x y : M
v : Fin n → M
⊢ f (update (Fin.cons 0 v) 0 (x - y)) = f (vecCons x v) - f (vecCons y v)
Module: Mathlib.Topology.Algebra.Module.Alternating.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
inst✝⁹ : Semiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : TopologicalSpace M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : TopologicalSpace N
inst✝² : IsTopologicalAddGroup N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
f x✝¹ x✝ : ContinuousMultilinearMap R (fun x ↦ M) N
⊢ (let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • domDomCongr σ (x✝¹ + x✝);
    { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }) =
    (let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • domDomCongr σ x✝¹;
      { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }) +
      let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • domDomCongr σ x✝;
      { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ }

Tactic:
ext; simp [Finset.sum_add_distrib]

Goal state after: