awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
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 := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (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
rw :
  (↑((1 * HPow.hPow (β := ℕ) (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) :
    R)
| 1

Tactic:
rw [← Int.cast_one, hc]

Premises used: Int.cast_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
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 := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (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
succ :
  ((1 * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (n + 1 + 1)) : R) 2 * if Even (n + 1) then 1 else 4) -
      HMul.hMul (α := R) (↑(expCoeff (n + 1 + 2)) : R) (↑(expCoeff (n + 1)) : R) * if Even (n + 1) then 4 else 1) =
    (↑((1 * HPow.hPow (β := ℕ) (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) :
      R)
⊢ ((1 * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (n + 1 + 1)) : R) 2 * if Even (n + 1) then 1 else 4) -
      HMul.hMul (α := R) (↑(expCoeff (n + 1 + 2)) : R) (↑(expCoeff (n + 1)) : R) * if Even (n + 1) then 4 else 1) =
    1

Tactic:
conv_rhs => rw [← Int.cast_one, hc]

Premises used: Int.cast_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
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 := ⋯
dp : ∀ {m n : ℕ} {p : R[X]}, p.natDegree ≤ m → (p ^ n).natDegree ≤ n * m := ⋯
cm : ∀ {m n : ℕ} {p q : R[X]}, p.natDegree ≤ m → q.natDegree ≤ n → (p * q).coeff (m + n) = p.coeff m * q.coeff n := ⋯
h : ∀ {n : ℕ}, natDegree (W.preΨ' n) ≤ expDegree n ∧ coeff (W.preΨ' n) (expDegree n) = (↑(expCoeff n) : R) := ⋯
n : ℕ
hd : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = 1 + 2 * expDegree (n + 2) + if Even (n + 1) then 0 else 3
hd' : HPow.hPow (β := ℕ) (n + 1 + 1) 2 = expDegree (n + 3) + expDegree (n + 1) + if Even (n + 1) then 3 else 0
hc :
  1 =
    (1 * HPow.hPow (β := ℕ) (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
succ succ₁ succ₂ succ₃ :
  Eq.{u + 1} (α := R)
    (↑(1 * HPow.hPow (β := ℕ) (expCoeff (n + 1 + 1)) 2 * (↑(if Even (n + 1) then 1 else 4) : ℤ) -
          expCoeff (n + 1 + 2) * expCoeff (n + 1) * (↑(if Even (n + 1) then 4 else 1) : ℤ)) :
      R)
    (↑(1 * HPow.hPow (β := ℕ) (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) : ℤ)) :
      R)
⊢ ((1 * HPow.hPow (α := R) (β := ℕ) (↑(expCoeff (n + 1 + 1)) : R) 2 * if Even (n + 1) then 1 else 4) -
      HMul.hMul (α := R) (↑(expCoeff (n + 1 + 2)) : R) (↑(expCoeff (n + 1)) : R) * if Even (n + 1) then 4 else 1) =
    (↑((1 * HPow.hPow (β := ℕ) (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) :
      R)

Tactic:
norm_cast
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2

Tactic:
(W.natDegree_coeff_Φ_ofNat n).left

Premises used: And.left, _private.0.WeierstrassCurve.natDegree_coeff_Φ_ofNat, Int.natAbs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2

Tactic:
exact (W.natDegree_coeff_Φ_ofNat n).left

Premises used: And.left, _private.0.WeierstrassCurve.natDegree_coeff_Φ_ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2
n : ℕ
neg : natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2
neg₁ : natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2
⊢ natDegree (W.Φ (-(↑n : ℤ))) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2

Tactic:
simp_rw [Φ_neg, Int.natAbs_neg, ih]

Premises used: WeierstrassCurve.Φ_neg, Int.natAbs_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
nat : ∀ (n : ℕ), natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2
neg :
  ∀ (ih : ∀ (n : ℕ), natDegree (W.Φ (↑n : ℤ)) ≤ HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) (n : ℕ),
    natDegree (W.Φ (-(↑n : ℤ))) ≤ HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2
⊢ natDegree (W.Φ n) ≤ HPow.hPow (β := ℕ) n.natAbs 2

Tactic:
induction n using Int.negInduction with
  | nat n => exact (W.natDegree_coeff_Φ_ofNat n).left
  | neg ih => simp_rw [Φ_neg, Int.natAbs_neg, ih]

Premises used: WeierstrassCurve.Φ_neg, Int.natAbs_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1

Tactic:
(W.natDegree_coeff_Φ_ofNat n).right

Premises used: And.right, _private.0.WeierstrassCurve.natDegree_coeff_Φ_ofNat, Int.natAbs
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1

Tactic:
exact (W.natDegree_coeff_Φ_ofNat n).right

Premises used: And.right, _private.0.WeierstrassCurve.natDegree_coeff_Φ_ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1
n : ℕ
neg : coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2) = 1
neg₁ : coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1
neg₂ neg₃ : Eq.{u + 1} (α := R) 1 1
⊢ coeff (W.Φ (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2) = 1

Tactic:
rw [Φ_neg, Int.natAbs_neg, ih]

Premises used: WeierstrassCurve.Φ_neg, Int.natAbs_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
nat : ∀ (n : ℕ), coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1
neg :
  ∀ (ih : ∀ (n : ℕ), coeff (W.Φ (↑n : ℤ)) (HPow.hPow (β := ℕ) (Int.natAbs (↑n : ℤ)) 2) = 1) (n : ℕ),
    coeff (W.Φ (-(↑n : ℤ))) (HPow.hPow (β := ℕ) (Int.natAbs (-(↑n : ℤ))) 2) = 1
⊢ coeff (W.Φ n) (HPow.hPow (β := ℕ) n.natAbs 2) = 1

Tactic:
induction n using Int.negInduction with
  | nat n => exact (W.natDegree_coeff_Φ_ofNat n).right
  | neg ih => rw [Φ_neg, Int.natAbs_neg, ih]

Premises used: WeierstrassCurve.Φ_neg, Int.natAbs_neg
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
⊢ coeff (W.Φ n) (HPow.hPow (β := ℕ) n.natAbs 2) ≠ 0

Tactic:
W.coeff_Φ n ▸ one_ne_zero

Premises used: Eq.rec, WeierstrassCurve.coeff_Φ, one_ne_zero, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
⊢ natDegree (W.Φ n) = HPow.hPow (β := ℕ) n.natAbs 2

Tactic:
natDegree_eq_of_le_of_coeff_ne_zero (W.natDegree_Φ_le n) <| W.coeff_Φ_ne_zero n

Premises used: WeierstrassCurve.coeff_Φ_ne_zero, WeierstrassCurve.natDegree_Φ_le, Polynomial.natDegree_eq_of_le_of_coeff_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
hn : n ≠ 0
⊢ 0 < natDegree (W.Φ n)

Tactic:
simpa [sq_pos_iff]

Premises used: sq_pos_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
rw : coeff (W.Φ n) (natDegree (W.Φ n)) = 1
rw₁ : coeff (W.Φ n) (HPow.hPow (β := ℕ) n.natAbs 2) = 1
rw₂ rw₃ : Eq.{u + 1} (α := R) 1 1
⊢ leadingCoeff (W.Φ n) = 1

Tactic:
rw [leadingCoeff, natDegree_Φ, coeff_Φ]

Premises used: Polynomial.leadingCoeff, WeierstrassCurve.coeff_Φ, WeierstrassCurve.natDegree_Φ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
pos : ∀ (hn : n = 0), Ne (α := R[X]) (W.Φ n) 0
neg : ∀ (hn : ¬n = 0), Ne (α := R[X]) (W.Φ n) 0
⊢ Ne (α := R[X]) (W.Φ n) 0

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
hn : n = 0
⊢ Ne (α := R[X]) (W.Φ n) 0

Tactic:
simpa only [hn, Φ_zero] using one_ne_zero

Premises used: one_ne_zero, WeierstrassCurve.Φ_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
hn : ¬n = 0
⊢ Ne (α := R[X]) (W.Φ n) 0

Tactic:
ne_zero_of_natDegree_gt <| W.natDegree_Φ_pos hn

Premises used: Polynomial.ne_zero_of_natDegree_gt, WeierstrassCurve.natDegree_Φ_pos
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
Goal:
R : Type u
inst : CommRing R
W : WeierstrassCurve R
inst_1 : Nontrivial R
n : ℤ
hn : ¬n = 0
⊢ Ne (α := R[X]) (W.Φ n) 0

Tactic:
exact ne_zero_of_natDegree_gt <| W.natDegree_Φ_pos hn

Premises used: Polynomial.ne_zero_of_natDegree_gt, WeierstrassCurve.natDegree_Φ_pos
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
⊢ Dvd.dvd (α := ℕ) 2 2

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
⊢ LE.le (α := ℕ) 2 2

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
obtain : ∀ (s : F) (hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0), ∃ (C : VariableChange F), C • E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
obtain ⟨s, hs⟩ := IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' 2 2
    1 1 (E.a₂ + E'.a₂) (by simp) (by simp) one_ne_zero

Premises used: WeierstrassCurve.a₂, HAdd.hAdd, IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C', one_ne_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
h : HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E = E'
⊢ ∃ (C : VariableChange F), C • E = E'

Tactic:
use ⟨1, 0, s, 0⟩
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
h : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₁ = E'.a₁
h₁ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₂ = E'.a₂
h₂ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₃ = E'.a₃
h₃ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₄ = E'.a₄
h₄ : (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₆ = E'.a₆
⊢ HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E = E'

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
h : 1 * (1 + 2 * s) = 1
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₁ = E'.a₁

Tactic:
simp_rw [variableChange_a₁, inv_one, Units.val_one, a₁_of_isCharTwoJNeZeroNF]

Premises used: WeierstrassCurve.variableChange_a₁, inv_one, WeierstrassCurve.a₁_of_isCharTwoJNeZeroNF, Units.val_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 * (1 + 2 * s) = 1

Tactic:
linear_combination s * CharP.cast_eq_zero F 2

Premises used: CharP.cast_eq_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
h : HPow.hPow (α := F) (β := ℕ) 1 2 * (E.a₂ - s * 1 + HMul.hMul (α := F) 3 0 - HPow.hPow (β := ℕ) s 2) = E'.a₂
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₂ = E'.a₂

Tactic:
simp_rw [variableChange_a₂, inv_one, Units.val_one, a₁_of_isCharTwoJNeZeroNF]

Premises used: inv_one, WeierstrassCurve.a₁_of_isCharTwoJNeZeroNF, WeierstrassCurve.variableChange_a₂, Units.val_one
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ HPow.hPow (α := F) (β := ℕ) 1 2 * (E.a₂ - s * 1 + HMul.hMul (α := F) 3 0 - HPow.hPow (β := ℕ) s 2) = E'.a₂

Tactic:
linear_combination -hs + E.a₂ * CharP.cast_eq_zero F 2

Premises used: CharP.cast_eq_zero, WeierstrassCurve.a₂, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
h : HPow.hPow (α := F) (β := ℕ) 1 3 * (0 + 0 * E.a₁ + HMul.hMul (α := F) 2 0) = 0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₃ = E'.a₃

Tactic:
simp_rw [variableChange_a₃, inv_one, Units.val_one, a₃_of_isCharTwoJNeZeroNF]

Premises used: inv_one, WeierstrassCurve.variableChange_a₃, Units.val_one, WeierstrassCurve.a₃_of_isCharTwoJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ HPow.hPow (α := F) (β := ℕ) 1 3 * (0 + 0 * E.a₁ + HMul.hMul (α := F) 2 0) = 0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
h :
  HPow.hPow (α := F) (β := ℕ) 1 4 *
      (0 - s * 0 + HMul.hMul (α := F) 2 0 * E.a₂ - (0 + 0 * s) * E.a₁ + 3 * HPow.hPow (α := F) (β := ℕ) 0 2 -
        2 * s * 0) =
    0
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₄ = E'.a₄

Tactic:
simp_rw [variableChange_a₄, inv_one, Units.val_one, a₃_of_isCharTwoJNeZeroNF,
      a₄_of_isCharTwoJNeZeroNF]

Premises used: inv_one, WeierstrassCurve.variableChange_a₄, Units.val_one, WeierstrassCurve.a₄_of_isCharTwoJNeZeroNF, WeierstrassCurve.a₃_of_isCharTwoJNeZeroNF
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ HPow.hPow (α := F) (β := ℕ) 1 4 *
      (0 - s * 0 + HMul.hMul (α := F) 2 0 * E.a₂ - (0 + 0 * s) * E.a₁ + 3 * HPow.hPow (α := F) (β := ℕ) 0 2 -
        2 * s * 0) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
h :
  HPow.hPow (α := F) (β := ℕ) 1 6 *
      (E'.a₆ + 0 * E.a₄ + HPow.hPow (α := F) (β := ℕ) 0 2 * E.a₂ + HPow.hPow (α := F) (β := ℕ) 0 3 - 0 * E.a₃ -
          HPow.hPow (α := F) (β := ℕ) 0 2 -
        HMul.hMul (α := F) 0 0 * E.a₁) =
    E'.a₆
⊢ (HSMul.hSMul (α := VariableChange F) { u := 1, r := 0, s := s, t := 0 : VariableChange F } E).a₆ = E'.a₆

Tactic:
simp_rw [variableChange_a₆, inv_one, Units.val_one, heq]

Premises used: inv_one, Units.val_one, WeierstrassCurve.variableChange_a₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : CharP F 2
inst_3 : E.IsCharTwoJNeZeroNF
inst_4 : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * HPow.hPow (β := ℕ) s 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ HPow.hPow (α := F) (β := ℕ) 1 6 *
      (E'.a₆ + 0 * E.a₄ + HPow.hPow (α := F) (β := ℕ) 0 2 * E.a₂ + HPow.hPow (α := F) (β := ℕ) 0 3 - 0 * E.a₃ -
          HPow.hPow (α := F) (β := ℕ) 0 2 -
        HMul.hMul (α := F) 0 0 * E.a₁) =
    E'.a₆

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
⊢ (↑E.Δ' : F) ≠ 0

Tactic:
have ha₃ := E.Δ'.ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : (↑E.Δ' : F) ≠ 0
⊢ E.a₃ ≠ 0

Tactic:
rw [E.coe_Δ', Δ_of_isCharTwoJEqZeroNF_of_char_two, pow_ne_zero_iff (Nat.succ_ne_zero _)] at ha₃

Premises used: Nat.succ_ne_zero, WeierstrassCurve.coe_Δ', WeierstrassCurve.Δ_of_isCharTwoJEqZeroNF_of_char_two, pow_ne_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
⊢ (↑E'.Δ' : F) ≠ 0

Tactic:
have ha₃' := E'.Δ'.ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : (↑E'.Δ' : F) ≠ 0
⊢ E'.a₃ ≠ 0

Tactic:
rw [E'.coe_Δ', Δ_of_isCharTwoJEqZeroNF_of_char_two, pow_ne_zero_iff (Nat.succ_ne_zero _)] at ha₃'

Premises used: Nat.succ_ne_zero, WeierstrassCurve.coe_Δ', WeierstrassCurve.Δ_of_isCharTwoJEqZeroNF_of_char_two, pow_ne_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
⊢ Eq.{u_1 + 1} (α := F) 3 1

Tactic:
linear_combination CharP.cast_eq_zero F 2

Premises used: CharP.cast_eq_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
rw : Ne.{u_1 + 1} (α := F) 1 0
⊢ Ne.{u_1 + 1} (α := F) 3 0

Tactic:
rw [show (3 : F) = 1 by linear_combination CharP.cast_eq_zero F 2]
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
⊢ Ne.{u_1 + 1} (α := F) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
⊢ Ne.{u_1 + 1} (α := F) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
Goal:
F : Type u_1
inst : Field F
inst_1 : IsSepClosed F
E E' : WeierstrassCurve F
inst_2 : E.IsElliptic
inst_3 : E'.IsElliptic
inst_4 : CharP F 2
inst_5 : E.IsCharTwoJEqZeroNF
inst_6 : E'.IsCharTwoJEqZeroNF
ha₃ : E.a₃ ≠ 0
ha₃' : E'.a₃ ≠ 0
⊢ NeZero.{u_1} (R := F) 3

Tactic:
haveI : NeZero (3 : F) := NeZero.mk <| by
    rw [show (3 : F) = 1 by linear_combination CharP.cast_eq_zero F 2]
    exact one_ne_zero