Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ ∀ (x y : W.Point),
    (match x + y with
      | zero => 0
      | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
      (match x with
        | zero => 0
        | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) +
        match y with
        | zero => 0
        | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)

Tactic:
rintro (_ | ⟨x₁, y₁, h₁⟩) (_ | ⟨x₂, y₂, h₂⟩)

Goal state after:
case zero.zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ (match zero + zero with
    | zero => 0
    | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
    (match zero with
      | zero => 0
      | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) +
      match zero with
      | zero => 0
      | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)

case zero.some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
⊢ (match zero + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
    (match zero with
      | zero => 0
      | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)

case some.zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
⊢ (match some x₁ y₁ h₁ + zero with
    | zero => 0
    | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) +
      match zero with
      | zero => 0
      | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)

case some.some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x₁ y₁ : F
h₁ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h₂ : W.Nonsingular x₂ y₂
⊢ (match some x₁ y₁ h₁ + some x₂ y₂ h₂ with
    | zero => 0
    | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
    (match some x₁ y₁ h₁ with
      | zero => 0
      | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) +
      match some x₂ y₂ h₂ with
      | zero => 0
      | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)