mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * ↑m + 1) =
    (preNormEDS b c d (↑m + 2) * preNormEDS b c d ↑m ^ 3 * if Even ↑m then b else 1) -
      preNormEDS b c d (↑m - 1) * preNormEDS b c d (↑m + 1) ^ 3 * if Even ↑m then 1 else b

Tactic:
rcases m with _ | _ | _

Goal state after:
case nat.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑0 + 1) =
    (preNormEDS b c d (↑0 + 2) * preNormEDS b c d ↑0 ^ 3 * if Even ↑0 then b else 1) -
      preNormEDS b c d (↑0 - 1) * preNormEDS b c d (↑0 + 1) ^ 3 * if Even ↑0 then 1 else b

case nat.succ.zero
R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ preNormEDS b c d (2 * ↑(0 + 1) + 1) =
    (preNormEDS b c d (↑(0 + 1) + 2) * preNormEDS b c d ↑(0 + 1) ^ 3 * if Even ↑(0 + 1) then b else 1) -
      preNormEDS b c d (↑(0 + 1) - 1) * preNormEDS b c d (↑(0 + 1) + 1) ^ 3 * if Even ↑(0 + 1) then 1 else b

case nat.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
n✝ : ℕ
⊢ preNormEDS b c d (2 * ↑(n✝ + 1 + 1) + 1) =
    (preNormEDS b c d (↑(n✝ + 1 + 1) + 2) * preNormEDS b c d ↑(n✝ + 1 + 1) ^ 3 * if Even ↑(n✝ + 1 + 1) then b else 1) -
      preNormEDS b c d (↑(n✝ + 1 + 1) - 1) * preNormEDS b c d (↑(n✝ + 1 + 1) + 1) ^ 3 *
        if Even ↑(n✝ + 1 + 1) then 1 else b
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
b c d : R
⊢ normEDS b c d 3 = c

Tactic:
by
  simp [normEDS, show ¬Even (3 : ℤ) by decide]

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

Goal state before:
pp: F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : -W.a₂ ^ 3 * W.a₆ ≠ 0
⊢ -W.a₂ ^ 3 ≠ 0 ∧ W.a₆ ≠ 0

Tactic:
mul_ne_zero_iff

Goal state after:
F : Type u_2
inst✝³ : Field F
W : WeierstrassCurve F
inst✝² : W.IsElliptic
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP F 3
h : -W.a₂ ^ 3 ≠ 0 ∧ W.a₆ ≠ 0
⊢ -W.a₂ ^ 3 ≠ 0 ∧ W.a₆ ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (W.toCharThreeNF • W).IsShortNF

Tactic:
rw [toCharThreeNF, toShortNFOfCharThree_a₂, hb₂, div_zero, ← VariableChange.one_def, one_mul]

Goal state after:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (W.toShortNFOfCharThree • W).IsShortNF
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case neg
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 : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
⊢ ∃ C, C • E = E'

Tactic:
by_cases ha₆ : E.a₆ = 0

Goal state after:
case pos
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 : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
⊢ ∃ C, C • E = E'

case neg
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 : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
h : ↑(2 * n) ≠ 0
⊢ ↑n ≠ 0

Tactic:
exact right_ne_zero_of_mul <| by rwa [← Nat.cast_mul]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
⊢ (W.ΨSq ↑(n + 1)).natDegree ≤ (n + 1) ^ 2 - 1 ∧ (W.ΨSq ↑(n + 1)).coeff ((n + 1) ^ 2 - 1) = ↑(↑(n + 1) ^ 2)

Tactic:
have hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0 := by
    push_cast [← @Nat.cast_inj ℤ, add_sq, expDegree_cast n.succ_ne_zero]
    split_ifs <;> ring1

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) :=
  fun {n} ↦ natDegree_coeff_preΨ' W n
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
⊢ (W.ΨSq ↑(n + 1)).natDegree ≤ (n + 1) ^ 2 - 1 ∧ (W.ΨSq ↑(n + 1)).coeff ((n + 1) ^ 2 - 1) = ↑(↑(n + 1) ^ 2)
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 : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : u ^ 4 = E.a₄ / E'.a₄
hu6 : u ^ 6 = E.a₆ / E'.a₆
⊢ u ≠ 0

