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

Goal state before:
pp: case of_j_eq_zero
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝³ : E.IsElliptic
inst✝² : E'.IsElliptic
inst✝¹ : CharP F 3
heq : E.j = E'.j
C : VariableChange F
inst✝ : (C • E).IsShortNF
⊢ ∃ C, C • E = E'

Tactic:
obtain ⟨C', _ | _⟩ := E'.exists_variableChange_isCharThreeNF
    · have h := (C' • E').j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three
      rw [variableChange_j, ← heq, ← variableChange_j E C, j_of_isShortNF_of_char_three] at h
      exact False.elim (h rfl)
    · obtain ⟨C'', hC⟩ := exists_variableChange_of_char_three_of_j_eq_zero (C • E) (C' • E')
      use C'⁻¹ * C'' * C
      rw [mul_smul, mul_smul, hC, ← mul_smul, inv_mul_cancel, one_smul]

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

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝⁴ : NeZero 2
this✝³ : NeZero 4
this✝² : NeZero 6
this✝¹ : Invertible 2 := invertibleOfNonzero hchar2
this✝ : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq :
  (-48 * E.a₄) ^ 3 * (-16 * (4 * E'.a₄ ^ 3 + 27 * E'.a₆ ^ 2)) =
    (-48 * E'.a₄) ^ 3 * (-16 * (4 * E.a₄ ^ 3 + 27 * E.a₆ ^ 2))
this : Invertible 47775744 := invertibleOfNonzero ⋯
⊢ E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2

Tactic:
← mul_right_inj_of_invertible (47775744 : F)

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝⁴ : NeZero 2
this✝³ : NeZero 4
this✝² : NeZero 6
this✝¹ : Invertible 2 := invertibleOfNonzero hchar2
this✝ : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq :
  (-48 * E.a₄) ^ 3 * (-16 * (4 * E'.a₄ ^ 3 + 27 * E'.a₆ ^ 2)) =
    (-48 * E'.a₄) ^ 3 * (-16 * (4 * E.a₄ ^ 3 + 27 * E.a₆ ^ 2))
this : Invertible 47775744 := invertibleOfNonzero ⋯
⊢ 47775744 * (E.a₄ ^ 3 * E'.a₆ ^ 2) = 47775744 * (E'.a₄ ^ 3 * E.a₆ ^ 2)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 ≠ W'.negY Q * P z ^ 3
⊢ P y ≠ W'.negY P

Tactic:
by
  have hy' : P y * Q z ^ 3 - Q y * P z ^ 3 = 0 :=
    (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_right <| sub_ne_zero_of_ne hy
  contrapose hy
  linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z ^ 3 * hy - hy'

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * P x ^ 2 * P z ^ 2 - 2 * P y * W'.neg P y * P z * W'.neg P z + P x ^ 2 * P x * W'.neg P z ^ 2 -
                        W'.a₁ * P x * W'.neg P y * P z ^ 2 * W'.neg P z -
                      W'.a₁ * P y * P x * P z * W'.neg P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * W'.neg P z ^ 2 -
                  W'.a₃ * W'.neg P y * P z ^ 4 * W'.neg P z -
                W'.a₃ * P y * P z * W'.neg P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * W'.neg P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * W'.neg P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * W'.neg P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      (W'.dblZ P ^ 2 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0

Tactic:
neg_Y,

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * P x ^ 2 * P z ^ 2 - 2 * P y * W'.negY P * P z * W'.neg P z + P x ^ 2 * P x * W'.neg P z ^ 2 -
                        W'.a₁ * P x * W'.negY P * P z ^ 2 * W'.neg P z -
                      W'.a₁ * P y * P x * P z * W'.neg P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * W'.neg P z ^ 2 -
                  W'.a₃ * W'.negY P * P z ^ 4 * W'.neg P z -
                W'.a₃ * P y * P z * W'.neg P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * W'.neg P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * W'.neg P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * W'.neg P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      (W'.dblZ P ^ 2 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
exact ⟨hu.unit ^ 4, by convert! (add_smul_of_equiv h hu hv).symm⟩

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addX P P = 0

Tactic:
linear_combination (norm := (rw [addX]; ring1)) -2 * P z ^ 2 * (equation_iff _).mp hP

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
a b : Γ₀
hab : b < a
⊢ {a | a.2 < a.1} ∈ map (Prod.mk a) (𝓝 b)

Tactic:
exact Iio_mem_nhds hab

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : a₁ * ↑b₂ ≤ᵥ b₁ * ↑a₂
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : b₁ * ↑c₂ ≤ᵥ c₁ * ↑b₂
⊢ a₁ * ↑c₂ * ↑b₂ =ᵥ a₁ * ↑b₂ * ↑c₂

Tactic:
grw [veq_mul_right_comm]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : a₁ * ↑b₂ ≤ᵥ b₁ * ↑a₂
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : b₁ * ↑c₂ ≤ᵥ c₁ * ↑b₂
⊢ b₁ * ↑a₂ * ↑c₂ =ᵥ b₁ * ↑c₂ * ↑a₂

Tactic:
grw [veq_mul_right_comm]

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x x' y y' z a₁ : R
a₂ : ↥(posSubmonoid R)
b₁ : R
b₂ : ↥(posSubmonoid R)
hab : a₁ * ↑b₂ ≤ᵥ b₁ * ↑a₂
c₁ : R
c₂ : ↥(posSubmonoid R)
hbc : b₁ * ↑c₂ ≤ᵥ c₁ * ↑b₂
⊢ c₁ * ↑b₂ * ↑a₂ =ᵥ c₁ * ↑a₂ * ↑b₂

Tactic:
grw [veq_mul_right_comm]

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

Goal state before:
pp: case mpr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h : ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
γ : (ofClass v).ValueGroup₀ˣ
⊢ ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))

Tactic:
simp_rw [restrict_lt_iff_lt_embedding] at h

Goal state after:
case mpr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
γ : (ofClass v).ValueGroup₀ˣ
h : ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v (y - x) < embedding ↑γ
⊢ ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
h : ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v.restrict (y - x) < ↑γ
γ : (ofClass v).ValueGroup₀ˣ
⊢ ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))

