-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma toClass_eq_zero (P : W.Point) : toClass P = 0 ↔ P = 0

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some ⋯) = 0
⊢ ↑(CoordinateRing.XYIdeal' ⋯) = ↑?m.692865

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
F : Type u
inst✝ : Field F
W : Affine F
P : W.Point
⊢ P = 0 → toClass P = 0

Tactic:
exact congr_arg toClass

Result:
no goals

Proof state:
case mp
F : Type u
inst✝ : Field F
W : Affine F
P : W.Point
⊢ toClass P = 0 → P = 0

Tactic:
intro hP

Result:
case mp
F : Type u
inst✝ : Field F
W : Affine F
P : W.Point
hP : toClass P = 0
⊢ P = 0

Proof state:
case mp.some.intro
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some ⋯) = 0
⊢ some ⋯ = 0

Tactic:
rcases (ClassGroup.mk_eq_one_of_coe_ideal <| by rfl).mp hP with ⟨p, h0, hp⟩

Result:
case mp.some.intro.intro.intro
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some ⋯) = 0
p : W.CoordinateRing
h0 : p ≠ 0
hp : CoordinateRing.XYIdeal W x✝ (C y✝) = span {p}
⊢ some ⋯ = 0

Proof state:
case mp.zero
F : Type u
inst✝ : Field F
W : Affine F
hP : toClass zero = 0
⊢ zero = 0

Tactic:
rfl

Result:
no goals

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

Tactic:
constructor

Result:
case mp
F : Type u
inst✝ : Field F
W : Affine F
P : W.Point
⊢ toClass P = 0 → P = 0

case mpr
F : Type u
inst✝ : Field F
W : Affine F
P : W.Point
⊢ P = 0 → toClass P = 0

Proof state:
case mp
F : Type u
inst✝ : Field F
W : Affine F
P : W.Point
hP : toClass P = 0
⊢ P = 0

Tactic:
rcases P with (_ | ⟨h, _⟩)

Result:
case mp.zero
F : Type u
inst✝ : Field F
W : Affine F
hP : toClass zero = 0
⊢ zero = 0

case mp.some.intro
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some ⋯) = 0
⊢ some ⋯ = 0

Proof state:
case mp.some.intro.intro.intro
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some ⋯) = 0
p : W.CoordinateRing
h0 : p ≠ 0
hp : CoordinateRing.XYIdeal W x✝ (C y✝) = span {p}
⊢ some ⋯ = 0

Tactic:
apply (p.natDegree_norm_ne_one _).elim

Result:
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some ⋯) = 0
p : W.CoordinateRing
h0 : p ≠ 0
hp : CoordinateRing.XYIdeal W x✝ (C y✝) = span {p}
⊢ ((Algebra.norm F[X]) p).natDegree = 1

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some ⋯) = 0
p : W.CoordinateRing
h0 : p ≠ 0
hp : CoordinateRing.XYIdeal W x✝ (C y✝) = span {p}
⊢ ((Algebra.norm F[X]) p).natDegree = 1

Tactic:
rw [← finrank_quotient_span_eq_natDegree_norm (CoordinateRing.basis W) h0,
  ← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq,
  (CoordinateRing.quotientXYIdealEquiv W h).toLinearEquiv.finrank_eq,
  Module.finrank_self]

Result:
no goals