mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.negAddY P Q = (-(Q x * P z)) ^ 3 * W'.negY P

Tactic:
linear_combination (norm := (rw [negAddY, negY, hQz]; ring1))
    (P y - W'.negY P) * P z ^ 3 * (equation_of_Z_eq_zero hQz).mp hQ

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ n / (P z * Q z * d) * (W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (n / (P z * Q z * d)) - P x / P z ^ 2) +
      P y / P z ^ 3 =
    (n *
            (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
                Q x * P z ^ 2 * d ^ 2 -
              P x * Q z ^ 2 * d ^ 2) +
          P y * Q z ^ 3 * d ^ 3) /
        (P z * Q z) ^ 3 /
      d ^ 3

Tactic:
toAffine_addX_of_ne hPz hQz hd

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ n / (P z * Q z * d) *
        ((n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
                Q x * P z ^ 2 * d ^ 2) /
              (P z * Q z) ^ 2 /
            d ^ 2 -
          P x / P z ^ 2) +
      P y / P z ^ 3 =
    (n *
            (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
                Q x * P z ^ 2 * d ^ 2 -
              P x * Q z ^ 2 * d ^ 2) +
          P y * Q z ^ 3 * d ^ 3) /
        (P z * Q z) ^ 3 /
      d ^ 3
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup

Tactic:
rw [← generator_zpowers_eq_valueGroup]

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝¹ : Ring A
v : Valuation A Γ
inst✝ : v.IsRankOneDiscrete
⊢ IsCyclic ↥(zpowers (generator v))
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case h
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha₀ : ↑a ≠ 0
h_unit_a : IsUnit a
⊢ ↑r = ↑π.val ^ n * (↑π.val ^ n)⁻¹ * ↑r

Tactic:
mul_inv_cancel₀ (pow_ne_zero _ π.ne_zero),

Goal state after:
case h
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : r ≠ 0
π : v.Uniformizer
hr₀ : v ↑r ≠ 0
vr : Γˣ := Units.mk0 (v ↑r) hr₀
hvr_def : vr = Units.mk0 (v ↑r) hr₀
m : ℤ
hm : Units.mk0 (v ↑π.val) ⋯ ^ m = vr
hm' : v ↑π.val ^ m = v ↑r
hm₀ : 0 ≤ m
n : ℕ
hn : m = ↑n
hpow : v (↑π.val ^ (-m) * ↑r) = 1
a : ↥v.valuationSubring := ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha : a = ⟨↑π.val ^ (-m) * ↑r, ⋯⟩
ha₀ : ↑a ≠ 0
h_unit_a : IsUnit a
⊢ ↑r = 1 * ↑r
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: case neg
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
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
H : (valuation K (maximalIdeal A)) ((algebraMap A K) ↑u * (algebraMap A K) (π ^ n) / (algebraMap A K) (π ^ m * ↑w)) ≤ 1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
map_mul _ _ (w : A),

Goal state after:
case neg
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
x : K
π : A
hπ : Irreducible π
n : ℕ
u : Aˣ
ha : ¬↑u * π ^ n = 0
m : ℕ
w : Aˣ
H :
  (valuation K (maximalIdeal A))
      ((algebraMap A K) ↑u * (algebraMap A K) (π ^ n) / ((algebraMap A K) (π ^ m) * (algebraMap A K) ↑w)) ≤
    1
h_frac : (algebraMap A K) (↑u * π ^ n) / (algebraMap A K) (↑w * π ^ m) = x
hb : π ^ m ∈ nonZeroDivisors A
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
x : UniformSpace.Completion (WithVal v)
⊢ Valued.v x ≤ 1 ↔ Valued.v.restrict x ≤ 1

Tactic:
restrict_le_one_iff

Goal state after:
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
x : UniformSpace.Completion (WithVal v)
⊢ Valued.v x ≤ 1 ↔ Valued.v x ≤ 1
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
h1 : ∀ (x : UniformSpace.Completion (WithVal v)), Valued.v x ≤ 1 ↔ Valued.v.restrict x ≤ 1
x✝ : UniformSpace.Completion (WithVal v)
⊢ Valued.v ((mapEquiv h.uniformEquiv) x✝) ≤ 1 ↔ Valued.v.restrict ((mapEquiv h.uniformEquiv).toHomeomorph x✝) ≤ 1

Tactic:
restrict_le_one_iff

Goal state after:
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀'
K : Type u_7
inst✝ : Field K
v : Valuation K Γ₀
w : Valuation K Γ₀'
h : v.IsEquiv w
h1 : ∀ (x : UniformSpace.Completion (WithVal v)), Valued.v x ≤ 1 ↔ Valued.v.restrict x ≤ 1
x✝ : UniformSpace.Completion (WithVal v)
⊢ Valued.v ((mapEquiv h.uniformEquiv) x✝) ≤ 1 ↔ Valued.v ((mapEquiv h.uniformEquiv).toHomeomorph x✝) ≤ 1
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
pp: case refine_1
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ ↑((↑z).unbot ⋯) ∈ s

pp: case refine_2
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ x < (↑z).unbot ⋯

pp: case refine_3
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ (↑z).unbot ⋯ < y

Tactic:
· simp

Goal state after:
case refine_2
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ x < (↑z).unbot ⋯

case refine_3
X : Type u_1
inst✝¹ : LinearOrder X
inst✝ : LocallyFiniteOrder X
s : Set (WithBot X)
H : DenselyOrdered ↑s
x : X
hx : ↑x ∈ s
y : X
hy : ↑y ∈ s
hxy : x < y
this : ⟨↑x, hx⟩ < ⟨↑y, hy⟩
z : { x // x ∈ s }
hz : ↑x < ↑z
hz' : ↑z < ↑y
⊢ (↑z).unbot ⋯ < y
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
this : ∀ {a : G}, b = |a|ₘ ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
x✝ : G
⊢ x✝ ∈ closure {a} ↔ x✝ ∈ closure {a⁻¹}

pp: case mpr.inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
this : ∀ {a : G}, b = |a|ₘ ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ b = |a⁻¹|ₘ ∧ 1 < b

Tactic:
· simp

Goal state after:
case mpr.inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : b = |a|ₘ ∧ 1 < b
this : ∀ {a : G}, b = |a|ₘ ∧ 1 < b → 1 ≤ a → IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
ha : ¬1 ≤ a
⊢ b = |a⁻¹|ₘ ∧ 1 < b
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
⊢ extension x = 0 ↔ x = 0

Tactic:
suffices extensionValuation x = 0 ↔ x = 0 by
    simpa only [extensionValuation_toFun, map_eq_zero]
  rw [Valuation.zero_iff]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
⊢ ∃ C, IsMinimal R (C • W)

Tactic:
refine ⟨C, ⟨⟨by simp only [one_smul, hC.1], ?_⟩⟩⟩

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsDiscreteValuationRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
W : WeierstrassCurve K
C : VariableChange K
hC : MaximalFor (fun C ↦ IsIntegral R (C • W)) (fun C ↦ valuation_Δ_aux R (C • W)) C
⊢ ∀ ⦃j : VariableChange K⦄,
    (fun C_1 ↦ IsIntegral R (C_1 • C • W)) j →
      (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1 ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j →
        (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) j ≤ (fun C_1 ↦ valuation_Δ_aux R (C_1 • C • W)) 1
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst✝² : Preorder β
inst✝¹ : LE γ
inst✝ : Northcott h
H : ∀ (c : γ), BddAbove (h' ⁻¹' {x | x ≤ c})
c : γ
b : β
hb : ∀ y ∈ h' ⁻¹' {x | x ≤ c}, y ≤ b
⊢ {a | (h' ∘ h) a ≤ c} ⊆ {a | h a ≤ b}

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst✝² : LE γ
inst✝¹ : Northcott h'
inst✝ : Filter.TendstoCofinite h
c : γ
⊢ h '' {a | (h' ∘ h) a ≤ c} ⊆ {a | h' a ≤ c}

Tactic:
by grind

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff 0) φ = (coeff 0) ((mk fun p ↦ (coeff (p + 1)) φ) * X + C (constantCoeff φ))

pp: case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ (coeff (n + 1)) φ = (coeff (n + 1)) ((mk fun p ↦ (coeff (p + 1)) φ) * X + C (constantCoeff φ))

Tactic:
· simp

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ (coeff (n + 1)) φ = (coeff (n + 1)) ((mk fun p ↦ (coeff (p + 1)) φ) * X + C (constantCoeff φ))
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ (coeff (n + 1)) φ = (coeff (n + 1)) ((mk fun p ↦ (coeff (p + 1)) φ) * X + C (constantCoeff φ))

Tactic:
simp only [coeff_succ_mul_X, coeff_mk, map_add, coeff_C, n.succ_ne_zero,
      if_false, add_zero]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ (coeff 0) φ = (coeff 0) ((X * mk fun p ↦ (coeff (p + 1)) φ) + C (constantCoeff φ))

pp: case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ (coeff (n + 1)) φ = (coeff (n + 1)) ((X * mk fun p ↦ (coeff (p + 1)) φ) + C (constantCoeff φ))

Tactic:
· simp

Goal state after:
case succ
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
⊢ (coeff (n + 1)) φ = (coeff (n + 1)) ((X * mk fun p ↦ (coeff (p + 1)) φ) + C (constantCoeff φ))
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
⊢ v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)

Tactic:
by_cases hxy : x + y = 0
      · rw [intValuationDef, if_pos hxy]; exact zero_le
      · rw [v.intValuationDef_if_neg hxy, v.intValuationDef_if_neg hx, v.intValuationDef_if_neg hy,
          le_max_iff]
        simp only [exp_le_exp, neg_le_neg_iff, Nat.cast_le, ← min_le_iff]
        set nmin :=
          min ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {x})).factors)
            ((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {y})).factors)
        have h_dvd_x : x ∈ v.asIdeal ^ nmin := by
          rw [← Associates.le_singleton_iff x nmin _,
            Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hx) _]
          · exact min_le_left _ _
          exact v.associates_irreducible
        have h_dvd_y : y ∈ v.asIdeal ^ nmin := by
          rw [← Associates.le_singleton_iff y nmin _,
            Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hy) _]
          · exact min_le_right _ _
          exact v.associates_irreducible
        have h_dvd_xy : Associates.mk v.asIdeal ^ nmin ≤ Associates.mk (Ideal.span {x + y}) := by
          rw [Associates.le_singleton_iff]
          exact Ideal.add_mem (v.asIdeal ^ nmin) h_dvd_x h_dvd_y
        rw [Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hxy) _] at h_dvd_xy
        · exact h_dvd_xy
        exact v.associates_irreducible

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

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ v.intValuation 0 ≤ 1

pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ v.intValuation x ≤ 1

Tactic:
· simp

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
x : R
hx : x ≠ 0
⊢ v.intValuation x ≤ 1
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case inl
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
⊢ (coeff 1) (φ ^ 0) = ↑0 * (coeff 1) φ * constantCoeff φ ^ (0 - 1)

pp: case inr
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
φ : R⟦X⟧
hn : n > 0
⊢ (coeff 1) (φ ^ n) = ↑n * (coeff 1) φ * constantCoeff φ ^ (n - 1)

Tactic:
· simp

Goal state after:
case inr
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
φ : R⟦X⟧
hn : n > 0
⊢ (coeff 1) (φ ^ n) = ↑n * (coeff 1) φ * constantCoeff φ ^ (n - 1)
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ exp (-↑n) ≤ v.intValuation r ↔ exp (-↑(n + 1)) < v.intValuation r

Tactic:
Nat.cast_add,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
n : ℕ
⊢ exp (-↑n) ≤ v.intValuation r ↔ exp (-(↑n + ↑1)) < v.intValuation r
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| constantCoeff φ ^ n' * (coeff 1) φ + ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1) * constantCoeff φ

Tactic:
arg 2

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
φ : R⟦X⟧
n' : ℕ
ih : n' > 0 → (coeff 1) (φ ^ n') = ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1)
hn : n' + 1 > 0
h₁ : ∀ (m : ℕ), φ ^ (m + 1) = φ ^ m * φ
h₂ : antidiagonal 1 = {(0, 1), (1, 0)}
h' : 1 ≤ n'
| ↑n' * (coeff 1) φ * constantCoeff φ ^ (n' - 1) * constantCoeff φ
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
⊢ ∀ x ∈ (range n).finsuppAntidiag d, ∏ i ∈ range n, (coeff (x i)) f = 0

