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₂ ≠ 0
⊢ 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]))
have neg : 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])
      (0 : F[X][Y]) *
    HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
  HAdd.hAdd (β := F[X][Y])
    (HAdd.hAdd (β := 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₂)) : F[X][Y])
        (1 : F[X][Y]))
      ((C : (a : F[X]) → F[X][Y])
          ((C : (a : F) → F[X]) 1 * HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
        F[X][Y]))
    ((C : (a : F[X]) → F[X][Y])
        (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (HMul.hMul (α := F) 1 (-1)) : F[X])
          (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]))) :
      F[X][Y])
Tactic: simp only [← mul_assoc, mul_add, ← C_mul, mul_inv_cancel₀ 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
⊢ 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])
        (0 : F[X][Y]) *
      HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
    HAdd.hAdd (β := F[X][Y])
      (HAdd.hAdd (β := 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₂)) : F[X][Y])
          (1 : F[X][Y]))
        ((C : (a : F[X]) → F[X][Y])
            ((C : (a : F) → F[X]) 1 * HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₁ : F[X])) :
          F[X][Y]))
      ((C : (a : F[X]) → F[X][Y])
          (HMul.hMul (α := F[X]) ((C : (a : F) → F[X]) (HMul.hMul (α := F) 1 (-1)) : F[X])
            (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) x₂ : F[X]))) :
        F[X][Y])
have neg : HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y]) *
      0 *
    HSub.hSub (α := F[X][Y]) Y W.negPolynomial =
  HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y]) *
        1 +
      1 *
        HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
          ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₁) : F[X][Y]) +
    HMul.hMul (α := F[X][Y]) 1 (-1) *
      HSub.hSub (α := F[X][Y]) (β := F[X][Y]) ((C : (a : F[X]) → F[X][Y]) X : F[X][Y])
        ((C : (a : F[X]) → F[X][Y]) ((C : (a : F) → F[X]) x₂) : F[X][Y])
Tactic: C_simp
-- 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 y : F
h : W.Nonsingular x y
⊢ (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
have rw : HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
    (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
  1
Tactic: rw [← mul_assoc, ← coeIdeal_mul, mul_comm <| XYIdeal W .., XYIdeal_neg_mul h, XIdeal,
      FractionalIdeal.coe_ideal_span_singleton_mul_inv W.FunctionField <| XClass_ne_zero x]
-- 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 y : F
h : W.Nonsingular x y
rw :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
⊢ (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
have rw₁ : HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
    (↑(HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x ((C : (a : F) → F[X]) y))
          (XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y)))) :
      FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
    (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
  1
Tactic: rw [← mul_assoc, ← coeIdeal_mul, mul_comm <| XYIdeal W .., XYIdeal_neg_mul h, XIdeal,
      FractionalIdeal.coe_ideal_span_singleton_mul_inv W.FunctionField <| XClass_ne_zero x]
-- 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 y : F
h : W.Nonsingular x y
rw :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₁ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x ((C : (a : F) → F[X]) y))
            (XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y)))) :
        FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
⊢ (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
have rw₂ : HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
    (↑(HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y)))
          (XYIdeal W x ((C : (a : F) → F[X]) y))) :
      FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
    (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
  1
Tactic: rw [← mul_assoc, ← coeIdeal_mul, mul_comm <| XYIdeal W .., XYIdeal_neg_mul h, XIdeal,
      FractionalIdeal.coe_ideal_span_singleton_mul_inv W.FunctionField <| XClass_ne_zero x]
-- 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 y : F
h : W.Nonsingular x y
rw :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₁ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x ((C : (a : F) → F[X]) y))
            (XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y)))) :
        FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₂ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y)))
            (XYIdeal W x ((C : (a : F) → F[X]) y))) :
        FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
⊢ (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
have rw₃ : HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
    (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
    (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
  1
Tactic: rw [← mul_assoc, ← coeIdeal_mul, mul_comm <| XYIdeal W .., XYIdeal_neg_mul h, XIdeal,
      FractionalIdeal.coe_ideal_span_singleton_mul_inv W.FunctionField <| XClass_ne_zero x]
-- 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 y : F
h : W.Nonsingular x y
rw :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₁ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x ((C : (a : F) → F[X]) y))
            (XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y)))) :
        FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₂ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y)))
            (XYIdeal W x ((C : (a : F) → F[X]) y))) :
        FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₃ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
⊢ (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
have rw₄ : HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
    (↑(span {XClass W x}) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
    (↑(span {XClass W x}) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
  1
Tactic: rw [← mul_assoc, ← coeIdeal_mul, mul_comm <| XYIdeal W .., XYIdeal_neg_mul h, XIdeal,
      FractionalIdeal.coe_ideal_span_singleton_mul_inv W.FunctionField <| XClass_ne_zero x]
-- 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 y : F
h : W.Nonsingular x y
rw :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₁ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x ((C : (a : F) → F[X]) y))
            (XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y)))) :
        FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₂ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(HMul.hMul (α := Ideal W.CoordinateRing) (XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y)))
            (XYIdeal W x ((C : (a : F) → F[X]) y))) :
        FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₃ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
