Theorem: nat_valuation_add_two (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
⊢ nat_valuation (q + 2) m = nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) m
Tactic:
cases m
State after:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
⊢ nat_valuation (q + 2) Nat.zero = nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) Nat.zero

case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q n✝ : ℕ
⊢ nat_valuation (q + 2) (Nat.succ n✝) = nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (Nat.succ n✝)

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
⊢ nat_valuation (q + 2) Nat.zero = nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) Nat.zero

case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q n✝ : ℕ
⊢ nat_valuation (q + 2) (Nat.succ n✝) = nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (Nat.succ n✝)
Tactic:
. rfl
State after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q n✝ : ℕ
⊢ nat_valuation (q + 2) (Nat.succ n✝) = nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (Nat.succ n✝)

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q n✝ : ℕ
⊢ nat_valuation (q + 2) (Nat.succ n✝) = nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (Nat.succ n✝)
Tactic:
. simp [nat_valuation]
State after:
no goals

State before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
⊢ nat_valuation (q + 2) Nat.zero = nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) Nat.zero
Tactic:
rfl
State after:
no goals

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q n✝ : ℕ
⊢ nat_valuation (q + 2) (Nat.succ n✝) = nat_valuation_aux (q + 2) (_ : Nat.succ 0 < Nat.succ (q + 1)) (Nat.succ n✝)
Tactic:
simp [nat_valuation]
State after:
no goals