Theorem: ValidModel.v_b8_of_v_ai (ECTate/Algebra/EllipticCurve/LocalEC.lean)

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
⊢ v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
Tactic:
apply_rules [val_add_ge_of_ge, val_sub_ge_of_ge] <;>
. simp
  elinarith
State after:
no goals

State before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 1 ≤ v valp (e.a4 * e.a4)
Tactic:
simp
State after:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 1 ≤ v valp e.a4 + v valp e.a4

State before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h2 : v valp e.a2 = 1
h3 : v valp e.a3 ≥ ↑q
h4 : v valp e.a4 ≥ ↑q + 1
h6 : v valp e.a6 ≥ 2 * ↑q
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 1 ≤ v valp e.a4 + v valp e.a4
Tactic:
elinarith
State after:
no goals