internlm/Lean-Github huggingface dataset:
Theorem: Model.move_singular_point_to_origin
Proof 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), ?_⟩
Proof 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)
Theorem: Model.move_singular_point_to_origin
Proof 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
Proof 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)
Theorem: Model.move_singular_point_to_origin
Proof 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
Proof state after:
no goals
Theorem: Model.move_singular_point_to_origin
Proof 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]
Proof 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))
Theorem: Model.move_singular_point_to_origin
Proof 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
Proof 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)
Theorem: Model.move_singular_point_to_origin
Proof 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
Proof 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)
Theorem: Model.move_singular_point_to_origin
Proof 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]
Proof 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)
Theorem: Model.move_singular_point_to_origin
Proof 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
Proof state after:
no goals
Theorem: Model.move_singular_point_to_origin
Proof 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
Proof state after:
no goals
Theorem: Model.a6_of_is_local_singular_point_zero_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst : IsDomain R
p : R
inst✝ : DecidableEq R
evr : ENatValRing p
e : Model R
h : is_local_singular_point evr.valtn e (0, 0)
⊢ 0 < SurjVal.v evr.valtn e.a6
Tactic:
simpa [is_local_singular_point, weierstrass] using h.1
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b2
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ENatValRing.sub_val evr 2 (b2 e) =
    ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 1 e.a1 + 4 * ENatValRing.sub_val evr 2 e.a2
Tactic:
erw [←evr.sub_val_mul_right h1, ←evr.sub_val_mul_left h1, evr.sub_val_sub_val,
  ←evr.sub_val_mul_right h2, ←evr.sub_val_add _ _]
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ENatValRing.sub_val evr 2 (b2 e) = ENatValRing.sub_val evr (One.one + One.one) (e.a1 * e.a1 + 4 * e.a2)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (e.a1 * e.a1)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)
Theorem: Model.pi_scaling_of_b2
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ENatValRing.sub_val evr 2 (b2 e) = ENatValRing.sub_val evr (One.one + One.one) (e.a1 * e.a1 + 4 * e.a2)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (e.a1 * e.a1)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)
Tactic:
. rfl
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (e.a1 * e.a1)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)
Theorem: Model.pi_scaling_of_b2
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (e.a1 * e.a1)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)
Tactic:
. exact val_mul_ge_of_both_ge evr.valtn h1 h1
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)
Theorem: Model.pi_scaling_of_b2
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)
Tactic:
. exact val_mul_ge_of_right_ge evr.valtn h2
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b2
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ENatValRing.sub_val evr 2 (b2 e) = ENatValRing.sub_val evr (One.one + One.one) (e.a1 * e.a1 + 4 * e.a2)
Tactic:
rfl
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b2
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (e.a1 * e.a1)
Tactic:
exact val_mul_ge_of_both_ge evr.valtn h1 h1
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b2
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)
Tactic:
exact val_mul_ge_of_right_ge evr.valtn h2
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b4
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ENatValRing.sub_val evr 4 (b4 e) =
    ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 + 2 * ENatValRing.sub_val evr 4 e.a4
Tactic:
erw [←evr.sub_val_mul_right h3, ←evr.sub_val_mul_left h1, evr.sub_val_sub_val,
  ←evr.sub_val_mul_right h4, ←evr.sub_val_add _ _]
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ENatValRing.sub_val evr 4 (b4 e) = ENatValRing.sub_val evr (One.one + 3) (e.a1 * e.a3 + 2 * e.a4)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (e.a1 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)
Theorem: Model.pi_scaling_of_b4
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ENatValRing.sub_val evr 4 (b4 e) = ENatValRing.sub_val evr (One.one + 3) (e.a1 * e.a3 + 2 * e.a4)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (e.a1 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)
Tactic:
. rfl
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (e.a1 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)
Theorem: Model.pi_scaling_of_b4
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (e.a1 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)
Tactic:
. exact val_mul_ge_of_both_ge evr.valtn h1 h3
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)
Theorem: Model.pi_scaling_of_b4
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)
Tactic:
. exact val_mul_ge_of_right_ge evr.valtn h4
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b4
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ENatValRing.sub_val evr 4 (b4 e) = ENatValRing.sub_val evr (One.one + 3) (e.a1 * e.a3 + 2 * e.a4)
Tactic:
rfl
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b4
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (e.a1 * e.a3)
Tactic:
exact val_mul_ge_of_both_ge evr.valtn h1 h3
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b4
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)
Tactic:
exact val_mul_ge_of_right_ge evr.valtn h4
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b6
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 6 (b6 e) =
    ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 + 4 * ENatValRing.sub_val evr 6 e.a6
Tactic:
rw [←evr.sub_val_mul_right h3, ←evr.sub_val_mul_left h3, evr.sub_val_sub_val,
  ←evr.sub_val_mul_right h6, ←evr.sub_val_add _ _]
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 6 (b6 e) = ENatValRing.sub_val evr (3 + 3) (e.a3 * e.a3 + 4 * e.a6)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
Theorem: Model.pi_scaling_of_b6
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 6 (b6 e) = ENatValRing.sub_val evr (3 + 3) (e.a3 * e.a3 + 4 * e.a6)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
Tactic:
. rfl
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
Theorem: Model.pi_scaling_of_b6
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
Tactic:
. exact val_mul_ge_of_both_ge evr.valtn h3 h3
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
Theorem: Model.pi_scaling_of_b6
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
Tactic:
. exact val_mul_ge_of_right_ge evr.valtn h6
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b6
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 6 (b6 e) = ENatValRing.sub_val evr (3 + 3) (e.a3 * e.a3 + 4 * e.a6)
Tactic:
rfl
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b6
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)
Tactic:
exact val_mul_ge_of_both_ge evr.valtn h3 h3
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b6
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
Tactic:
exact val_mul_ge_of_right_ge evr.valtn h6
Proof state after:
no goals
Theorem: Model.pi_scaling_of_b8
Proof state before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 6 e.a6 -
            ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 4 e.a4 +
          4 * ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 6 e.a6 +
        ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 -
      ENatValRing.sub_val evr 4 e.a4 * ENatValRing.sub_val evr 4 e.a4
Tactic:
erw [←evr.sub_val_mul_right h1, ←evr.sub_val_mul_left h1, evr.sub_val_sub_val,
  ←evr.sub_val_mul_right h6, ←evr.sub_val_mul_left (val_mul_ge_of_both_ge evr.valtn h1 h1), evr.sub_val_sub_val]
Proof state after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 8 (b8 e) =
    ENatValRing.sub_val evr (Add.add 1 1 + 6) (e.a1 * e.a1 * e.a6) -
            ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 4 e.a4 +
          4 * ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 6 e.a6 +
        ENatValRing.sub_val evr 2 e.a2 * ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 -
      ENatValRing.sub_val evr 4 e.a4 * ENatValRing.sub_val evr 4 e.a4