Tactic:
simp_rw [restrict_lt_iff_lt_embedding] at h

Goal state after:
case mpr
R : Type u_1
inst✝⁵ : Ring R
inst✝⁴ : ValuativeRel R
Γ₀ : Type u_3
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
_u : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
F : Filter R
γ : (ofClass v).ValueGroup₀ˣ
h : ∀ (γ : (ofClass v).ValueGroup₀ˣ), ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, v (y - x) < embedding ↑γ
⊢ ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ ↑(v.ltAddSubgroup ((Units.map ↑embedding) γ))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x : R
⊢ (embed v) ((valuation R) x) = (restrict₀ (ofClass v)) x

Tactic:
convert! embed_mk v x 1

Goal state after:
case e'_3
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x : R
⊢ (restrict₀ (ofClass v)) x = (restrict₀ (ofClass v)) x / (restrict₀ (ofClass v)) ↑1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ W.negAddY P Q / addZ P Q ^ 3 =
    W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Tactic:
rw [negAddY_eq hPz hQz, addX_eq' hP hQ, toAffine_slope_of_ne hPz hQz hx,
    toAffine_negAddY_of_ne hPz hQz <| addZ_ne_zero_of_X_ne hx]

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

Goal state before:
pp: case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y✝ : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y✝
y₀ : (ofClass Valued.v).ValueGroup₀ := ⋯
hy₀_def : y₀ = h_val.orderMonoidIso ↑x
hy₀_ne_zero : y₀ ≠ 0
y : (ofClass Valued.v).ValueGroup₀ˣ := ⋯
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
⊢ ∀ (x_1 : R), Valued.v.restrict x_1 < ↑y → Valued.v.restrict x_1 < ↑x

Tactic:
intro b

