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

Goal state before:
pp: case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.252} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.252} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
i j : 𝒱.I₀
hij : i ⟶ j
this :
  d.transitionMap hij ≫ (d.isColimit j).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).mapCocone s) =
    (MorphismProperty.Over.map ⊤ ⋯).map
        ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)) ≫
      (Over.pullbackMapHomPullback (Cover.trans 𝒰 hij) ⋯ trivial (𝒰.f j) (𝒰.f i) ⋯).app s.pt
⊢ (d.transitionMap hij).left ≫
      ((d.isColimit j).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).mapCocone s)).left ≫
        pullback.fst s.pt.hom (𝒰.f j) =
    ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
      pullback.fst s.pt.hom (𝒰.f i)

Tactic:
rw [← Over.comp_left_assoc, ← Comma.comp_hom, this]

Goal state after:
case refine_1.refine_2
P : MorphismProperty Scheme
inst✝⁸ : P.IsStableUnderBaseChange
inst✝⁷ : P.IsMultiplicative
S : Scheme
J : Type u_1
inst✝⁶ : Category.{v_1, u_1} J
D : J ⥤ P.Over ⊤ S
𝒰 : S.OpenCover
inst✝⁵ : Category.{v_2, ?u.252} 𝒰.I₀
inst✝⁴ : LocallyDirected 𝒰
d : ColimitGluingData D 𝒰
inst✝³ :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), PreservesColimitsOfShape J (MorphismProperty.Over.pullback P ⊤ (Cover.trans 𝒰 hij))
inst✝² : Quiver.IsThin 𝒰.I₀
inst✝¹ : Small.{u, ?u.252} 𝒰.I₀
inst✝ : IsZariskiLocalAtTarget P
𝒱 : d.glued.left.OpenCover := d.relativeGluingData.cover
s : Cocone D
i j : 𝒱.I₀
hij : i ⟶ j
this :
  d.transitionMap hij ≫ (d.isColimit j).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).mapCocone s) =
    (MorphismProperty.Over.map ⊤ ⋯).map
        ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)) ≫
      (Over.pullbackMapHomPullback (Cover.trans 𝒰 hij) ⋯ trivial (𝒰.f j) (𝒰.f i) ⋯).app s.pt
⊢ Over.Hom.left
        (Comma.Hom.hom
          ((MorphismProperty.Over.map ⊤ ⋯).map
              ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)) ≫
            (Over.pullbackMapHomPullback (Cover.trans 𝒰 hij) ⋯ trivial (𝒰.f j) (𝒰.f i) ⋯).app s.pt)) ≫
      pullback.fst s.pt.hom (𝒰.f j) =
    ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)).left ≫
      pullback.fst s.pt.hom (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 3
⊢ W.j = 0 ↔ W.b₂ ^ 6 = 0

Tactic:
by
  rw [j_of_char_three, Units.mul_right_eq_zero]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound k₀ (fun x ↦ Nat.casesOn x k D) (n + 1 + 1) = numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)

Tactic:
rw [numBound_succ (n := n + 1), numBound_casesOn_succ k₀ k D n, numBound_succ,
      degBound_casesOn_succ]

Goal state after:
k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
        ((k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n) *
      Nat.casesOn (n + 1) k D =
    numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) n *
      ((k₀ * k) ^ (k₀ * k) • D) n
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ ↑C.u ^ 12 * ↑W.Δ'⁻¹ * ↑C.u⁻¹ ^ (4 * 3) * W.c₄ ^ 3 = ↑W.Δ'⁻¹ * W.c₄ ^ 3

Tactic:
mul_right_comm (C.u.val ^ 12),

Goal state after:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
inst✝ : W.IsElliptic
⊢ ↑C.u ^ 12 * ↑C.u⁻¹ ^ (4 * 3) * ↑W.Δ'⁻¹ * W.c₄ ^ 3 = ↑W.Δ'⁻¹ * W.c₄ ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
x : R[X][Y]
⊢ (map W' f) ((mk W') x) = (mk (W'.map f)) (Polynomial.map (mapRingHom f) x)

Tactic:
rw [map, AdjoinRoot.lift_mk, ← eval₂_map]
  exact AdjoinRoot.aeval_eq <| x.map <| mapRingHom f

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : n = 0
⊢ complEDS b c d k ↑n = complEDS' b c d k n

pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : ¬n = 0
⊢ complEDS b c d k ↑n = complEDS' b c d k n

Tactic:
· simp [hn, complEDS]

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
n : ℕ
hn : ¬n = 0
⊢ complEDS b c d k ↑n = complEDS' b c d k n
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
h₁ : W.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
⊢ some x₁ y₁ h₁ + some x₂ y₂ h₂ = some (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) ⋯

Tactic:
simp only [add_def, add, dif_neg hxy]

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 * 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₆ =
    -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
a₂_of_isShortNF

Goal state after:
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)
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))⁻¹ ^ 3 * (E.a₃ + s ^ 2 * E.a₁ + 2 * t) = E'.a₃

