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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), 2 < (↑n).natAbs → ↑↑n ≠ 0 → 0 < (W.preΨ ↑n).natDegree
n : ℕ
hn : 2 < (-↑n).natAbs
h : ↑(-↑n) ≠ 0
⊢ 2 < (↑n).natAbs

Tactic:
← Int.natAbs_neg

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), 2 < (↑n).natAbs → ↑↑n ≠ 0 → 0 < (W.preΨ ↑n).natDegree
n : ℕ
hn : 2 < (-↑n).natAbs
h : ↑(-↑n) ≠ 0
⊢ 2 < (-↑n).natAbs
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
h : ↑n ≠ 0
⊢ (W.preΨ n).leadingCoeff = ↑(if Even n then n / 2 else n)

Tactic:
by
  rw [leadingCoeff, W.natDegree_preΨ h, coeff_preΨ]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.ΨSq ↑n).coeff ((↑n).natAbs ^ 2 - 1) = ↑↑n ^ 2
n✝ : ℕ
⊢ (W.ΨSq ↑n✝).coeff ((↑n✝).natAbs ^ 2 - 1) = ↑(-↑n✝) ^ 2

Tactic:
← Int.cast_pow,

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.ΨSq ↑n).coeff ((↑n).natAbs ^ 2 - 1) = ↑↑n ^ 2
n✝ : ℕ
⊢ (W.ΨSq ↑n✝).coeff ((↑n✝).natAbs ^ 2 - 1) = ↑((-↑n✝) ^ 2)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : P y = 0 ∧ 2 * P y ≠ 0
⊢ False

Tactic:
hP.left,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P : Fin 3 → R
hPz : P z = 0
hPx : P x = 0
hP : 0 = 0 ∧ 2 * 0 ≠ 0
⊢ False
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: case h.e'_3
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ : Q y ^ 2 = Q x ^ 3 ∧ (3 * Q x ^ 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
⊢ P y ^ 2 / P x ^ 2 * (Q x ^ 2 / Q y ^ 2) * Q x = P x

Tactic:
hP.left,

Goal state after:
case h.e'_3
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
hPx : IsUnit (P x)
hPy : IsUnit (P y)
hQx : IsUnit (Q x)
hQy : IsUnit (Q y)
hP : P y ^ 2 = P x ^ 3 ∧ (3 * P x ^ 2 ≠ 0 ∨ 2 * P y ≠ 0 ∨ W.a₁ * P x * P y ≠ 0)
hQ : Q y ^ 2 = Q x ^ 3 ∧ (3 * Q x ^ 2 ≠ 0 ∨ 2 * Q y ≠ 0 ∨ W.a₁ * Q x * Q y ≠ 0)
⊢ P x ^ 3 / P x ^ 2 * (Q x ^ 2 / Q y ^ 2) * Q x = P x
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P) W.polynomialY = P y - W.negY P
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ 0 ≠ 0) ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0

Tactic:
ne_self_iff_false,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
hy : P y = W.negY P
hy' : (eval P) W.polynomialY = P y - W.negY P
⊢ W.Equation P ∧ ((eval P) W.polynomialX ≠ 0 ∨ False) ↔ W.Equation P ∧ (eval P) W.polynomialX ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.negAddY P (W'.neg P) = W'.dblZ P ^ 3

Tactic:
linear_combination (norm := (rw [negAddY, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1))
    -2 * P z ^ 3 * (P y - W'.negY P) * (equation_iff _).mp hP

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P : PointClass F
Q : Fin 3 → F
hP : W.NonsingularLift P
hQ : W.Nonsingular Q
hQz : Q z = 0
⊢ W.addMap P ⟦Q⟧ = P

Tactic:
revert hP
  refine P.inductionOn (motive := fun P => _ → W.addMap P _ = P) fun P hP => ?_
  by_cases hPz : P z = 0
  · rw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
      smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2, Quotient.eq]
    exact Setoid.symm <| equiv_zero_of_Z_eq_zero hP hPz
  · rw [addMap_eq, add_of_Z_eq_zero_right hQ.left hPz hQz,
      smul_eq _ ((isUnit_X_of_Z_eq_zero hQ hQz).mul <| Ne.isUnit hPz).neg]

Goal state after:
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
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ (P y / P z ^ 3 - Q y / Q z ^ 3) / ((P x * Q z ^ 2 - P z ^ 2 * Q x) / (P z ^ 2 * Q z ^ 2)) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * addZ P Q)

Tactic:
mul_comm <| _ ^ 2,

Goal state after:
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ (P y / P z ^ 3 - Q y / Q z ^ 3) / ((P x * Q z ^ 2 - Q x * P z ^ 2) / (P z ^ 2 * Q z ^ 2)) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * addZ P Q)
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑a + ↑b + ↑c = ↑a + (↑b + ↑c)

