internlm/Lean-Github huggingface dataset:
Theorem: Model.pi_scaling_of_discr
Proof state before:
case hx.ha.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (-b2 e * b2 e * b8 e)

case hx.ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (8 * b4 e ^ 3)

case hx.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (27 * b6 e * b6 e)
Tactic:
. exact val_mul_ge_of_both_ge evr.valtn
    (val_mul_ge_of_both_ge evr.valtn (by simpa : evr.valtn (-b2 e) ≥ 2) hb2) hb8
Proof state after:
case hx.ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (8 * b4 e ^ 3)

case hx.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (27 * b6 e * b6 e)
Theorem: Model.pi_scaling_of_discr
Proof state before:
case hx.ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (8 * b4 e ^ 3)

case hx.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (27 * b6 e * b6 e)
Tactic:
. apply val_mul_ge_of_right_ge evr.valtn
  exact val_pow_ge_of_ge evr.valtn 3 hb4
Proof state after:
case hx.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (27 * b6 e * b6 e)
Theorem: Model.pi_scaling_of_discr
Proof state before:
case hx.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (27 * b6 e * b6 e)
Tactic:
. exact val_mul_ge_of_both_ge evr.valtn (val_mul_ge_of_right_ge evr.valtn hb6) hb6
Proof state after:
no goals
Theorem: Model.pi_scaling_of_discr
Proof state before:
case hx.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (-b2 e * b2 e * b8 e - 8 * b4 e ^ 3)
Tactic:
apply val_sub_ge_of_ge
Proof state after:
case hx.ha.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (-b2 e * b2 e * b8 e)

case hx.ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (8 * b4 e ^ 3)
Theorem: Model.pi_scaling_of_discr
Proof state before:
case hx.ha.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (-b2 e * b2 e * b8 e)
Tactic:
exact val_mul_ge_of_both_ge evr.valtn
  (val_mul_ge_of_both_ge evr.valtn (by simpa : evr.valtn (-b2 e) ≥ 2) hb2) hb8
Proof state after:
no goals
Theorem: Model.pi_scaling_of_discr
Proof state before:
case hx.ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (8 * b4 e ^ 3)
Tactic:
apply val_mul_ge_of_right_ge evr.valtn
Proof state after:
case hx.ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (b4 e ^ 3)
Theorem: Model.pi_scaling_of_discr
Proof state before:
case hx.ha.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (b4 e ^ 3)
Tactic:
exact val_pow_ge_of_ge evr.valtn 3 hb4
Proof state after:
no goals
Theorem: Model.pi_scaling_of_discr
Proof state before:
case hx.hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (27 * b6 e * b6 e)
Tactic:
exact val_mul_ge_of_both_ge evr.valtn (val_mul_ge_of_right_ge evr.valtn hb6) hb6
Proof state after:
no goals
Theorem: Model.pi_scaling_of_discr
Proof state before:
case hy
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
hb8 : v evr.valtn (b8 e) ≥ 8
⊢ ↑12 ≤ v evr.valtn (9 * b2 e * b4 e * b6 e)
Tactic:
exact val_mul_ge_of_both_ge
  evr.valtn (val_mul_ge_of_both_ge evr.valtn (val_mul_ge_of_right_ge evr.valtn hb2) hb4) hb6
Proof state after:
no goals
Theorem: Model.b2_of_pi_scaling
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
⊢ b2 (pi_scaling evr e) = ENatValRing.sub_val evr 2 (b2 e)
Tactic:
simp only [b2, pi_scaling]
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 1 e.a1 * ENatValRing.sub_val evr 1 e.a1 + 4 * ENatValRing.sub_val evr 2 e.a2 =
    ENatValRing.sub_val evr 2 (e.a1 * e.a1 + 4 * e.a2)
Theorem: Model.b2_of_pi_scaling
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 1 e.a1 * ENatValRing.sub_val evr 1 e.a1 + 4 * ENatValRing.sub_val evr 2 e.a2 =
    ENatValRing.sub_val evr 2 (e.a1 * e.a1 + 4 * e.a2)
Tactic:
exact (pi_scaling_of_b2 evr e h1 h2).symm
Proof state after:
no goals
Theorem: Model.b4_of_pi_scaling
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
⊢ b4 (pi_scaling evr e) = ENatValRing.sub_val evr 4 (b4 e)
Tactic:
simp only [b4, pi_scaling]
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 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 + 2 * ENatValRing.sub_val evr 4 e.a4 =
    ENatValRing.sub_val evr 4 (e.a1 * e.a3 + 2 * e.a4)
