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

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
q : ℕ∞
p : R
valp : SurjVal p
e : ValidModel R
h1 : v valp e.a1 ≥ 1
h3 : v valp e.a3 ≥ q
h4 : v valp e.a4 ≥ q + 1
⊢ v valp (Model.b4 e.toModel) ≥ q + 1
Tactic:
apply val_add_ge_of_ge valp <;>
. simp
  elinarith
State after:
no goals

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

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