mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ order 0 = ↑n ↔ (coeff n) 0 ≠ 0 ∧ ∀ i < n, (coeff i) 0 = 0

pp: case inr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hφ : φ ≠ 0
⊢ φ.order = ↑n ↔ (coeff n) φ ≠ 0 ∧ ∀ i < n, (coeff i) φ = 0

Tactic:
· simp

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
hφ : φ ≠ 0
⊢ φ.order = ↑n ↔ (coeff n) φ ≠ 0 ∧ ∀ i < n, (coeff i) φ = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDedekindDomain R
K : Type u_2
S : Type u_3
inst✝³ : Field K
inst✝² : CommSemiring S
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
b : ℝ≥0
hb : 1 < b
r : R
x : K
x✝¹ x✝ : R
⊢ ↑(v.intAdicAbvDef hb (x✝¹ * x✝)) = ↑(v.intAdicAbvDef hb x✝¹) * ↑(v.intAdicAbvDef hb x✝)

Tactic:
by simp [intAdicAbvDef]

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
S : Type u_2
inst✝ : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
⊢ eval₂ G s ((trunc (n + 1)) f) = ∑ i ∈ range (n + 1), G ((coeff i) f) * s ^ i

Tactic:
| succ n =>

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : IsCentralScalar R M
⊢ IsLinearTopology Rᵐᵒᵖ M ↔ IsLinearTopology R M

Tactic:
constructor <;> intro H
  · exact mk_of_hasBasis' R (IsLinearTopology.hasBasis_submodule Rᵐᵒᵖ)
      fun S r m hm ↦ op_smul_eq_smul r m ▸ S.smul_mem _ hm
  · exact mk_of_hasBasis' Rᵐᵒᵖ (IsLinearTopology.hasBasis_submodule R)
      fun S r m hm ↦ unop_smul_eq_smul r m ▸ S.smul_mem _ hm

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

Goal state before:
pp: case inl
R : Type u_2
inst✝ : Semiring R
⊢ order 0 = emultiplicity X 0

pp: case inr
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
⊢ φ.order = emultiplicity X φ

Tactic:
· simp

Goal state after:
case inr
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
⊢ φ.order = emultiplicity X φ
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : 1 = 0
⊢ ↑n < ⊤

pp: case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(φ.order.toNat + 1)

Tactic:
· simp

Goal state after:
case neg
R : Type u_2
inst✝ : Semiring R
φ : R⟦X⟧
hφ : φ ≠ 0
n : ℕ
ho : φ.order = ↑n
hn : φ.order.toNat = n
ψ : R⟦X⟧
H : φ = X ^ (φ.order.toNat + 1) * ψ
this : (coeff n) φ = (coeff n) (ψ * X ^ (φ.order.toNat + 1))
h✝ : ¬1 = 0
⊢ ↑n < ↑(φ.order.toNat + 1)
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
⊢ ∀ (x : ι), (coeff n) (f x) ≠ 0 → x ≤ i

Tactic:
intro k hk

Goal state after:
case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_2
f : ι → R⟦X⟧
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
k : ι
hk : (coeff n) (f k) ≠ 0
⊢ k ≤ i
Module: Mathlib.RingTheory.PowerSeries.Evaluation

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
this : HasSum (fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
⊢ HasSum (fun d ↦ φ ((coeff d) f) * a ^ d) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)

Tactic:
← (Finsupp.single_injective ()).hasSum_iff

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
this :
  HasSum ((fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) ∘ Finsupp.single ())
    (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
⊢ HasSum (fun d ↦ φ ((coeff d) f) * a ^ d) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)

R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
φ : R →+* S
a : S
inst✝⁸ : UniformSpace R
inst✝⁷ : UniformSpace S
inst✝⁶ : IsUniformAddGroup R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : IsUniformAddGroup S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
inst✝¹ : IsTopologicalRing S
inst✝ : IsLinearTopology S S
hφ : Continuous ⇑φ
ha : HasEval a
f : R⟦X⟧
this : HasSum (fun d ↦ φ ((MvPowerSeries.coeff d) f) * d.prod fun s e ↦ a ^ e) (MvPowerSeries.eval₂ φ (fun x ↦ a) f)
⊢ ∀ x ∉ Set.range (Finsupp.single ()), (φ ((MvPowerSeries.coeff x) f) * x.prod fun s e ↦ a ^ e) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Evaluation

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst✝⁹.toTopologicalSpace] ⇑ε
p : MvPolynomial σ R
⊢ ε ↑p = (ε.comp (coeToMvPowerSeries.algHom R)) p

pp: σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst✝⁹.toTopologicalSpace] ⇑ε
p : MvPolynomial σ R
⊢ (ε.comp (coeToMvPowerSeries.algHom R)) p = MvPolynomial.eval₂ (algebraMap R S) (fun s ↦ ε.toRingHom (X s)) p

Tactic:
· simp

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : UniformSpace R
S : Type u_3
inst✝¹⁰ : CommRing S
inst✝⁹ : UniformSpace S
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : IsUniformAddGroup R
inst✝⁶ : IsUniformAddGroup S
inst✝⁵ : CompleteSpace S
inst✝⁴ : T2Space S
inst✝³ : IsTopologicalRing S
inst✝² : IsLinearTopology S S
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
ε : MvPowerSeries σ R →ₐ[R] S
hε : Continuous[instTopologicalSpace R, inst✝⁹.toTopologicalSpace] ⇑ε
p : MvPolynomial σ R
⊢ (ε.comp (coeToMvPowerSeries.algHom R)) p = MvPolynomial.eval₂ (algebraMap R S) (fun s ↦ ε.toRingHom (X s)) p
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} 𝔠 ≤ lift.{v, u} c ↔ 𝔠 ≤ c

Tactic:
lift_le

Goal state after:
c : Cardinal.{u}
⊢ 𝔠 ≤ c ↔ 𝔠 ≤ c
Module: Mathlib.SetTheory.Cardinal.Continuum

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c ≤ lift.{v, u} 𝔠 ↔ c ≤ 𝔠

Tactic:
lift_le

Goal state after:
c : Cardinal.{u}
⊢ c ≤ 𝔠 ↔ c ≤ 𝔠
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q n : ℕ
hq : ¬1 < q
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff 1)) n = 1 n

Tactic:
· simp

Goal state after:
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
⊢ ∀ k < n, f k = g k

Tactic:
intro k hk

Goal state after:
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
f g : ℕ → Bool
h : ¬f = g
this : ∃ n, f n ≠ g n
n : ℕ := Nat.find this
k : ℕ
hk : k < n
⊢ f k = g k
Module: Mathlib.Analysis.Real.Cardinality

Goal state before:
pp: case a.convert_2
⊢ 0 < 1 / 3

pp: case a.convert_3
⊢ 1 / 3 < 1 / 2

Tactic:
· simp

Goal state after:
case a.convert_3
⊢ 1 / 3 < 1 / 2
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inl
f : ℕ → ℂ
s : ℂ
⊢ ‖term f s 0‖ = if 0 = 0 then 0 else ‖f 0‖ / ↑0 ^ s.re

pp: case inr
f : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re

Tactic:
· simp

Goal state after:
case inr
f : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ ‖term f s n‖ = if n = 0 then 0 else ‖f n‖ / ↑n ^ s.re
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: case inl
s : ℂ
⊢ term δ s 0 = if 0 = 1 then 1 else 0

pp: case inr
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term δ s n = if n = 1 then 1 else 0

Tactic:
· simp

Goal state after:
case inr
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term δ s n = if n = 1 then 1 else 0
Module: Mathlib.NumberTheory.ArithmeticFunction.LFunction

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
f g : PowerSeries R
n : ℕ
hq : ¬1 < q
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff (f * g))) n =
    ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff f) *
        (algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff g))
      n

Tactic:
· simp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
q : ℕ
x : R
n : ℕ
hq : ¬1 < q
⊢ ((algebraMap R (ArithmeticFunction R)) (PowerSeries.constantCoeff ((algebraMap R (PowerSeries R)) x))) n =
    ((algebraMap R (ArithmeticFunction R)) x) n

Tactic:
· simp

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

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬(MvPowerSeries.coeff i) f = 0
⊢ f.order * MvPowerSeries.weightedOrder w a ≤ ↑(i ()) * MvPowerSeries.weightedOrder w a

pp: R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬(MvPowerSeries.coeff i) f = 0
⊢ ↑(i ()) * MvPowerSeries.weightedOrder w a ≤ (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a))) i

Tactic:
· exact mul_le_mul_left (f.order_le (i ()) (by delta PowerSeries.coeff; convert! hi; aesop)) _

Goal state after:
R : Type u_2
inst✝² : CommRing R
τ : Type u_3
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : MvPowerSeries τ S
w : τ → ℕ
ha : HasSubst a
f : R⟦X⟧
i : Unit →₀ ℕ
hi : ¬(MvPowerSeries.coeff i) f = 0
⊢ ↑(i ()) * MvPowerSeries.weightedOrder w a ≤ (Finsupp.weight (Function.const Unit (MvPowerSeries.weightedOrder w a))) i
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
h : 0 • x ∈ s
⊢ egauge 𝕜 s x ≤ ‖0‖ₑ⁻¹

pp: case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹

Tactic:
· simp

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
h : c • x ∈ s
hc : c ≠ 0
⊢ egauge 𝕜 s x ≤ ‖c‖ₑ⁻¹
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = 0 • x
⊢ ‖0‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ

pp: case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = c • x
hc : c ≠ 0
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ

Tactic:
· simp

Goal state after:
case inr
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
a : 𝕜
y : E
hy : y ∈ s
hxy : (fun x ↦ a • x) y = c • x
hc : c ≠ 0
⊢ ‖c‖ₑ * egauge 𝕜 s x ≤ ‖a‖ₑ
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case e_a.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ 0) = (coeff (n + 1 + 1)) (B ^ 0) - if 0 = 1 then k else 0

pp: case e_a.succ.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ (0 + 1)) =
    (coeff (n + 1 + 1)) (B ^ (0 + 1)) - if 0 + 1 = 1 then k else 0

pp: case e_a.succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ (i + 1 + 1)) =
    (coeff (n + 1 + 1)) (B ^ (i + 1 + 1)) - if i + 1 + 1 = 1 then k else 0

Tactic:
· simp

Goal state after:
case e_a.succ.zero
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
⊢ (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ (0 + 1)) =
    (coeff (n + 1 + 1)) (B ^ (0 + 1)) - if 0 + 1 = 1 then k else 0

case e_a.succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ (i + 1 + 1)) =
    (coeff (n + 1 + 1)) (B ^ (i + 1 + 1)) - if i + 1 + 1 = 1 then k else 0
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
this : ∀ (w : Finset ι), (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k
⊢ ∀ k ≤ n, (∏ x ∈ u \ t, f x) k = (∏ x ∈ v \ t, f x) k

Tactic:
intro k hk

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
this : ∀ (w : Finset ι), (∀ i ∈ w, i ∈ s) → ∀ k ≤ n, (∏ x ∈ w, f x) k = 1 k
k : ℕ
hk : k ≤ n
⊢ (∏ x ∈ u \ t, f x) k = (∏ x ∈ v \ t, f x) k
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 ≤ n, (∏ x ∈ insert i w, f x) k = 1 k

Tactic:
intro k hk

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
⊢ (∏ x ∈ insert i w, f x) k = 1 k
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case e_a.succ.succ
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ 0 * B ^ (i + 2 - 0) * ↑((i + 2).choose 0)) =
    (coeff (n + 2)) (B ^ (i + 2)) - if i + 2 = 1 then k else 0

pp: case e_a.succ.succ.h₀
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ ∀ b ∈ Finset.range (i + 2 + 1),
    b ≠ 0 → (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ b * B ^ (i + 2 - b) * ↑((i + 2).choose b)) = 0

pp: case e_a.succ.succ.h₁
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ 0 ∉ Finset.range (i + 2 + 1) →
    (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ 0 * B ^ (i + 2 - 0) * ↑((i + 2).choose 0)) = 0

Tactic:
· simp

Goal state after:
case e_a.succ.succ.h₀
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ ∀ b ∈ Finset.range (i + 2 + 1),
    b ≠ 0 → (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ b * B ^ (i + 2 - b) * ↑((i + 2).choose b)) = 0