Tactic:
repeat' rw_mod_cast [add_assoc]

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

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : IsUniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α →+ β
hf✝ : Continuous ⇑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ Completion.extension (⇑f) (↑a + ↑b) = Completion.extension ⇑f ↑a + Completion.extension ⇑f ↑b

Tactic:
rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, f.map_add]

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ v x * v ↑r = v y * v ↑s →
    (restrict₀ (ofClass v)) x * (restrict₀ (ofClass v)) ↑r = (restrict₀ (ofClass v)) y * (restrict₀ (ofClass v)) ↑s

pp: case hb
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑s ≠ 0

pp: case hd
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑r ≠ 0

Tactic:
· simp only [ValueGroup₀.restrict₀_apply, dite_mul, zero_mul]
      split_ifs with h1 h2 h3 <;>
      simp_all [← WithZero.coe_mul, ← Units.val_inj] <;> simpa

Goal state after:
case hb
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑s ≠ 0

case hd
R✝ : Type u_1
inst✝⁵ : Semiring R✝
inst✝⁴ : ValuativeRel R✝
R : Type u_2
Γ : Type u_3
inst✝³ : Ring R
inst✝² : ValuativeRel R
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst✝ : v.Compatible
x y : R
r s : ↥(posSubmonoid R)
⊢ (restrict₀ (ofClass v)) ↑r ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
rw [negAddY]
  ring1

Goal state after:
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 Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
h0 : v π = 0
⊢ False

Tactic:
simp only [IsUniformizer, h0] at hπ

Goal state after:
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst✝ : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
h0 : v π = 0
hπ : 0 = ↑(IsRankOneDiscrete.generator v)
⊢ False
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case neg
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : x ∈ maximalIdeal ↥v.valuationSubring
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑x = ↑(π.val ^ n) * ↑↑u
⊢ x ∈ span {π.val}

Tactic:
← Subring.coe_mul,

Goal state after:
case neg
Γ : Type u_1
inst✝¹ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝ : Field K
v : Valuation K Γ
hv : v.IsRankOneDiscrete
π : v.Uniformizer
x : ↥v.valuationSubring
hx : x ∈ maximalIdeal ↥v.valuationSubring
hx₀ : ¬x = 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑x = ↑(π.val ^ n * ↑u)
⊢ x ∈ span {π.val}
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case pos
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := ⋯.some
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑x = ↑(π.val ^ n) * ↑↑u
hn : n = 0
⊢ Submodule.IsPrincipal P

Tactic:
← Subring.coe_mul,

Goal state after:
case pos
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := ⋯.some
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑x = ↑(π.val ^ n * ↑u)
hn : n = 0
⊢ Submodule.IsPrincipal P
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case neg
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := ⋯.some
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑x = ↑(π.val ^ n) * ↑↑u
hn : ¬n = 0
⊢ Submodule.IsPrincipal P

Tactic:
← Subring.coe_mul,

Goal state after:
case neg
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
I P : Ideal ↥v.valuationSubring
hP : P.IsPrime
h_ne_bot : ¬P = ⊥
π : v.Uniformizer := ⋯.some
x : ↥v.valuationSubring
hx_mem : x ∈ P
hx₀ : x ≠ 0
n : ℕ
u : (↥v.valuationSubring)ˣ
hu : ↑x = ↑(π.val ^ n * ↑u)
hn : ¬n = 0
⊢ Submodule.IsPrincipal P
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
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 ⋯

Tactic:
rw [← WithBot.coe_lt_coe]

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 ⋯)
Module: Mathlib.Order.Interval.Finset.DenselyOrdered

Goal state before:
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:
rw [← WithBot.coe_lt_coe]

Goal state after:
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: e : ℤ ≃+ ℤ
⊢ e = AddEquiv.refl ℤ ∨ e = AddEquiv.neg ℤ

Tactic:
suffices e 1 = 1 ∨ -e 1 = 1 by simpa [AddEquiv.ext_int_iff, neg_eq_iff_eq_neg]

Goal state after:
e : ℤ ≃+ ℤ
⊢ e 1 = 1 ∨ -e 1 = 1
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case hp
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x y : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ IsClosed {x | extension (x.1 + x.2) ≤ extension x.1 ∨ extension (x.1 + x.2) ≤ extension x.2}

Tactic:
have cont : Continuous (Valued.extension : hat K → _) := Valued.continuous_extension
      exact (isClosed_le (by fun_prop) <| cont.comp continuous_fst).union
          (isClosed_le (by fun_prop) <| cont.comp continuous_snd)

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ Nonempty (Additive G ≃+o ℤ) ↔ Nonempty (G ≃*o Multiplicative ℤ)

Tactic:
OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr

Goal state after:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : Nontrivial G
g : G
e : G ≃o Additive G := OrderIso.refl G
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2) ↔ {x | e g ≤ x}.WellFoundedOn fun x1 x2 ↦ x1 < x2
⊢ Nonempty (G ≃*o Multiplicative ℤ) ↔ Nonempty (G ≃*o Multiplicative ℤ)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h : x ≠ 0
⊢ IsClosed {b | ∃ r, embedding (extension b) = v r}

Tactic:
have hr (r : K) : ValueGroup₀.embedding (restrict₀ (.ofClass hv.v) r) = v r := by
        simp [embedding_restrict₀]

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
x : hat K
h : x ≠ 0
hr : ∀ (r : K), embedding ((restrict₀ (ofClass v)) r) = v r
⊢ IsClosed {b | ∃ r, embedding (extension b) = v r}
Module: Mathlib.RingTheory.MvPowerSeries.Basic

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

Tactic:
simpa using coeff_add_mul_monomial n 0 φ a

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hsr : Ideal.span {r} ≠ 0
hfm : FiniteMultiplicity v.asIdeal (Ideal.span {r})
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors) =
    ↑(multiplicity v.asIdeal (Ideal.span {r}))

Tactic:
← FiniteMultiplicity.emultiplicity_eq_multiplicity hfm,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
r : R
hr : r ≠ 0
hsr : Ideal.span {r} ≠ 0
hfm : FiniteMultiplicity v.asIdeal (Ideal.span {r})
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors) = emultiplicity v.asIdeal (Ideal.span {r})
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
⊢ (1 * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0

pp: case neg
σ : 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
⊢ (0 * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0

Tactic:
· exfalso
          apply hne
          rw [← hij, ← hi, Prod.mk_inj]
          refine ⟨rfl, ?_⟩
          ext t
          simp only [add_tsub_cancel_left]

Goal state after:
case neg
σ : 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
⊢ (0 * (coeff (i, j).2) fun m ↦ (coeff (m + single s n)) φ) = 0
Module: Mathlib.RingTheory.DedekindDomain.AdicValuation

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ exp (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors)) = exp (-1)

Tactic:
exp_inj

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
hv : Irreducible (Associates.mk v.asIdeal)
hlt : v.asIdeal ^ 2 < v.asIdeal
π : R
mem : π ∈ v.asIdeal
notMem : π ∉ v.asIdeal ^ 2
hπ : Associates.mk (Ideal.span {π}) ≠ 0
⊢ -↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {π})).factors) = -1
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
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
i : ℕ
hi : i ∈ s
⊢ (coeff (k i)) f = constantCoeff f

Tactic:
simp only [hs_def, mem_filter] at hi

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 : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
i : ℕ
hi : i ∈ range n ∧ k i = 0
⊢ (coeff (k i)) f = constantCoeff f
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
k : ℕ →₀ σ →₀ ℕ
hk : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
i : ℕ
hi : i ∈ s
⊢ k i = 0

Tactic:
simp only [hs_def, mem_filter] at hi

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 : (range n).sum ⇑k = d ∧ k.support ⊆ range n
s : Finset ℕ := {i ∈ range n | k i = 0}
hs_def : s = {i ∈ range n | k i = 0}
hs : s ⊆ range n
hs' : ∀ i ∈ s, (coeff (k i)) f = constantCoeff f
i : ℕ
hi : i ∈ range n ∧ k i = 0
⊢ k i = 0
Module: Mathlib.RingTheory.MvPowerSeries.Order

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
H : weightedOrder w f < ↑n
this : ↑(weightedOrder w f).toNat = weightedOrder w f
d : σ →₀ ℕ
hfd : (coeff d) f ≠ 0
hd : ↑((weight w) d) = weightedOrder w f
⊢ False

Tactic:
← hd,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
w : σ → ℕ
f : MvPowerSeries σ R
n : ℕ
h : ∀ (d : σ →₀ ℕ), (weight w) d < n → (coeff d) f = 0
this : ↑(weightedOrder w f).toNat = weightedOrder w f
d : σ →₀ ℕ
H : ↑((weight w) d) < ↑n
hfd : (coeff d) f ≠ 0
hd : ↑((weight w) d) = weightedOrder w f
⊢ False
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h : (trunc' R n) f = (trunc' R n) g
f' : MvPowerSeries σ R
⊢ (coeff n) f' = MvPolynomial.coeff n ((trunc' R n) f')

Tactic:
coeff_trunc',

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h : (trunc' R n) f = (trunc' R n) g
f' : MvPowerSeries σ R
⊢ (coeff n) f' = if n ≤ n then (coeff n) f' else 0
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
h : ∃ᶠ (m : σ →₀ ℕ) in atTop, (trunc' R m) f = (trunc' R m) g
n m : σ →₀ ℕ
hm₁ : n ≤ m
hm₂ : (trunc' R m) f = (trunc' R m) g
f' : MvPowerSeries σ R
⊢ (coeff n) f' = MvPolynomial.coeff n ((trunc' R m) f')

Tactic:
coeff_trunc',

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommSemiring R
f g : MvPowerSeries σ R
h : ∃ᶠ (m : σ →₀ ℕ) in atTop, (trunc' R m) f = (trunc' R m) g
n m : σ →₀ ℕ
hm₁ : n ≤ m
hm₂ : (trunc' R m) f = (trunc' R m) g
f' : MvPowerSeries σ R
⊢ (coeff n) f' = if n ≤ m then (coeff n) f' else 0
Module: Mathlib.RingTheory.PowerSeries.PiTopology

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
⊢ (support fun i ↦ (coeff n) (∏ i ∈ i, f i)) ⊆ ↑(Finset.Iio i).powerset

Tactic:
suffices ∀ s : Finset ι, coeff n (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i by simpa

Goal state after:
case inr
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : CommSemiring R
ι : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → R⟦X⟧
hempty : Nonempty ι
n : ℕ
h : ∀ (n : ℕ), ∃ a, ∀ (b : ι), a ≤ b → ↑n < (f b).order
i : ι
hi : ∀ (b : ι), i ≤ b → ↑n < (f b).order
⊢ ∀ (s : Finset ι), (coeff n) (∏ i ∈ s, f i) ≠ 0 → ↑s ⊆ Set.Iio i
Module: Mathlib.RingTheory.PowerSeries.Order

Goal state before:
pp: case neg.inr.inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h✝ : φ ≠ 0 ∧ ψ ≠ 0
ij : ℕ × ℕ
hij : ij ∈ antidiagonal (φ.order.toNat + ψ.order.toNat)
h : ij ≠ (φ.order.toNat, ψ.order.toNat)
h' : ij.1 < φ.order.toNat
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0

pp: case neg.inr.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h✝ : φ ≠ 0 ∧ ψ ≠ 0
ij : ℕ × ℕ
hij : ij ∈ antidiagonal (φ.order.toNat + ψ.order.toNat)
h : ij ≠ (φ.order.toNat, ψ.order.toNat)
h' : ij.2 < ψ.order.toNat
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0

Tactic:
· rw [coeff_of_lt_order_toNat ij.1 h', zero_mul]

Goal state after:
case neg.inr.inr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h✝ : φ ≠ 0 ∧ ψ ≠ 0
ij : ℕ × ℕ
hij : ij ∈ antidiagonal (φ.order.toNat + ψ.order.toNat)
h : ij ≠ (φ.order.toNat, ψ.order.toNat)
h' : ij.2 < ψ.order.toNat
⊢ (coeff ij.1) φ * (coeff ij.2) ψ = 0
Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional

Goal state before:
pp: E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ finrank ℝ E = 2 * finrank ℂ E

Tactic:
← Module.finrank_mul_finrank ℝ ℂ E,

Goal state after:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
⊢ finrank ℝ ℂ * finrank ℂ E = 2 * finrank ℂ E