Theorem: Model.move_singular_point_to_origin (ECTate/Algebra/EllipticCurve/LocalEC.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
⊢ (∃ P, is_local_singular_point evr.valtn e P) →
    is_local_singular_point evr.valtn (move_singular_point_to_origin_iso evr e) (0, 0)
Tactic:
rintro ⟨P, h⟩
State after:
case intro
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
⊢ is_local_singular_point evr.valtn (move_singular_point_to_origin_iso evr e) (0, 0)

State before:
case intro
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
⊢ is_local_singular_point evr.valtn (move_singular_point_to_origin_iso evr e) (0, 0)
Tactic:
have := Model.Field.move_singular_point_to_origin' (e.map (Ideal.Quotient.mk evr.valtn.ideal)) ⟨P.map (Ideal.Quotient.mk evr.valtn.ideal) (Ideal.Quotient.mk evr.valtn.ideal), ?_⟩
State after:
case intro.refine_2
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
⊢ is_local_singular_point evr.valtn (move_singular_point_to_origin_iso evr e) (0, 0)

case intro.refine_1
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
⊢ is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
    (Prod.map (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) P)

State before:
case intro.refine_2
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
⊢ is_local_singular_point evr.valtn (move_singular_point_to_origin_iso evr e) (0, 0)

case intro.refine_1
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
⊢ is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
    (Prod.map (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) P)
Tactic:
. rw [is_local_singular_point_iff]
  simp
  convert this
  simp [move_singular_point_to_origin_iso, Field.move_singular_point_to_origin_iso,
        move_singular_point_to_origin_triple, Field.move_singular_point_to_origin_triple]
  sorry
State after:
case intro.refine_1
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
⊢ is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
    (Prod.map (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) P)

State before:
case intro.refine_1
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
⊢ is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
    (Prod.map (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) P)
Tactic:
. rwa [is_local_singular_point_iff] at h
State after:
no goals

State before:
case intro.refine_2
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
⊢ is_local_singular_point evr.valtn (move_singular_point_to_origin_iso evr e) (0, 0)
Tactic:
rw [is_local_singular_point_iff]
State after:
case intro.refine_2
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
⊢ is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (move_singular_point_to_origin_iso evr e))
    (Prod.map ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (0, 0))

State before:
case intro.refine_2
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
⊢ is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (move_singular_point_to_origin_iso evr e))
    (Prod.map ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) ↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (0, 0))
Tactic:
simp
State after:
case intro.refine_2
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
⊢ is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (move_singular_point_to_origin_iso evr e)) (0, 0)

State before:
case intro.refine_2
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
⊢ is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (move_singular_point_to_origin_iso evr e)) (0, 0)
Tactic:
convert this
State after:
case h.e'_3.h
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
e_2✝ : Ideal.Quotient.commRing (SurjVal.ideal evr.valtn) = EuclideanDomain.toCommRing
⊢ map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (move_singular_point_to_origin_iso evr e) =
    Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)

State before:
case h.e'_3.h
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
e_2✝ : Ideal.Quotient.commRing (SurjVal.ideal evr.valtn) = EuclideanDomain.toCommRing
⊢ map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) (move_singular_point_to_origin_iso evr e) =
    Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
Tactic:
simp [move_singular_point_to_origin_iso, Field.move_singular_point_to_origin_iso,
      move_singular_point_to_origin_triple, Field.move_singular_point_to_origin_triple]
State after:
case h.e'_3.h
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
e_2✝ : Ideal.Quotient.commRing (SurjVal.ideal evr.valtn) = EuclideanDomain.toCommRing
⊢ map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn))
      (rst_triple e ((singular_point_on_special evr e).fst, 0, (singular_point_on_special evr e).snd)) =
    rst_triple (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
      ((Field.singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)).fst, 0,
        (Field.singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)).snd)

State before:
case h.e'_3.h
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
this :
  is_singular_point (Field.move_singular_point_to_origin_iso (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e))
    (0, 0)
e_2✝ : Ideal.Quotient.commRing (SurjVal.ideal evr.valtn) = EuclideanDomain.toCommRing
⊢ map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn))
      (rst_triple e ((singular_point_on_special evr e).fst, 0, (singular_point_on_special evr e).snd)) =
    rst_triple (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
      ((Field.singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)).fst, 0,
        (Field.singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)).snd)
Tactic:
sorry
State after:
no goals

State before:
case intro.refine_1
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
P : R × R
h : is_local_singular_point evr.valtn e P
⊢ is_singular_point (map (Ideal.Quotient.mk (SurjVal.ideal evr.valtn)) e)
    (Prod.map (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) (↑(Ideal.Quotient.mk (SurjVal.ideal evr.valtn))) P)
Tactic:
rwa [is_local_singular_point_iff] at h
State after:
no goals