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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ 4 * C X ^ 3 + (C (C W.a₁) ^ 2 + 4 * C (C W.a₂)) * C X ^ 2 + 2 * (2 * C (C W.a₄) + C (C W.a₁) * C (C W.a₃)) * C X +
      (C (C W.a₃) ^ 2 + 4 * C (C W.a₆)) =
    (2 * Y + (C (C W.toAffine.a₁) * C X + C (C W.toAffine.a₃))) ^ 2 -
      4 *
        (Y ^ 2 + (C (C W.toAffine.a₁) * C X + C (C W.toAffine.a₃)) * Y -
          (C X ^ 3 + C (C W.toAffine.a₂) * C X ^ 2 + C (C W.toAffine.a₄) * C X + C (C W.toAffine.a₆)))

Tactic:
ring1

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

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ (C (W.preΨ (m - 1)) ^ 2 * C (W.preΨ m) * C (W.preΨ (m + 2)) -
          C (W.preΨ (m - 2)) * C (W.preΨ m) * C (W.preΨ (m + 1)) ^ 2) *
        W.ψ₂ *
      W.ψ₂ =
    (C (W.preΨ (m - 1)) * 1) ^ 2 * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 2)) * W.ψ₂) -
      C (W.preΨ (m - 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) * (C (W.preΨ (m + 1)) * 1) ^ 2

Tactic:
ring1

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

Goal state before:
pp: case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ (C (W.preΨ (m - 1)) ^ 2 * C (W.preΨ m) * C (W.preΨ (m + 2)) -
          C (W.preΨ (m - 2)) * C (W.preΨ m) * C (W.preΨ (m + 1)) ^ 2) *
        W.ψ₂ *
      W.ψ₂ =
    (C (W.preΨ (m - 1)) * W.ψ₂) ^ 2 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 2)) * 1) -
      C (W.preΨ (m - 2)) * 1 * (C (W.preΨ m) * 1) * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 2

Tactic:
ring1

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

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * (W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial) ^ 2 -
        C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * 1) *
      1 =
    C (W.preΨ (m + 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) ^ 3 - C (W.preΨ (m - 1)) * 1 * (C (W.preΨ (m + 1)) * 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3)

Tactic:
ring1

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

Goal state before:
pp: case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * 1 -
        C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * (W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial) ^ 2) *
      1 =
    C (W.preΨ (m + 2)) * 1 * (C (W.preΨ m) * 1) ^ 3 - C (W.preΨ (m - 1)) * W.ψ₂ * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
        (-C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3)

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * 1 ^ 2 * (4 * X ^ 3 + C W.b₂ * X ^ 2 + 2 * C W.b₄ * X + C W.b₆) -
      (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈) * 1 * 1 =
    X ^ 4 - C W.b₄ * X ^ 2 - 2 * C W.b₆ * X - C W.b₈

Tactic:
ring1

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