Tactic:
rw [← pow_ne_zero_iff four_ne_zero, hu4, div_ne_zero_iff]

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 : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
ha₆' : E'.a₆ ≠ 0
u : F
hu : u ^ 2 = E.a₆ / E'.a₆ / (E.a₄ / E'.a₄)
hu4 : u ^ 4 = E.a₄ / E'.a₄
hu6 : u ^ 6 = E.a₆ / E'.a₆
⊢ E.a₄ ≠ 0 ∧ E'.a₄ ≠ 0
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
⊢ W.negY P / P z ^ 3 = W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3)

Tactic:
by
  linear_combination (norm := (rw [negY, Affine.negY]; ring1))
    -W.a₁ * P x / P z ^ 2 * div_self hPz - W.a₃ * div_self (pow_ne_zero 3 hPz)

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblX P + -8 * P x * P x ^ 3 - ((P x ^ 2) ^ 2 + -8 * P x * P y ^ 2) = 0

Tactic:
dblX,

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) - W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
          2 * P x * (P y - W'.negY P) ^ 2 +
        -8 * P x * P x ^ 3 -
      ((P x ^ 2) ^ 2 + -8 * P x * P y ^ 2) =
    0
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
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.dblX P = W'.dblU P ^ 2

Tactic:
dblX,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.dblU P ^ 2 - W'.a₁ * W'.dblU P * P z * (P y - W'.negY P) - W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
      2 * P x * (P y - W'.negY P) ^ 2 =
    W'.dblU P ^ 2
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case pos.inl
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : x * y = 0
hx : x = 0
⊢ (if hx : x * y = 0 then 0 else e ^ toAdd (unzero hx)) =
    (if hx : x = 0 then 0 else e ^ toAdd (unzero hx)) * if hx : y = 0 then 0 else e ^ toAdd (unzero hx)

pp: case pos.inr
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : x * y = 0
hy : y = 0
⊢ (if hx : x * y = 0 then 0 else e ^ toAdd (unzero hx)) =
    (if hx : x = 0 then 0 else e ^ toAdd (unzero hx)) * if hx : y = 0 then 0 else e ^ toAdd (unzero hx)

Tactic:
· rw [dif_pos hxy, dif_pos hx, zero_mul]

Goal state after:
case pos.inr
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : x * y = 0
hy : y = 0
⊢ (if hx : x * y = 0 then 0 else e ^ toAdd (unzero hx)) =
    (if hx : x = 0 then 0 else e ^ toAdd (unzero hx)) * if hx : y = 0 then 0 else e ^ toAdd (unzero hx)
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
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ W.dblX P / W.dblZ P ^ 2 =
    W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Tactic:
dblX,

Goal state after:
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
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ (W.dblU P ^ 2 - W.a₁ * W.dblU P * P z * (P y - W.negY P) - W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
        2 * P x * (P y - W.negY P) ^ 2) /
      W.dblZ P ^ 2 =
    W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))
Module: Mathlib.RingTheory.Valuation.ExtendToLocalization

Goal state before:
pp: A : Type u_1
inst✝⁴ : CommRing A
Γ : Type u_2
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation A Γ
S : Submonoid A
hS : S ≤ v.supp.primeCompl
B : Type u_3
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsLocalization S B
f : S.LocalizationMap B := IsLocalization.toLocalizationMap S B
h : ∀ (s : ↥S), IsUnit (↑v.toMonoidWithZeroHom ↑s) := fun s ↦ isUnit_iff_ne_zero.mpr (hS s.property)
x y : B
⊢ ∃ a b s, f.mk' a s = x ∧ f.mk' b s = y

Tactic:
by
        obtain ⟨a, s, rfl⟩ := f.mk'_surjective x
        obtain ⟨b, t, rfl⟩ := f.mk'_surjective y
        use a * t, b * s, s * t
        constructor <;>
          · rw [f.mk'_eq_iff_eq, Submonoid.coe_mul]
            ring_nf

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
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
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ (-W.dblU P * (W.dblX P - P x * (P y - W.negY P) ^ 2) + P y * (P y - W.negY P) ^ 3) / W.dblZ P ^ 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:
dblX,

Goal state after:
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
hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3
⊢ (-W.dblU P *
          (W.dblU P ^ 2 - W.a₁ * W.dblU P * P z * (P y - W.negY P) - W.a₂ * P z ^ 2 * (P y - W.negY P) ^ 2 -
              2 * P x * (P y - W.negY P) ^ 2 -
            P x * (P y - W.negY P) ^ 2) +
        P y * (P y - W.negY P) ^ 3) /
      W.dblZ P ^ 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))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (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)),
        1] =
    toAffine W P + toAffine W Q
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ toAffine W
      (addZ P Q •
        ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
            (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
          W.toAffine.addY (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)),
          1]) =
    toAffine W P + toAffine W Q

Tactic:
toAffine_smul _ <| isUnit_addZ_of_X_ne hx

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Jacobian F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : ¬P z = 0
hQz : ¬Q z = 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
this :
  toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (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)),
        1] =
    toAffine W P + toAffine W Q
hx : ¬P x * Q z ^ 2 = Q x * P z ^ 2
⊢ toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (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)),
        1] =
    toAffine W P + toAffine W Q
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: case pos.refine_1
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
h : x * ↑v ≤ᵥ z * ↑s
⊢ y * ↑u ≤ᵥ 0

pp: case pos.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
h : y * ↑u ≤ᵥ w * ↑t
⊢ x * ↑v ≤ᵥ 0

Tactic:
· apply vle_mul_cancel (s * v).prop
        grw [veq_mul_right_comm, Submonoid.coe_mul, ← mul_assoc]
        apply (mul_vle_mul_left (mul_vle_mul_left h₂ v) u).trans
        grw [veq_mul_right_comm x]
        apply (mul_vle_mul_left (mul_vle_mul_left h t) u).trans
        apply vle_trans (mul_vle_mul_left (mul_vle_mul_left (mul_vle_mul_left hz s) t) u)
        simp

Goal state after:
case pos.refine_2
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z✝ x y z w : R
t s u v : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
h₃ : z * ↑u ≤ᵥ w * ↑v
h₄ : w * ↑v ≤ᵥ z * ↑u
hw : w ≤ᵥ 0
hz : z ≤ᵥ 0
h : y * ↑u ≤ᵥ w * ↑t
⊢ x * ↑v ≤ᵥ 0
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ IsOpen[topologicalSpace] s ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s

Tactic:
isOpen_iff_mem_nhds,

Goal state after:
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
s : Set Γ₀
⊢ (∀ x ∈ s, s ∈ 𝓝 x) ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
r : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk r s = (valuation R) r / (valuation R) ↑s

Tactic:
rw [eq_div_iff (valuation_posSubmonoid_ne_zero _)]

Goal state after:
R : Type u_2
inst✝¹ : Ring R
inst✝ : ValuativeRel R
r : R
s : ↥(posSubmonoid R)
⊢ ValueGroupWithZero.mk r s * (valuation R) ↑s = (valuation R) r
Module: Mathlib.Topology.Algebra.Valued.WithVal

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝⁶ : LinearOrderedCommGroupWithZero Γ₀
S✝ : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring S✝
inst✝³ : Algebra R S✝
v✝ : Valuation S✝ Γ₀
S : Type u_4
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
v : Valuation S Γ₀
⊢ IsLocalization M (WithVal v)

Tactic:
by
  rwa [← IsLocalization.isLocalization_iff_of_algEquiv M (algEquiv R v).symm]

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

Goal state before:
pp: Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
⊢ ¬IsField ↥v.valuationSubring

Tactic:
obtain ⟨π, hπ⟩ := exists_isUniformizer_of_isCyclic_of_nontrivial v

Goal state after:
Γ : Type u_1
inst✝³ : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝² : Field K
v : Valuation K Γ
inst✝¹ : Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup
inst✝ : IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
⊢ ¬IsField ↥v.valuationSubring
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝¹ : Field K
v : Valuation K Γ
inst✝ : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : maximalIdeal ↥v.valuationSubring = span {r}
hr₀ : r ≠ 0
⊢ v.IsUniformizer ↑r

Tactic:
obtain ⟨π, hπ⟩ := exists_isUniformizer_of_isCyclic_of_nontrivial v

Goal state after:
Γ : Type u_1
inst✝² : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst✝¹ : Field K
v : Valuation K Γ
inst✝ : v.IsRankOneDiscrete
r : ↥v.valuationSubring
hr : maximalIdeal ↥v.valuationSubring = span {r}
hr₀ : r ≠ 0
π : ↥v.valuationSubring
hπ : v.IsUniformizer ↑π
⊢ v.IsUniformizer ↑r
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
b : A
h : b ∉ (maximalIdeal A).asIdeal
⊢ ∃ x ∈ IsUnit.submonoid A, (algebraMap A K) x = (algebraMap A K) b

Tactic:
simp only [IsDiscreteValuationRing.maximalIdeal, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
      not_not] at h

Goal state after:
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
b : A
h : IsUnit b
⊢ ∃ x ∈ IsUnit.submonoid A, (algebraMap A K) x = (algebraMap A K) b
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 y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : ¬y = 0
this : y / x ∈ MonoidHom.mker (valuation K (maximalIdeal A))
⊢ ∃ u, u • x = y

Tactic:
mker_valuation_eq_isUnitSubmonoid

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 y : K
h : (valuation K (maximalIdeal A)) x = (valuation K (maximalIdeal A)) y
hx : ¬x = 0
hy : ¬y = 0
this : y / x ∈ Submonoid.map (algebraMap A K) (IsUnit.submonoid A)
⊢ ∃ u, u • x = y
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
this : closure {a} = closure {b}
⊢ b = |a|ₘ ∧ 1 < b

Tactic:
have ha : a ∈ closure ({b} : Set G) := by
      simp [← this]

Goal state after:
case mp
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a b : G
h : IsLeast {y | y ∈ closure {a} ∧ 1 < y} b
this : closure {a} = closure {b}
ha : a ∈ closure {b}
⊢ b = |a|ₘ ∧ 1 < b
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case pos.inr
G : Type u_2
inst✝³ : AddCommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedAddMonoid G
inst✝ : Nontrivial G
g : G
h : ∀ (s : Set ↑{x | 0 ≤ x}), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x < m
H : Archimedean G
hd : DenselyOrdered G
y : G
hy : y ≠ 0
this : ∀ (y : G), y ≠ 0 → 0 < y → False
hy' : y ≤ 0
⊢ False

Tactic:
refine this (-y) ?_ ?_
        · simp [hy]
        · simp [lt_of_le_of_ne hy' hy]

Goal state after:
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
⊢ ∃ r, extensionValuation x = v r

Tactic:
refine Completion.denseRange_coe.induction_on x ?_
      (fun a ↦ by simp [extensionValuation_apply_coe a])
    · simp only [extensionValuation_toFun]
      have hr (r : K) : ValueGroup₀.embedding (restrict₀ (.ofClass hv.v) r) = v r := by
        simp [embedding_restrict₀]
      have h (a b : ValueGroup₀ (.ofClass hv.v)) :
          ValueGroup₀.embedding a = ValueGroup₀.embedding b ↔ a = b := by
        rw [embedding_strictMono.injective.eq_iff]
      simp_rw [← hr, ← Valuation.restrict_def, h]
      convert! valuation_isClosedMap.isClosed_range.preimage (continuous_extension (hv := hv))
      simp_rw [eq_comm (a := extension _)]
      #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
      the new canonicalizer; a minimization would help. The original proof was: `grind` -/
      ext; simp

Goal state after: