awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x : W'.CoordinateRing
h :
  ∑ i : Fin 2,
      HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
        ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x i : R[X])
        ((CoordinateRing.basis W' : (a : Fin 2) → W'.CoordinateRing) i : W'.CoordinateRing) =
    x
⊢ ∃ (p : R[X]) (q : R[X]),
    HSMul.hSMul (β := W'.CoordinateRing) p 1 +
        HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
      x
have h₁ : HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
      ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x 0 : R[X]) 1 +
    HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing)
      ((Basis.equivFun (CoordinateRing.basis W') : (a : W'.CoordinateRing) → Fin 2 → R[X]) x 1 : R[X])
      ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
  x
Tactic: rw [Fin.sum_univ_succ, Fin.sum_univ_one, basis_zero, Fin.succ_zero_eq_one, basis_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
y p q : R[X]
⊢ HMul.hMul (β := W'.CoordinateRing)
      (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
        HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y))
      ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) y) : W'.CoordinateRing) =
    HSMul.hSMul (β := W'.CoordinateRing) (p * y) 1 +
      HSMul.hSMul (β := W'.CoordinateRing) (q * y) ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)
have simp : HMul.hMul (β := W'.CoordinateRing)
    (HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) p) : W'.CoordinateRing)
        (1 : W'.CoordinateRing) +
      HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) q) : W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y))
    ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) y) : W'.CoordinateRing) =
  HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) p) : W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) y) : W'.CoordinateRing) *
      1 +
    HMul.hMul (α := W'.CoordinateRing) (β := W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) q) : W'.CoordinateRing)
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) ((C : (a : R[X]) → R[X][Y]) y) : W'.CoordinateRing) *
      (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y
Tactic: simp only [smul, map_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
⊢ (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
        HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)) *
      (mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y =
    HSMul.hSMul (β := W'.CoordinateRing)
        (q *
          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]))
        1 +
      HSMul.hSMul (β := W'.CoordinateRing)
        (p -
          q *
            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]))
        ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)
have Y_sq : HPow.hPow (α := W'.CoordinateRing) (β := ℕ) ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) 2 =
  (mk W' : (a : R[X][Y]) → W'.CoordinateRing)
    (HSub.hSub (α := R[X][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])
      (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))
Tactic: have Y_sq : mk W' Y ^ 2 = mk W' (C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) -
      C (C W'.a₁ * X + C W'.a₃) * Y) := AdjoinRoot.mk_eq_mk.mpr ⟨1, by rw [polynomial]; ring1⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
