Theorem: Model.pi_scaling_of_b6 (ECTate/Algebra/EllipticCurve/LocalEC.lean)

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 6 (b6 e) =
    ENatValRing.sub_val evr 3 e.a3 * ENatValRing.sub_val evr 3 e.a3 + 4 * ENatValRing.sub_val evr 6 e.a6
Tactic:
rw [←evr.sub_val_mul_right h3, ←evr.sub_val_mul_left h3, evr.sub_val_sub_val,
  ←evr.sub_val_mul_right h6, ←evr.sub_val_add _ _]
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 6 (b6 e) = ENatValRing.sub_val evr (3 + 3) (e.a3 * e.a3 + 4 * e.a6)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 6 (b6 e) = ENatValRing.sub_val evr (3 + 3) (e.a3 * e.a3 + 4 * e.a6)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
Tactic:
. rfl
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)

R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
Tactic:
. exact val_mul_ge_of_both_ge evr.valtn h3 h3
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
Tactic:
. exact val_mul_ge_of_right_ge evr.valtn h6
State after:
no goals

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ENatValRing.sub_val evr 6 (b6 e) = ENatValRing.sub_val evr (3 + 3) (e.a3 * e.a3 + 4 * e.a6)
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
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (e.a3 * e.a3)
Tactic:
exact val_mul_ge_of_both_ge evr.valtn h3 h3
State after:
no goals

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : Model R
h3 : v evr.valtn e.a3 ≥ 3
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(3 + 3) ≤ v evr.valtn (4 * e.a6)
Tactic:
exact val_mul_ge_of_right_ge evr.valtn h6
State after:
no goals