Goal state after:
case h
R : Type u_4
Γ₀ : Type u_5
Γ₀' : Type u_6
inst✝² : Ring R
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ₀'
v : Valuation R Γ₀
w : Valuation R Γ₀'
h : v.IsEquiv w
h_val : Valued.v.IsEquiv Valued.v
h_res : v.restrict.IsEquiv w.restrict
x : (ofClass Valued.v).ValueGroup₀ˣ
u : ↥(ofClass Valued.v).valueGroup := WithZero.unzero ⋯
a : R
ha : (ofClass Valued.v) a ≠ 0
y✝ : R
hu : (ofClass Valued.v) a * ↑↑u = (ofClass Valued.v) y✝
y₀ : (ofClass Valued.v).ValueGroup₀ := h_val.orderMonoidIso ↑x
hy₀_def : y₀ = h_val.orderMonoidIso ↑x
hy₀_ne_zero : y₀ ≠ 0
y : (ofClass Valued.v).ValueGroup₀ˣ := Units.mk0 y₀ hy₀_ne_zero
hy_def : y = Units.mk0 y₀ hy₀_ne_zero
b : R
⊢ Valued.v.restrict b < ↑y → Valued.v.restrict b < ↑x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h✝ : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
a✝² : G₀
a✝¹ : g ≤ a✝²
ha0 : ¬a✝² = 0
b✝ : G₀
a✝ : g ≤ b✝
hb0 : ¬b✝ = 0
h : a✝² < b✝
⊢ (if h : a✝² = 0 then 1 else Units.mk0 a✝² h) < if h : b✝ = 0 then 1 else Units.mk0 b✝ h

Tactic:
simp [ha0, hb0, ← Units.val_lt_val, h]

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1.inl
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
⊢ 0 ∈ {x | g⁻¹ ≤ x} → (fun x ↦ x⁻¹) 0 ∈ {x | x ≤ g} \ {0}

pp: case refine_1.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
x : G₀
hx : x ≠ 0
⊢ x ∈ {x | g⁻¹ ≤ x} → (fun x ↦ x⁻¹) x ∈ {x | x ≤ g} \ {0}

Tactic:
· simp [hg]

Goal state after:
case refine_1.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
hg' : g⁻¹ ≠ 0
h : ({x | x ≤ g} \ {0}).WellFoundedOn fun x1 x2 ↦ x1 > x2
x : G₀
hx : x ≠ 0
⊢ x ∈ {x | g⁻¹ ≤ x} → (fun x ↦ x⁻¹) x ∈ {x | x ≤ g} \ {0}
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 Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
⊢ extensionValuation.restrict ↑xy = extensionValuation.restrict ↑x * extensionValuation.restrict ↑y

Tactic:
simp only [Valuation.restrict_def, restrict₀_apply, coe_ofClass, extensionValuation_apply_coe,
      map_eq_zero, mul_dite, mul_zero, dite_mul, zero_mul]

Goal state after:
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
xy : K := ⋯.choose
hxy_def : xy = ⋯.choose
hxy : v xy = embedding a * embedding b
hx : v x = embedding a
hy : v y = embedding b
⊢ (if h : extensionValuation ↑xy = 0 then 0 else ↑⟨Units.mk0 (v xy) ⋯, ⋯⟩) =
    if h : extensionValuation ↑y = 0 then 0
    else if h : extensionValuation ↑x = 0 then 0 else ↑⟨Units.mk0 (v x) ⋯, ⋯⟩ * ↑⟨Units.mk0 (v y) ⋯, ⋯⟩
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m n : ℕ
⊢ (coeff m) (X ^ n) = if m = n then 1 else 0

Tactic:
rw [X_pow_eq, coeff_monomial]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ (coeff n) ((φ₁ + φ₂) * φ₃) = (coeff n) (φ₁ * φ₃ + φ₂ * φ₃)

Tactic:
simp only [coeff_mul, add_mul, Finset.sum_add_distrib, map_add]

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

Goal state before:
pp: case e'_2.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, (coeff m) φ = 0
m : Unit →₀ ℕ
⊢ m () < n → (MvPowerSeries.coeff m) φ = 0

Tactic:
hm

Goal state after:
case e'_2.mp
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ m < n, (coeff m) φ = 0
m : Unit →₀ ℕ
hm : m () < n
⊢ (MvPowerSeries.coeff m) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case e'_2.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0
m : ℕ
⊢ m < n → (coeff m) φ = 0

Tactic:
hm

Goal state after:
case e'_2.mpr
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ : R⟦X⟧
h : ∀ (m : Unit →₀ ℕ), m () < n → (MvPowerSeries.coeff m) φ = 0
m : ℕ
hm : m < n
⊢ (coeff m) φ = 0
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 : ℕ
⊢ m < 1 → (coeff m) φ = 0

Tactic:
hm

Goal state after:
case mpr
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
h : (coeff 0) φ = 0
m : ℕ
hm : m < 1
⊢ (coeff m) φ = 0
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
n✝ : ℕ
⊢ ∀ (a_1 b : ℕ), a_1 + b = n✝ → a ^ n✝ * ((coeff a_1) f * (coeff b) g) = a ^ a_1 * (coeff a_1) f * (a ^ b * (coeff b) g)

Tactic:
intro b

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a : R
f g : R⟦X⟧
n✝ b : ℕ
⊢ ∀ (b_1 : ℕ), b + b_1 = n✝ → a ^ n✝ * ((coeff b) f * (coeff b_1) g) = a ^ b * (coeff b) f * (a ^ b_1 * (coeff b_1) g)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ False

Tactic:
apply hne

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
n : ℕ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < n → (coeff m) φ = 0
m : σ →₀ ℕ
H : m - single s n + single s n = m
i j : σ →₀ ℕ
hij : (i, j).1 + (i, j).2 = m
hne : (i, j) ≠ (single s n, m - single s n)
hi : (i, j).1 = single s n
⊢ (i, j) = (single s n, m - single s n)
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0
m : σ →₀ ℕ
⊢ m s = 0 → (coeff m) φ = 0

Tactic:
hm

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s < 1 → (coeff m) φ = 0
m : σ →₀ ℕ
hm : m s = 0
⊢ (coeff m) φ = 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0
m : σ →₀ ℕ
⊢ m s < 1 → (coeff m) φ = 0

Tactic:
hm

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
s : σ
φ : MvPowerSeries σ R
h : ∀ (m : σ →₀ ℕ), m s = 0 → (coeff m) φ = 0
m : σ →₀ ℕ
hm : m s < 1
⊢ (coeff m) φ = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case h
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
hd0 : d ≠ 0
z : R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K (d * z) ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K (d * z) ⟨d, hd⟩ * (algebraMap R K) ↑(d * z, ⟨d, hd⟩).2 = (algebraMap R K) (d * z, ⟨d, hd⟩).1
hn0 : d * z ≠ 0
this : Ideal.span {d} ∣ Ideal.span {d * z}
⊢ (algebraMap R K) z = IsLocalization.mk' K (d * z) ⟨d, hd⟩

Tactic:
rw [map_mul, mul_comm, mul_eq_mul_left_iff] at hx

Goal state after:
case h
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
hd0 : d ≠ 0
z : R
h : ∀ (v : HeightOneSpectrum R), (valuation K v) (IsLocalization.mk' K (d * z) ⟨d, hd⟩) ≤ 1
hx : IsLocalization.mk' K (d * z) ⟨d, hd⟩ = (algebraMap R K) z ∨ (algebraMap R K) ↑(d * z, ⟨d, hd⟩).2 = 0
hn0 : d * z ≠ 0
this : Ideal.span {d} ∣ Ideal.span {d * z}
⊢ (algebraMap R K) z = IsLocalization.mk' K (d * z) ⟨d, hd⟩
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: case monomial
R : Type u_1
inst✝ : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ ↑((MvPolynomial.monomial d) r) = ↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1}) ((MvPolynomial.monomial d) r))

Tactic:
have : single () (d ()) = d := by ext; simp

