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

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 (discr e) ≥ 12
Tactic:
have hb2 := val_b2_of_val_a12 evr e h1 h2
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
hb2 : v evr.valtn (b2 e) ≥ 2
⊢ v evr.valtn (discr e) ≥ 12

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
hb2 : v evr.valtn (b2 e) ≥ 2
⊢ v evr.valtn (discr e) ≥ 12
Tactic:
have hb4 := val_b4_of_val_a134 evr e h1 h3 h4
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
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
⊢ v evr.valtn (discr e) ≥ 12

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
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
⊢ v evr.valtn (discr e) ≥ 12
Tactic:
have hb6 := val_b6_of_val_a36 evr e h3 h6
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
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
⊢ v evr.valtn (discr e) ≥ 12

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
hb2 : v evr.valtn (b2 e) ≥ 2
hb4 : v evr.valtn (b4 e) ≥ 4
hb6 : v evr.valtn (b6 e) ≥ 6
⊢ v evr.valtn (discr e) ≥ 12
Tactic:
have hb8 := val_b8_of_val_ai evr e h1 h2 h3 h4 h6
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
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
⊢ v evr.valtn (discr e) ≥ 12

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
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
⊢ v evr.valtn (discr e) ≥ 12
Tactic:
simp only [discr, sub_eq_add_neg]
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
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
⊢ v evr.valtn (-b2 e * b2 e * b8 e + -(8 * b4 e ^ 3) + -(27 * b6 e * b6 e) + 9 * b2 e * b4 e * b6 e) ≥ 12

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
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
⊢ v evr.valtn (-b2 e * b2 e * b8 e + -(8 * b4 e ^ 3) + -(27 * b6 e * b6 e) + 9 * b2 e * b4 e * b6 e) ≥ 12
Tactic:
repeat' apply val_add_ge_of_ge
State after:
case ha.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
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 ha.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
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 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
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))

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
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)

State before:
case ha.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
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 ha.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
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 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
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))

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
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:
. rw [←neg_mul_eq_neg_mul, ←neg_mul_eq_neg_mul, val_neg]
  apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ hb2 hb2) hb8
State after:
case ha.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
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 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
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))

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
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)

State before:
case ha.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
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 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
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))

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
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:
. rw [val_neg, pow_succ', pow_succ', pow_one]
  apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ hb4 hb4) hb4)
State after:
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
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))

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
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)

State before:
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
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))

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
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:
. rw [val_neg, mul_assoc]
  apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ hb6 hb6)
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
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)

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
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:
. rw [mul_assoc, mul_assoc]
  apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ hb2 (val_mul_ge_of_both_ge _ hb4 hb6))
State after:
no goals

State before:
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
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_add_ge_of_ge
State after:
case ha.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
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 ha.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
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))

State before:
case ha.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
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:
rw [←neg_mul_eq_neg_mul, ←neg_mul_eq_neg_mul, val_neg]
State after:
case ha.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
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)

State before:
case ha.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
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:
apply val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ hb2 hb2) hb8
State after:
no goals

State before:
case ha.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
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:
rw [val_neg, pow_succ', pow_succ', pow_one]
State after:
case ha.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
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 * b4 e * b4 e))

State before:
case ha.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
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 * b4 e * b4 e))
Tactic:
apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ (val_mul_ge_of_both_ge _ hb4 hb4) hb4)
State after:
no goals

State before:
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
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:
rw [val_neg, mul_assoc]
State after:
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
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))

State before:
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
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 _ (val_mul_ge_of_both_ge _ hb6 hb6)
State after:
no goals

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
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:
rw [mul_assoc, mul_assoc]
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
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)))

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
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:
apply val_mul_ge_of_right_ge _ (val_mul_ge_of_both_ge _ hb2 (val_mul_ge_of_both_ge _ hb4 hb6))
State after:
no goals