Theorem: ValidModel.v_discr_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
hq : q > 1
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.discr e.toModel) ≥ 2 * ↑q + 3
Tactic:
have h2' : valp e.b2 ≥ 1 := v_b2_of_v_a1_a2 valp e h1 h2
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
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' : v valp (Model.b2 e.toModel) ≥ 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
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' : v valp (Model.b2 e.toModel) ≥ 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Tactic:
have h4' : valp e.b4 ≥ q + 1 := v_b4_of_v_a1_a3_a4 valp e h1 h3 h4
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
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' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
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' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Tactic:
have h6' : valp e.b6 ≥ 2 * q := v_b6_of_v_a3_a6 valp e h3 h6
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
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' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
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' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
Tactic:
have h8' : valp e.b8 ≥ 2 * q + 1 := v_b8_of_v_ai valp e h1 h2 h3 h4 h6
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
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' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
h8' : v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
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' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
h8' : v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
⊢ v valp (Model.discr e.toModel) ≥ 2 * ↑q + 3
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
hq : q > 1
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' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
h8' : v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 3 ≤ v valp (9 * Model.b2 e.toModel * Model.b4 e.toModel * Model.b6 e.toModel)
Tactic:
simp
State after:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
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' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
h8' : v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 3 ≤ v valp 9 + v valp (Model.b2 e.toModel) + v valp (Model.b4 e.toModel) + v valp (Model.b6 e.toModel)

State before:
case hb
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
q : ℕ
valp : SurjVal p
e : ValidModel R
hq : q > 1
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' : v valp (Model.b2 e.toModel) ≥ 1
h4' : v valp (Model.b4 e.toModel) ≥ ↑q + 1
h6' : v valp (Model.b6 e.toModel) ≥ 2 * ↑q
h8' : v valp (Model.b8 e.toModel) ≥ 2 * ↑q + 1
h2_symm : 1 = v valp e.a2
⊢ 2 * ↑q + 3 ≤ v valp 9 + v valp (Model.b2 e.toModel) + v valp (Model.b4 e.toModel) + v valp (Model.b6 e.toModel)
Tactic:
elinarith
State after:
no goals