Theorem: Model.pi_scaling_of_b4 (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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ENatValRing.sub_val evr 4 (b4 e) =
    ENatValRing.sub_val evr 1 e.a1 * ENatValRing.sub_val evr 3 e.a3 + 2 * ENatValRing.sub_val evr 4 e.a4
Tactic:
erw [←evr.sub_val_mul_right h3, ←evr.sub_val_mul_left h1, evr.sub_val_sub_val,
  ←evr.sub_val_mul_right h4, ←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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ENatValRing.sub_val evr 4 (b4 e) = ENatValRing.sub_val evr (One.one + 3) (e.a1 * e.a3 + 2 * e.a4)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (e.a1 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)

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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ENatValRing.sub_val evr 4 (b4 e) = ENatValRing.sub_val evr (One.one + 3) (e.a1 * e.a3 + 2 * e.a4)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (e.a1 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)
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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (e.a1 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)

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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (e.a1 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h1 : v evr.valtn e.a1 ≥ 1
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)
Tactic:
. exact val_mul_ge_of_both_ge evr.valtn h1 h3
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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)

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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)
Tactic:
. exact val_mul_ge_of_right_ge evr.valtn h4
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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ENatValRing.sub_val evr 4 (b4 e) = ENatValRing.sub_val evr (One.one + 3) (e.a1 * e.a3 + 2 * e.a4)
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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (e.a1 * e.a3)
Tactic:
exact val_mul_ge_of_both_ge evr.valtn h1 h3
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
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
⊢ ↑(One.one + 3) ≤ v evr.valtn (2 * e.a4)
Tactic:
exact val_mul_ge_of_right_ge evr.valtn h4
State after:
no goals