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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₈ = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2

Tactic:
by
  rw [b₈, a₁_of_isCharNeTwoNF, a₃_of_isCharNeTwoNF]
  ring1

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
⊢ W.j ≠ 0

Tactic:
rw [j_of_isCharThreeJNeZeroNF_of_char_three, div_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
⊢ -W.a₂ ^ 3 ≠ 0 ∧ W.a₆ ≠ 0
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
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ^ 4 ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
pow_ne_zero_iff (Nat.succ_ne_zero _)

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
⊢ ∃ C, C • E = E'
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
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ^ 4 ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
pow_ne_zero_iff (Nat.succ_ne_zero _)

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJEqZeroNF
inst✝ : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
⊢ ∃ C, C • E = E'
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
⊢ (({ u := 1, r := (W.toShortNFOfCharThree • W).a₄ / (W.toShortNFOfCharThree • W).a₂, s := 0, t := 0 } *
        W.toShortNFOfCharThree) •
      W).IsShortNF

Tactic:
toShortNFOfCharThree_a₂,

Goal state after:
F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 3
W : WeierstrassCurve F
hb₂ : W.b₂ = 0
⊢ (({ u := 1, r := (W.toShortNFOfCharThree • W).a₄ / W.b₂, s := 0, t := 0 } * W.toShortNFOfCharThree) • W).IsShortNF
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₈ = W.a₆ + 4 * W.a₂ * W.a₆

Tactic:
by
  rw [b₈, a₁_of_isCharTwoJNeZeroNF, a₃_of_isCharTwoJNeZeroNF, a₄_of_isCharTwoJNeZeroNF]
  ring1

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

Goal state before:
pp: case even.left
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
        W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2).natDegree ≤
    max (expDegree (2 * (m + 3))) (expDegree (2 * (m + 3)))

Tactic:
(expDegree_rec m).1.1,

Goal state after:
case even.left
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
        W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2).natDegree ≤
    max (2 * expDegree (m + 2) + expDegree (m + 3) + expDegree (m + 5)) (expDegree (2 * (m + 3)))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case even.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5)).coeff (expDegree (2 * (m + 3))) -
      (W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2).coeff (expDegree (2 * (m + 3))) =
    ↑(expCoeff (2 * (m + 3)))

Tactic:
(expDegree_rec m).1.1,

Goal state after:
case even.right
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).natDegree ≤ m + n :=
  fun {m n} {p q} ↦ natDegree_mul_le_of_le
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := fun {m n} {p} ↦ natDegree_pow_le_of_le n
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n :=
  fun {m n} {p q} ↦ coeff_mul_add_eq_of_natDegree_le
cp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m :=
  fun {m n} {p} ↦ coeff_pow_of_natDegree_le
m : ℕ
h₁ : (W.preΨ' (m + 1)).natDegree ≤ expDegree (m + 1) ∧ (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) = ↑(expCoeff (m + 1))
h₂ : (W.preΨ' (m + 2)).natDegree ≤ expDegree (m + 2) ∧ (W.preΨ' (m + 2)).coeff (expDegree (m + 2)) = ↑(expCoeff (m + 2))
h₃ : (W.preΨ' (m + 3)).natDegree ≤ expDegree (m + 3) ∧ (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) = ↑(expCoeff (m + 3))
h₄ : (W.preΨ' (m + 4)).natDegree ≤ expDegree (m + 4) ∧ (W.preΨ' (m + 4)).coeff (expDegree (m + 4)) = ↑(expCoeff (m + 4))
h₅ : (W.preΨ' (m + 5)).natDegree ≤ expDegree (m + 5) ∧ (W.preΨ' (m + 5)).coeff (expDegree (m + 5)) = ↑(expCoeff (m + 5))
⊢ (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5)).coeff
        (2 * expDegree (m + 2) + expDegree (m + 3) + expDegree (m + 5)) -
      (W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2).coeff (expDegree (2 * (m + 3))) =
    ↑(expCoeff (2 * (m + 3)))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ W'.polynomialX = C W'.a₁ * Y * Z - (C 3 * X ^ 2 + C (2 * W'.a₂) * X * Z ^ 2 + C W'.a₄ * Z ^ 4)

Tactic:
rw [polynomialX, polynomial]
  pderiv_simp
  ring1

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.preΨ ↑n).natDegree ≤ ((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2
n✝ : ℕ
⊢ (W.preΨ ↑n✝).natDegree ≤ ((↑n✝).natAbs ^ 2 - if Even ↑n✝ then 4 else 1) / 2

Tactic:
ih

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

Goal state before:
pp: case neg.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = if Even ↑n then ↑(↑n / 2) else ↑n
ih : (W.preΨ (2 * ↑n)).coeff (((2 * ↑n).natAbs ^ 2 - 4) / 2) = ↑(2 * ↑n / 2)
⊢ -(W.preΨ (2 * ↑n)).coeff (((2 * ↑n).natAbs ^ 2 - 4) / 2) = -↑(2 * ↑n / 2)

Tactic:
ih

Goal state after:
case neg.inl
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = if Even ↑n then ↑(↑n / 2) else ↑n
ih : (W.preΨ (2 * ↑n)).coeff (((2 * ↑n).natAbs ^ 2 - 4) / 2) = ↑(2 * ↑n / 2)
⊢ -↑(2 * ↑n / 2) = -↑(2 * ↑n / 2)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg.inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = if Even ↑n then ↑(↑n / 2) else ↑n
ih : (W.preΨ (2 * ↑n + 1)).coeff (((2 * ↑n + 1).natAbs ^ 2 - 1) / 2) = 2 * ↑n + 1
⊢ -(W.preΨ (2 * ↑n + 1)).coeff (((2 * ↑n + 1).natAbs ^ 2 - 1) / 2) = -(2 * ↑n + 1)

Tactic:
ih

Goal state after:
case neg.inr
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
ih✝ :
  ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = if Even ↑n then ↑(↑n / 2) else ↑n
ih : (W.preΨ (2 * ↑n + 1)).coeff (((2 * ↑n + 1).natAbs ^ 2 - 1) / 2) = 2 * ↑n + 1
⊢ -(2 * ↑n + 1) = -(2 * ↑n + 1)
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).natDegree ≤ (↑n).natAbs ^ 2 - 1
n✝ : ℕ
⊢ (W.ΨSq ↑n✝).natDegree ≤ (↑n✝).natAbs ^ 2 - 1

Tactic:
ih

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:
ih

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✝ : ℕ
⊢ ↑↑n✝ ^ 2 = ↑↑n✝ ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.Φ ↑n).natDegree ≤ (↑n).natAbs ^ 2
n✝ : ℕ
⊢ (W.Φ ↑n✝).natDegree ≤ (↑n✝).natAbs ^ 2

Tactic:
ih

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.Φ ↑n).coeff ((↑n).natAbs ^ 2) = 1
n✝ : ℕ
⊢ (W.Φ ↑n✝).coeff ((↑n✝).natAbs ^ 2) = 1

Tactic:
ih

Goal state after:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.Φ ↑n).coeff ((↑n).natAbs ^ 2) = 1
n✝ : ℕ
⊢ 1 = 1
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:
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.Point

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.add P Q =
    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]

Tactic:
add_of_not_equiv <| not_equiv_of_X_ne hx,

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
⊢ W.addXYZ P Q =
    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]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
W : Jacobian 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)
⊢ W.Nonsingular (W.add P Q)

Tactic:
· classical
        have := nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy
        by_cases hx : P x * Q z ^ 2 = Q x * P z ^ 2
        · simpa only [add_of_Y_ne' hP.left hQ.left hPz hQz hx <| not_and.mp hxy hx,
            nonsingular_smul _ <| isUnit_dblZ_of_Y_ne' hP.left hQ.left hPz hx <| not_and.mp hxy hx]
        · simpa only [add_of_X_ne hP.left hQ.left hPz hQz hx,
            nonsingular_smul _ <| isUnit_addZ_of_X_ne hx]

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

Goal state before:
pp: case mk.mk
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : PointClass F
a✝¹ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹)
a✝ : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift
    (W.addMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹) (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝))

Tactic:
exact nonsingular_add hP hQ

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

Goal state before:
pp: α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ ContinuousAt Inv.inv γ

Tactic:
rw [ContinuousAt, nhds_of_ne_zero h]

Goal state after:
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto Inv.inv (pure γ) (𝓝 γ⁻¹)
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 x : R
y : ↥(posSubmonoid R)
⊢ ⊥ ≤ ValueGroupWithZero.mk x y

Tactic:
rw [ValueGroupWithZero.bot_eq_zero, ← ValueGroupWithZero.mk_zero 1, ValueGroupWithZero.mk_le_mk]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x : R
y : ↥(posSubmonoid R)
⊢ 0 * ↑y ≤ᵥ x * ↑1
Module: Mathlib.Topology.Algebra.Valued.ValuationTopology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ IsClosed[_i.toTopologicalSpace] ↑v.integer

Tactic:
simp only [integer, Subring.coe_set_mk, Subsemiring.coe_set_mk, Submonoid.coe_set_mk,
    Subsemigroup.coe_set_mk, ← v.restrict_le_one_iff]
  exact isClosed_closedBall _ _

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 α
n : ℕ
a✝ : Completion α
a : α
⊢ ↑((n + 1) • a) = n • ↑a + ↑a

Tactic:
succ_nsmul,

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : IsUniformAddGroup α
n : ℕ
a✝ : Completion α
a : α
⊢ ↑(n • a + a) = n • ↑a + ↑a
Module: Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
inst✝³ : ValuativeRel R
Γ₀ : Type u_3
inst✝² : LinearOrderedCommGroupWithZero Γ₀
_t : TopologicalSpace R
inst✝¹ : IsValuativeTopology R
v : Valuation R Γ₀
inst✝ : v.Compatible
⊢ IsOpen[_t] {x | v.restrict x ≤ 1}

Tactic:
apply isOpen_closedBall one_ne_zero

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
⊢ -0 - W'.a₁ * 0 * addZ P P - W'.a₃ * addZ P P ^ 3 = 0

Tactic:
addZ_self

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -0 - W'.a₁ * 0 * 0 - W'.a₃ * 0 ^ 3 = 0
Module: Mathlib.RingTheory.Valuation.Discrete.Basic

Goal state before:
pp: case hH.ofNat
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n = n✝
⊢ ∃ a,
    ¬(MonoidWithZeroHom.ofClass v) a = 0 ∧
      ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑(Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n) = (MonoidWithZeroHom.ofClass v) x

Tactic:
refine ⟨1, ?_, π ^ n, ?_⟩

Goal state after:
case hH.ofNat.refine_1
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n = n✝
⊢ ¬(MonoidWithZeroHom.ofClass v) 1 = 0

case hH.ofNat.refine_2
A : Type u_2
inst✝ : Ring A
v : Valuation A (WithZero (Multiplicative ℤ))
hv : v.IsRankOneDiscrete
n✝ : (WithZero (Multiplicative ℤ))ˣ
hπ✝ : (exp 1)⁻¹ ∈ range ⇑v
x✝ : ∃ k, Units.mk0 (exp 1)⁻¹ ⋯ ^ k = n✝
π : A
hπ : v π = (exp 1)⁻¹
n : ℕ
h : Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n = n✝
⊢ (MonoidWithZeroHom.ofClass v) 1 * ↑(Units.mk0 (exp 1)⁻¹ ⋯ ^ Int.ofNat n) = (MonoidWithZeroHom.ofClass v) (π ^ n)
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 π
⊢ 0 < v π

Tactic:
rw [IsUniformizer.iff] at hπ; simp [zero_lt_iff, ne_eq, hπ]

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
⊢ ![0, 0, addZ P P] = ![0, 0, 0]

Tactic:
addZ_self

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ ![0, 0, 0] = ![0, 0, 0]
Module: Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Goal state before:
pp: 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
H : (valuation K (maximalIdeal A)) x ≤ 1
⊢ ∃ a, (algebraMap A K) a = x

Tactic:
obtain ⟨π, hπ⟩ := exists_irreducible A

Goal state after:
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
H : (valuation K (maximalIdeal A)) x ≤ 1
π : A
hπ : Irreducible π
⊢ ∃ a, (algebraMap A K) a = x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mp
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ Function.Injective fun x ↦ a ^ x

Tactic:
rcases ha.lt_or_gt with ha | ha

Goal state after:
case mp.inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha✝ : a ≠ 1
ha : a < 1
⊢ Function.Injective fun x ↦ a ^ x

case mp.inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha✝ : a ≠ 1
ha : 1 < a
⊢ Function.Injective fun x ↦ a ^ x
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : 1 < b ^ k
⊢ b ^ 1 ≤ (b ^ 1) ^ k

Tactic:
← zpow_mul,

Goal state after:
case refine_2
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
b : G
h : 1 < b
ha : 1 ≤ b
k : ℤ
hk : 1 < b ^ k
⊢ b ^ 1 ≤ b ^ (1 * k)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
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
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ Units.mk0 (v xy) ⋯ = Units.mk0 (v x) ⋯ * Units.mk0 (v y) ⋯

Tactic:
rw [← Units.mk0_mul]

Goal state after:
case neg
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
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ Units.mk0 (v xy) ⋯ = Units.mk0 (v x * v y) ?neg.hxy✝

case neg.hxy
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
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ v x * v y ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.Basic

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
m : ℕ
inst✝ : NeZero m
n : σ →₀ ℕ
a : R
i : σ
H : n + single i m = 0
⊢ False

Tactic:
simpa [NeZero.ne] using congr($(H) i)

Goal state after: