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

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
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)
inst✝ : c.pt.IsQuasiAffine
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
⊢ ∃ i f, IsAffineOpen ((D.obj i).basicOpen f) ∧ (c.π.app i) x ∈ (D.obj i).basicOpen f

Tactic:
obtain ⟨k, fki, fkj, -⟩ := IsCofilteredOrEmpty.cone_objs i j

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
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)
inst✝ : c.pt.IsQuasiAffine
x : ↥c.pt
i : I
U : TopologicalSpace.Opens ↥(D.obj i)
hU : U ∈ (D.obj i).affineOpens
hxU : (c.π.app i) x ∈ ↑U
j : I
r : ↑Γ(D.obj j, ⊤)
hr : IsAffineOpen (c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hxr : x ∈ ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r))
hrU : ↑(c.pt.basicOpen ((ConcreteCategory.hom (Hom.appTop (c.π.app j))) r)) ⊆ ↑(c.π.app i ⁻¹ᵁ U)
k : I
fki : k ⟶ i
fkj : k ⟶ j
⊢ ∃ i f, IsAffineOpen ((D.obj i).basicOpen f) ∧ (c.π.app i) x ∈ (D.obj i).basicOpen f
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
Nat.cast_succ,

Goal state after:
case nat.succ.succ.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS b c d (2 * (↑m + 1 + 1 + 1)) =
    preNormEDS b c d (↑m + 1 + 1 + 1 - 1) ^ 2 * preNormEDS b c d (↑m + 1 + 1 + 1) *
        preNormEDS b c d (↑m + 1 + 1 + 1 + 2) -
      preNormEDS b c d (↑m + 1 + 1 + 1 - 2) * preNormEDS b c d (↑m + 1 + 1 + 1) *
        preNormEDS b c d (↑m + 1 + 1 + 1 + 1) ^ 2
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n) =
      preNormEDS b c d (↑n - 1) ^ 2 * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 2) -
        preNormEDS b c d (↑n - 2) * preNormEDS b c d ↑n * preNormEDS b c d (↑n + 1) ^ 2
m : ℕ
⊢ preNormEDS b c d (2 * -↑m) =
    preNormEDS b c d (-↑m - 1) ^ 2 * preNormEDS b c d (-↑m) * preNormEDS b c d (-↑m + 2) -
      preNormEDS b c d (-↑m - 2) * preNormEDS b c d (-↑m) * preNormEDS b c d (-↑m + 1) ^ 2

Tactic:
simp_rw [mul_neg, ← sub_neg_eq_add, ← neg_sub', ← neg_add', preNormEDS_neg, ih]
    ring1

Goal state after:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
Nat.cast_succ,

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

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

Tactic:
Nat.cast_succ,

Goal state after:
case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
ih :
  ∀ (n : ℕ),
    preNormEDS b c d (2 * ↑n + 1) =
      (preNormEDS b c d (↑n + 2) * preNormEDS b c d ↑n ^ 3 * if Even ↑n then b else 1) -
        preNormEDS b c d (↑n - 1) * preNormEDS b c d (↑n + 1) ^ 3 * if Even ↑n then 1 else b
