-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_slope (f : F →+* K) (x₁ x₂ y₁ y₂ : F) :
    (W.map f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

Proof state:
case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : ¬x₁ = x₂
⊢ (f y₁ - f y₂) / (f x₁ - f x₂) = f ((y₁ - y₂) / (x₁ - x₂))

Tactic:
map_simp

Result:
no goals

Proof state:
case pos
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
⊢ (map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

Tactic:
by_cases hy : y₁ = W.negY x₂ y₂

Result:
case pos
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
⊢ (map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
⊢ (map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

Proof state:
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
⊢ (map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

Tactic:
by_cases hx : x₁ = x₂

Result:
case pos
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
⊢ (map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : ¬x₁ = x₂
⊢ (map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

Proof state:
case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : ¬x₁ = x₂
⊢ (map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

Tactic:
rw [slope_of_X_ne fun h => hx <| f.injective h, slope_of_X_ne hx]

Result:
case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : ¬x₁ = x₂
⊢ (f y₁ - f y₂) / (f x₁ - f x₂) = f ((y₁ - y₂) / (x₁ - x₂))

Proof state:
case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
⊢ (map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

Tactic:
rw [slope_of_Y_ne (congr_arg f hx) <| map_negY f x₂ y₂ ▸ fun h => hy <| f.injective h,
  map_negY, slope_of_Y_ne hx hy]

Result:
case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
⊢ (3 * f x₁ ^ 2 + 2 * (map W f).toAffine.a₂ * f x₁ + (map W f).toAffine.a₄ - (map W f).toAffine.a₁ * f y₁) /
      (f y₁ - f (W.negY x₁ y₁)) =
    f ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))

Proof state:
case pos
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
⊢ (map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

Tactic:
rw [slope_of_Y_eq (congr_arg f hx) <| by rw [hy, map_negY], slope_of_Y_eq hx hy, map_zero]

Result:
no goals

Proof state:
case neg
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : ¬y₁ = W.negY x₂ y₂
⊢ (3 * f x₁ ^ 2 + 2 * (map W f).toAffine.a₂ * f x₁ + (map W f).toAffine.a₄ - (map W f).toAffine.a₁ * f y₁) /
      (f y₁ - f (W.negY x₁ y₁)) =
    f ((3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁))

Tactic:
map_simp

Result:
no goals

Proof state:
F : Type u
K : Type v
inst✝¹ : Field F
inst✝ : Field K
W : Affine F
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : x₁ = x₂
hy : y₁ = W.negY x₂ y₂
⊢ f y₁ = (map W f).toAffine.negY (f x₂) (f y₂)

Tactic:
rw [hy, map_negY]

Result:
no goals