awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ = x₂
hy : y₁ ≠ W.negY x₂ y₂
⊢ ∃ (x : F[X][Y]),
    (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
        a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
          x +
              HMul.hMul (β := F[X][Y]) a
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                  F[X][Y]) +
            HMul.hMul (β := F[X][Y]) a_1
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
                F[X][Y])) ∧
      Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
        ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
        (1 : W.CoordinateRing)
have pos : ∀ (h₂ : W.Equation x₁ y₁) (hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)) (hy : y₁ ≠ W.negY x₁ y₁),
  ∃ (x : F[X][Y]),
    (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
        a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
          x +
              HMul.hMul (β := F[X][Y]) a
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                  F[X][Y]) +
            HMul.hMul (β := F[X][Y]) a_1
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                F[X][Y])) ∧
      Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
        ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
        (1 : W.CoordinateRing)
Tactic: rcases hx, Y_eq_of_Y_ne h₁ h₂ hx hy with ⟨rfl, rfl⟩
Cleared hypotheses: x₂, y₂, h₂, hxy, hx, hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hxy : ¬(x₁ = x₁ ∧ y₁ = W.negY x₁ y₁)
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
⊢ ∃ (x : F[X][Y]),
    (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
        a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
          x +
              HMul.hMul (β := F[X][Y]) a
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                  F[X][Y]) +
            HMul.hMul (β := F[X][Y]) a_1
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                F[X][Y])) ∧
      Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
        ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
        (1 : W.CoordinateRing)
have hxy₁ : HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0
Tactic: replace hxy := pow_ne_zero 2 <| sub_ne_zero_of_ne hy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
hxy : HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0
⊢ Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
    ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
        (1 +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
      AdjoinRoot (R := F[X]) W.polynomial)
    (1 : W.CoordinateRing)
have rw : HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
    ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) 1 : AdjoinRoot (R := F[X]) W.polynomial)
    ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
        (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y])
          W.polynomial) :
      AdjoinRoot (R := F[X]) W.polynomial) =
  1
Tactic: rw [map_add, map_one, map_mul <| mk W, AdjoinRoot.mk_self, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
hxy : HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0
rw :
  HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) 1 : AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
        AdjoinRoot (R := F[X]) W.polynomial) =
    1
⊢ Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
    ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
        (1 +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
      AdjoinRoot (R := F[X]) W.polynomial)
    (1 : W.CoordinateRing)
have rw₁ : HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
    (1 : AdjoinRoot (R := F[X]) W.polynomial)
    ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
        (HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y])
          W.polynomial) :
      AdjoinRoot (R := F[X]) W.polynomial) =
  1
Tactic: rw [map_add, map_one, map_mul <| mk W, AdjoinRoot.mk_self, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
hxy : HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0
rw :
  HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) 1 : AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
        AdjoinRoot (R := F[X]) W.polynomial) =
    1
rw₁ :
  HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
      (1 : AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
        AdjoinRoot (R := F[X]) W.polynomial) =
    1
⊢ Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
    ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
        (1 +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
      AdjoinRoot (R := F[X]) W.polynomial)
    (1 : W.CoordinateRing)
have rw₂ : 1 +
    HMul.hMul (α := W.CoordinateRing) (β := W.CoordinateRing)
      ((mk W : (a : F[X][Y]) → W.CoordinateRing) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4))) :
        W.CoordinateRing)
      ((mk W : (a : F[X][Y]) → W.CoordinateRing) W.polynomial) =
  1
Tactic: rw [map_add, map_one, map_mul <| mk W, AdjoinRoot.mk_self, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
hxy : HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0
rw :
  HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) 1 : AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
        AdjoinRoot (R := F[X]) W.polynomial) =
    1
rw₁ :
  HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
      (1 : AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
        AdjoinRoot (R := F[X]) W.polynomial) =
    1
rw₂ :
  1 +
      HMul.hMul (α := W.CoordinateRing) (β := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4))) :
          W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing) W.polynomial) =
    1