Tactic:
Units.val_mk0,

Goal state after:
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
⊢ u⁻¹ ^ 3 * (E.a₃ + s ^ 2 * E.a₁ + 2 * t) = E'.a₃
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
⊢ W.j = 110592 * W.a₄ ^ 3 / (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

Tactic:
by
  have h := W.Δ'.ne_zero
  rw [coe_Δ', Δ_of_isCharTwoJEqZeroNF] at h
  rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
    c₄_of_isCharTwoJEqZeroNF, Δ_of_isCharTwoJEqZeroNF, div_eq_div_iff h (neg_ne_zero.1 h)]
  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))⁻¹ ^ 2 * (E.a₂ - 0 * 0 + 3 * 0 - 0 ^ 2) = E'.a₂

Tactic:
Units.val_mk0,

Goal state after:
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
⊢ u⁻¹ ^ 2 * (E.a₂ - 0 * 0 + 3 * 0 - 0 ^ 2) = E'.a₂
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
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
heq : -E.a₂ ^ 3 * E'.a₆ = -E'.a₂ ^ 3 * E.a₆
⊢ (↑(Units.mk0 u hu0))⁻¹ ^ 6 * (E.a₆ + 0 * 0 + 0 ^ 2 * E.a₂ + 0 ^ 3 - 0 * 0 - 0 ^ 2 - 0 * 0 * 0) = E'.a₆

Tactic:
Units.val_mk0,

Goal state after:
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
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
heq : -E.a₂ ^ 3 * E'.a₆ = -E'.a₂ ^ 3 * E.a₆
⊢ u⁻¹ ^ 6 * (E.a₆ + 0 * 0 + 0 ^ 2 * E.a₂ + 0 ^ 3 - 0 * 0 - 0 ^ 2 - 0 * 0 * 0) = E'.a₆
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.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (↑(Units.mk0 u hu0))⁻¹ ^ 4 * (E.a₄ - 0 * 0 + 2 * r * 0 - (0 + r * 0) * 0 + 3 * r ^ 2 - 2 * 0 * 0) = E'.a₄

Tactic:
Units.val_mk0,

Goal state after:
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.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ u⁻¹ ^ 4 * (E.a₄ - 0 * 0 + 2 * r * 0 - (0 + r * 0) * 0 + 3 * r ^ 2 - 2 * 0 * 0) = E'.a₄
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.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ (↑(Units.mk0 u hu0))⁻¹ ^ 6 * (E.a₆ + r * E.a₄ + r ^ 2 * 0 + r ^ 3 - 0 * 0 - 0 ^ 2 - r * 0 * 0) = E'.a₆

Tactic:
Units.val_mk0,