Goal state before:
pp: case pos
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝¹⁹ : CommRing R
inst✝¹⁸ : CommRing S
inst✝¹⁷ : CommRing A
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
W : Affine F
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x₁ y₁ : F
h₁ : (W'⁄F).Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯

Tactic:
rw [add_of_Y_eq hxy.left hxy.right,
        add_of_Y_eq (congr_arg _ hxy.left) <| by rw [hxy.right, baseChange_negY]]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - (W.preΨ₄ * 1 ^ 3 * W.Ψ₂Sq ^ 2 - 1 * W.Ψ₃ ^ 3 * 1) * W.Ψ₃ * 1 =
    X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C X * (C W.preΨ₄ * W.ψ₂) ^ 2 - (C W.preΨ₄ * W.ψ₂ * W.ψ₂ ^ 3 - 1 * C W.Ψ₃ ^ 3) * C W.Ψ₃ =
    C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
P : W'.Point
⊢ (-P).xRep = P.xRep

Tactic:
by
  cases P <;> simp [← zero_def]

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

Goal state before:
pp: n : ℕ
hn : 2 * (n + 1) ≠ 0
⊢ (2 * (n + 1)) ^ 2 = 2 * (2 * n * (n + 2)) + 4

Tactic:
ring1

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

Goal state before:
pp: case inl.succ
n : ℕ
hn : 2 * (n + 1) ≠ 0
⊢ 2 * (2 * ↑n * (↑n + 2)) = (2 * (↑n + 1)) ^ 2 - 4

Tactic:
ring1

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

Goal state before:
pp: n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ (2 * n + 1) ^ 2 = 2 * (2 * n * (n + 1)) + 1

Tactic:
ring1

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

Goal state before:
pp: case inr
n : ℕ
hn : 2 * n + 1 ≠ 0
⊢ 2 * (2 * ↑n * (↑n + 1)) = (2 * ↑n + 1) ^ 2 - 1

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 + 4 * W.a₂ = 4 * W.a₂

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₄ = 2 * W.a₄

Tactic:
rw [b₄, a₃_of_isCharNeTwoNF]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 2 * W.a₄ + W.a₁ * 0 = 2 * W.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 2 * W.a₄ + W.a₁ * 0 = 2 * W.a₄

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 + 4 * W.a₆ = 4 * W.a₆

Tactic:
ring1

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

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

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ (4 * W.a₂) ^ 2 - 24 * (2 * W.a₄) = 16 * W.a₂ ^ 2 - 48 * W.a₄

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 3 + 36 * (4 * W.a₂) * (2 * W.a₄) - 216 * (4 * W.a₆) = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 2 * (4 * W.a₂ * W.a₆ - W.a₄ ^ 2) - 8 * (2 * W.a₄) ^ 3 - 27 * (4 * W.a₆) ^ 2 +
      9 * (4 * W.a₂) * (2 * W.a₄) * (4 * W.a₆) =
    -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ -64 * 0 ^ 3 * W.a₆ + 16 * 0 ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * 0 * W.a₄ * W.a₆ =
    -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
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.IsShortNF
h : -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) ≠ 0
⊢ (-48 * W.a₄) ^ 3 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) = 6912 * W.a₄ ^ 3 * (-16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2))

Tactic:
ring1

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

Goal state before:
pp: case h.a₃
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 ^ 3 * (0 + 0 * E.a₁ + 2 * 0) = 0

Tactic:
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
h : -W.a₂ ^ 3 * W.a₆ ≠ 0
⊢ (W.a₂ ^ 2) ^ 3 * W.a₆ = -W.a₂ ^ 3 * (-W.a₂ ^ 3 * W.a₆)

Tactic:
ring1

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

Goal state before:
pp: case h.a₄
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 ^ 4 * (0 - s * 0 + 2 * 0 * E.a₂ - (0 + 0 * s) * E.a₁ + 3 * 0 ^ 2 - 2 * s * 0) = 0

Tactic:
ring1

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

Goal state before:
pp: case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = 2 * ((↑m + 2) ^ 2 - 4) + ((↑m + 3) ^ 2 - 1) + ((↑m + 5) ^ 2 - 1)

Tactic:
ring1

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

Goal state before:
pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = 2 * ((↑m + 2) ^ 2 - 1) + ((↑m + 3) ^ 2 - 4) + ((↑m + 5) ^ 2 - 4)

Tactic:
ring1

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

Goal state before:
pp: case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = (↑m + 1) ^ 2 - 1 + ((↑m + 3) ^ 2 - 1) + 2 * ((↑m + 4) ^ 2 - 4)

Tactic:
ring1

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

Goal state before:
pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = (↑m + 1) ^ 2 - 4 + ((↑m + 3) ^ 2 - 4) + 2 * ((↑m + 4) ^ 2 - 1)

Tactic:
ring1

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

Goal state before:
pp: case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 4) ^ 2 - 4 + 3 * ((↑m + 2) ^ 2 - 4) + 2 * 6

Tactic:
ring1

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

Goal state before:
pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 4) ^ 2 - 1 + 3 * ((↑m + 2) ^ 2 - 1) + 2 * 0

Tactic:
ring1

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

Goal state before:
pp: case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 1) ^ 2 - 1 + 3 * ((↑m + 3) ^ 2 - 1) + 2 * 0

Tactic:
ring1

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

Goal state before:
pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 1) ^ 2 - 4 + 3 * ((↑m + 3) ^ 2 - 4) + 2 * 6

Tactic:
ring1

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

