mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case refine_1
A : Type u_1
K : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : IsDiscreteValuationRing A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
a : K
h : (valuation K (maximalIdeal A)) a = 1
⊢ ∃ x ∈ IsUnit.submonoid A, (algebraMap A K) x = a

Tactic:
obtain ⟨b, rfl⟩ := IsDiscreteValuationRing.exists_lift_of_le_one h.le
    rw [valuation_eq_one_iff_notMem] at h
    simp only [IsDiscreteValuationRing.maximalIdeal, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
      not_not] at h
    use b, h

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: x : ℤ ≃+ ℤ
⊢ x ∈ Finset.cons (AddEquiv.neg ℤ) {AddEquiv.refl ℤ} instFintypeAddEquivInt._proof_2

Tactic:
by
    obtain rfl | rfl := Int.addEquiv_eq_refl_or_neg x <;>
    simp

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU : ∀ x ∉ U, ∃ γ, U ⊆ {a | ↑γ ≤ v.restrict (a - x)}
h : 0 ∉ U
⊢ ∃ γ, ¬γ = 0 ∧ U ⊆ ⇑v.restrict ⁻¹' Ici γ

Tactic:
obtain ⟨γ, h⟩ := hU _ h

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
U : Set K
hU' : U.Nonempty
hU : ∀ x ∉ U, ∃ γ, U ⊆ {a | ↑γ ≤ v.restrict (a - x)}
h✝ : 0 ∉ U
γ : (ofClass v).ValueGroup₀ˣ
h : U ⊆ {a | ↑γ ≤ v.restrict (a - 0)}
⊢ ∃ γ, ¬γ = 0 ∧ U ⊆ ⇑v.restrict ⁻¹' Ici γ
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
this : ⊤ = AddSubgroup.closure {x}
e : G ≃+o ↥⊤ := { toAddEquiv := AddSubsemigroup.topEquiv.symm, map_le_map_iff' := ⋯ }
e' : ↥⊤ ≃+o ↥(AddSubgroup.closure {x}) := { toAddEquiv := AddEquiv.subsemigroupCongr ⋯, map_le_map_iff' := ⋯ }
g : ↥⊤ ≃+o ℤ := { toAddEquiv := AddSubsemigroup.topEquiv, map_le_map_iff' := ⋯ }
g' : ↥(AddSubgroup.closure {1}) ≃+o ↥⊤ :=
  { toAddEquiv := AddEquiv.subsemigroupCongr int_orderAddMonoidIso_of_isLeast_pos._proof_2, map_le_map_iff' := ⋯ }
⊢ G ≃+o ℤ

Tactic:
let f := closure_equiv_closure x (1 : ℤ) (by simp [h.left.ne'])

Goal state after:
G✝ : Type u_1
inst✝⁷ : CommGroup G✝
inst✝⁶ : LinearOrder G✝
inst✝⁵ : IsOrderedMonoid G✝
inst✝⁴ : MulArchimedean G✝
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Archimedean G
x : G
h : IsLeast {y | 0 < y} x
this : ⊤ = AddSubgroup.closure {x}
e : G ≃+o ↥⊤ := { toAddEquiv := AddSubsemigroup.topEquiv.symm, map_le_map_iff' := ⋯ }
e' : ↥⊤ ≃+o ↥(AddSubgroup.closure {x}) := { toAddEquiv := AddEquiv.subsemigroupCongr ⋯, map_le_map_iff' := ⋯ }
g : ↥⊤ ≃+o ℤ := { toAddEquiv := AddSubsemigroup.topEquiv, map_le_map_iff' := ⋯ }
g' : ↥(AddSubgroup.closure {1}) ≃+o ↥⊤ :=
  { toAddEquiv := AddEquiv.subsemigroupCongr int_orderAddMonoidIso_of_isLeast_pos._proof_2, map_le_map_iff' := ⋯ }
f : ↥(AddSubgroup.closure {x}) ≃+o ↥(AddSubgroup.closure {1}) := closure_equiv_closure x 1 ⋯
⊢ G ≃+o ℤ
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
γ : Γ₀ˣ
x : hat K
γ₀' : (ofClass v).ValueGroup₀ := extension x
hγ₀'_def : γ₀' = extension x
γ₀ : Γ₀ := extensionValuation x
hγ₀_def : γ₀ = extensionValuation x
heq : γ₀ = embedding γ₀'
this : γ₀ ≠ 0 → (x ∈ closure (Completion.coe' '' {x | v x < ↑γ}) ↔ γ₀ < ↑γ)
h : γ₀ = 0
⊢ 0 ∈ {x | v x < ↑γ} ∧ ↑0 = 0

Tactic:
by simp only [mem_ofPred_eq, Valuation.map_zero, Units.zero_lt, true_and]; rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₁
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ lmax

Tactic:
apply le_self_pow hlmax_ge_1.le

Goal state after:
case h.h₁
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ lmax
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₂
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ lmax ^ 2

Tactic:
apply le_self_pow hlmax_ge_1.le

Goal state after:
case h.h₂
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ 2 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₃
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ lmax ^ 3

Tactic:
apply le_self_pow hlmax_ge_1.le

Goal state after:
case h.h₃
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ 3 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₄
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ lmax ^ 4

Tactic:
apply le_self_pow hlmax_ge_1.le

Goal state after:
case h.h₄
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ 4 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Reduction

Goal state before:
pp: case h.h₆
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := [W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
l : List (ValueGroup R K) := List.map (fun a ↦ (valuation R K) a) l₀
lmax : ValueGroup R K := List.maximum_of_length_pos ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ lmax ≤ lmax ^ 6

Tactic:
apply le_self_pow hlmax_ge_1.le

Goal state after:
case h.h₆
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsDomain R
inst✝¹ : ValuationRing R
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
l₀ : List K := ⋯
l : List (ValueGroup R K) := ⋯
lmax : ValueGroup R K := ⋯
hlmax_mem : lmax ∈ l
hlmax : ∀ v ∈ l, v ≤ lmax
hlmax_le_1 : ¬lmax ≤ 1
hlmax_ge_1 : lmax ≥ 1
a : K
ha : (valuation R K) a = lmax
ha₀ : a ≠ 0
⊢ 6 ≠ 0
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
h : α → β
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
⊢ (∀ (b : β), {a | h a ≤ b}.Finite) ↔ Tendsto h cofinite atTop

Tactic:
tendsto_atTop,

Goal state after:
α : Type u_1
β : Type u_2
h : α → β
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
⊢ (∀ (b : β), {a | h a ≤ b}.Finite) ↔ ∀ (b : β), ∀ᶠ (a : α) in cofinite, b ≤ h a
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
H : X = 0
⊢ False

Tactic:
simpa only [coeff_one_X, one_ne_zero, map_zero] using congr_arg (coeff 1) H

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
⊢ X s ^ n = (monomial (single s n)) 1

Tactic:
by
  induction n with
  | zero => simp
  | succ n ih => rw [pow_succ, ih, Finsupp.single_add, X, monomial_mul_monomial, one_mul]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors)) ≤
      exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)) ∨
    exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors)) ≤
      exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors))

Tactic:
simp only [exp_le_exp, neg_le_neg_iff, Nat.cast_le, ← min_le_iff]

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x y : R
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
      ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors) ≤
    (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x + y})).factors
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : (coeff 0) φ = 0
⊢ ∀ m < 1, (coeff m) φ = 0

