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) =
    if (m + 1) % (q + 2) ≠ 0 then 0 else nat_valuation_aux (q + 2) hq ((m + 1) / (q + 2)) + 1
Tactic:
simp only [nat_valuation_aux, 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 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0

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 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0
Tactic:
by_cases hmq : (m + 1) % (q + 2) = 0
State after:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : (m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0

case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : ¬(m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0

State before:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : (m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0

case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : ¬(m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0
Tactic:
. have h : (m + 1) / (q + 2) ≠ 0 := by
    apply Nat.ne_of_gt
    exact Nat.div_pos (x' hmq) (lt_trans (Nat.lt_succ_self 0) hq)
  rw [if_pos hmq, dif_neg h]
  exact nat_valuation_aux'_of_dvd (q+2) hq (m+1) _ hmq
State after:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : ¬(m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0

State before:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : ¬(m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0
Tactic:
. rw [if_neg hmq]
  exact nat_valuation_aux'_of_not_dvd (q+2) hq (m+1) _ hmq
State after:
no goals

State before:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : (m + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0
Tactic:
have h : (m + 1) / (q + 2) ≠ 0 := by
  apply Nat.ne_of_gt
  exact Nat.div_pos (x' hmq) (lt_trans (Nat.lt_succ_self 0) hq)
State after:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : (m + 1) % (q + 2) = 0
h : (m + 1) / (q + 2) ≠ 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0

State before:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : (m + 1) % (q + 2) = 0
h : (m + 1) / (q + 2) ≠ 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) =
    if (m + 1) % (q + 2) = 0 then
      (if hm : (m + 1) / (q + 2) = 0 then ⊤
        else nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2))) +
        1
    else 0
Tactic:
rw [if_pos hmq, dif_neg h]
State after:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : (m + 1) % (q + 2) = 0
h : (m + 1) / (q + 2) ≠ 0
⊢ nat_valuation_aux' (q + 2) hq (m + 1) (_ : 0 < m + 1) =
    nat_valuation_aux' (q + 2) hq ((m + 1) / (q + 2)) (_ : 0 < (m + 1) / (q + 2)) + 1

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

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : (m + 1) % (q + 2) = 0
⊢ (m + 1) / (q + 2) ≠ 0
Tactic:
apply Nat.ne_of_gt
State after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : (m + 1) % (q + 2) = 0
⊢ 0 < (m + 1) / (q + 2)

State before:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
hq : 1 < q + 2
hmq : (m + 1) % (q + 2) = 0
⊢ 0 < (m + 1) / (q + 2)
Tactic:
exact Nat.div_pos (x' hmq) (lt_trans (Nat.lt_succ_self 0) hq)
State after:
no goals

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

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