rw₄ :
  HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
      (↑(span {XClass W x}) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
      (↑(span {XClass W x}) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
⊢ (↑(XYIdeal W x ((C : (a : F) → F[X]) y)) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) *
      HMul.hMul (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField)
        (↑(XYIdeal W x ((C : (a : F) → F[X]) (W.negY x y))) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)
        (↑(XIdeal W x) : FractionalIdeal W.CoordinateRing⁰ W.FunctionField)⁻¹ =
    1
have rw₅ : Eq.{u + 1} (α := FractionalIdeal (R := W.CoordinateRing) W.CoordinateRing⁰ W.FunctionField) 1 1
Tactic: rw [← mul_assoc, ← coeIdeal_mul, mul_comm <| XYIdeal W .., XYIdeal_neg_mul h, XIdeal,
      FractionalIdeal.coe_ideal_span_singleton_mul_inv W.FunctionField <| XClass_ne_zero x]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
F : Type u
inst : Field F
W : Affine F
x y : F
h : W.Nonsingular x y
⊢ HMul.hMul (α := ClassGroup W.CoordinateRing) (β := ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (XYIdeal' ⋯) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (XYIdeal' h) :
        ClassGroup W.CoordinateRing) =
    1
have rw : Eq (α := ClassGroup W.CoordinateRing)
  ((ClassGroup.mk W.FunctionField :
        (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
      (XYIdeal' sorry * XYIdeal' h) :
    ClassGroup W.CoordinateRing)
  (1 : ClassGroup W.CoordinateRing)
Tactic: rw [← map_mul]
-- 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.Nonsingular x₁ y₁
h₂ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ HMul.hMul (α := ClassGroup W.CoordinateRing) (β := ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (XYIdeal' h₂) :
        ClassGroup W.CoordinateRing) =
    (ClassGroup.mk W.FunctionField :
        (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
      (XYIdeal' (x := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) ⋯)
have rw : Eq (α := ClassGroup W.CoordinateRing)
  ((ClassGroup.mk W.FunctionField :
        (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
      (XYIdeal' h₁ * XYIdeal' h₂) :
    ClassGroup W.CoordinateRing)
  ((ClassGroup.mk W.FunctionField :
        (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
      (XYIdeal' (x := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) sorry) :
    ClassGroup W.CoordinateRing)
Tactic: rw [← map_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
p q : R[X]
⊢ (Algebra.norm R[X] : (a : W'.CoordinateRing) → R[X])
      (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
        HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y)) =
    HPow.hPow (β := ℕ) p 2 -
        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]) -
      HPow.hPow (β := ℕ) q 2 *
        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])
have simp_rw : (p * 1 + q * 0) *
      ((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]) *
          if Eq (α := Fin 2) 0 1 then 1 else 0) +
        (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])) *
          1) -
    (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 +
        (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])) *
          0) *
      ((p * if Eq (α := Fin 2) 0 1 then 1 else 0) + q * 1) =
  HPow.hPow (β := ℕ) p 2 -
      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]) -
    HPow.hPow (β := ℕ) q 2 *
      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])
Tactic: simp_rw [Algebra.norm_eq_matrix_det <| CoordinateRing.basis W', Matrix.det_fin_two,
    Algebra.leftMulMatrix_eq_repr_mul, basis_zero, mul_one, basis_one, smul_basis_mul_Y, map_add,
    Finsupp.add_apply, map_smul, Finsupp.smul_apply, ← basis_zero, ← basis_one,
    Basis.repr_self_apply, if_pos, one_ne_zero, if_false, smul_eq_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (hypothesis)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
⊢ degree.{r} (R := R)
      ((Algebra.norm R[X] : (a : W'.CoordinateRing) → R[X])
        (HSMul.hSMul (β := W'.CoordinateRing) p 1 +
          HSMul.hSMul (β := W'.CoordinateRing) q ((mk W' : (a : R[X][Y]) → W'.CoordinateRing) Y))) =
    max (HSMul.hSMul (α := ℕ) 2 p.degree) (HSMul.hSMul (α := ℕ) 2 q.degree + 3)
have hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree
Tactic: have hdp : (p ^ 2).degree = 2 • p.degree := degree_pow p 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point (goal)
Goal:
R : Type r
inst : CommRing R
W' : Affine R
inst_1 : IsDomain R
p q : R[X]
hdp : (HPow.hPow (β := ℕ) p 2).degree = HSMul.hSMul (α := ℕ) 2 p.degree
⊢ (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])).degree ≤
    p.degree + q.degree + 1
have grw : (p * q).degree +
    (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])).degree ≤
  p.degree + q.degree + 1
Tactic: grw [degree_mul, degree_mul, degree_linear_le]