-- 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
inst_7 : DecidableEq F
inst_8 : DecidableEq K
inst_9 : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
pos :
  ∀ (hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂),
    (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
      | zero => 0
      | some x y h =>
        (ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h)) =
      HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
        ((ClassGroup.mk W.FunctionField :
              (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
            (CoordinateRing.XYIdeal' h₁) :
          ClassGroup W.CoordinateRing)
        ((ClassGroup.mk W.FunctionField :
              (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
            (CoordinateRing.XYIdeal' h₂) :
          ClassGroup W.CoordinateRing)
⊢ (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h =>
      (ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h)) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)
have neg : ∀ (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)),
  (match (motive := W.Point → Additive (ClassGroup W.CoordinateRing)) some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h =>
      (ClassGroup.mk W.FunctionField :
          (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
        (CoordinateRing.XYIdeal' h)) =
    HAdd.hAdd (α := Additive (ClassGroup W.CoordinateRing)) (β := Additive (ClassGroup W.CoordinateRing))
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₁) :
        ClassGroup W.CoordinateRing)
      ((ClassGroup.mk W.FunctionField :
            (a : (FractionalIdeal W.CoordinateRing⁰ W.FunctionField)ˣ) → ClassGroup W.CoordinateRing)
          (CoordinateRing.XYIdeal' h₂) :
        ClassGroup W.CoordinateRing)
Tactic: by_cases hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