Tactic:
intro m hm
    rwa [Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hm)]

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

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : (coeff 0) φ = 0
⊢ ∀ m < 1, (coeff m) φ = 0

Tactic:
· intro m hm
    rwa [Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hm)]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ f (∑ p ∈ antidiagonal n, (coeff p.1) φ * (coeff p.2) ψ) =
    (coeff n) ((fun n ↦ f ((coeff n) φ)) * fun n ↦ f ((coeff n) ψ))

Tactic:
map_sum,

Goal state after:
σ : Type u_1
R : Type u_2
S : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
φ ψ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ ∑ x ∈ antidiagonal n, f ((coeff x.1) φ * (coeff x.2) ψ) =
    (coeff n) ((fun n ↦ f ((coeff n) φ)) * fun n ↦ f ((coeff n) ψ))
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ X s ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0

Tactic:
← pow_one (X s : MvPowerSeries σ R),

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
⊢ X s ^ 1 ∣ φ ↔ ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0
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
r : R
⊢ v.intValuation r < 1 ↔ r ∈ v.asIdeal

Tactic:
exact v.intValuation_lt_one_iff_mem r

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type u_4
inst✝¹ : Semiring B
inst✝ : Algebra R B
φ : A →ₐ[R] B
r : R
⊢ (↑↑(map ↑φ)).toFun ((algebraMap R (MvPowerSeries σ A)) r) = (algebraMap R (MvPowerSeries σ B)) r

Tactic:
simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe,
      MonoidHom.coe_coe, MvPowerSeries.algebraMap_apply, map_C, RingHom.coe_coe, AlgHom.commutes]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
a : R
i : σ →₀ ℕ
hi : ↑((weight w) i) < weightedOrder w f
⊢ (coeff i) (a • f) = 0

Tactic:
simp [coeff_eq_zero_of_lt_weightedOrder _ hi]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
S : Type u_3
inst✝ : Semiring S
φ : R →+* S
i : σ →₀ ℕ
hi : ↑((weight w) i) < weightedOrder w f
⊢ (coeff i) ((map φ) f) = 0

Tactic:
simp [coeff_eq_zero_of_lt_weightedOrder _ hi]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), degree d < n → (coeff d) f = 0
⊢ ↑n ≤ f.order

Tactic:
simp_rw [degree_eq_weight_one] at h
  exact nat_le_weightedOrder _ h

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

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ constantCoeff f = 0 → 1 ≤ f.order

Tactic:
intro h
    refine MvPowerSeries.le_order fun d hd ↦ ?_
    rw [Nat.cast_lt_one] at hd
    simp [(degree_eq_zero_iff d).mp hd, h]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
H : IsTopologicallyNilpotent (constantCoeff f)
⊢ IsNilpotent (constantCoeff f)

Tactic:
simp_rw [IsTopologicallyNilpotent, nhds_discrete, tendsto_pure] at H

Goal state after:
σ : Type u_1
R : Type u_2
inst✝² : TopologicalSpace R
inst✝¹ : CommRing R
inst✝ : DiscreteTopology R
f : MvPowerSeries σ R
H : ∀ᶠ (x : ℕ) in atTop, constantCoeff f ^ x = 0
⊢ IsNilpotent (constantCoeff f)
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 : ℕ
this : ((trunc (n + 1)) f).natDegree < n + 1
⊢ eval₂ G s ((trunc (n + 1)) f) = ∑ i ∈ range (n + 1), G ((coeff i) f) * s ^ i

Tactic:
rw [eval₂_eq_sum_range' (hn := this)]

Goal state after:
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 : ℕ
this : ((trunc (n + 1)) f).natDegree < n + 1
⊢ ∑ i ∈ range (n + 1), G (((trunc (n + 1)) f).coeff i) * s ^ i = ∑ i ∈ range (n + 1), G ((coeff i) f) * s ^ i
Module: Mathlib.RingTheory.MvPowerSeries.LinearTopology

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Ring R
Jd : TwoSidedIdeal R × (σ →₀ ℕ)
x✝ y✝ : MvPowerSeries σ R
hf : x✝ ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
hg : y✝ ∈ {f | ∀ e ≤ Jd.2, (coeff e) f ∈ Jd.1}
e : σ →₀ ℕ
he : e ≤ Jd.2
⊢ (coeff e) (x✝ + y✝) ∈ Jd.1

Tactic:
by rw [map_add]; exact add_mem (hf e he) (hg e he)

Goal state after:
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
a : σ → 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
ha : HasEval a
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : IsUniformAddGroup T
inst✝⁵ : IsTopologicalRing T
inst✝⁴ : IsLinearTopology T T
inst✝³ : T2Space T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst✝¹⁸.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑ε
⊢ ⇑↑ε ∘ eval₂ (algebraMap R S) a = ⇑(aeval ⋯)

Tactic:
comp_eval₂ (continuous_algebraMap R S) ha (show Continuous (ε : S →+* T) from hε),

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
a : σ → 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
ha : HasEval a
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : IsUniformAddGroup T
inst✝⁵ : IsTopologicalRing T
inst✝⁴ : IsLinearTopology T T
inst✝³ : T2Space T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous[inst✝¹⁸.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑ε
⊢ eval₂ ((↑ε).comp (algebraMap R S)) (⇑↑ε ∘ a) = ⇑(aeval ⋯)
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
ha : HasSubst a
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ eval₂ (algebraMap R (MvPowerSeries τ S)) a = subst a

Tactic:
subst_eq_eval₂

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
ha : HasSubst a
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
⊢ eval₂ (algebraMap R (MvPowerSeries τ S)) a = eval₂ (algebraMap R (MvPowerSeries τ S)) a
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
ha : HasSubst a
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
⊢ Continuous (subst a)

Tactic:
subst_eq_eval₂

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
ha : HasSubst a
inst✝³ : UniformSpace R
inst✝² : DiscreteUniformity R
inst✝¹ : UniformSpace S
inst✝ : DiscreteUniformity S
⊢ Continuous (eval₂ (algebraMap R (MvPowerSeries τ S)) a)
Module: Mathlib.Analysis.Convex.EGauge

Goal state before:
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:
exact (egauge_le_of_smul_mem_of_ne h hc).trans ENNReal.coe_inv_le

Goal state after:
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)) (∑ m ∈ Finset.range (i + 2 + 1), (-(C k * X ^ (n + 2))) ^ m * B ^ (i + 2 - m) * ↑((i + 2).choose m)) =
    (coeff (n + 2)) (B ^ (i + 2)) - if i + 2 = 1 then k else 0

