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

Goal state before:
pp: case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C 1) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) +
        -4 * C (C (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆)) -
      (C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 1 +
              C (C (1 * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
            C
              ((C (1 * 4) * X ^ 2 + C (1 * 4 * x₁ + 1 * (W.a₁ ^ 2 + 4 * W.a₂)) * X +
                  C (1 * 4 * x₁ ^ 2 + 1 * (W.a₁ ^ 2 + 4 * W.a₂) * x₁ + 1 * 2 * (2 * W.a₄ + W.a₁ * W.a₃))) *
                (X - C x₁)) +
          C (C ((y₁ - W.negY x₁ y₁) ^ 2)) * 0 * C (X - C x₁) +
        -4 * C (C (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁))) =
    0

Tactic:
negY

Goal state after:
case a
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := (y₁ - W.negY x₁ y₁) ^ 2
hxy : (y₁ - W.negY x₁ y₁) ^ 2 ≠ 0
⊢ C (C 1) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) * (Y - (-Y - C (C W.a₁ * X + C W.a₃))) +
        -4 * C (C (x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆)) -
      (C (C ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2)) * 1 +
              C (C (1 * 4)) * (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) +
            C
              ((C (1 * 4) * X ^ 2 + C (1 * 4 * x₁ + 1 * (W.a₁ ^ 2 + 4 * W.a₂)) * X +
                  C (1 * 4 * x₁ ^ 2 + 1 * (W.a₁ ^ 2 + 4 * W.a₂) * x₁ + 1 * 2 * (2 * W.a₄ + W.a₁ * W.a₃))) *
                (X - C x₁)) +
          C (C ((y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) ^ 2)) * 0 * C (X - C x₁) +
        -4 * C (C (y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁))) =
    0
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case nat.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n✝ : ℕ
⊢ complEDS b c d k ↑(2 * (n✝ + 1) + 1) =
    complEDS b c d k ↑(n✝ + 1) ^ 2 * normEDS b c d (↑(n✝ + 1 + 1) * k + 1) * normEDS b c d (↑(n✝ + 1 + 1) * k - 1) -
      complEDS b c d k ↑(n✝ + 1 + 1) ^ 2 * normEDS b c d (↑(n✝ + 1) * k + 1) * normEDS b c d (↑(n✝ + 1) * k - 1)

Tactic:
simpa only [complEDS_ofNat] using! complEDS'_odd ..

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : WeierstrassCurve R
ij : Fin 3 × Fin 3
⊢ (W.addSubMapCoeff ij).IsHomogeneous 2