⊢ Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
    ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
        (1 +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
      AdjoinRoot (R := F[X]) W.polynomial)
    (1 : W.CoordinateRing)
have rw₃ : 1 +
    HMul.hMul (α := W.CoordinateRing) (β := W.CoordinateRing)
      ((mk W : (a : F[X][Y]) → W.CoordinateRing) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4))) :
        W.CoordinateRing)
      (0 : AdjoinRoot (R := F[X]) W.polynomial) =
  1
Tactic: rw [map_add, map_one, map_mul <| mk W, AdjoinRoot.mk_self, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
hxy : HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0
rw :
  HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) 1 : AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
        AdjoinRoot (R := F[X]) W.polynomial) =
    1
rw₁ :
  HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
      (1 : AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
        AdjoinRoot (R := F[X]) W.polynomial) =
    1
rw₂ :
  1 +
      HMul.hMul (α := W.CoordinateRing) (β := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4))) :
          W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing) W.polynomial) =
    1
rw₃ :
  1 +
      HMul.hMul (α := W.CoordinateRing) (β := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4))) :
          W.CoordinateRing)
        (0 : AdjoinRoot (R := F[X]) W.polynomial) =
    1
⊢ Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
    ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
        (1 +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
      AdjoinRoot (R := F[X]) W.polynomial)
    (1 : W.CoordinateRing)
have rw₄ : HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) 1 0 = 1
Tactic: rw [map_add, map_one, map_mul <| mk W, AdjoinRoot.mk_self, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
hxy : HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0
rw :
  HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) 1 : AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
        AdjoinRoot (R := F[X]) W.polynomial) =
    1
rw₁ :
  HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) (β := AdjoinRoot (R := F[X]) W.polynomial)
      (1 : AdjoinRoot (R := F[X]) W.polynomial)
      ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
          (HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
        AdjoinRoot (R := F[X]) W.polynomial) =
    1
rw₂ :
  1 +
      HMul.hMul (α := W.CoordinateRing) (β := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4))) :
          W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing) W.polynomial) =
    1
rw₃ :
  1 +
      HMul.hMul (α := W.CoordinateRing) (β := W.CoordinateRing)
        ((mk W : (a : F[X][Y]) → W.CoordinateRing) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4))) :
          W.CoordinateRing)
        (0 : AdjoinRoot (R := F[X]) W.polynomial) =
    1
rw₄ : HAdd.hAdd (α := AdjoinRoot (R := F[X]) W.polynomial) 1 0 = 1
⊢ Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
    ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial)
        (1 +
          HMul.hMul (α := F[X][Y]) (β := F[X][Y])
            ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y]) W.polynomial) :
      AdjoinRoot (R := F[X]) W.polynomial)
    (1 : W.CoordinateRing)
have rw₅ : Eq.{u + 1} (α := AdjoinRoot (R := F[X]) W.polynomial) 1 1
Tactic: rw [map_add, map_one, map_mul <| mk W, AdjoinRoot.mk_self, mul_zero, add_zero]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ y₁ : F
h₁ : W.Equation x₁ y₁
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
h₂ : W.Equation x₁ y₁
hy : y₁ ≠ W.negY x₁ y₁
y : F := HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2
hxy : HPow.hPow (β := ℕ) (y₁ - W.negY x₁ y₁) 2 ≠ 0
⊢ ∃ (x : F[X][Y]),
    (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
        a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
          x +
              HMul.hMul (β := F[X][Y]) a
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                  F[X][Y]) +
            HMul.hMul (β := F[X][Y]) a_1
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                F[X][Y])) ∧
      Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
        ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
        (1 : W.CoordinateRing)
