Theorem: Model.pi_scaling_of_b2 (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
⊢ ENatValRing.sub_val evr 2 (b2 e) =
    ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 1 e.a1 + 4 * ENatValRing.sub_val evr 2 e.a2
Tactic:
erw [←evr.sub_val_mul_right h1, ←evr.sub_val_mul_left h1, evr.sub_val_sub_val,
  ←evr.sub_val_mul_right h2, ←evr.sub_val_add _ _]
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
⊢ ENatValRing.sub_val evr 2 (b2 e) = ENatValRing.sub_val evr (One.one + One.one) (e.a1 * e.a1 + 4 * e.a2)

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
⊢ ↑(One.one + One.one) ≤ v evr.valtn (e.a1 * e.a1)

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
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)

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
⊢ ENatValRing.sub_val evr 2 (b2 e) = ENatValRing.sub_val evr (One.one + One.one) (e.a1 * e.a1 + 4 * e.a2)

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
⊢ ↑(One.one + One.one) ≤ v evr.valtn (e.a1 * e.a1)

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
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)
Tactic:
. rfl
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
⊢ ↑(One.one + One.one) ≤ v evr.valtn (e.a1 * e.a1)

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
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)

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
⊢ ↑(One.one + One.one) ≤ v evr.valtn (e.a1 * e.a1)

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
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)
Tactic:
. exact val_mul_ge_of_both_ge evr.valtn h1 h1
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
⊢ ↑(One.one + One.one) ≤ v evr.valtn (4 * e.a2)

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

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
⊢ ENatValRing.sub_val evr 2 (b2 e) = ENatValRing.sub_val evr (One.one + One.one) (e.a1 * e.a1 + 4 * e.a2)
Tactic:
rfl
State after:
no goals

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
⊢ ↑(One.one + One.one) ≤ v evr.valtn (e.a1 * e.a1)
Tactic:
exact val_mul_ge_of_both_ge evr.valtn h1 h1
State after:
no goals

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