Goal state after:
case monomial
R : Type u_1
inst✝ : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
this : single () (d ()) = d
⊢ ↑((MvPolynomial.monomial d) r) = ↑((MvPolynomial.uniqueAlgEquiv R PUnit.{1}) ((MvPolynomial.monomial d) r))
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
a s : R
hs : s ∈ v.asIdeal.primeCompl
this : (valuation K v) (↑a / ↑s) ≤ 1
⊢ (algebraMap R K) a * ((algebraMap R K) s)⁻¹ ∈ (valuation K v).valuationSubring

Tactic:
division_def (a : K) s

Goal state after:
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 s : R
hs : s ∈ v.asIdeal.primeCompl
this : (valuation K v) (↑a * (↑s)⁻¹) ≤ 1
⊢ (algebraMap R K) a * ((algebraMap R K) s)⁻¹ ∈ (valuation K v).valuationSubring
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
⊢ ∀ (d_1 : σ →₀ ℕ), (weight w) d_1 < (weight w) d → (coeff d_1) ((monomial d) a) = 0

Tactic:
intro b

Goal state after:
case neg.right
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
w : σ → ℕ
d : σ →₀ ℕ
a : R
inst✝ : Decidable (a = 0)
h : ¬a = 0
b : σ →₀ ℕ
⊢ (weight w) b < (weight w) d → (coeff b) ((monomial d) a) = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: case right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
⊢ ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) (f + g) = 0

Tactic:
intro b

Goal state after:
case right
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f g : MvPowerSeries σ R
H : weightedOrder w f < weightedOrder w g
n : ℕ
hn : ↑n = weightedOrder w f
d : σ →₀ ℕ
hd' : (coeff d) f ≠ 0
hd : (weight w) d = n
b : σ →₀ ℕ
⊢ (weight w) b < n → (coeff b) (f + g) = 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
n : (WithZero (Multiplicative ℤ))ˣ
x✝ : ∃ a, ¬Valued.v a = 0 ∧ ∃ x, Valued.v a * ↑n = Valued.v x
a : adicCompletion K v
ha0 : ¬Valued.v a = 0
x : adicCompletion K v
hx : Valued.v a * ↑n = Valued.v x
b : K
hb : (valuation K v) b = Valued.v a
y : K
hy : (valuation K v) y = Valued.v x
⊢ ∃ a, ¬(valuation K v) a = 0 ∧ ∃ x, (valuation K v) a * ↑n = (valuation K v) x

Tactic:
exact ⟨b, by rw [hb]; exact ha0, y, by rw [hb, hy]; exact hx⟩

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∃ a, HasSum f a) ↔ ∀ (d : σ →₀ ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a

Tactic:
hasSum_iff_hasSum_coeff

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
ι : Type u_3
f : ι → MvPowerSeries σ R
⊢ (∃ a, ∀ (d : σ →₀ ℕ), HasSum (fun i ↦ (coeff d) (f i)) ((coeff d) a)) ↔
    ∀ (d : σ →₀ ℕ), ∃ a, HasSum (fun i ↦ (coeff d) (f i)) a
Module: Mathlib.RingTheory.PowerSeries.Order

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

Tactic:
convert! nat_le_order φ n _

Goal state after:
case coe
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
n : ℕ
h : ∀ (i : ℕ), ↑i < ↑n → (coeff i) φ = 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 x✝¹ x✝ : K
⊢ ↑(v.adicAbvDef hb (x✝¹ * x✝)) = ↑(v.adicAbvDef hb x✝¹) * ↑(v.adicAbvDef hb x✝)

Tactic:
simp [adicAbvDef]

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
b : ℝ≥0
hb : 1 < b
r : R
x x✝ : K
⊢ ↑(v.adicAbvDef hb x✝) = 0 ↔ x✝ = 0

Tactic:
simp [adicAbvDef]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ (monomial n) r = C r * X ^ n

Tactic:
ext; simp [coeff_X_pow, coeff_monomial]

Goal state after: