awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ y₁ *
          (x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
            ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - HPow.hPow (β := ℕ) (x₁ - x₂) 2 * W.a₂ -
                x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
              x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2)) +
        y₂ *
          ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - HPow.hPow (β := ℕ) (x₁ - x₂) 2 * W.a₂ -
                x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
              x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
            x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2) +
      ((y₁ - y₂) *
          ((y₁ - y₂) * (y₁ - y₂ + (x₁ - x₂) * W.a₁) - HPow.hPow (β := ℕ) (x₁ - x₂) 2 * W.a₂ -
                x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
              x₂ * HPow.hPow (β := ℕ) (x₁ - x₂) 2 -
            x₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 2) +
        y₁ * HPow.hPow (β := ℕ) (x₁ - x₂) 3) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
simp_rw :
  (-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃ -
        (-(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃) -
            W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) -
          W.a₃)) *
      (x₂ - x₁) =
    (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
⊢ let x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂);
  let y₃ := W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂);
  y₃ - W.negY x₃ y₃ = ((y₂ - W.negY x₂ y₂) * (x₁ - x₃) - (y₁ - W.negY x₁ y₁) * (x₂ - x₃)) / (x₂ - x₁)

Tactic:
simp_rw [addY, negY, eq_div_iff (sub_ne_zero.mpr hx.symm)]

Premises used: Iff.mpr, sub_ne_zero, Ne.symm, WeierstrassCurve.Affine.negY, WeierstrassCurve.Affine.addY, eq_div_iff
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
⊢ (-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃ -
            (-(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃) -
                W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) -
              W.a₃)) *
          (x₂ - x₁) +
        HMul.hMul (α := F) 2 0 -
      ((y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
          (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
        2 *
          (y₁ * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) +
            W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂))) =
    0

Tactic:
ring1
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
hx : x₁ ≠ x₂
a :
  (-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃ -
            (-(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃) -
                W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) -
              W.a₃)) *
          (x₂ - x₁) +
        HMul.hMul (α := F) 2 0 -
      ((y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
          (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) +
        2 *
          (y₁ * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) +
            W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂))) =
    0
⊢ (-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃ -
        (-(-W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.a₃) -
            W.a₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) -
          W.a₃)) *
      (x₂ - x₁) =
    (y₂ - (-y₂ - W.a₁ * x₂ - W.a₃)) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) -
      (y₁ - (-y₁ - W.a₁ * x₁ - W.a₃)) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))

Tactic:
linear_combination (norm := ring1) 2 * cyclic_sum_Y_mul_X_sub_X y₁ y₂ hx

Premises used: WeierstrassCurve.Affine.cyclic_sum_Y_mul_X_sub_X
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
⊢ HSub.hSub (α := S[X][Y]) (β := 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)
      (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:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x y : R
simp :
  HSub.hSub (α := S) (-(f : (a : R) → S) y : S) (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) x : S)) -
      (W'.map f).a₃ =
    (f : (a : R) → S) (-y - W'.a₁ * x - W'.a₃)
⊢ (W'.map f).negY ((f : (a : R) → S) x) ((f : (a : R) → S) y) = (f : (a : R) → S) (W'.negY x y)

Tactic:
simp only [negY]

Premises used: WeierstrassCurve.Affine.negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x y : R
⊢ HSub.hSub (α := S) (-(f : (a : R) → S) y : S) (HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) x : S)) -
      (W'.map f).a₃ =
    (f : (a : R) → S) (-y - W'.a₁ * x - W'.a₃)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
x y ℓ : R
⊢ HAdd.hAdd (β := S[X])
      (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) ℓ) : S[X])
        (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) ((f : (a : R) → S) x) : S[X])))
      ((C : (a : S) → S[X]) ((f : (a : R) → S) y) : S[X]) =
    Polynomial.map f
      (HAdd.hAdd (β := R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
          (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
        ((C : (a : R) → R[X]) y : R[X]))

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x y ℓ : R
rw :
  eval₂ (mapRingHom f)
      (HAdd.hAdd (β := S[X])
        (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) ℓ) : S[X])
          (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) ((f : (a : R) → S) x) : S[X])))
        ((C : (a : S) → S[X]) ((f : (a : R) → S) y) : S[X]))
      W'.polynomial =
    eval₂ (mapRingHom f)
      ((mapRingHom f : (a : R[X]) → S[X])
        (HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
          ((C : (a : R) → R[X]) y : R[X])))
      W'.polynomial
⊢ (W'.map f).addPolynomial ((f : (a : R) → S) x) ((f : (a : R) → S) y) ((f : (a : R) → S) ℓ) =
    Polynomial.map f (W'.addPolynomial x y ℓ)

Tactic:
rw [addPolynomial, map_polynomial, eval_map, linePolynomial, addPolynomial, ← coe_mapRingHom,
    ← eval₂_hom, linePolynomial]

Premises used: Polynomial.eval_map, Polynomial.eval₂_hom, WeierstrassCurve.Affine.map_polynomial, Polynomial.coe_mapRingHom, WeierstrassCurve.Affine.addPolynomial, WeierstrassCurve.Affine.linePolynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x y ℓ : R
⊢ eval₂ (mapRingHom f)
      (HAdd.hAdd (β := S[X])
        (HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) ℓ) : S[X])
          (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) ((f : (a : R) → S) x) : S[X])))
        ((C : (a : S) → S[X]) ((f : (a : R) → S) y) : S[X]))
      W'.polynomial =
    eval₂ (mapRingHom f)
      ((mapRingHom f : (a : R[X]) → S[X])
        (HAdd.hAdd (β := R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ℓ : R[X])
            (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])))
          ((C : (a : R) → R[X]) y : R[X])))
      W'.polynomial

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x₁ x₂ ℓ : R
simp :
  HSub.hSub (β := S)
      (HSub.hSub (β := S)
        (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) ℓ : S) 2 +
            HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) ℓ : S) -
          (W'.map f).a₂)
        ((f : (a : R) → S) x₁ : S))
      ((f : (a : R) → S) x₂ : S) =
    (f : (a : R) → S) (HPow.hPow (β := ℕ) ℓ 2 + W'.a₁ * ℓ - W'.a₂ - x₁ - x₂)
⊢ (W'.map f).addX ((f : (a : R) → S) x₁) ((f : (a : R) → S) x₂) ((f : (a : R) → S) ℓ) =
    (f : (a : R) → S) (W'.addX x₁ x₂ ℓ)

Tactic:
simp only [addX]

Premises used: WeierstrassCurve.Affine.addX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x₁ x₂ ℓ : R
⊢ HSub.hSub (β := S)
      (HSub.hSub (β := S)
        (HPow.hPow (α := S) (β := ℕ) ((f : (a : R) → S) ℓ : S) 2 +
            HMul.hMul (β := S) (W'.map f).a₁ ((f : (a : R) → S) ℓ : S) -
          (W'.map f).a₂)
        ((f : (a : R) → S) x₁ : S))
      ((f : (a : R) → S) x₂ : S) =
    (f : (a : R) → S) (HPow.hPow (β := ℕ) ℓ 2 + W'.a₁ * ℓ - W'.a₂ - x₁ - x₂)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x₁ y₁ x₂ ℓ : R
simp :
  HAdd.hAdd (β := S)
      (HMul.hMul (α := S) ((f : (a : R) → S) ℓ : S)
        (HSub.hSub (α := S) (β := S) ((f : (a : R) → S) (W'.addX x₁ x₂ ℓ) : S) ((f : (a : R) → S) x₁ : S)))
      ((f : (a : R) → S) y₁ : S) =
    (f : (a : R) → S) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
⊢ (W'.map f).negAddY ((f : (a : R) → S) x₁) ((f : (a : R) → S) x₂) ((f : (a : R) → S) y₁) ((f : (a : R) → S) ℓ) =
    (f : (a : R) → S) (W'.negAddY x₁ x₂ y₁ ℓ)

Tactic:
simp only [negAddY, map_addX]

Premises used: WeierstrassCurve.Affine.negAddY, WeierstrassCurve.Affine.map_addX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x₁ y₁ x₂ ℓ : R
⊢ HAdd.hAdd (β := S)
      (HMul.hMul (α := S) ((f : (a : R) → S) ℓ : S)
        (HSub.hSub (α := S) (β := S) ((f : (a : R) → S) (W'.addX x₁ x₂ ℓ) : S) ((f : (a : R) → S) x₁ : S)))
      ((f : (a : R) → S) y₁ : S) =
    (f : (a : R) → S) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x₁ y₁ x₂ ℓ : R
⊢ (W'.map f).addY ((f : (a : R) → S) x₁) ((f : (a : R) → S) x₂) ((f : (a : R) → S) y₁) ((f : (a : R) → S) ℓ) =
    (f : (a : R) → S) (W'.addY x₁ x₂ y₁ ℓ)

Tactic:
simp only [addY, map_negAddY, map_addX, map_negY]

Premises used: WeierstrassCurve.Affine.addY, WeierstrassCurve.Affine.map_negAddY, WeierstrassCurve.Affine.map_negY, WeierstrassCurve.Affine.map_addX
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
pos :
  ∀ (hx : x₁ = x₂),
    (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
      (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
neg :
  ∀ (hx : ¬x₁ = x₂),
    (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
      (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)

Tactic:
by_cases hx : x₁ = x₂
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
pos :
  ∀ (hy : y₁ = W.negY x₂ y₂),
    (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
      (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
neg :
  ∀ (hy : ¬y₁ = W.negY x₂ y₂),
    (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
      (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)

Tactic:
by_cases hy : y₁ = W.negY x₂ y₂

Premises used: WeierstrassCurve.Affine.negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
rw : (f : (a : F) → K) (W.negY x₂ y₂) = (W.map f).negY ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₂)
rw₁ rw₂ : Eq.{v + 1} (α := K) ((f : (a : F) → K) (W.negY x₂ y₂) : K) ((f : (a : F) → K) (W.negY x₂ y₂) : K)
⊢ (f : (a : F) → K) y₁ = (W.map f).negY ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₂)

Tactic:
rw [hy, map_negY]

Premises used: WeierstrassCurve.Affine.map_negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
pos : Eq.{v + 1} (α := K) (0 : K) ((f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂) : K)
pos₁ : Eq.{v + 1} (α := K) (0 : K) ((f : (a : F) → K) 0 : K)
pos₂ pos₃ : Eq.{v + 1} (α := K) 0 0
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)

Tactic:
rw [slope_of_Y_eq (congr_arg f hx) <| by rw [hy, map_negY], slope_of_Y_eq hx hy, map_zero]

Premises used: map_zero, congr_arg, WeierstrassCurve.Affine.slope_of_Y_eq, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
neg :
  (3 * HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) x₁ : K) 2 +
            HMul.hMul (β := K) (2 * (W.map f).a₂) ((f : (a : F) → K) x₁ : K) +
          (W.map f).a₄ -
        HMul.hMul (β := K) (W.map f).a₁ ((f : (a : F) → K) y₁ : K)) /
      HSub.hSub (α := K) (β := K) ((f : (a : F) → K) y₁ : K) ((f : (a : F) → K) (W.negY x₁ y₁) : K) =
    (f : (a : F) → K) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)

Tactic:
rw [slope_of_Y_ne (congr_arg f hx) <| map_negY f x₂ y₂ ▸ fun h => hy <| f.injective h,
        map_negY, slope_of_Y_ne hx hy]

Premises used: WeierstrassCurve.Affine.slope_of_Y_ne, congr_arg, WeierstrassCurve.Affine.map_negY, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
⊢ (3 * HPow.hPow (α := K) (β := ℕ) ((f : (a : F) → K) x₁ : K) 2 +
            HMul.hMul (β := K) (2 * (W.map f).a₂) ((f : (a : F) → K) x₁ : K) +
          (W.map f).a₄ -
        HMul.hMul (β := K) (W.map f).a₁ ((f : (a : F) → K) y₁ : K)) /
      HSub.hSub (α := K) (β := K) ((f : (a : F) → K) y₁ : K) ((f : (a : F) → K) (W.negY x₁ y₁) : K) =
    (f : (a : F) → K) ((3 * HPow.hPow (β := ℕ) x₁ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : ¬x₁ = x₂
neg :
  HSub.hSub (α := K) (β := K) ((f : (a : F) → K) y₁ : K) ((f : (a : F) → K) y₂ : K) /
      HSub.hSub (α := K) (β := K) ((f : (a : F) → K) x₁ : K) ((f : (a : F) → K) x₂ : K) =
    (f : (a : F) → K) ((y₁ - y₂) / (x₁ - x₂))
⊢ (W.map f).slope ((f : (a : F) → K) x₁) ((f : (a : F) → K) x₂) ((f : (a : F) → K) y₁) ((f : (a : F) → K) y₂) =
    (f : (a : F) → K) (W.slope x₁ x₂ y₁ y₂)

Tactic:
rw [slope_of_X_ne fun h => hx <| f.injective h, slope_of_X_ne hx]

Premises used: WeierstrassCurve.Affine.slope_of_X_ne, RingHom.injective
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
F : Type u
K : Type v
inst : Field F
inst_1 : Field K
W : Affine F
inst_2 : DecidableEq F
inst_3 : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : ¬x₁ = x₂
⊢ HSub.hSub (α := K) (β := K) ((f : (a : F) → K) y₁ : K) ((f : (a : F) → K) y₂ : K) /
      HSub.hSub (α := K) (β := K) ((f : (a : F) → K) x₁ : K) ((f : (a : F) → K) x₂ : K) =
    (f : (a : F) → K) ((y₁ - y₂) / (x₁ - x₂))

Tactic:
map_simp
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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).negPolynomial ((W'⁄A).map (↑f : A →+* B)).negPolynomial
rw₁ rw₂ : Eq (α := B[X][Y]) (W'⁄B).negPolynomial (W'⁄B).negPolynomial
⊢ Eq (α := B[X][Y]) (W'⁄B).negPolynomial (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W'⁄A).negPolynomial)

Tactic:
rw [← map_negPolynomial, map_baseChange]

Premises used: WeierstrassCurve.Affine.map_negPolynomial, WeierstrassCurve.Affine.map_baseChange
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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
rw :
  (W'⁄B).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).negY x y)
rw₁ :
  (W'⁄B).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y) =
    ((W'⁄A).map (↑f : A →+* B)).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
rw₂ rw₃ :
  (W'⁄B).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y) =
    (W'⁄B).negY (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
⊢ (W'⁄B).negY ((f : (a : A) → B) x) ((f : (a : A) → B) y) = (f : (a : A) → B) ((W'⁄A).negY x y)

Tactic:
rw [← RingHom.coe_coe, ← map_negY, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Affine.map_baseChange, WeierstrassCurve.Affine.map_negY
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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
rw :
  Eq (α := B[X])
    ((W'⁄B).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
      (((↑f : A →+* B) : (a : A) → B) ℓ))
    (Polynomial.map (↑f : A →+* B) ((W'⁄A).addPolynomial x y ℓ))
rw₁ :
  Eq (α := B[X])
    ((W'⁄B).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
      (((↑f : A →+* B) : (a : A) → B) ℓ))
    (((W'⁄A).map (↑f : A →+* B)).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
      (((↑f : A →+* B) : (a : A) → B) ℓ))
rw₂ rw₃ :
  Eq (α := B[X])
    ((W'⁄B).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
      (((↑f : A →+* B) : (a : A) → B) ℓ))
    ((W'⁄B).addPolynomial (((↑f : A →+* B) : (a : A) → B) x) (((↑f : A →+* B) : (a : A) → B) y)
      (((↑f : A →+* B) : (a : A) → B) ℓ))
⊢ Eq (α := B[X]) ((W'⁄B).addPolynomial ((f : (a : A) → B) x) ((f : (a : A) → B) y) ((f : (a : A) → B) ℓ))
    (Polynomial.map (↑f : A →+* B) ((W'⁄A).addPolynomial x y ℓ))

Tactic:
rw [← RingHom.coe_coe, ← map_addPolynomial, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Affine.map_baseChange, WeierstrassCurve.Affine.map_addPolynomial
-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
Goal:
R : Type r
S : Type s
A : Type u
B : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
W' : Affine R
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₁ x₂ ℓ : A
rw :
  (W'⁄B).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((↑f : A →+* B) : (a : A) → B) ((W'⁄A).addX x₁ x₂ ℓ)
rw₁ :
  (W'⁄B).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) ℓ) =
    ((W'⁄A).map (↑f : A →+* B)).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) ℓ)
rw₂ rw₃ :
  (W'⁄B).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) ℓ) =
    (W'⁄B).addX (((↑f : A →+* B) : (a : A) → B) x₁) (((↑f : A →+* B) : (a : A) → B) x₂)
      (((↑f : A →+* B) : (a : A) → B) ℓ)
⊢ (W'⁄B).addX ((f : (a : A) → B) x₁) ((f : (a : A) → B) x₂) ((f : (a : A) → B) ℓ) =
    (f : (a : A) → B) ((W'⁄A).addX x₁ x₂ ℓ)

Tactic:
rw [← RingHom.coe_coe, ← map_addX, map_baseChange]

Premises used: RingHom.coe_coe, WeierstrassCurve.Affine.map_baseChange, WeierstrassCurve.Affine.map_addX