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

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
hp : p = 2 ∨ p = 3
valp : SurjVal p
⊢ v valp 12 ≥ 1
Tactic:
cases hp with
| inl p2 =>
  rw [(show (12 : R) = 2 * 6 by norm_num)]
  apply val_mul_ge_of_left_ge
  rw [←p2]
  exact le_of_eq (valp.v_uniformizer).symm
| inr p3 =>
  rw [(show (12 : R) = 3 * 4 by norm_num)]
  apply val_mul_ge_of_left_ge
  rw [←p3]
  exact le_of_eq (valp.v_uniformizer).symm
State after:
no goals

State before:
case inl
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ v valp 12 ≥ 1
Tactic:
rw [(show (12 : R) = 2 * 6 by norm_num)]
State after:
case inl
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ v valp (2 * 6) ≥ 1

State before:
case inl
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ v valp (2 * 6) ≥ 1
Tactic:
apply val_mul_ge_of_left_ge
State after:
case inl.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 1 ≤ v valp 2

State before:
case inl.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 1 ≤ v valp 2
Tactic:
rw [←p2]
State after:
case inl.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 1 ≤ v valp p

State before:
case inl.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 1 ≤ v valp p
Tactic:
exact le_of_eq (valp.v_uniformizer).symm
State after:
no goals

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p2 : p = 2
⊢ 12 = 2 * 6
Tactic:
norm_num
State after:
no goals

State before:
case inr
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ v valp 12 ≥ 1
Tactic:
rw [(show (12 : R) = 3 * 4 by norm_num)]
State after:
case inr
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ v valp (3 * 4) ≥ 1

State before:
case inr
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ v valp (3 * 4) ≥ 1
Tactic:
apply val_mul_ge_of_left_ge
State after:
case inr.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ 1 ≤ v valp 3

State before:
case inr.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ 1 ≤ v valp 3
Tactic:
rw [←p3]
State after:
case inr.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ 1 ≤ v valp p

State before:
case inr.ha
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ 1 ≤ v valp p
Tactic:
exact le_of_eq (valp.v_uniformizer).symm
State after:
no goals

State before:
R : Type u
inst✝ : CommRing R
inst : IsDomain R
p : R
valp : SurjVal p
p3 : p = 3
⊢ 12 = 3 * 4
Tactic:
norm_num
State after:
no goals