Tactic:
simp only [addSubMapCoeff]
  fin_cases ij <;>
    simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue, Function.uncurry_apply_pair,
      Matrix.cons_val', Matrix.cons_val_zero, Matrix.cons_val_fin_one, neg_mul, Fin.mk_one,
      Matrix.cons_val_one, Fin.reduceFinMk, Matrix.cons_val, Fin.zero_eta]
    -- The following works, but is slow (44894 vs. 11717 heartbeats):
    -- <;> repeat first | refine .add ?_ CXY | refine .add ?_ CXX | exact CXX | exact CXY
  · exact CXX.add CXY |>.add CXY |>.add CXX |>.add CXY
  · exact CXX.add CXY |>.add CXY |>.add CXX |>.add CXY
  · exact CXX.add CXY |>.add CXY
  · exact CXY.add CXX |>.add CXY
  · exact CXX.add CXY |>.add CXX |>.add CXY
  · exact CXX.add CXY |>.add CXY |>.add CXX |>.add CXY
  · exact CXX.add CXY |>.add CXX
  · exact CXY.add CXY |>.add CXY |>.add CXX
  · exact CXY.add CXY |>.add CXX

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case two
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
⊢ f (preNormEDS' b c d 2) = preNormEDS' (f b) (f c) (f d) 2

Tactic:
| two =>

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

Goal state before:
pp: R : Type r
F : Type u
K : Type v
L : Type w
inst✝¹³ : CommRing R
inst✝¹² : Field F
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
W' : Affine R
inst✝⁹ : DecidableEq F
inst✝⁸ : DecidableEq K
inst✝⁷ : DecidableEq L
inst✝⁶ : Algebra R F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : Algebra F K
inst✝² : IsScalarTower R F K
inst✝¹ : Algebra F L
inst✝ : IsScalarTower R F L
f : K →ₐ[F] L
P : (W'⁄F).Point
⊢ (map f) ((baseChange F K) P) = (baseChange F L) P

Tactic:
by
  have : Subsingleton (F →ₐ[F] L) := inferInstance
  convert! map_map (Algebra.ofId F K) f P

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Ψ₃.coeff 4 = 3

Tactic:
rw [Ψ₃]
  compute_degree!

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

Goal state before:
pp: case two
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
⊢ (W.preΨ' 2).natDegree ≤ expDegree 2 ∧ (W.preΨ' 2).coeff (expDegree 2) = ↑(expCoeff 2)

Tactic:
| two =>

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

Goal state before:
pp: F : Type u_2
inst✝¹ : Field F
inst✝ : CharP F 2
W : WeierstrassCurve F
ha₁ : W.a₁ ≠ 0
⊢ (W.toCharTwoJNeZeroNF ha₁ • W).IsCharTwoJNeZeroNF

Tactic:
by
  constructor
  · simp [toCharTwoJNeZeroNF, ha₁, variableChange_a₁]
  · simp [field, toCharTwoJNeZeroNF, variableChange_a₃, -mul_eq_zero]
    linear_combination (W.a₃ * W.a₁ ^ 3 + W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) * CharP.cast_eq_zero F 2
  · simp [field, toCharTwoJNeZeroNF, variableChange_a₄, -mul_eq_zero]
    linear_combination (W.a₃ ^ 2 + W.a₁ * W.a₃ * W.a₂) * CharP.cast_eq_zero F 2

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
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, P y, P z]

Tactic:
hPz

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z = 0
hQz : Q z = 0
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, P y, 0]
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian 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
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) +
        (Q z ^ 6 * 0 +
            P z ^ 6 *
              (Q y ^ 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 3 -
                (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z ^ 2 + W'.a₄ * Q x * Q z ^ 4 + W'.a₆ * Q z ^ 6)) +
          (P x ^ 2 * Q z ^ 4 + P x * Q x * P z ^ 2 * Q z ^ 2 + Q x ^ 2 * P z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4 +
                  W'.a₂ * P x * P z ^ 2 * Q z ^ 4 +
                W'.a₂ * Q x * P z ^ 4 * Q z ^ 2 +
              W'.a₄ * P z ^ 4 * Q z ^ 4) *
            (Q x * P z ^ 2)) -
      (0 +
        (Q z ^ 6 *
              (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)) +
            P z ^ 6 * 0 +
          (P x ^ 2 * Q z ^ 4 + P x * Q x * P z ^ 2 * Q z ^ 2 + Q x ^ 2 * P z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4 +
                  W'.a₂ * P x * P z ^ 2 * Q z ^ 4 +
                W'.a₂ * Q x * P z ^ 4 * Q z ^ 2 +
              W'.a₄ * P z ^ 4 * Q z ^ 4) *
            (P x * Q z ^ 2))) =
    0

Tactic:
negY

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian 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
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) * P z ^ 3) +
        (Q z ^ 6 * 0 +
            P z ^ 6 *
              (Q y ^ 2 + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 3 -
                (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z ^ 2 + W'.a₄ * Q x * Q z ^ 4 + W'.a₆ * Q z ^ 6)) +
          (P x ^ 2 * Q z ^ 4 + P x * Q x * P z ^ 2 * Q z ^ 2 + Q x ^ 2 * P z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4 +
                  W'.a₂ * P x * P z ^ 2 * Q z ^ 4 +
                W'.a₂ * Q x * P z ^ 4 * Q z ^ 2 +
              W'.a₄ * P z ^ 4 * Q z ^ 4) *
            (Q x * P z ^ 2)) -
      (0 +
        (Q z ^ 6 *
              (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)) +
            P z ^ 6 * 0 +
          (P x ^ 2 * Q z ^ 4 + P x * Q x * P z ^ 2 * Q z ^ 2 + Q x ^ 2 * P z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4 +
                  W'.a₂ * P x * P z ^ 2 * Q z ^ 4 +
                W'.a₂ * Q x * P z ^ 4 * Q z ^ 2 +
              W'.a₄ * P z ^ 4 * Q z ^ 4) *
            (P x * Q z ^ 2))) =
    0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ P y * Q z ^ 3 - Q y * P z ^ 3 + (P y * Q z ^ 3 - (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) * P z ^ 3) +
        -W'.a₁ * P z * Q z * (Q x * P z ^ 2) -
      ((P y - W'.negY P) * Q z ^ 3 + -W'.a₁ * P z * Q z * (P x * Q z ^ 2)) =
    0

Tactic:
negY

Goal state after:
case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ P y * Q z ^ 3 - Q y * P z ^ 3 + (P y * Q z ^ 3 - (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) * P z ^ 3) +
        -W'.a₁ * P z * Q z * (Q x * P z ^ 2) -
      ((P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) * Q z ^ 3 + -W'.a₁ * P z * Q z * (P x * Q z ^ 2)) =
    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'.dblU P = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)

Tactic:
dblU,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) W'.polynomialX = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
hPz

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ ![P x, -P y, P z] = ![P x, -P y, 0]

Tactic:
hPz

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ ![P x, -P y, 0] = ![P x, -P y, 0]
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
⊢ (-3 * P x ^ 2) ^ 2 - W'.a₁ * (-3 * P x ^ 2) * P z * (P y - -P y) - W'.a₂ * P z ^ 2 * (P y - -P y) ^ 2 -
          2 * P x * (P y - -P y) ^ 2 +
        -8 * P x * P x ^ 3 -
      ((P x ^ 2) ^ 2 + -8 * P x * P y ^ 2) =
    0

Tactic:
hPz

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
⊢ (-3 * P x ^ 2) ^ 2 - W'.a₁ * (-3 * P x ^ 2) * 0 * (P y - -P y) - W'.a₂ * 0 ^ 2 * (P y - -P y) ^ 2 -
          2 * P x * (P y - -P y) ^ 2 +
        -8 * P x * P x ^ 3 -
      ((P x ^ 2) ^ 2 + -8 * P x * P y ^ 2) =
    0
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'.negY P * P z * P z + P x ^ 2 * P x * P z ^ 2 -
                        W'.a₁ * P x * W'.negY P * P z ^ 2 * P z -
                      W'.a₁ * P y * P x * P z * P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * P z ^ 2 -
                  W'.a₃ * W'.negY P * P z ^ 4 * P z -
                W'.a₃ * P y * P z * P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      ((P z * (P y - W'.negY 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:
negY

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 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z * P z +
                          P x ^ 2 * P x * P z ^ 2 -
                        W'.a₁ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 2 * P z -
                      W'.a₁ * P y * P x * P z * P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * P z ^ 2 -
                  W'.a₃ * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 4 * P z -
                W'.a₃ * P y * P z * P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      ((P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3))) ^ 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.Data.Int.WithZero

Goal state before:
pp: case neg
e : ℝ≥0
he : e ≠ 0
x y : WithZero (Multiplicative ℤ)
hxy : ¬x * 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:
obtain ⟨hx, hy⟩ := mul_ne_zero_iff.mp hxy
      -- x ≠ 0 and y ≠ 0
      rw [dif_neg hxy, dif_neg hx, dif_neg hy, ← zpow_add' (Or.inl he), ← toAdd_mul]
      congr
      rw [← WithZero.coe_inj, WithZero.coe_mul, coe_unzero hx, coe_unzero hy, coe_unzero hxy]

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: e : ℝ≥0
he : 1 < e
⊢ StrictMono ⇑(toNNReal ⋯)

Tactic:
intro x y
  cases y
  · simp
  cases x
  · simpa using! zpow_pos he.pos _
  · simp [toNNReal, he]

Goal state after:
Module: Mathlib.Data.Int.WithZero

Goal state before:
pp: case neg
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : (toNNReal he0) m = 1
⊢ m = 1

Tactic:
toNNReal_neg_apply he0 hm,

Goal state after:
case neg
e : ℝ≥0
m : WithZero (Multiplicative ℤ)
he0 : e ≠ 0
he1 : e ≠ 1
hm : ¬m = 0
h1 : e ^ toAdd (unzero hm) = 1
⊢ m = 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
⊢ P x * Q z ^ 2 - Q x * P z ^ 2 = P x * Q z * Q z

Tactic:
hPz

Goal state after:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hPz : P z = 0
⊢ P x * Q z ^ 2 - Q x * 0 ^ 2 = P x * Q z * Q z
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
⊢ W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * addZ P Q)

Tactic:
Affine.slope_of_X_ne <| by rwa [ne_eq, ← X_eq_iff hPz hQz],

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 / P z ^ 2 - Q x / Q z ^ 2) =
    (P y * Q z ^ 3 - Q y * P z ^ 3) / (P z * Q z * addZ P Q)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

Tactic:
hPz

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hPz : P z = 0
⊢ P x * Q x ^ 2 * 0 ^ 2 - 2 * P y * Q y * 0 * Q z + P x ^ 2 * Q x * Q z ^ 2 - W'.a₁ * P x * Q y * 0 ^ 2 * Q z -
                  W'.a₁ * P y * Q x * 0 * Q z ^ 2 +
                2 * W'.a₂ * P x * Q x * 0 ^ 2 * Q z ^ 2 -
              W'.a₃ * Q y * 0 ^ 4 * Q z -
            W'.a₃ * P y * 0 * Q z ^ 4 +
          W'.a₄ * Q x * 0 ^ 4 * Q z ^ 2 +
        W'.a₄ * P x * 0 ^ 2 * Q z ^ 4 +
      2 * W'.a₆ * 0 ^ 4 * Q z ^ 4 =
    (P x * Q z) ^ 2 * Q x
Module: Mathlib.Topology.Algebra.WithZeroTopology

Goal state before:
pp: Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ {γ} ∈ 𝓝 γ

Tactic:
by simp [h]

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

Goal state before:
pp: case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto ((fun p ↦ p.1 * p.2) ∘ fun a ↦ (a, y)) (𝓝 0) (𝓝 0)

Tactic:
refine (hasBasis_nhds_zero.tendsto_iff hasBasis_nhds_zero).2 fun γ hγ => ?_

Goal state after:
case inl.inr
α : Type u_1
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
γ✝ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
γ : Γ₀
hγ : γ ≠ 0
⊢ ∃ ia, ia ≠ 0 ∧ ∀ x ∈ Iio ia, ((fun p ↦ p.1 * p.2) ∘ fun a ↦ (a, y)) x ∈ Iio γ
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 y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

Tactic:
by_cases hx : x ≤ᵥ 0 <;> by_cases hy : y ≤ᵥ 0

Goal state after:
case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩

case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
x✝ x' y✝ y' z x y : R
t s : ↥(posSubmonoid R)
h₁ : x * ↑t ≤ᵥ y * ↑s
h₂ : y * ↑s ≤ᵥ x * ↑t
hx : ¬x ≤ᵥ 0
hy : ¬y ≤ᵥ 0
⊢ (if h : x ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑s ⟨x, h⟩) =
    if h : y ≤ᵥ 0 then 0 else ValueGroupWithZero.mk ↑t ⟨y, h⟩
Module: Mathlib.Topology.Algebra.UniformField

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : IsTopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ y.hatInv = if y = 0 then 0 else y.hatInv

Tactic:
rw [if_neg y_ne]

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 Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * Q z +
                                          3 * P x * P y * Q x ^ 2 * P z * Q z ^ 2 +
                                        P x ^ 3 * Q y * Q z ^ 3 -
                                      2 * P y ^ 2 * Q y * Q z ^ 3 +
                                    W'.a₁ * P x * Q y ^ 2 * P z ^ 4 +
                                  W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
                                W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
                              W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                            2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
                          2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
                        W'.a₃ * Q y ^ 2 * P z ^ 6 -
                      W'.a₃ * P y ^ 2 * Q z ^ 6 -
                    W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
                  W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
                W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
              W'.a₄ * P x * P y * P z * Q z ^ 6 -
            2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
          2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6 +
        (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3 - Q y) * Q z ^ 3 * P x ^ 3 -
      ((P x * Q z) ^ 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) +
        (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3 - Q y) * Q z ^ 3 * P y ^ 2) =
    0

Tactic:
hPz

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