Goal state before:
pp: case h.a₆
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 ^ 6 * (E'.a₆ + 0 * E.a₄ + 0 ^ 2 * E.a₂ + 0 ^ 3 - 0 * E.a₃ - 0 ^ 2 - 0 * 0 * E.a₁) = E'.a₆

Tactic:
ring1

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

Goal state before:
pp: case pos
m : ℕ
h✝ : Even m
⊢ 2 * (↑m + 3) / 2 = ((↑m + 2) / 2) ^ 2 * (↑m + 3) * (↑m + 5) - (↑m + 1) * (↑m + 3) * ((↑m + 4) / 2) ^ 2

Tactic:
ring1

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

Goal state before:
pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ 2 * (↑m + 3) / 2 = (↑m + 2) ^ 2 * ((↑m + 3) / 2) * ((↑m + 5) / 2) - (↑m + 1) / 2 * ((↑m + 3) / 2) * (↑m + 4) ^ 2

Tactic:
ring1

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

Goal state before:
pp: case pos
m : ℕ
h✝ : Even m
⊢ 2 * (↑m + 2) + 1 = (↑m + 4) / 2 * ((↑m + 2) / 2) ^ 3 * 16 - (↑m + 1) * (↑m + 3) ^ 3 * 1

Tactic:
ring1

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

Goal state before:
pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ 2 * (↑m + 2) + 1 = (↑m + 4) * (↑m + 2) ^ 3 * 1 - (↑m + 1) / 2 * ((↑m + 3) / 2) ^ 3 * 16

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
⊢ ∃ i' fi'i, ∀ (j : ↥s), D.map fi'i ⁻¹ᵁ 𝒱 j ≤ t.app i' ⁻¹ᵁ ↑(↑(↑↑j).2).2

Tactic:
choose k fk hk using fun j ↦ exists_map_preimage_le_map_preimage D c hc (h𝒱𝒰 j).1.isCompact
      (V := t.app i ⁻¹ᵁ j.1.1.2.1.2.1) (by
      rw [← Hom.comp_preimage, ← NatTrans.comp_app, ha]
      exact (h𝒱𝒰 j).2.symm.trans_le (j.1.prop.2.trans (a.preimage_mono j.1.1.2.prop.2)))
    obtain ⟨i', fi'i, fi', hfi'⟩ := IsCofiltered.wideCospan fk
    refine ⟨i', fi'i, fun j ↦ ?_⟩
    rw [← hfi', Functor.map_comp, Hom.comp_preimage]
    refine (Hom.preimage_mono _ (hk _)).trans ?_
    simp only [← Hom.comp_preimage, t.naturality, Functor.const_obj_obj,
      Functor.const_obj_map, Category.comp_id, le_refl]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 1 ^ 2 + 4 * W.a₂ = 1 + 4 * W.a₂

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 2 * 0 + W.a₁ * 0 = 0

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 0 ^ 2 + 4 * W.a₆ = 4 * W.a₆

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 1 ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - 1 * 0 * 0 + W.a₂ * 0 ^ 2 - 0 ^ 2 = W.a₆ + 4 * W.a₂ * W.a₆

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₂ ^ 2 - 24 * 0 = W.b₂ ^ 2

Tactic:
ring1

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

Goal state before:
pp: case h.a₁
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
this : NeZero 3
u : F
hu : u ^ 3 = E.a₃ / E'.a₃
s : F
hs : 1 * s ^ 4 + E.a₃ * s + (E.a₄ - u ^ 4 * E'.a₄) = 0
t : F
ht : 1 * t ^ 2 + E.a₃ * t + (s ^ 6 + E.a₄ * s ^ 2 + E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ↑(Units.mk0 u hu0)⁻¹ * (0 + 0 * s) = 0

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ -W.b₂ ^ 3 + 36 * W.b₂ * 0 - 216 * (4 * W.a₆) = -W.b₂ ^ 3 - 864 * W.a₆

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharTwoJNeZeroNF
inst✝ : CharP R 2
⊢ 1 ^ 2 = 1

Tactic:
ring1

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

Goal state before:
pp: case h.a₂
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
this : NeZero 3
u : F
hu : u ^ 3 = E.a₃ / E'.a₃
s : F
hs : 1 * s ^ 4 + E.a₃ * s + (E.a₄ - u ^ 4 * E'.a₄) = 0
t : F
ht : 1 * t ^ 2 + E.a₃ * t + (s ^ 6 + E.a₄ * s ^ 2 + E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 2 * (0 - s * 0 + 1 * s ^ 2 - s ^ 2) = 0

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 0 ^ 2 + 4 * 0 = 0

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 2 * W.a₄ + 0 * W.a₃ = 2 * W.a₄

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 0 ^ 2 * W.a₆ + 4 * 0 * W.a₆ - 0 * W.a₃ * W.a₄ + 0 * W.a₃ ^ 2 - W.a₄ ^ 2 = -W.a₄ ^ 2

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ 0 ^ 2 - 24 * (2 * W.a₄) = -48 * W.a₄

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ -0 ^ 3 + 36 * 0 * (2 * W.a₄) - 216 * W.b₆ = -216 * W.b₆

Tactic:
ring1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJEqZeroNF
⊢ -0 ^ 2 * W.b₈ - 8 * (2 * W.a₄) ^ 3 - 27 * W.b₆ ^ 2 + 9 * 0 * (2 * W.a₄) * W.b₆ = -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Tactic:
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.IsCharTwoJEqZeroNF
h : -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2) ≠ 0
⊢ (-48 * W.a₄) ^ 3 * (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2) = 110592 * W.a₄ ^ 3 * -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u ^ 2 * Q x * Q z ^ 2 = Q x * (↑u * Q z) ^ 2

Tactic:
ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u ^ 3 * Q y * Q z ^ 3 = Q y * (↑u * Q z) ^ 3

Tactic:
ring1

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P x * 1 ^ 2 + -P x * 1 - (P x / P z ^ 2 * P z ^ 2 + -P x * (P z ^ 2 / P z ^ 2)) = 0

Tactic:
ring1

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

Goal state before:
pp: case h.a₁
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ↑(Units.mk0 u hu0)⁻¹ * (0 + 2 * 0) = 0

Tactic:
ring1

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ P y * 1 ^ 3 + -P y * 1 - (P y / P z ^ 3 * P z ^ 3 + -P y * (P z ^ 3 / P z ^ 3)) = 0

Tactic:
ring1

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

Goal state before:
pp: case h.a₃
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 3 * (0 + 0 * 0 + 2 * 0) = 0

Tactic:
ring1

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

Goal state before:
pp: case h.a₄
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝⁴ : E.IsElliptic
inst✝³ : E'.IsElliptic
inst✝² : CharP F 3
inst✝¹ : E.IsCharThreeJNeZeroNF
inst✝ : E'.IsCharThreeJNeZeroNF
heq : E.j = E'.j
ha₂ : E.a₂ ≠ 0
ha₆ : E.a₆ ≠ 0
ha₂' : E'.a₂ ≠ 0
ha₆' : E'.a₆ ≠ 0
this : NeZero 2
u : F
hu : u ^ 2 = E.a₂ / E'.a₂
hu0 : u ≠ 0
⊢ ↑(Units.mk0 u hu0)⁻¹ ^ 4 * (0 - 0 * 0 + 2 * 0 * E.a₂ - (0 + 0 * 0) * 0 + 3 * 0 ^ 2 - 2 * 0 * 0) = 0

Tactic:
ring1

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

Goal state before:
pp: case a
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (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 +
        (W.a₁ * P x * P y / P z ^ 5 * 1 + W.a₃ * P y / P z ^ 3 * 1 + W.a₂ * P x ^ 2 / P z ^ 4 * (P z ^ 2 / P z ^ 2) +
            W.a₄ * P x / P z ^ 2 * (P z ^ 4 / P z ^ 4) +
          W.a₆ * (P z ^ 6 / P z ^ 6)) -
      ((P y / P z ^ 3) ^ 2 + W.toAffine.a₁ * (P x / P z ^ 2) * (P y / P z ^ 3) + W.toAffine.a₃ * (P y / P z ^ 3) -
          ((P x / P z ^ 2) ^ 3 + W.toAffine.a₂ * (P x / P z ^ 2) ^ 2 + W.toAffine.a₄ * (P x / P z ^ 2) +
            W.toAffine.a₆) +
        (W.a₁ * P x * P y / P z ^ 5 * (P z / P z) + W.a₃ * P y / P z ^ 3 * (P z ^ 3 / P z ^ 3) +
              W.a₂ * P x ^ 2 / P z ^ 4 * 1 +
            W.a₄ * P x / P z ^ 2 * 1 +
          W.a₆ * 1)) =
    0

Tactic:
ring1

Goal state after: