awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
⊢ -(W.a₁ * y - (3 * HPow.hPow (β := ℕ) x 2 + 2 * W.a₂ * x + W.a₄)) =
    HPow.hPow (α := R) (β := ℕ) 1 4 *
      (W.a₄ - 0 * W.a₃ + 2 * x * W.a₂ - (y + x * 0) * W.a₁ + 3 * HPow.hPow (β := ℕ) x 2 - HMul.hMul (α := R) 2 0 * y)

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
hΔ : Δ W ≠ 0
simp : W.a₆ = 0 → W.a₃ ≠ 0 ∨ W.a₄ ≠ 0
⊢ W.Equation 0 0 ↔ W.Nonsingular 0 0

Tactic:
simp only [equation_zero, nonsingular_zero, iff_self_and]

Premises used: WeierstrassCurve.Affine.nonsingular_zero, iff_self_and, WeierstrassCurve.Affine.equation_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
hΔ : Δ W ≠ 0
contrapose! : ∀ (hΔ : W.a₆ = 0 ∧ W.a₃ = 0 ∧ W.a₄ = 0), Δ W = 0
⊢ W.a₆ = 0 → W.a₃ ≠ 0 ∨ W.a₄ ≠ 0

Tactic:
contrapose! hΔ
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
hΔ : W.a₆ = 0 ∧ W.a₃ = 0 ∧ W.a₄ = 0
simp :
  -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) 2 *
            (HPow.hPow (β := ℕ) W.a₁ 2 * 0 + 4 * W.a₂ * 0 - W.a₁ * 0 * 0 + W.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 -
              HPow.hPow (α := R) (β := ℕ) 0 2) -
          8 * HPow.hPow (β := ℕ) (HMul.hMul (α := R) 2 0 + W.a₁ * 0) 3 -
        27 * HPow.hPow (β := ℕ) (HPow.hPow (α := R) (β := ℕ) 0 2 + HMul.hMul (α := R) 4 0) 2 +
      9 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) * (HMul.hMul (α := R) 2 0 + W.a₁ * 0) *
        (HPow.hPow (α := R) (β := ℕ) 0 2 + HMul.hMul (α := R) 4 0) =
    0
⊢ Δ W = 0

Tactic:
simp only [b₂, b₄, b₆, b₈, Δ, hΔ]

Premises used: WeierstrassCurve.Δ, WeierstrassCurve.b₂, WeierstrassCurve.b₄, WeierstrassCurve.b₈, WeierstrassCurve.b₆
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
hΔ : W.a₆ = 0 ∧ W.a₃ = 0 ∧ W.a₄ = 0
⊢ -HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) 2 *
            (HPow.hPow (β := ℕ) W.a₁ 2 * 0 + 4 * W.a₂ * 0 - W.a₁ * 0 * 0 + W.a₂ * HPow.hPow (α := R) (β := ℕ) 0 2 -
              HPow.hPow (α := R) (β := ℕ) 0 2) -
          8 * HPow.hPow (β := ℕ) (HMul.hMul (α := R) 2 0 + W.a₁ * 0) 3 -
        27 * HPow.hPow (β := ℕ) (HPow.hPow (α := R) (β := ℕ) 0 2 + HMul.hMul (α := R) 4 0) 2 +
      9 * (HPow.hPow (β := ℕ) W.a₁ 2 + 4 * W.a₂) * (HMul.hMul (α := R) 2 0 + W.a₁ * 0) *
        (HPow.hPow (α := R) (β := ℕ) 0 2 + HMul.hMul (α := R) 4 0) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
rwa : HPow.hPow (β := ℕ) (↑(VariableChange.u { u := 1, r := x, s := 0, t := y : VariableChange R })⁻¹ : R) 12 * Δ W ≠ 0
rwa₁ : HPow.hPow (α := R) (β := ℕ) (↑1 : R) 12 * Δ W ≠ 0
rwa₂ : HPow.hPow (α := R) (β := ℕ) 1 12 * Δ W ≠ 0
rwa₃ : 1 * Δ W ≠ 0
rwa₄ rwa₅ rwa₆ rwa₇ : Δ W ≠ 0
⊢ Δ (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)) ≠ 0

Tactic:
rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]

Premises used: one_pow, inv_one, WeierstrassCurve.variableChange_Δ, Units.val_one, one_mul
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
rw :
  (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Equation 0
      0 ↔
    W.Nonsingular x y
rw₁ :
  (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Equation 0
      0 ↔
    (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Nonsingular
      0 0
rw₂ rw₃ :
  (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Nonsingular 0
      0 ↔
    (toAffine (HSMul.hSMul (α := VariableChange R) { u := 1, r := x, s := 0, t := y : VariableChange R } W)).Nonsingular
      0 0
⊢ W.Equation x y ↔ W.Nonsingular x y

Tactic:
rw [equation_iff_variableChange, nonsingular_iff_variableChange,
    equation_zero_iff_nonsingular_zero_of_Δ_ne_zero <| by
      rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]]

Premises used: WeierstrassCurve.Affine.nonsingular_iff_variableChange, WeierstrassCurve.Affine.equation_iff_variableChange, _private.0.WeierstrassCurve.Affine.equation_zero_iff_nonsingular_zero_of_Δ_ne_zero
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
inst_1 : Nontrivial R
inst_2 : WeierstrassCurve.IsElliptic W
x y : R
⊢ W.Equation x y ↔ W.Nonsingular x y

Tactic:
W.equation_iff_nonsingular_of_Δ_ne_zero <| W.coe_Δ' ▸ W.Δ'.ne_zero

Premises used: Eq.rec, Units.ne_zero, WeierstrassCurve.Affine.equation_iff_nonsingular_of_Δ_ne_zero, WeierstrassCurve.Δ', WeierstrassCurve.coe_Δ'
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
f : R →+* S
⊢ HSub.hSub (β := S[X][Y])
      (HPow.hPow (α := S[X][Y]) (β := ℕ) Y 2 +
        HMul.hMul (α := S[X][Y]) (β := S[X][Y])
          ((C : (a : S[X]) → S[X][Y])
              (HAdd.hAdd (β := S[X]) (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) (W.map f).a₁ : S[X]) X)
                ((C : (a : S) → S[X]) (W.map f).a₃ : S[X])) :
            S[X][Y])
          Y)
      ((C : (a : S[X]) → S[X][Y])
          (HAdd.hAdd (β := S[X])
            (HPow.hPow (α := S[X]) (β := ℕ) X 3 +
                HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (W.map f).a₂ : S[X]) (HPow.hPow (α := S[X]) (β := ℕ) X 2) +
              HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) (W.map f).a₄ : S[X]) X)
            ((C : (a : S) → S[X]) (W.map f).a₆ : S[X])) :
        S[X][Y]) =
    Polynomial.map (mapRingHom f)
      (HSub.hSub (β := R[X][Y])
        (HPow.hPow (α := R[X][Y]) (β := ℕ) Y 2 +
          HMul.hMul (α := R[X][Y]) (β := R[X][Y])
            ((C : (a : R[X]) → R[X][Y])
                (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.a₁ : R[X]) X)
                  ((C : (a : R) → R[X]) W.a₃ : R[X])) :
              R[X][Y])
            Y)
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X])
              (HPow.hPow (α := R[X]) (β := ℕ) X 3 +
                  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) W.a₂ : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.a₄ : R[X]) X)
              ((C : (a : R) → R[X]) W.a₆ : R[X])) :
          R[X][Y]))

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
f : R →+* S
x y : R
h : W.Equation x y
rw : Eq.{s + 1} (α := S) (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (W.map f).polynomial : S) (0 : S)
rw₁ :
  Eq.{s + 1} (α := S)
    (evalEval ((f : (a : R) → S) x) ((f : (a : R) → S) y) (Polynomial.map (mapRingHom f) W.polynomial) : S) (0 : S)
rw₂ : Eq.{s + 1} (α := S) ((f : (a : R) → S) (evalEval x y W.polynomial) : S) (0 : S)
rw₃ : Eq.{s + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)
rw₄ rw₅ : Eq.{s + 1} (α := S) 0 0
⊢ (W.map f).Equation ((f : (a : R) → S) x) ((f : (a : R) → S) y)

Tactic:
rw [Equation, map_polynomial, map_mapRingHom_evalEval, h, map_zero]

Premises used: map_zero, Polynomial.map_mapRingHom_evalEval, WeierstrassCurve.Affine.map_polynomial, WeierstrassCurve.Affine.Equation
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : R
⊢ (W.map f).Equation ((f : (a : R) → S) x) ((f : (a : R) → S) y) ↔ W.Equation x y

Tactic:
simp only [Equation, map_polynomial, map_mapRingHom_evalEval, map_eq_zero_iff f hf]

Premises used: Polynomial.map_mapRingHom_evalEval, WeierstrassCurve.Affine.map_polynomial, map_eq_zero_iff, WeierstrassCurve.Affine.Equation
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
f : R →+* S
⊢ HSub.hSub (β := S[X][Y])
      (HMul.hMul (α := S[X][Y]) (β := S[X][Y])
        ((C : (a : S[X]) → S[X][Y]) ((C : (a : S) → S[X]) (W.map f).a₁) : S[X][Y]) Y)
      ((C : (a : S[X]) → S[X][Y])
          (HAdd.hAdd (β := S[X])
            ((C : (a : S) → S[X]) 3 * HPow.hPow (α := S[X]) (β := ℕ) X 2 +
              HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) (2 * (W.map f).a₂) : S[X]) X)
            ((C : (a : S) → S[X]) (W.map f).a₄ : S[X])) :
        S[X][Y]) =
    Polynomial.map (mapRingHom f)
      (HSub.hSub (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W.a₁) : R[X][Y]) Y)
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X])
              ((C : (a : R) → R[X]) 3 * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
                HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (2 * W.a₂) : R[X]) X)
              ((C : (a : R) → R[X]) W.a₄ : R[X])) :
          R[X][Y]))

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
f : R →+* S
⊢ HAdd.hAdd (β := S[X][Y])
      (HMul.hMul (α := S[X][Y]) (β := S[X][Y]) ((C : (a : S[X]) → S[X][Y]) ((C : (a : S) → S[X]) 2) : S[X][Y]) Y)
      ((C : (a : S[X]) → S[X][Y])
          (HAdd.hAdd (β := S[X]) (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) (W.map f).a₁ : S[X]) X)
            ((C : (a : S) → S[X]) (W.map f).a₃ : S[X])) :
        S[X][Y]) =
    Polynomial.map (mapRingHom f)
      (HAdd.hAdd (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) 2) : R[X][Y]) Y)
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W.a₁ : R[X]) X)
              ((C : (a : R) → R[X]) W.a₃ : R[X])) :
          R[X][Y]))

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x y : R
⊢ (W.map f).Nonsingular ((f : (a : R) → S) x) ((f : (a : R) → S) y) ↔ W.Nonsingular x y

Tactic:
simp only [Nonsingular, evalEval, W.map_equation hf, map_polynomialX, map_polynomialY,
    map_mapRingHom_evalEval, map_ne_zero_iff f hf]

Premises used: WeierstrassCurve.Affine.map_polynomialY, Polynomial.map_mapRingHom_evalEval, Polynomial.evalEval, WeierstrassCurve.Affine.Nonsingular, WeierstrassCurve.Affine.map_equation, WeierstrassCurve.Affine.map_polynomialX, map_ne_zero_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W⁄A).map (↑f : A →+* B) = W⁄B

Tactic:
WeierstrassCurve.map_baseChange W f

Premises used: WeierstrassCurve.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := B[X][Y]) (W⁄B).polynomial ((W⁄A).map (↑f : A →+* B)).polynomial
rw₁ rw₂ : Eq (α := B[X][Y]) (W⁄B).polynomial (W⁄B).polynomial
⊢ Eq (α := B[X][Y]) (W⁄B).polynomial (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).polynomial)

Tactic:
rw [← map_polynomial, map_baseChange]

Premises used: WeierstrassCurve.Affine.map_baseChange, WeierstrassCurve.Affine.map_polynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
x y : A
h : (W⁄A).Equation x y
⊢ ((W⁄A).map f.toRingHom).Equation ((f.toRingHom : (a : A) → B) x) ((f.toRingHom : (a : A) → B) y)

Tactic:
Equation.map f.toRingHom h

Premises used: AlgHom.toRingHom, WeierstrassCurve.Affine.Equation.map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
x y : A
h : (W⁄A).Equation x y
h₁ : W⁄B = (W⁄A).map f.toRingHom
⊢ (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y)

Tactic:
convert! Equation.map f.toRingHom h using 1

Premises used: AlgHom.toRingHom, WeierstrassCurve.Affine.Equation.map
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
x y : A
h : (W⁄A).Equation x y
h₁ : W⁄B = (W⁄A).map (↑f : A →+* B)
h₂ h₃ : W⁄B = W⁄B
⊢ W⁄B = (W⁄A).map f.toRingHom

Tactic:
rw [AlgHom.toRingHom_eq_coe, map_baseChange]

Premises used: WeierstrassCurve.Affine.map_baseChange, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
x y : A
rw :
  (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map f.toRingHom).Equation ((f.toRingHom : (a : A) → B) x) ((f.toRingHom : (a : A) → B) y)
rw₁ :
  (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map (↑f : A →+* B)).Equation (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
rw₂ :
  (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    (W⁄B).Equation (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
rw₃ rw₄ :
  (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y)
⊢ (W⁄B).Equation ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔ (W⁄A).Equation x y

Tactic:
rw [← map_equation _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]

Premises used: RingHom.coe_coe, WeierstrassCurve.Affine.map_baseChange, WeierstrassCurve.Affine.map_equation, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := B[X][Y]) (W⁄B).polynomialX ((W⁄A).map (↑f : A →+* B)).polynomialX
rw₁ rw₂ : Eq (α := B[X][Y]) (W⁄B).polynomialX (W⁄B).polynomialX
⊢ Eq (α := B[X][Y]) (W⁄B).polynomialX (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).polynomialX)

Tactic:
rw [← map_polynomialX, map_baseChange]

Premises used: WeierstrassCurve.Affine.map_baseChange, WeierstrassCurve.Affine.map_polynomialX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := B[X][Y]) (W⁄B).polynomialY ((W⁄A).map (↑f : A →+* B)).polynomialY
rw₁ rw₂ : Eq (α := B[X][Y]) (W⁄B).polynomialY (W⁄B).polynomialY
⊢ Eq (α := B[X][Y]) (W⁄B).polynomialY (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).polynomialY)

Tactic:
rw [← map_polynomialY, map_baseChange]

Premises used: WeierstrassCurve.Affine.map_polynomialY, WeierstrassCurve.Affine.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
Goal:
R : Type r
inst : CommRing R
W : Affine R
S : Type s
inst_1 : CommRing S
A : Type u
inst_2 : CommRing A
B : Type v
inst_3 : CommRing B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective.{u + 1, v + 1} (α := A) (β := B) (⇑f : (a : A) → B)
x y : A
rw :
  (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map f.toRingHom).Nonsingular ((f.toRingHom : (a : A) → B) x) ((f.toRingHom : (a : A) → B) y)
rw₁ :
  (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    ((W⁄A).map (↑f : A →+* B)).Nonsingular (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
rw₂ :
  (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    (W⁄B).Nonsingular (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
rw₃ rw₄ :
  (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔
    (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y)
⊢ (W⁄B).Nonsingular ((f : (a : A) → B) x) ((f : (a : A) → B) y) ↔ (W⁄A).Nonsingular x y

Tactic:
rw [← map_nonsingular _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]

Premises used: RingHom.coe_coe, WeierstrassCurve.Affine.map_baseChange, WeierstrassCurve.Affine.map_nonsingular, AlgHom.toRingHom_eq_coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
C_simp :
  Y -
      (HMul.hMul (α := R[X][Y]) 2 Y +
        HAdd.hAdd (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
            ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y])) =
    -Y -
      HAdd.hAdd (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y])
⊢ Y -
      HAdd.hAdd (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) 2) : R[X][Y]) Y)
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
          R[X][Y]) =
    HSub.hSub (α := R[X][Y]) (β := R[X][Y]) (-Y)
      ((C : (a : R[X]) → R[X][Y])
          (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
            ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
        R[X][Y])

Tactic:
C_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
⊢ Y -
      (HMul.hMul (α := R[X][Y]) 2 Y +
        HAdd.hAdd (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
            ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
          ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y])) =
    -Y -
      HAdd.hAdd (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₁) : R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]))
        ((C : (a : R[X]) → R[X][Y]) ((C : (a : R) → R[X]) W'.a₃) : R[X][Y])

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
rw : Y - HSub.hSub (α := R[X][Y]) Y W'.polynomialY = W'.polynomialY
rw₁ rw₂ : Eq (α := R[X][Y]) W'.polynomialY W'.polynomialY
⊢ HSub.hSub (α := R[X][Y]) Y W'.negPolynomial = W'.polynomialY

Tactic:
rw [← Y_sub_polynomialY, sub_sub_cancel]

Premises used: WeierstrassCurve.Affine.Y_sub_polynomialY, sub_sub_cancel
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
simp : -(-y - W'.a₁ * x - W'.a₃) - W'.a₁ * x - W'.a₃ = y
⊢ W'.negY x (W'.negY x y) = y

Tactic:
simp only [negY]

Premises used: WeierstrassCurve.Affine.negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
⊢ -(-y - W'.a₁ * x - W'.a₃) - W'.a₁ * x - W'.a₃ = y

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
rw :
  evalEval x y
      (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) (-Y)
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
          R[X][Y])) =
    -y - (W'.a₁ * x + W'.a₃)
⊢ evalEval x y W'.negPolynomial = W'.negY x y

Tactic:
rw [negY, sub_sub, negPolynomial]

Premises used: WeierstrassCurve.Affine.negY, sub_sub, WeierstrassCurve.Affine.negPolynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y
      (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) (-Y)
        ((C : (a : R[X]) → R[X][Y])
            (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) W'.a₁ : R[X]) X)
              ((C : (a : R) → R[X]) W'.a₃ : R[X])) :
          R[X][Y])) =
    -y - (W'.a₁ * x + W'.a₃)

Tactic:
eval_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hx : x₁ = x₂
⊢ HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆

Tactic:
rw [equation_iff] at h₁ h₂

Premises used: WeierstrassCurve.Affine.equation_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hx : x₁ = x₂
h₃ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
⊢ HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ =
    HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆

Tactic:
rw [equation_iff] at h₁ h₂

Premises used: WeierstrassCurve.Affine.equation_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hx : x₁ = x₂
h₃ :
  HPow.hPow (β := ℕ) y₁ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ =
    HPow.hPow (β := ℕ) x₁ 3 + W.a₂ * HPow.hPow (β := ℕ) x₁ 2 + W.a₄ * x₁ + W.a₆
h₄ :
  HPow.hPow (β := ℕ) y₂ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ =
    HPow.hPow (β := ℕ) x₂ 3 + W.a₂ * HPow.hPow (β := ℕ) x₂ 2 + W.a₄ * x₂ + W.a₆
⊢ x₁ = x₂

Tactic:
rw [equation_iff] at h₁ h₂

Premises used: WeierstrassCurve.Affine.equation_iff