m : ℕ
⊢ preNormEDS b c d (2 * -(↑m + 1) + 1) =
    (preNormEDS b c d (-(↑m + 1) + 2) * preNormEDS b c d (-(↑m + 1)) ^ 3 * if Even (-(↑m + 1)) then b else 1) -
      preNormEDS b c d (-(↑m + 1) - 1) * preNormEDS b c d (-(↑m + 1) + 1) ^ 3 * if Even (-(↑m + 1)) then 1 else b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ ((CoordinateRing.basis W').repr (p • 1) + (CoordinateRing.basis W').repr (q • (mk W') Y)) 0 *
        ((CoordinateRing.basis W').repr ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • 1) +
            (CoordinateRing.basis W').repr ((p - q * (C W'.a₁ * X + C W'.a₃)) • (mk W') Y))
          1 -
      ((CoordinateRing.basis W').repr ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • 1) +
            (CoordinateRing.basis W').repr ((p - q * (C W'.a₁ * X + C W'.a₃)) • (mk W') Y))
          0 *
        ((CoordinateRing.basis W').repr (p • 1) + (CoordinateRing.basis W').repr (q • (mk W') Y)) 1 =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)

Tactic:
Finsupp.add_apply,

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
p q : R[X]
⊢ (((CoordinateRing.basis W').repr (p • 1)) 0 + ((CoordinateRing.basis W').repr (q • (mk W') Y)) 0) *
        (((CoordinateRing.basis W').repr ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • 1)) 1 +
          ((CoordinateRing.basis W').repr ((p - q * (C W'.a₁ * X + C W'.a₃)) • (mk W') Y)) 1) -
      (((CoordinateRing.basis W').repr ((q * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) • 1)) 0 +
          ((CoordinateRing.basis W').repr ((p - q * (C W'.a₁ * X + C W'.a₃)) • (mk W') Y)) 0) *
        (((CoordinateRing.basis W').repr (p • 1)) 1 + ((CoordinateRing.basis W').repr (q • (mk W') Y)) 1) =
    p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) - q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

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

Tactic:
Nat.cast_succ,

Goal state after:
case neg.succ
R : Type u_1
inst✝ : CommRing R
b c d : R
k : ℤ
ih :
  ∀ (n : ℕ),
    complEDS b c d k (2 * ↑n + 1) =
      complEDS b c d k ↑n ^ 2 * normEDS b c d ((↑n + 1) * k + 1) * normEDS b c d ((↑n + 1) * k - 1) -
        complEDS b c d k (↑n + 1) ^ 2 * normEDS b c d (↑n * k + 1) * normEDS b c d (↑n * k - 1)
m : ℕ
⊢ complEDS b c d k (2 * -(↑m + 1) + 1) =
    complEDS b c d k (-(↑m + 1)) ^ 2 * normEDS b c d ((-(↑m + 1) + 1) * k + 1) *
        normEDS b c d ((-(↑m + 1) + 1) * k - 1) -
      complEDS b c d k (-(↑m + 1) + 1) ^ 2 * normEDS b c d (-(↑m + 1) * k + 1) * normEDS b c d (-(↑m + 1) * k - 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg
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
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' ⋯) =
    (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₁) +
      (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h₂)

Tactic:
exact (CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' h₁ h₂ hxy).symm

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

Goal state before:
pp: case mp
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
P : W.Point
hP : toClass P = 0
⊢ P = 0

Tactic:
rcases P with (_ | ⟨_, _, h, _⟩)

Goal state after:
case mp.zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
hP : toClass zero = 0
⊢ zero = 0

case mp.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some x✝ y✝ ⋯) = 0
⊢ some x✝ y✝ ⋯ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

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

Tactic:
simp [φ, mul_assoc, sq]

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

Goal state before:
pp: case some.some
R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field F
inst✝⁹ : Field K
W' : Affine R
inst✝⁸ : DecidableEq F
inst✝⁷ : DecidableEq K
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
f : F →ₐ[S] K
x✝¹ y✝¹ : F
h✝¹ : (W'⁄F).Nonsingular x✝¹ y✝¹
x✝ y✝ : F
h✝ : (W'⁄F).Nonsingular x✝ y✝
h : (map f) (some x✝¹ y✝¹ h✝¹) = (map f) (some x✝ y✝ h✝)
⊢ some x✝¹ y✝¹ h✝¹ = some x✝ y✝ h✝

Tactic:
· simpa only [some.injEq] using ⟨f.injective (some.inj h).left, f.injective (some.inj h).right⟩

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

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W⁄B).Ψ₃ = Polynomial.map (↑f) (W⁄A).Ψ₃

Tactic:
rw [← map_Ψ₃, map_baseChange]

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
⊢ W.b₈ = -W.a₄ ^ 2

Tactic:
by
  rw [b₈, a₁_of_isCharTwoJEqZeroNF, a₂_of_isCharTwoJEqZeroNF]
  ring1

Goal state after:
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))
⊢ ↑(expCoeff (m + 2)) ^ 2 * ↑(expCoeff (m + 3)) * ↑(expCoeff (m + 5)) -
      (W.preΨ' (m + 1)).coeff (expDegree (m + 1)) * (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) *
        (W.preΨ' (m + 4) ^ 2).coeff (2 * expDegree (m + 4)) =
    ↑(expCoeff (2 * (m + 3)))

Tactic:
h₁.2,

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))
⊢ ↑(expCoeff (m + 2)) ^ 2 * ↑(expCoeff (m + 3)) * ↑(expCoeff (m + 5)) -
      ↑(expCoeff (m + 1)) * (W.preΨ' (m + 3)).coeff (expDegree (m + 3)) *
        (W.preΨ' (m + 4) ^ 2).coeff (2 * expDegree (m + 4)) =
    ↑(expCoeff (2 * (m + 3)))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : E.a₄ = 0
ha₆ : -16 * (4 * 0 + 27 * E.a₆ ^ 2) ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
mul_zero,

Goal state after:
case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : E.a₄ = 0
ha₆ : -16 * (0 + 27 * E.a₆ ^ 2) ≠ 0
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : E.a₄ = 0
ha₆ : E.a₆ ≠ 0
ha₄' : E'.a₄ = 0
ha₆' : -16 * (4 * 0 + 27 * E'.a₆ ^ 2) ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
mul_zero,

Goal state after:
case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : E.a₄ = 0
ha₆ : E.a₆ ≠ 0
ha₄' : E'.a₄ = 0
ha₆' : -16 * (0 + 27 * E'.a₆ ^ 2) ≠ 0
⊢ ∃ C, C • E = E'
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄✝ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : -16 * (4 * E.a₄ ^ 3 + 27 * 0) ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
mul_zero,

Goal state after:
case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄✝ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : -16 * (4 * E.a₄ ^ 3 + 0) ≠ 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
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 * 0
ha₄✝ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
⊢ E'.a₆ = 0

Tactic:
mul_zero,

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = 0
ha₄✝ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
⊢ E'.a₆ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ

Goal state before:
pp: case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄✝ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : -16 * (4 * E'.a₄ ^ 3 + 27 * 0) ≠ 0
⊢ ∃ C, C • E = E'

Tactic:
mul_zero,

Goal state after:
case pos
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : E.a₄ ^ 3 * E'.a₆ ^ 2 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄✝ : ¬E.a₄ = 0
ha₆ : E.a₆ = 0
ha₄ : E.a₄ ≠ 0
ha₆' : E'.a₆ = 0
ha₄' : -16 * (4 * E'.a₄ ^ 3 + 0) ≠ 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
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 * 0 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
h : E'.a₆ = 0
⊢ False

Tactic:
mul_zero,

Goal state after:
F : Type u_1
inst✝⁶ : Field F
inst✝⁵ : IsSepClosed F
E✝ E'✝ : WeierstrassCurve F
inst✝⁴ : E✝.IsElliptic
inst✝³ : E'✝.IsElliptic
p : ℕ
inst✝² : CharP F p
hchar2 : 2 ≠ 0
hchar3 : 3 ≠ 0
this✝³ : NeZero 2
this✝² : NeZero 4
this✝¹ : NeZero 6
this✝ : Invertible 2 := invertibleOfNonzero hchar2
this : Invertible 3 := invertibleOfNonzero hchar3
E : WeierstrassCurve F
inst✝¹ : E.IsElliptic
h✝¹ : E.IsShortNF
E' : WeierstrassCurve F
inst✝ : E'.IsElliptic
h✝ : E'.IsShortNF
heq : 0 = E'.a₄ ^ 3 * E.a₆ ^ 2
ha₄ : ¬E.a₄ = 0
ha₆ : ¬E.a₆ = 0
ha₄' : E'.a₄ ≠ 0
h : E'.a₆ = 0
⊢ False