f : R →+* S
⊢ Eq (α := (W'.map f).CoordinateRing)
    (eval₂ (RingHom.comp (AdjoinRoot.of (W'.map f).polynomial) (mapRingHom f)) (AdjoinRoot.root (W'.map f).polynomial)
      W'.polynomial)
    0
have rw : Eq (α := (W'.map f).CoordinateRing)
  (eval₂ (AdjoinRoot.of (W'.map f).polynomial) (AdjoinRoot.root (W'.map f).polynomial)
    (Polynomial.map (mapRingHom f) W'.polynomial))
  0
Tactic: rw [← eval₂_map, ← map_polynomial, AdjoinRoot.eval₂_root]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
f : R →+* S
rw :
  Eq (α := (W'.map f).CoordinateRing)
    (eval₂ (AdjoinRoot.of (W'.map f).polynomial) (AdjoinRoot.root (W'.map f).polynomial)
      (Polynomial.map (mapRingHom f) W'.polynomial))
    0
⊢ Eq (α := (W'.map f).CoordinateRing)
    (eval₂ (RingHom.comp (AdjoinRoot.of (W'.map f).polynomial) (mapRingHom f)) (AdjoinRoot.root (W'.map f).polynomial)
      W'.polynomial)
    0
have rw₁ : Eq (α := (W'.map f).CoordinateRing)
  (eval₂ (AdjoinRoot.of (W'.map f).polynomial) (AdjoinRoot.root (W'.map f).polynomial) (W'.map f).polynomial) 0
Tactic: rw [← eval₂_map, ← map_polynomial, AdjoinRoot.eval₂_root]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
f : R →+* S
rw :
  Eq (α := (W'.map f).CoordinateRing)
    (eval₂ (AdjoinRoot.of (W'.map f).polynomial) (AdjoinRoot.root (W'.map f).polynomial)
      (Polynomial.map (mapRingHom f) W'.polynomial))
    0
rw₁ :
  Eq (α := (W'.map f).CoordinateRing)
    (eval₂ (AdjoinRoot.of (W'.map f).polynomial) (AdjoinRoot.root (W'.map f).polynomial) (W'.map f).polynomial) 0
⊢ Eq (α := (W'.map f).CoordinateRing)
    (eval₂ (RingHom.comp (AdjoinRoot.of (W'.map f).polynomial) (mapRingHom f)) (AdjoinRoot.root (W'.map f).polynomial)
      W'.polynomial)
    0
have rw₂ : Eq.{s + 1} (α := (W'.map f).CoordinateRing) 0 0
Tactic: rw [← eval₂_map, ← map_polynomial, AdjoinRoot.eval₂_root]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x : R[X][Y]
⊢ Eq.{s + 1} (α := (W'.map f).CoordinateRing)
    ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) x) :
      (W'.map f).CoordinateRing)
    ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) (Polynomial.map (mapRingHom f) x) :
      (W'.map f).CoordinateRing)
have rw : eval₂ (AdjoinRoot.of (W'.map f).polynomial) (AdjoinRoot.root (W'.map f).polynomial) (Polynomial.map (mapRingHom f) x) =
  (mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) (Polynomial.map (mapRingHom f) x)
Tactic: rw [map, AdjoinRoot.lift_mk, ← eval₂_map]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
x : R[X]
y : W'.CoordinateRing
⊢ (map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) (x • y) =
    HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f x)
      ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) y : (W'.map f).CoordinateRing)
have rw : HMul.hMul (α := (W'.map f).CoordinateRing) (β := (W'.map f).CoordinateRing)
    ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing)
        ((C : (a : S[X]) → S[X][Y]) ((mapRingHom f : (a : R[X]) → S[X]) x)) :
      (W'.map f).CoordinateRing)
    ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) y : (W'.map f).CoordinateRing) =
  HMul.hMul (α := (W'.map f).CoordinateRing) (β := (W'.map f).CoordinateRing)
    ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) ((C : (a : S[X]) → S[X][Y]) (Polynomial.map f x)) :
      (W'.map f).CoordinateRing)
    ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) y : (W'.map f).CoordinateRing)
Tactic: rw [smul, map_mul, map_mk, map_C, smul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
y : W'.CoordinateRing
hy :
  Eq.{s + 1} (α := (W'.map f).CoordinateRing)
    ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing) y : (W'.map f).CoordinateRing)
    (0 : (W'.map f).CoordinateRing)
⊢ y = 0
have obtain : ∀ (p q : R[X])
  (hy :
    Eq.{s + 1} (α := (W'.map f).CoordinateRing)
      ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing)
          (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
            HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)) :
        (W'.map f).CoordinateRing)
      (0 : (W'.map f).CoordinateRing)),
  HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
Tactic: obtain ⟨p, q, rfl⟩ := exists_smul_basis_eq y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  Eq.{s + 1} (α := (W'.map f).CoordinateRing)
    ((map W' f : (a : W'.CoordinateRing) → (W'.map f).CoordinateRing)
        (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
          HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)) :
      (W'.map f).CoordinateRing)
    (0 : (W'.map f).CoordinateRing)
⊢ HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
have hy₁ : HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
    HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
      ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
  0
Tactic: simp_rw [map_add, CoordinateRing.map_smul, map_one, map_mk, map_X] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
⊢ HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
have hp : Polynomial.map f p = 0
Tactic: obtain ⟨hp, hq⟩ := smul_basis_eq_zero hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
hp : Polynomial.map f p = 0
⊢ HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
have hq : Polynomial.map f q = 0
Tactic: obtain ⟨hp, hq⟩ := smul_basis_eq_zero hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
hp : Polynomial.map f p = 0
hq : Polynomial.map f q = 0
⊢ HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
have hp₁ : p = 0
Tactic: rw [Polynomial.map_eq_zero_iff hf] at hp hq
Cleared hypotheses: hp, hq
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
hp : Polynomial.map f p = 0
hq : Polynomial.map f q = 0
hp₁ : p = 0
⊢ HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
have hq₁ : q = 0
Tactic: rw [Polynomial.map_eq_zero_iff hf] at hp hq
Cleared hypotheses: hp, hq
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
hp : p = 0
hq : q = 0
⊢ HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
have simp_rw : HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing) 0 1 +
    HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
  0
Tactic: simp_rw [hp, hq, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
hp : p = 0
hq : q = 0
simp_rw :
  HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing) 0 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
⊢ HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
have simp_rw₁ : HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing) 0 1 +
    HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing) 0 ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
  0
Tactic: simp_rw [hp, hq, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W' : Affine R
f : R →+* S
hf : Function.Injective.{r + 1, s + 1} (α := R) (β := S) (⇑f : (a : R) → S)
p q : R[X]
hy :
  HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f p) 1 +
      HSMul.hSMul (β := (W'.map f).CoordinateRing) (Polynomial.map f q)
        ((mk (W'.map f) : (a : S[X][Y]) → (W'.map f).CoordinateRing) Y) =
    0
hp : p = 0
hq : q = 0
simp_rw :
  HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing) 0 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
simp_rw₁ :
  HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing) 0 1 +
      HSMul.hSMul (α := R[X]) (β := W'.CoordinateRing) 0 ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
⊢ HSMul.hSMul (β := W'.CoordinateRing) p 1 +
      HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y) =
    0
have simp_rw₂ : HAdd.hAdd (α := W'.CoordinateRing) 0 0 = 0
Tactic: simp_rw [hp, hq, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
x : R
⊢ natDegree.{r} (R := R[X])
      ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))) <
    natDegree (R := R[X]) W'.polynomial
have rw : LT.lt (α := ℕ) 0 2
Tactic: rw [natDegree_polynomial, natDegree_C]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : Nontrivial R
y : R[X]
⊢ (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) y : R[X][Y])).natDegree <
    natDegree (R := R[X]) W'.polynomial
have rw : LT.lt (α := ℕ) 1 2
Tactic: rw [natDegree_polynomial, natDegree_X_sub_C]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
⊢ HSub.hSub (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W'.addPolynomial x y ℓ) : R[X][Y])
      (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
        HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
          ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y])) =
    HMul.hMul (α := R[X][Y]) W'.polynomial 1
have rw : HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
        HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
          ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) +
      W'.polynomial -
    HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
      HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
        ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) =
  HMul.hMul (α := R[X][Y]) W'.polynomial 1
Tactic: rw [W'.C_addPolynomial, add_sub_cancel_left, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
rw :
  HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
          HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
            ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) +
        W'.polynomial -
      HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
        HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
          ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) =
    HMul.hMul (α := R[X][Y]) W'.polynomial 1
⊢ HSub.hSub (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W'.addPolynomial x y ℓ) : R[X][Y])
      (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
        HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
          ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y])) =
    HMul.hMul (α := R[X][Y]) W'.polynomial 1
have rw₁ : W'.polynomial = HMul.hMul (α := R[X][Y]) W'.polynomial 1
Tactic: rw [W'.C_addPolynomial, add_sub_cancel_left, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
x y ℓ : R
rw :
  HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
          HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
            ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) +
        W'.polynomial -
      HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
        HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
          ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) =
    HMul.hMul (α := R[X][Y]) W'.polynomial 1
rw₁ : W'.polynomial = HMul.hMul (α := R[X][Y]) W'.polynomial 1
⊢ HSub.hSub (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W'.addPolynomial x y ℓ) : R[X][Y])
      (HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y]) *
        HSub.hSub (α := R[X][Y]) (β := R[X][Y]) W'.negPolynomial
          ((C : (a : R[X]) → R[X][Y]) (linePolynomial x y ℓ) : R[X][Y])) =
    HMul.hMul (α := R[X][Y]) W'.polynomial 1
have rw₂ : Eq (α := R[X][Y]) W'.polynomial W'.polynomial
Tactic: rw [W'.C_addPolynomial, add_sub_cancel_left, mul_one]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing A
inst_3 : CommRing B
inst_4 : Field F
inst_5 : Field K
inst_6 : Field L
W' : Affine R
W : Affine F
x : R
y : R[X]
h : eval x (eval y W'.polynomial) = 0
⊢ XYIdeal W' x y =
    Ideal.map (R := R[X][Y]) (F :=
      R[X][Y] →ₐ[R] HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y]) (span {W'.polynomial}))
      (Quotient.mkₐ R (span {W'.polynomial}))
      (span
        (insert (α := R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) : R[X][Y])
          {HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) y : R[X][Y])}))
have simp : Eq (α := Ideal (HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y]) (span {W'.polynomial})))
  (Ideal.map (R := R[X][Y]) (F := R[X][Y] →+* W'.CoordinateRing) (mk W')
    (span
      (insert (α := R[X][Y])
        ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) : R[X][Y])
        {HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) y : R[X][Y])})))
  (Ideal.map (R := R[X][Y]) (F :=
    R[X][Y] →ₐ[R] HasQuotient.Quotient R[X][Y] (B := Ideal R[X][Y]) (span {W'.polynomial}))
    (Quotient.mkₐ R (span {W'.polynomial}))
    (span
      (insert (α := R[X][Y])
        ((C : (a : R[X]) → R[X][Y]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) : R[X][Y])
        {HSub.hSub (α := R[X][Y]) (β := R[X][Y]) Y ((C : (a : R[X]) → R[X][Y]) y : R[X][Y])})))
Tactic: simp only [XYIdeal, XClass, YClass, ← Set.image_pair, ← map_span]