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

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ v valp (Model.b2 (rst_iso r s t e).toModel) ≥ 1
Tactic:
simp only [rst_iso]
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ v valp (Model.b2 (Model.rst_iso r s t e.toModel)) ≥ 1

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ v valp (Model.b2 (Model.rst_iso r s t e.toModel)) ≥ 1
Tactic:
rw [Model.rst_b2]
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ v valp (Model.b2 e.toModel + 12 * r) ≥ 1

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ v valp (Model.b2 e.toModel + 12 * r) ≥ 1
Tactic:
apply val_add_ge_of_ge valp h_b2
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ 1 ≤ v valp (12 * r)

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
e : ValidModel R
r s t : R
h_b2 : v valp (Model.b2 e.toModel) ≥ 1
h_p : v valp 12 ≥ 1
⊢ 1 ≤ v valp (12 * r)
Tactic:
exact val_mul_ge_of_left_ge valp h_p
State after:
no goals