-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addMap_of_Z_eq_zero_left {P : Fin 3 → F} {Q : PointClass F} (hP : W.Nonsingular P)
    (hQ : W.NonsingularLift Q) (hPz : P z = 0) : W.addMap ⟦P⟧ Q = Q

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q)
hQz : ¬Q z = 0
⊢ ⟦Q⟧ = Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q

Tactic:
rfl

Result:
no goals

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q)
hQz : ¬Q z = 0
⊢ W.addMap ⟦P⟧ (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q) = Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q

Tactic:
erw [addMap_eq, add_of_Z_eq_zero_left hP.left hPz hQz,
  smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).mul <| Ne.isUnit hQz]

Result:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q)
hQz : ¬Q z = 0
⊢ ⟦Q⟧ = Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q)
hQz : Q z = 0
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F)) ![1, 1, 0] Q

Tactic:
exact Setoid.symm <| equiv_zero_of_Z_eq_zero hQ hQz

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q : PointClass F
hP : W.Nonsingular P
hQ : W.NonsingularLift Q
hPz : P z = 0
⊢ W.addMap ⟦P⟧ Q = Q

Tactic:
rcases Q with ⟨Q⟩

Result:
case mk
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q)
⊢ W.addMap ⟦P⟧ (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q) = Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q)
hQz : Q z = 0
⊢ W.addMap ⟦P⟧ (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q) = Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q

Tactic:
erw [addMap_eq, add_of_Z_eq_zero hP hQ hPz hQz,
  smul_eq _ <| (isUnit_X_of_Z_eq_zero hP hPz).pow 2, Quotient.eq]

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q)
hQz : Q z = 0
⊢ (MulAction.orbitRel Fˣ (Fin 3 → F)) ![1, 1, 0] Q

Proof state:
case mk
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q)
⊢ W.addMap ⟦P⟧ (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q) = Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q

Tactic:
by_cases hQz : Q z = 0

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q)
hQz : Q z = 0
⊢ W.addMap ⟦P⟧ (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q) = Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q

case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
Q✝ : PointClass F
hP : W.Nonsingular P
hPz : P z = 0
Q : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q)
hQz : ¬Q z = 0
⊢ W.addMap ⟦P⟧ (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q) = Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) Q