Theorem: nat_val_aux'_succ (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < Nat.succ m) =
    if hmq : (m + 1) % (q + 2) ≠ 0 then 0
    else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2)) + 1
Tactic:
simp only [Nat.succ_ne_zero, dite_false, ne_eq, ite_not]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < Nat.succ m) =
    if hmq : ¬(m + 1) % (q + 2) = 0 then 0
    else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2)) + 1

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < Nat.succ m) =
    if hmq : ¬(m + 1) % (q + 2) = 0 then 0
    else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2)) + 1
Tactic:
cases em ((m + 1) % (q + 2) = 0) with
| inl h =>
  rw [dif_neg (not_not_intro h)]
  exact nat_valuation_aux'_of_dvd _ _ _ _ h
| inr h =>
  rw [dif_pos h]
  exact nat_valuation_aux'_of_not_dvd _ _ _ _ h
State after:
no goals

State before:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
h : (m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < Nat.succ m) =
    if hmq : ¬(m + 1) % (q + 2) = 0 then 0
    else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2)) + 1
Tactic:
rw [dif_neg (not_not_intro h)]
State after:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
h : (m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < Nat.succ m) =
    nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2)) + 1

State before:
case inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
h : (m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < Nat.succ m) =
    nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2)) + 1
Tactic:
exact nat_valuation_aux'_of_dvd _ _ _ _ h
State after:
no goals

State before:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
h : ¬(m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < Nat.succ m) =
    if hmq : ¬(m + 1) % (q + 2) = 0 then 0
    else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2)) + 1
Tactic:
rw [dif_pos h]
State after:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
h : ¬(m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < Nat.succ m) = 0

State before:
case inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
h : ¬(m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < Nat.succ m) = 0
Tactic:
exact nat_valuation_aux'_of_not_dvd _ _ _ _ h
State after:
no goals