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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p m : ℕ
hp : 1 < p
⊢ nat_valuation p m = nat_valuation_aux p hp m
Tactic:
cases p
State after:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hp : 1 < Nat.zero
⊢ nat_valuation Nat.zero m = nat_valuation_aux Nat.zero hp m

case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m n✝ : ℕ
hp : 1 < Nat.succ n✝
⊢ nat_valuation (Nat.succ n✝) m = nat_valuation_aux (Nat.succ n✝) hp m

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hp : 1 < Nat.zero
⊢ nat_valuation Nat.zero m = nat_valuation_aux Nat.zero hp m
Tactic:
case zero => cases hp
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m p : ℕ
hp : 1 < Nat.succ p
⊢ nat_valuation (Nat.succ p) m = nat_valuation_aux (Nat.succ p) hp m
Tactic:
case succ p =>
  cases p
  case zero => cases hp.ne rfl
  case succ q =>
    cases m
    . rfl
    . simp [nat_valuation]
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hp : 1 < Nat.zero
⊢ nat_valuation Nat.zero m = nat_valuation_aux Nat.zero hp m
Tactic:
cases hp
State after:
no goals

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

case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m n✝ : ℕ
hp : 1 < Nat.succ (Nat.succ n✝)
⊢ nat_valuation (Nat.succ (Nat.succ n✝)) m = nat_valuation_aux (Nat.succ (Nat.succ n✝)) hp m

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hp : 1 < Nat.succ Nat.zero
⊢ nat_valuation (Nat.succ Nat.zero) m = nat_valuation_aux (Nat.succ Nat.zero) hp m
Tactic:
case zero => cases hp.ne rfl
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m q : ℕ
hp : 1 < Nat.succ (Nat.succ q)
⊢ nat_valuation (Nat.succ (Nat.succ q)) m = nat_valuation_aux (Nat.succ (Nat.succ q)) hp m
Tactic:
case succ q =>
  cases m
  . rfl
  . simp [nat_valuation]
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hp : 1 < Nat.succ Nat.zero
⊢ nat_valuation (Nat.succ Nat.zero) m = nat_valuation_aux (Nat.succ Nat.zero) hp m
Tactic:
cases hp.ne rfl
State after:
no goals

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

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

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

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

State before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hp : 1 < Nat.succ (Nat.succ q)
n✝ : ℕ
⊢ nat_valuation (Nat.succ (Nat.succ q)) (Nat.succ n✝) = nat_valuation_aux (Nat.succ (Nat.succ q)) hp (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 : ℕ
hp : 1 < Nat.succ (Nat.succ q)
⊢ nat_valuation (Nat.succ (Nat.succ q)) Nat.zero = nat_valuation_aux (Nat.succ (Nat.succ q)) hp Nat.zero
Tactic:
rfl
State after:
no goals

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