Tactic:
map_sum,

Goal state after:
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 : ℕ
⊢ ∑ x ∈ Finset.range (i + 2 + 1), (coeff (n + 2)) ((-(C k * X ^ (n + 2))) ^ x * B ^ (i + 2 - x) * ↑((i + 2).choose x)) =
    (coeff (n + 2)) (B ^ (i + 2)) - if i + 2 = 1 then k else 0
Module: Mathlib.RingTheory.MvPowerSeries.Substitution

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_9
inst✝ : CommSemiring R
n : ℕ
r : R
f : MvPowerSeries σ R
hf : ∀ d ∈ Function.support f, Finsupp.degree d = n
e : σ →₀ ℕ
he : e ∉ Function.support f
⊢ (r ^ ∑ i ∈ e.support, e i) * (coeff e) f = r ^ n * (coeff e) f

Tactic:
· simp only [Function.mem_support, ne_eq, not_not] at he
    simp [he, mul_zero, coeff_apply]

Goal state after:
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 ↦ (aeval ⋯) (x i)

Tactic:
exact hx.map _ <| continuous_aeval ha.hasEval

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

Goal state before:
pp: case neg
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : ι) → AddCommGroup (E i)
inst✝ : (i : ι) → Module 𝕜 (E i)
I : Set ι
hI : I.Finite
U : (i : ι) → Set (E i)
hU : ∀ i ∈ I, Balanced 𝕜 (U i)
x : (i : ι) → E i
hI₀ : I = univ ∨ (∃ i ∈ I, x i ≠ 0) ∨ (𝓝[≠] 0).NeBot
r : ℝ≥0∞
hr : ⨆ i ∈ I, egauge 𝕜 (U i) (x i) < r
c : ι → 𝕜
hc : ∀ i ∈ I, x i ∈ c i • U i
hcr : ∀ i ∈ I, ‖c i‖ₑ < r
hr₀ : 0 < r
hIne : I.Nonempty
i₀ : ι
hi₀I : i₀ ∈ I
hc_max : IsMaxOn (fun x ↦ ‖c x‖ₑ) I i₀
H : c i₀ = 0 ∧ I ≠ univ
⊢ ∃ c₀, (c₀ ≠ 0 ∨ I = univ) ∧ (∀ i ∈ I, ‖c i‖ ≤ ‖c₀‖) ∧ ‖c₀‖ₑ < r

Tactic:
· have hc0 (i : ι) (hi : i ∈ I) : c i = 0 := by simpa [H] using hc_max hi
        have heg0 (i : ι) (hi : i ∈ I) : x i = 0 :=
          zero_smul_set_subset (α := 𝕜) (U i) (hc0 i hi ▸ hc i hi)
        have : (𝓝[≠] (0 : 𝕜)).NeBot := (hI₀.resolve_left H.2).resolve_left (by simpa)
        rcases exists_enorm_lt 𝕜 hr₀.ne' with ⟨c₁, hc₁, hc₁r⟩
        refine ⟨c₁, .inl hc₁, fun i hi ↦ ?_, hc₁r⟩
        simp [hc0 i hi]

Goal state after:
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
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivAt f 0 x

Tactic:
← hasFDerivWithinAt_univ,

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
h : Subsingleton E
f : E → F
x : E
⊢ HasFDerivWithinAt f 0 univ x