Tactic:
intro k hk

Goal state after:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPowerSeries σ R
m : ℕ
hf : constantCoeff f ^ m = 0
d : σ →₀ ℕ
n : ℕ
hn : m + degree d ≤ n
k : ℕ →₀ σ →₀ ℕ
hk : k ∈ (range n).finsuppAntidiag d
⊢ ∏ i ∈ range n, (coeff (k i)) f = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inl
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
⊢ ∃ a, (valuation K v) a = 0

pp: case inr
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
x : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ a, (valuation K v) a = ↑x

Tactic:
· simp

Goal state after:
case inr
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
x : (WithZero (Multiplicative ℤ))ˣ
⊢ ∃ a, (valuation K v) a = ↑x
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case inl
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
d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K 0 ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K 0 ⟨d, hd⟩ * (algebraMap R K) ↑(0, ⟨d, hd⟩).2 = (algebraMap R K) (0, ⟨d, hd⟩).1
⊢ IsLocalization.mk' K 0 ⟨d, hd⟩ ∈ (algebraMap R K).range

pp: case inr
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
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
⊢ IsLocalization.mk' K n ⟨d, hd⟩ ∈ (algebraMap R K).range

Tactic:
· simp

Goal state after:
case inr
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
n d : R
hd : d ∈ nonZeroDivisors R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K n ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K n ⟨d, hd⟩ * (algebraMap R K) ↑(n, ⟨d, hd⟩).2 = (algebraMap R K) (n, ⟨d, hd⟩).1
hn0 : n ≠ 0
⊢ IsLocalization.mk' K n ⟨d, hd⟩ ∈ (algebraMap R K).range
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
a b : (ofClass (valuation K v)).ValueGroup₀
⊢ (map' ↑(valueGroupEquiv K v)) a ≤ (map' ↑(valueGroupEquiv K v)) b ↔ a ≤ b

