-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
private lemma add_eq_zero (P Q : W.Point) : P + Q = 0 ↔ P = -Q

Proof state:
case some.some
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some h✝¹ + some h✝ = 0 ↔ some h✝¹ = -some h✝

Tactic:
rw [neg_some, some.injEq]

Result:
case some.some
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some h✝¹ + some h✝ = 0 ↔ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
P Q : W.Point
⊢ P + Q = 0 ↔ P = -Q

Tactic:
rcases P, Q with ⟨_ | @⟨x₁, y₁, _⟩, _ | @⟨x₂, y₂, _⟩⟩

Result:
case zero.zero
F : Type u
inst✝ : Field F
W : Affine F
⊢ zero + zero = 0 ↔ zero = -zero

case zero.some
F : Type u
inst✝ : Field F
W : Affine F
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ zero + some h✝ = 0 ↔ zero = -some h✝

case some.zero
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝ : W.Nonsingular x₁ y₁
⊢ some h✝ + zero = 0 ↔ some h✝ = -zero

case some.some
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some h✝¹ + some h✝ = 0 ↔ some h✝¹ = -some h✝

Proof state:
case some.some.mp
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) → ¬some h✝¹ + some h✝ = 0

Tactic:
exact fun hxy => by simpa only [add_some hxy] using some_ne_zero _

Result:
no goals

Proof state:
case some.some
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some h✝¹ + some h✝ = 0 ↔ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂

Tactic:
constructor

Result:
case some.some.mp
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some h✝¹ + some h✝ = 0 → x₁ = x₂ ∧ y₁ = W.negY x₂ y₂

case some.some.mpr
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ → some h✝¹ + some h✝ = 0

Proof state:
case some.some.mpr
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ → some h✝¹ + some h✝ = 0

Tactic:
exact fun ⟨hx, hy⟩ => add_of_Y_eq hx hy

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ ¬some h✝¹ + some h✝ = 0

Tactic:
simpa only [add_some hxy] using some_ne_zero _

Result:
no goals

Proof state:
case some.some.mp
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some h✝¹ + some h✝ = 0 → x₁ = x₂ ∧ y₁ = W.negY x₂ y₂

Tactic:
contrapose

Result:
case some.some.mp
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) → ¬some h✝¹ + some h✝ = 0

Proof state:
case some.zero
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝ : W.Nonsingular x₁ y₁
⊢ some h✝ + zero = 0 ↔ some h✝ = -zero

Tactic:
rfl

Result:
no goals

Proof state:
case zero.some
F : Type u
inst✝ : Field F
W : Affine F
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ zero + some h✝ = 0 ↔ zero = -some h✝

Tactic:
rw [← zero_def, zero_add, ← neg_eq_iff_eq_neg, neg_zero, eq_comm]

Result:
no goals

Proof state:
case zero.zero
F : Type u
inst✝ : Field F
W : Affine F
⊢ zero + zero = 0 ↔ zero = -zero

case zero.some
F : Type u
inst✝ : Field F
W : Affine F
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ zero + some h✝ = 0 ↔ zero = -some h✝

case some.zero
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝ : W.Nonsingular x₁ y₁
⊢ some h✝ + zero = 0 ↔ some h✝ = -zero

case some.some
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some h✝¹ + some h✝ = 0 ↔ some h✝¹ = -some h✝

Tactic:
any_goals rfl

Result:
case zero.some
F : Type u
inst✝ : Field F
W : Affine F
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ zero + some h✝ = 0 ↔ zero = -some h✝

case some.some
F : Type u
inst✝ : Field F
W : Affine F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some h✝¹ + some h✝ = 0 ↔ some h✝¹ = -some h✝