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

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ val_discr_to_nat evr.valtn (pi_scaling evr e h1 h2 h3 h4 h6) = val_discr_to_nat evr.valtn e - 12
Tactic:
apply_fun (Nat.cast : ℕ → ℕ∞) using Nat.cast_injective (R := ℕ∞)
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(val_discr_to_nat evr.valtn (pi_scaling evr e h1 h2 h3 h4 h6)) = ↑(val_discr_to_nat evr.valtn e - 12)

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑(val_discr_to_nat evr.valtn (pi_scaling evr e h1 h2 h3 h4 h6)) = ↑(val_discr_to_nat evr.valtn e - 12)
Tactic:
rw [ofN_val_discr_to_nat, pi_scaling_toModel evr e h1 h2 h3 h4 h6,
  Model.discr_of_pi_scaling _ _ h1 h2 h3 h4 h6, evr.val_sub_val_eq]
State after:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑?m - ↑12 = ↑(val_discr_to_nat evr.valtn e - 12)

case m
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ℕ

case h
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ v evr.valtn (Model.discr e.toModel) = ↑?m

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ↑?m - ↑12 = ↑(val_discr_to_nat evr.valtn e - 12)

case m
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ ℕ

case h
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ v evr.valtn (Model.discr e.toModel) = ↑?m
Tactic:
norm_cast
State after:
case h
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ v evr.valtn (Model.discr e.toModel) = ↑(val_discr_to_nat evr.valtn e)

State before:
case h
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
evr : ENatValRing p
e : ValidModel R
h1 : v evr.valtn e.a1 ≥ 1
h2 : v evr.valtn e.a2 ≥ 2
h3 : v evr.valtn e.a3 ≥ 3
h4 : v evr.valtn e.a4 ≥ 4
h6 : v evr.valtn e.a6 ≥ 6
⊢ v evr.valtn (Model.discr e.toModel) = ↑(val_discr_to_nat evr.valtn e)
Tactic:
rw [ofN_val_discr_to_nat]
State after:
no goals