Tactic:
by
    match a, b with
    | 0, 0 => simp
    | 0, .coe _ => simp
    | .coe _, 0 => simp
    | .coe a, .coe b => simp [← Subtype.coe_le_coe]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hp : (weight w) x.1 = p
hq : (weight w) x.2 = q
⊢ (weight w) x.1 + (weight w) x.2 = p + q

Tactic:
hp,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : IsWeightedHomogeneous w f p
hg : IsWeightedHomogeneous w g q
d : σ →₀ ℕ
hd : ¬(weight w) d = p + q
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = d
hp : (weight w) x.1 = p
hq : (weight w) x.2 = q
⊢ p + (weight w) x.2 = p + q
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case refine_2.refine_2
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
s : Set (adicCompletion K v)
x✝ : ∃ γ, {x | (valuation K v).restrict x < ↑γ} ⊆ s
γ : (ofClass (valuation K v)).ValueGroup₀ˣ
hγ : {x | (valuation K v).restrict x < ↑γ} ⊆ s
x : adicCompletion K v
hx : x ∈ toCompletion ⁻¹' {y | Valued.v.restrict y < ↑((Units.mapEquiv (valueGroupOrderIso K v).toMulEquiv) γ)}
⊢ x ∈ {x | (valuation K v).restrict x < ↑γ}

Tactic:
· rw [Set.mem_ofPred_eq, ← map_lt_map_iff (valueGroupOrderIso K v),
          valueGroupOrderIso_restrict]
        simpa using hx

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
p q : ℕ
hf : ↑p ≤ weightedOrder w f
hg : ↑q ≤ weightedOrder w g
⊢ (weightedHomogeneousComponent w (p + q)) (f * g) =
    (weightedHomogeneousComponent w p) f * (weightedHomogeneousComponent w q) g

Tactic:
classical
  ext d
  rw [coeff_weightedHomogeneousComponent]
  split_ifs with hd
  · apply Finset.sum_congr rfl
    intro x hx
    rw [Finset.mem_antidiagonal] at hx
    rw [← hx, map_add] at hd
    simp only [coeff_weightedHomogeneousComponent]
    rcases trichotomy_of_add_eq_add hd with h | h | h
    · rw [if_pos h.1, if_pos h.2]
    · rw [if_neg (ne_of_lt h), zero_mul]
      rw [← ENat.natCast_lt_natCast] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hf), zero_mul]
    · rw [if_neg (ne_of_lt h), mul_zero]
      rw [← ENat.natCast_lt_natCast] at h
      rw [coeff_eq_zero_of_lt_weightedOrder w (lt_of_lt_of_le h hg), mul_zero]
  · symm
    apply IsWeightedHomogeneous.coeff_eq_zero _ hd
    exact IsWeightedHomogeneous.mul
      (isWeightedHomogeneous_weightedHomogeneousComponent w f p)
      (isWeightedHomogeneous_weightedHomogeneousComponent w g q)

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
⊢ IsTopologicallyNilpotent f ↔ IsNilpotent (constantCoeff f)

Tactic:
by
  refine ⟨fun H ↦ ?_, isTopologicallyNilpotent_of_constantCoeff_isNilpotent⟩
  replace H := H.map (continuous_constantCoeff R)
  simp_rw [IsTopologicallyNilpotent, nhds_discrete, tendsto_pure] at H
  exact H.exists

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

Goal state before:
pp: case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
d : σ →₀ ℕ
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
⊢ ∀ (x : ι), (coeff d) (f x) ≠ 0 → x ≤ i

Tactic:
intro k hk

Goal state after:
case inr
σ : Type u_1
R : Type u_2
inst✝³ : TopologicalSpace R
inst✝² : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
w : σ → ℕ
hempty : Nonempty ι
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < weightedOrder w (f b)
d : σ →₀ ℕ
i : ι
hi : ∀ (b : ι), i ≤ b → ↑((Finsupp.weight w) d) < weightedOrder w (f b)
k : ι
hk : (coeff d) (f k) ≠ 0
⊢ k ≤ i
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
h✝ : φ = 0
⊢ ↑n ≤ ⊤

pp: case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
h✝ : ¬φ = 0
⊢ ↑n ≤ ↑(Nat.find ⋯)

Tactic:
· simp

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ i < n, (coeff i) φ = 0
h✝ : ¬φ = 0
⊢ ↑n ≤ ↑(Nat.find ⋯)