have pos : HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) y⁻¹) : F[X][Y])
      (HSub.hSub (α := F[X][Y]) Y W.negPolynomial) *
    HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
  1 +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (y⁻¹ * 4)) : F[X][Y])
          W.polynomial +
      HMul.hMul (α := F[X][Y]) (β := F[X][Y])
        ((C : (a : F[X]) → F[X][Y])
            (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) y⁻¹ : F[X])
              (HAdd.hAdd (β := F[X])
                ((C : (a : F) → F[X]) 4 * HPow.hPow (α := F[X]) (β := ℕ) X 2 +
                  HMul.hMul (α := F[X]) (β := F[X]) ((C : (a : F) → F[X]) (4 * x₁ + b₂ W) : F[X]) X)
                ((C : (a : F) → F[X]) (4 * HPow.hPow (β := ℕ) x₁ 2 + b₂ W * x₁ + 2 * b₄ W) : F[X]))) :
          F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) : F[X][Y]) +
    HMul.hMul (α := F[X][Y]) (β := F[X][Y]) (0 : F[X][Y])
      ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) : F[X][Y])
Tactic: refine ⟨1 + C (C <| y⁻¹ * 4) * W.polynomial,
      ⟨C <| C y⁻¹ * (C 4 * X ^ 2 + C (4 * x₁ + W.b₂) * X + C (4 * x₁ ^ 2 + W.b₂ * x₁ + 2 * W.b₄)),
        0, C (C y⁻¹) * (Y - W.negPolynomial), ?_⟩, by
      rw [map_add, map_one, map_mul <| mk W, AdjoinRoot.mk_self, mul_zero, add_zero]⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : ¬x₁ = x₂
⊢ ∃ (x : F[X][Y]),
    (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
        a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
          x +
              HMul.hMul (β := F[X][Y]) a
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                  F[X][Y]) +
            HMul.hMul (β := F[X][Y]) a_1
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
                F[X][Y])) ∧
      Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
        ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
        (1 : W.CoordinateRing)
have hx₁ : x₁ - x₂ ≠ 0
Tactic: replace hx := sub_ne_zero_of_ne hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ - x₂ ≠ 0
⊢ ∃ (x : F[X][Y]),
    (∃ (a : F[X][Y]) (a_1 : F[X][Y]) (a_2 : F[X][Y]),
        a_2 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
          x +
              HMul.hMul (β := F[X][Y]) a
                ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
                  F[X][Y]) +
            HMul.hMul (β := F[X][Y]) a_1
              ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) :
                F[X][Y])) ∧
      Eq (α := AdjoinRoot (R := F[X]) W.polynomial)
        ((AdjoinRoot.mk W.polynomial : (a : F[X][Y]) → AdjoinRoot W.polynomial) x : AdjoinRoot (R := F[X]) W.polynomial)
        (1 : W.CoordinateRing)
have neg : 0 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
  1 +
      HMul.hMul (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)⁻¹) : F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) : F[X][Y]) +
    HMul.hMul (α := F[X][Y]) (β := F[X][Y])
      ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) ((x₁ - x₂)⁻¹ * -1)) : F[X][Y])
      ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) : F[X][Y])
Tactic: refine ⟨_, ⟨⟨C <| C (x₁ - x₂)⁻¹, C <| C <| (x₁ - x₂)⁻¹ * -1, 0, ?_⟩, map_one _⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
inst_1 : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : W.Equation x₁ y₁
h₂ : W.Equation x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
sup_rw : ∀ (a b c d : Ideal W.CoordinateRing), a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ d ⊔ b ⊔ c
hx : x₁ - x₂ ≠ 0
⊢ 0 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
    1 +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)⁻¹) : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
            F[X][Y]) +
      HMul.hMul (α := F[X][Y]) (β := F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) ((x₁ - x₂)⁻¹ * -1)) : F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) : F[X][Y])
have neg : HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)) : F[X][Y])
    (0 * HSub.hSub (α := F[X][Y]) Y W.negPolynomial) =
  HMul.hMul (α := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)) : F[X][Y])
    (1 +
        HMul.hMul (α := F[X][Y]) (β := F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) (x₁ - x₂)⁻¹) : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
            F[X][Y]) +
      HMul.hMul (α := F[X][Y]) (β := F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) ((x₁ - x₂)⁻¹ * -1)) : F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X])) : F[X][Y]))
Tactic: rw [← mul_right_inj' <| C_ne_zero.mpr <| C_ne_zero.mpr hx]