Theorem: Model.b4_of_pi_scaling
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 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 + 2 * ENatValRing.sub_val evr 4 e.a4 =
    ENatValRing.sub_val evr 4 (e.a1 * e.a3 + 2 * e.a4)
Tactic:
exact (pi_scaling_of_b4 evr e h1 h3 h4).symm
Proof state after:
no goals
Theorem: Model.b6_of_pi_scaling
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
⊢ b6 (pi_scaling evr e) = ENatValRing.sub_val evr 6 (b6 e)
Tactic:
simp only [b6, pi_scaling]
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 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 + 4 * ENatValRing.sub_val evr 6 e.a6 =
    ENatValRing.sub_val evr 6 (e.a3 * e.a3 + 4 * e.a6)
Theorem: Model.b6_of_pi_scaling
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 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 + 4 * ENatValRing.sub_val evr 6 e.a6 =
    ENatValRing.sub_val evr 6 (e.a3 * e.a3 + 4 * e.a6)
Tactic:
exact (pi_scaling_of_b6 evr e h3 h6).symm
Proof state after:
no goals
Theorem: Model.b8_of_pi_scaling
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
⊢ b8 (pi_scaling evr e) = ENatValRing.sub_val evr 8 (b8 e)
Tactic:
simp only [b8, pi_scaling]
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 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 =
    ENatValRing.sub_val evr 8
      (e.a1 * e.a1 * e.a6 - e.a1 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4)
Theorem: Model.b8_of_pi_scaling
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 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 =
    ENatValRing.sub_val evr 8
      (e.a1 * e.a1 * e.a6 - e.a1 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4)
Tactic:
exact (pi_scaling_of_b8 evr e h1 h2 h3 h4 h6).symm
Proof state after:
no goals
Theorem: Model.val_b2_of_val_a12
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
⊢ v evr.valtn (b2 e) ≥ 2
Tactic:
simp only [b2]
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
⊢ v evr.valtn (e.a1 * e.a1 + 4 * e.a2) ≥ 2
Theorem: Model.val_b2_of_val_a12
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
⊢ v evr.valtn (e.a1 * e.a1 + 4 * e.a2) ≥ 2
Tactic:
apply val_add_ge_of_ge
Proof state after:
case ha
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
⊢ 2 ≤ v evr.valtn (e.a1 * e.a1)

case hb
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
⊢ 2 ≤ v evr.valtn (4 * e.a2)
Theorem: Model.val_b2_of_val_a12
Proof state before:
case ha
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
⊢ 2 ≤ v evr.valtn (e.a1 * e.a1)

case hb
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
⊢ 2 ≤ v evr.valtn (4 * e.a2)
Tactic:
. apply val_mul_ge_of_both_ge evr.valtn h1 h1
Proof state after:
case hb
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
⊢ 2 ≤ v evr.valtn (4 * e.a2)
Theorem: Model.val_b2_of_val_a12
Proof state before:
case hb
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
⊢ 2 ≤ v evr.valtn (4 * e.a2)
Tactic:
. apply val_mul_ge_of_right_ge evr.valtn h2
Proof state after:
no goals
Theorem: Model.val_b2_of_val_a12
Proof state before:
case ha
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
⊢ 2 ≤ v evr.valtn (e.a1 * e.a1)
Tactic:
apply val_mul_ge_of_both_ge evr.valtn h1 h1
Proof state after:
no goals
Theorem: Model.val_b2_of_val_a12
Proof state before:
case hb
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
⊢ 2 ≤ v evr.valtn (4 * e.a2)
Tactic:
apply val_mul_ge_of_right_ge evr.valtn h2
Proof state after:
no goals
Theorem: Model.val_b4_of_val_a134
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
⊢ v evr.valtn (b4 e) ≥ 4
Tactic:
simp only [b4]
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
⊢ v evr.valtn (e.a1 * e.a3 + 2 * e.a4) ≥ 4
Theorem: Model.val_b4_of_val_a134
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
⊢ v evr.valtn (e.a1 * e.a3 + 2 * e.a4) ≥ 4
Tactic:
apply val_add_ge_of_ge
Proof state after:
case ha
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
⊢ 4 ≤ v evr.valtn (e.a1 * e.a3)

case hb
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
⊢ 4 ≤ v evr.valtn (2 * e.a4)
Theorem: Model.val_b4_of_val_a134
Proof state before:
case ha
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
⊢ 4 ≤ v evr.valtn (e.a1 * e.a3)

case hb
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
⊢ 4 ≤ v evr.valtn (2 * e.a4)
Tactic:
. apply val_mul_ge_of_both_ge evr.valtn h1 h3
Proof state after:
case hb
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
⊢ 4 ≤ v evr.valtn (2 * e.a4)
Theorem: Model.val_b4_of_val_a134
Proof state before:
case hb
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
⊢ 4 ≤ v evr.valtn (2 * e.a4)
Tactic:
. apply val_mul_ge_of_right_ge evr.valtn h4
Proof state after:
no goals
Theorem: Model.val_b4_of_val_a134
Proof state before:
case ha
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
⊢ 4 ≤ v evr.valtn (e.a1 * e.a3)
Tactic:
apply val_mul_ge_of_both_ge evr.valtn h1 h3
Proof state after:
no goals
Theorem: Model.val_b4_of_val_a134
Proof state before:
case hb
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
⊢ 4 ≤ v evr.valtn (2 * e.a4)
Tactic:
apply val_mul_ge_of_right_ge evr.valtn h4
Proof state after:
no goals
Theorem: Model.val_b6_of_val_a36
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
⊢ v evr.valtn (b6 e) ≥ 6
Tactic:
simp only [b6]
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
⊢ v evr.valtn (e.a3 * e.a3 + 4 * e.a6) ≥ 6
Theorem: Model.val_b6_of_val_a36
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
⊢ v evr.valtn (e.a3 * e.a3 + 4 * e.a6) ≥ 6
Tactic:
apply val_add_ge_of_ge
Proof state after:
case ha
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
⊢ 6 ≤ v evr.valtn (e.a3 * e.a3)

case hb
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
⊢ 6 ≤ v evr.valtn (4 * e.a6)
Theorem: Model.val_b6_of_val_a36
Proof state before:
case ha
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
⊢ 6 ≤ v evr.valtn (e.a3 * e.a3)

case hb
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
⊢ 6 ≤ v evr.valtn (4 * e.a6)
Tactic:
. apply val_mul_ge_of_both_ge evr.valtn h3 h3
Proof state after:
case hb
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
⊢ 6 ≤ v evr.valtn (4 * e.a6)
Theorem: Model.val_b6_of_val_a36
Proof state before:
case hb
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
⊢ 6 ≤ v evr.valtn (4 * e.a6)
Tactic:
. apply val_mul_ge_of_right_ge evr.valtn h6
Proof state after:
no goals
Theorem: Model.val_b6_of_val_a36
Proof state before:
case ha
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
⊢ 6 ≤ v evr.valtn (e.a3 * e.a3)
Tactic:
apply val_mul_ge_of_both_ge evr.valtn h3 h3
Proof state after:
no goals
Theorem: Model.val_b6_of_val_a36
Proof state before:
case hb
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
⊢ 6 ≤ v evr.valtn (4 * e.a6)
Tactic:
apply val_mul_ge_of_right_ge evr.valtn h6
Proof state after:
no goals
Theorem: Model.val_b8_of_val_ai
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
⊢ v evr.valtn (b8 e) ≥ 8
Tactic:
simp only [b8, sub_eq_add_neg]
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
⊢ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 + -(e.a4 * e.a4)) ≥ 8
Theorem: Model.val_b8_of_val_ai
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
⊢ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 + -(e.a4 * e.a4)) ≥ 8
Tactic:
apply val_add_ge_of_ge
Proof state after:
case ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3)

case hb
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
⊢ 8 ≤ v evr.valtn (-(e.a4 * e.a4))
Theorem: Model.val_b8_of_val_ai
Proof state before:
case ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3)

case hb
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
⊢ 8 ≤ v evr.valtn (-(e.a4 * e.a4))
Tactic:
. apply val_add_ge_of_ge
  . apply val_add_ge_of_ge
    . apply val_add_ge_of_ge
      . apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h1) h6
      . rw [val_neg]
        apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h1 h3) h4
    . rw [mul_assoc]
      apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ h2 h6)
  . apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ h2 h3) h3
Proof state after:
case hb
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
⊢ 8 ≤ v evr.valtn (-(e.a4 * e.a4))
Theorem: Model.val_b8_of_val_ai
Proof state before:
case hb
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
⊢ 8 ≤ v evr.valtn (-(e.a4 * e.a4))
Tactic:
. rw [val_neg]
  apply val_mul_ge_of_both_ge _ h4 h4
Proof state after:
no goals
Theorem: Model.val_b8_of_val_ai
Proof state before:
case ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3)
Tactic:
apply val_add_ge_of_ge
Proof state after:
case ha.ha
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
⊢ 8 ≤ v evr.valtn (e.a1 * e.a1 * e.a6 + -(e.a1 * e.a3 * e.a4) + 4 * e.a2 * e.a6)

case ha.hb
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
⊢ 8 ≤ v evr.valtn (e.a2 * e.a3 * e.a3)