Theorem: Int.nat_val_aux_mul_eq_add (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
⊢ nat_valuation_aux p hp (a * b) = nat_valuation_aux p hp a + nat_valuation_aux p hp b
Tactic:
cases a with
  | zero => simp [nat_valuation_aux]
  | succ a => cases b with
    | zero => simp [nat_valuation_aux]
    | succ b =>
      exact nat_val_aux'_mul_eq_add p prime prime.one_lt a.succ b.succ _ _
State after:
no goals

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
b : ℕ
⊢ nat_valuation_aux p hp (Nat.zero * b) = nat_valuation_aux p hp Nat.zero + nat_valuation_aux p hp b
Tactic:
simp [nat_valuation_aux]
State after:
no goals

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
b a : ℕ
⊢ nat_valuation_aux p hp (Nat.succ a * b) = nat_valuation_aux p hp (Nat.succ a) + nat_valuation_aux p hp b
Tactic:
cases b with
| zero => simp [nat_valuation_aux]
| succ b =>
exact nat_val_aux'_mul_eq_add p prime prime.one_lt a.succ b.succ _ _
State after:
no goals

State before:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a : ℕ
⊢ nat_valuation_aux p hp (Nat.succ a * Nat.zero) = nat_valuation_aux p hp (Nat.succ a) + nat_valuation_aux p hp Nat.zero
Tactic:
simp [nat_valuation_aux]
State after:
no goals

State before:
case succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
⊢ nat_valuation_aux p hp (Nat.succ a * Nat.succ b) =
    nat_valuation_aux p hp (Nat.succ a) + nat_valuation_aux p hp (Nat.succ b)
Tactic:
exact nat_val_aux'_mul_eq_add p prime prime.one_lt a.succ b.succ _ _
State after:
no goals