case e_a.succ.succ.h₁
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ 0 ∉ Finset.range (i + 2 + 1) →
    (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ 0 * B ^ (i + 2 - 0) * ↑((i + 2).choose 0)) = 0
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: case e_a.succ.succ.h₁
R : Type u_2
inst✝¹ : CommRing R
P : R⟦X⟧
hP : constantCoeff P = 0
inst✝ : Invertible ((coeff 1) P)
n : ℕ
B : R⟦X⟧
hB : ∑ i, C (P.substInvFun ↑i) * X ^ ↑i = B
hB' : constantCoeff B = 0
k : R
hk : ⅟((coeff 1) P) * (coeff (n + 1 + 1)) (subst B P) = k
i : ℕ
⊢ 0 ∉ Finset.range (i + 2 + 1) →
    (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ 0 * B ^ (i + 2 - 0) * ↑((i + 2).choose 0)) = 0

Tactic:
· simp

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

Goal state before:
pp: case zero
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n : ℕ
i : ι
hi : 0 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) 0 = 1 0

pp: case succ.zero
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n : ℕ
i : ι
hi : 0 + 1 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) (0 + 1) = 1 (0 + 1)

pp: case succ.succ
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n✝ : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) (n + 1 + 1) = 1 (n + 1 + 1)

Tactic:
· simp

Goal state after:
case succ.zero
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n : ℕ
i : ι
hi : 0 + 1 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) (0 + 1) = 1 (0 + 1)

case succ.succ
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
q : ι → ℕ
hq : Northcott q
f : ι → PowerSeries R
hf : ∀ (i : ι), PowerSeries.constantCoeff (f i) = 1
n✝ : ℕ
i : ι
n : ℕ
hi : n + 1 + 1 + 1 ≤ q i
⊢ ((ofPowerSeries (q i)) (f i)) (n + 1 + 1) = 1 (n + 1 + 1)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
P : R⟦X⟧
hP' : IsUnit ((coeff 1) P)
this : Invertible ((coeff 1) P) := hP'.invertible
⊢ (coeff 1) (P.substInvOfIsUnit hP') = ↑hP'.unit⁻¹

Tactic:
rw [substInvOfIsUnit_eq_substInv, coeff_one_substInv]

Goal state after:
R : Type u_2
inst✝ : CommRing R
P : R⟦X⟧
hP' : IsUnit ((coeff 1) P)
this : Invertible ((coeff 1) P) := hP'.invertible
⊢ ⅟((coeff 1) P) = ↑hP'.unit⁻¹
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) (∏ x ∈ {default}, (X₀ + X₁) ^ d x) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff (e 0 + e 1)) f

Tactic:
PUnit.default_eq_unit,

Goal state after:
R : Type u_2
inst✝ : CommRing R
f : R⟦X⟧
e : Fin 2 →₀ ℕ
⊢ ∑ᶠ (d : Unit →₀ ℕ), (MvPowerSeries.coeff d) f • (MvPowerSeries.coeff e) (∏ x ∈ {PUnit.unit}, (X₀ + X₁) ^ d x) =
    ↑((e 0 + e 1).choose (e 0)) * (coeff (e 0 + e 1)) f
Module: Mathlib.Analysis.Calculus.FDeriv.Const

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
⊢ ¬AccPt x (𝓟 {x})

Tactic:
rw [accPt_iff_clusterPt, inf_principal]

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
x : E
⊢ ¬ClusterPt x (𝓟 ({x}ᶜ ∩ {x}))
Module: Mathlib.Analysis.Calculus.FDeriv.Const

Goal state before:
pp: case inl
𝕜 : 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
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivWithinAt f 0 ∅ x

pp: case inr
𝕜 : 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
h : Subsingleton E
f : E → F
x a : E
⊢ HasFDerivWithinAt f 0 {a} x

Tactic:
· simp

Goal state after:
case inr
𝕜 : 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
h : Subsingleton E
f : E → F
x a : E
⊢ HasFDerivWithinAt f 0 {a} x
Module: Mathlib.Analysis.Calculus.Deriv.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f f₁ : 𝕜 → F
x : 𝕜
h : f₁ =ᶠ[𝓝[≠] x] f
⊢ deriv f₁ =ᶠ[𝓝[≠] x] deriv f

Tactic:
by
  rw [Filter.EventuallyEq, ← eventually_nhdsNE_eventually_nhds_iff] at *
  filter_upwards [h] with y hy
  apply Filter.EventuallyEq.deriv hy

Goal state after: