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

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

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

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

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
State after:
no goals

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
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
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
State after:
no goals