Theorem: Model.val_b2_of_val_a12 (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
⊢ v evr.valtn (b2 e) ≥ 2
Tactic:
simp only [b2]
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

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

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

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
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
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
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
⊢ 2 ≤ v evr.valtn (4 * e.a2)
Tactic:
apply val_mul_ge_of_right_ge evr.valtn h2
State after:
no goals