Goal state after:
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.IsShortNF
inst✝ : E'.IsShortNF
ha₄ : E.a₄ ≠ 0
ha₄' : E'.a₄ ≠ 0
this : NeZero 4
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
r : F
hr : 1 * r ^ 3 + E.a₄ * r + (E.a₆ - u ^ 6 * E'.a₆) = 0
hu0 : u ≠ 0
⊢ u⁻¹ ^ 6 * (E.a₆ + r * E.a₄ + r ^ 2 * 0 + r ^ 3 - 0 * 0 - 0 ^ 2 - r * 0 * 0) = E'.a₆
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
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 ^ 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ (↑(Units.mk0 u hu0))⁻¹ ^ 6 * (E.a₆ + 0 * 0 + 0 ^ 2 * 0 + 0 ^ 3 - 0 * 0 - 0 ^ 2 - 0 * 0 * 0) = E'.a₆

Tactic:
Units.val_mk0,

Goal state after:
case h.a₆
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 ^ 6 = E.a₆ / E'.a₆
hu0 : u ≠ 0
⊢ u⁻¹ ^ 6 * (E.a₆ + 0 * 0 + 0 ^ 2 * 0 + 0 ^ 3 - 0 * 0 - 0 ^ 2 - 0 * 0 * 0) = E'.a₆
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
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
ha₄' : E'.a₄ ≠ 0
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
hu0 : u ≠ 0
⊢ (↑(Units.mk0 u hu0))⁻¹ ^ 4 * (E.a₄ - 0 * 0 + 2 * 0 * 0 - (0 + 0 * 0) * 0 + 3 * 0 ^ 2 - 2 * 0 * 0) = E'.a₄

Tactic:
Units.val_mk0,

Goal state after:
case h.a₄
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
ha₄' : E'.a₄ ≠ 0
u : F
hu : u ^ 4 = E.a₄ / E'.a₄
hu0 : u ≠ 0
⊢ u⁻¹ ^ 4 * (E.a₄ - 0 * 0 + 2 * 0 * 0 - (0 + 0 * 0) * 0 + 3 * 0 ^ 2 - 2 * 0 * 0) = E'.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case succ.left
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
h : ∀ {n : ℕ}, (W.preΨ' n).natDegree ≤ expDegree n ∧ (W.preΨ' n).coeff (expDegree n) = ↑(expCoeff n) := ⋯
n : ℕ
hd : (n + 1) ^ 2 - 1 = 2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc : ↑(n + 1) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
⊢ (W.preΨ' (n + 1) ^ 2 * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    2 * expDegree (n + 1) + if Even (n + 1) then 3 else 0

Tactic:
refine natDegree_mul_le_of_le (dp h.1) ?_

Goal state after:
case succ.left
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
hc : ↑(n + 1) ^ 2 = expCoeff (n + 1) ^ 2 * if Even (n + 1) then 4 else 1
⊢ (if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤ if Even (n + 1) then 3 else 0
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
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₆
hu0 : u ≠ 0
⊢ (↑(Units.mk0 u hu0))⁻¹ ^ 4 * (E.a₄ - 0 * 0 + 2 * 0 * 0 - (0 + 0 * 0) * 0 + 3 * 0 ^ 2 - 2 * 0 * 0) = E'.a₄

Tactic:
Units.val_mk0,

Goal state after:
case h.a₄
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₆
hu0 : u ≠ 0
⊢ u⁻¹ ^ 4 * (E.a₄ - 0 * 0 + 2 * 0 * 0 - (0 + 0 * 0) * 0 + 3 * 0 ^ 2 - 2 * 0 * 0) = E'.a₄
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
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₆
hu0 : u ≠ 0
⊢ (↑(Units.mk0 u hu0))⁻¹ ^ 6 * (E.a₆ + 0 * E.a₄ + 0 ^ 2 * 0 + 0 ^ 3 - 0 * 0 - 0 ^ 2 - 0 * 0 * 0) = E'.a₆

Tactic:
Units.val_mk0,

Goal state after:
case h.a₆
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₆
hu0 : u ≠ 0
⊢ u⁻¹ ^ 6 * (E.a₆ + 0 * E.a₄ + 0 ^ 2 * 0 + 0 ^ 3 - 0 * 0 - 0 ^ 2 - 0 * 0 * 0) = E'.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case succ.succ.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
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 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    max ((n + 1 + 1) ^ 2) ((n + 1 + 1) ^ 2)

Tactic:
hd,

Goal state after:
case succ.succ.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
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 + 1) ^ 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : (n + 1 + 1) ^ 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * expCoeff (n + 2) ^ 2 * if Even (n + 1) then 1 else 4) -
      expCoeff (n + 3) * expCoeff (n + 1) * if Even (n + 1) then 4 else 1
⊢ ((X * W.preΨ' (n + 1 + 1) ^ 2 * if Even (n + 1) then 1 else W.Ψ₂Sq) -
        W.preΨ' (n + 1 + 2) * W.preΨ' (n + 1) * if Even (n + 1) then W.Ψ₂Sq else 1).natDegree ≤
    max (1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3) ((n + 1 + 1) ^ 2)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic

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

Tactic:
rw [hP.left, pow_succ, (hPx.pow 2).mul_div_cancel_left, hQ.left, pow_succ _ 2,
      (hQx.pow 2).div_mul_cancel_left, hQx.inv_mul_cancel_right]

Goal state after: