mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
⊢ (MonoidWithZeroHom.ofClass Valued.v).valueGroup = (MonoidWithZeroHom.ofClass (valuation K v)).valueGroup

Tactic:
ext n
  simp only [MonoidWithZeroHom.mem_valueGroup_iff_of_comm, ne_eq, MonoidWithZeroHom.coe_ofClass]
  refine ⟨fun ⟨a, ha0, x, hx⟩ ↦ ?_, fun ⟨a, ha0, x, hx⟩ ↦
    ⟨↑a, by simpa using ha0, ↑x, by simpa using hx⟩⟩
  obtain ⟨b, hb⟩ := valuation_surjective K v (Valued.v a)
  obtain ⟨y, hy⟩ := valuation_surjective K v (Valued.v x)
  exact ⟨b, by rw [hb]; exact ha0, y, by rw [hb, hy]; exact hx⟩

Goal state after:
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
inst✝ : Algebra S K
r : S
x : (valuation K v).Completion
⊢ (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r * x =
    x * (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r

Tactic:
induction x using Completion.induction_on with

Goal state after:
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
inst✝ : Algebra S K
r : S
x : (valuation K v).Completion
⊢ r • x = (Completion.coeRingHom.comp (algebraMap S (WithVal (valuation K v)))) r * x

Tactic:
induction x using Completion.induction_on with

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

Goal state before:
pp: case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) φ + 0 ≠ 0

Tactic:
add_zero

Goal state after:
case left
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
i : ℕ
H : ↑i < ψ.order
hi : ↑i = φ.order
⊢ (coeff i) φ ≠ 0
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
φ : R⟦X⟧
S : Type u_2
inst✝ : Semiring S
f : R →+* S
i : ℕ
hi : ↑i < φ.order
⊢ (coeff i) ((map f) φ) = 0

Tactic:
simp [coeff_of_lt_order i hi]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
a : R
i : ℕ
hi : ↑i < φ.order
⊢ (coeff i) (a • φ) = 0

Tactic:
simp [coeff_of_lt_order i hi]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
f : R⟦X⟧
⊢ f = (mk fun i ↦ (coeff (i + n)) f) * X ^ n + ↑((trunc n) f)

Tactic:
ext j
  rw [map_add, Polynomial.coeff_coe, coeff_mul_X_pow', coeff_trunc]
  simp_rw [← not_le, ite_not, ite_add_ite]
  simp +contextual

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

Goal state before:
pp: case self
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ f.order + ?m.34 = 0

pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ ℕ∞

Tactic:
← hf,

Goal state after:
case self
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ (↑{ val := u, inv := v, val_inv := hu, inv_val := hv }).order + ?m.34 = 0

R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f u v : R⟦X⟧
hu : u * v = 1
hv : v * u = 1
hf : ↑{ val := u, inv := v, val_inv := hu, inv_val := hv } = f
⊢ ℕ∞
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
τ : Type u_4
S : Type u_5
inst✝¹ : CommRing S
a : σ → MvPowerSeries τ S
x : σ → ℕ
inst✝ : Finite τ
ha : HasSubst a
i : σ
⊢ IsNilpotent (constantCoeff ↑((MvPowerSeries.truncTotal (x i)) (a i)))

Tactic:
by
    rw [← coeff_zero_eq_constantCoeff_apply, MvPolynomial.coeff_coe,
      ← MvPolynomial.constantCoeff_eq, constantCoeff_truncTotal_eq_ite]
    split_ifs <;> simp [ha.const_coeff i]

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

Goal state before:
pp: case e'_4
c : ℝ
h1 : 0 < c
h2 : c < 1 / 2
h3 : c < 1
f g : ℕ → Bool
hn : ∀ k < 0, f k = g k
fn : f 0 = false
gn : g 0 = true
f_max : ℕ → Bool := fun n ↦ rec false (fun x x_1 ↦ true) n
hf_max : ∀ (n : ℕ), f n = true → f_max n = true
g_min : ℕ → Bool := fun n ↦ rec true (fun x x_1 ↦ false) n
hg_min : ∀ (n : ℕ), g_min n = true → g n = true
this : c / (1 - c) < 1
⊢ cantorFunction c g_min = 1

Tactic:
refine (tsum_eq_single 0 ?_).trans ?_
      · intro n hn
        cases n
        · contradiction
        simp [g_min]
      · exact cantorFunctionAux_zero _

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

Goal state before:
pp: ⊢ ℵ₀ < #↑Set.univ

Tactic:
Cardinal.mk_univ_complex

Goal state after:
⊢ ℵ₀ < 𝔠
Module: Mathlib.NumberTheory.LSeries.Basic

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
s : ℂ
⊢ LSeries f s = ∑' (n : ℕ), f n / ↑n ^ s

Tactic:
by
  simp [LSeries, LSeries.term_def₀ hf, cpow_neg, div_eq_mul_inv]

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

Goal state before:
pp: case neg
σ : 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
n : σ →₀ ℕ
h : ¬n = 0
⊢ ((coeff n) fun n ↦ if n = 0 then n.prod fun s m ↦ a s ^ m else 0) = 0

Tactic:
· simp only [coeff_apply, ite_eq_right_iff]
      exact fun a_1 ↦ False.elim (h a_1)

Goal state after:
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
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ (∏ x_1 ∈ x.1.support ∪ x.2.support, a x_1 ^ (x.1 + x.2) x_1) * f x.1 * g x.2 =
    ((∏ x_1 ∈ x.1.support ∪ ?m.185, a x_1 ^ x.1 x_1) * f x.1 * ∏ x_1 ∈ ?m.199 ∪ x.2.support, a x_1 ^ x.2 x_1) * g x.2

Tactic:
congr 1

Goal state after:
case e_a
σ : 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
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ (∏ x_1 ∈ x.1.support ∪ x.2.support, a x_1 ^ (x.1 + x.2) x_1) * f x.1 =
    (∏ x_1 ∈ x.1.support ∪ ?m.185, a x_1 ^ x.1 x_1) * f x.1 * ∏ x_1 ∈ ?m.199 ∪ x.2.support, a x_1 ^ x.2 x_1
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case e_a
σ : 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
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ (∏ x_1 ∈ x.1.support ∪ x.2.support, a x_1 ^ (x.1 + x.2) x_1) * f x.1 =
    ((∏ x_1 ∈ x.1.support ∪ ?m.185, a x_1 ^ x.1 x_1) * ∏ x_1 ∈ ?m.199 ∪ x.2.support, a x_1 ^ x.2 x_1) * f x.1

Tactic:
congr 1

Goal state after:
case e_a.e_a
σ : 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
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ ∏ x_1 ∈ x.1.support ∪ x.2.support, a x_1 ^ (x.1 + x.2) x_1 =
    (∏ x_1 ∈ x.1.support ∪ ?m.185, a x_1 ^ x.1 x_1) * ∏ x_1 ∈ ?m.199 ∪ x.2.support, a x_1 ^ x.2 x_1
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: 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
⊢ ∑ᶠ (d : ℕ), (coeff d) P * (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ d) =
    ∑ᶠ (d : ℕ), (coeff d) P * ((coeff (n + 1 + 1)) (B ^ d) - if d = 1 then k else 0)

Tactic:
refine finsum_congr fun i ↦ ?_

Goal state after:
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 i) P * (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ i) =
    (coeff i) P * ((coeff (n + 1 + 1)) (B ^ i) - if i = 1 then k else 0)
Module: Mathlib.RingTheory.PowerSeries.Substitution

Goal state before:
pp: 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 i) P * (coeff (n + 1 + 1)) ((B + -(C k * X ^ (n + 2))) ^ i) =
    (coeff i) P * ((coeff (n + 1 + 1)) (B ^ i) - if i = 1 then k else 0)

Tactic:
congr 1

Goal state after:
case e_a
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) = (coeff (n + 1 + 1)) (B ^ i) - if i = 1 then k else 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
x : ℕ → MvPowerSeries σ R
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ Summable fun i ↦ subst a (x i)

Tactic:
rw [← coe_substAlgHom ha, substAlgHom_eq_aeval ha]

Goal state after:
σ : Type u_1
R : Type u_3
inst✝⁶ : CommRing R
τ : Type u_4
S : Type u_5
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
a : σ → MvPowerSeries τ S
x : ℕ → MvPowerSeries σ R
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ Summable fun i ↦ (aeval ⋯) (x i)
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 : ℕ
⊢ ∀ 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:
· rintro (_ | _ | j) hj hj'
              · simp at hj'
              · simp [mul_comm (C k), hB', mul_assoc, coeff_X_pow_mul']
              · rw [← neg_mul, mul_pow, ← pow_mul, mul_comm (_ ^ _)]
                simp [mul_assoc, coeff_X_pow_mul']

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 : ℕ
⊢ 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.Analysis.Calculus.FDeriv.Defs

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
s : Set E
⊢ HasFDerivWithinAt f f' s x ↔ (fun x' ↦ f x' - f x - f' (x' - x)) =o[𝕜; 𝓝[s] x] fun x' ↦ x' - x

Tactic:
by
  simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS, Function.comp_def]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
s : Set 𝕜
x : 𝕜
hx : AccPt x (𝓟 s)
y : 𝕜
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun x_1 ↦ x_1 - x

Tactic:
by fun_prop

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
x : ℕ → R⟦X⟧
a : MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ Summable fun i ↦ subst a (x i)

Tactic:
rw [← coe_substAlgHom ha, substAlgHom_eq_aeval ha]

Goal state after:
R : Type u_2
inst✝⁶ : CommRing R
τ : Type u_3
S : Type u_4
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : ℕ → R⟦X⟧
a : MvPowerSeries τ S
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
hx : Summable x
ha : HasSubst a
⊢ Summable fun i ↦ (aeval ⋯) (x i)
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
inst✝ : ContinuousAdd E
s : Set E
x : E
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
⊢ Continuous[inst✝¹, inst✝¹] fun x_1 ↦ x_1 + -x

Tactic:
by fun_prop

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
inst✝ : ContinuousAdd E
s : Set E
x : E
hx : ∃ᶠ (x : E) in 𝓝 x, x ∈ s
⊢ Continuous[inst✝¹, inst✝¹] fun n ↦ n + -x

Tactic:
by fun_prop

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
x y : E
h : openSegment ℝ x y ⊆ s
a : ℝ≥0
ha : a ∈ Ioo 0 1
⊢ x + id a • (y - x) ∈ openSegment ℝ x y

Tactic:
rw [openSegment_eq_image_lineMap]

Goal state after:
E : Type u_1
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
a : ℝ≥0
ha : a ∈ Ioo 0 1
⊢ x + id a • (y - x) ∈ ⇑(AffineMap.lineMap x y) '' Ioo 0 1
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
x y : 𝕜
⊢ (fderiv 𝕜 f x) y = y • deriv f x

Tactic:
by
  rw [← fderiv_apply_one_eq_deriv, ← map_smul]
  simp only [smul_eq_mul, mul_one]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst✝ : T1Space E
y : E
⊢ HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x

Tactic:
← hasFDerivWithinAt_insert,

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
f' : E →L[𝕜] F
x : E
s : Set E
inst✝ : T1Space E
y : E
⊢ HasFDerivWithinAt f f' (insert ?m.91 (s \ {y})) x ↔ HasFDerivWithinAt f f' s x

𝕜 : 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
s : Set E
inst✝ : T1Space E
y : E
⊢ E
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' - 0 - 0) =o[𝓝[s] x₀] fun x' ↦ x' - x₀

Tactic:
sub_zero,

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
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₀
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 : ℕ
⊢ (p (n + 1)) (cons 1 1) = (p (n + 1)) 1

Tactic:
congr 1

Goal state after:
case e_6
𝕜 : Type u
E : Type v
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
n : ℕ
⊢ cons 1 1 = 1
Module: Mathlib.Analysis.Calculus.FDeriv.Basic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
V' : Type u_3
W : Type u_4
W' : Type u_5
inst✝¹⁰ : NontriviallyNormedField 𝕜
σ σ' : 𝕜 →+* 𝕜
inst✝⁹ : NormedAddCommGroup V
inst✝⁸ : NormedSpace 𝕜 V
inst✝⁷ : NormedAddCommGroup V'
inst✝⁶ : NormedSpace 𝕜 V'
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace 𝕜 W
inst✝³ : NormedAddCommGroup W'
inst✝² : NormedSpace 𝕜 W'
inst✝¹ : RingHomIsometric σ
inst✝ : RingHomInvPair σ σ'
L : W →SL[σ] W'
R : V' →SL[σ'] V
f : V → W
z : V'
hf : DifferentiableAt 𝕜 f (R z)
⊢ DifferentiableAt 𝕜 (⇑L ∘ f ∘ ⇑R) z

Tactic:
by
  simpa using (hf.hasFDerivAt.comp_semilinear L R).differentiableAt

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ k + l - l = k

Tactic:
add_tsub_cancel_right

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
x y : E
r : ℝ≥0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
⊢ k = k
Module: Mathlib.Analysis.Analytic.ChangeOrigin

Goal state before:
pp: case refine_2
𝕜 : 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
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
hsf : Summable f
k : ℕ
this : HasSum (fun n ↦ (p.changeOriginSeries k n) fun x_1 ↦ x) (p.changeOrigin x k)
⊢ Summable fun c ↦ (p.changeOriginSeriesTerm k c.fst ↑c.snd ⋯) fun x_1 ↦ x

Tactic:
refine .of_nnnorm_bounded
          (p.changeOriginSeries_summable_aux₂ (mem_eball_zero_iff.1 x_mem_ball) k)
            fun s => ?_

Goal state after:
case refine_2
𝕜 : 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
x y : E
h : ↑‖x‖₊ + ↑‖y‖₊ < p.radius
x_mem_ball : x ∈ Metric.eball 0 p.radius
y_mem_ball : y ∈ Metric.eball 0 (p.changeOrigin x).radius
x_add_y_mem_ball : x + y ∈ Metric.eball 0 p.radius
f : (k : ℕ) × (l : ℕ) × { s // s.card = l } → F :=
  fun s ↦ ((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 ↦ x) fun x ↦ y
hsf : Summable f
k : ℕ
this : HasSum (fun n ↦ (p.changeOriginSeries k n) fun x_1 ↦ x) (p.changeOrigin x k)
s : (b : ℕ) × { s // s.card = b }
⊢ ‖(p.changeOriginSeriesTerm k s.fst ↑s.snd ⋯) fun x_1 ↦ x‖₊ ≤ ‖p (k + s.fst)‖₊ * ‖x‖₊ ^ s.fst