internlm/Lean-Github huggingface dataset:
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inr.inr.hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ M →
      ∀ (hm : 0 < m) (n : ℕ) (hmq : m % q = 0),
        nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
m : ℕ
m_le_sM : m ≤ Nat.succ M
hm : 0 < m
n : ℕ
hmq : m % q = 0
meqsM : m = Nat.succ M
h : ¬(m / q % q == 0) = true
⊢ (m % q == 0) = true

case succ.inr.inr.hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ M →
      ∀ (hm : 0 < m) (n : ℕ) (hmq : m % q = 0),
        nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
m : ℕ
m_le_sM : m ≤ Nat.succ M
hm : 0 < m
n : ℕ
hmq : m % q = 0
meqsM : m = Nat.succ M
h : ¬(m / q % q == 0) = true
⊢ (m % q == 0) = true

case succ.inr.inr.hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ M →
      ∀ (hm : 0 < m) (n : ℕ) (hmq : m % q = 0),
        nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
m : ℕ
m_le_sM : m ≤ Nat.succ M
hm : 0 < m
n : ℕ
hmq : m % q = 0
meqsM : m = Nat.succ M
h : ¬(m / q % q == 0) = true
⊢ (m % q == 0) = true
Tactic:
simp
Proof state after:
case succ.inr.inr.hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ M →
      ∀ (hm : 0 < m) (n : ℕ) (hmq : m % q = 0),
        nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
m : ℕ
m_le_sM : m ≤ Nat.succ M
hm : 0 < m
n : ℕ
hmq : m % q = 0
meqsM : m = Nat.succ M
h : ¬(m / q % q == 0) = true
⊢ m % q = 0
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inr.inr.hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ M →
      ∀ (hm : 0 < m) (n : ℕ) (hmq : m % q = 0),
        nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
m : ℕ
m_le_sM : m ≤ Nat.succ M
hm : 0 < m
n : ℕ
hmq : m % q = 0
meqsM : m = Nat.succ M
h : ¬(m / q % q == 0) = true
⊢ m % q = 0
Tactic:
. simp only [hmq]
Proof state after:
no goals
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inr.inr.hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
IH :
  ∀ (m : ℕ),
    m ≤ M →
      ∀ (hm : 0 < m) (n : ℕ) (hmq : m % q = 0),
        nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
m : ℕ
m_le_sM : m ≤ Nat.succ M
hm : 0 < m
n : ℕ
hmq : m % q = 0
meqsM : m = Nat.succ M
h : ¬(m / q % q == 0) = true
⊢ m % q = 0
Tactic:
simp only [hmq]
Proof state after:
no goals
Theorem: nat_valuation_aux''_of_not_dvd
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
⊢ nat_valuation_aux'' q hq m hm 0 = 0
Tactic:
have hmq_bool : ¬m % q == 0 := by
  intro H
  apply hmq (eq_of_beq H)
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
hmq_bool : ¬(m % q == 0) = true
⊢ nat_valuation_aux'' q hq m hm 0 = 0
Theorem: nat_valuation_aux''_of_not_dvd
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
hmq_bool : ¬(m % q == 0) = true
⊢ nat_valuation_aux'' q hq m hm 0 = 0
Tactic:
rw [nat_valuation_aux'', dif_neg hmq_bool]
Proof state after:
no goals
Theorem: nat_valuation_aux''_of_not_dvd
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
⊢ ¬(m % q == 0) = true
Tactic:
intro H
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
H : (m % q == 0) = true
⊢ False
Theorem: nat_valuation_aux''_of_not_dvd
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
H : (m % q == 0) = true
⊢ False
Tactic:
apply hmq (eq_of_beq H)
Proof state after:
no goals
Theorem: nat_valuation_aux'_of_not_dvd
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
⊢ nat_valuation_aux' q hq m hm = 0
Tactic:
rw [nat_valuation_aux']
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
⊢ (match m, hm with
    | m, hm => ↑(nat_valuation_aux'' q hq m hm 0)) =
    0
Theorem: nat_valuation_aux'_of_not_dvd
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q ≠ 0
⊢ (match m, hm with
    | m, hm => ↑(nat_valuation_aux'' q hq m hm 0)) =
    0
Tactic:
simp [nat_valuation_aux''_of_not_dvd q hq m hm hmq]
Proof state after:
no goals
Theorem: nat_valuation_aux'_of_dvd
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
hm : 0 < m
hmq : m % q = 0
⊢ nat_valuation_aux' q hq m hm = nat_valuation_aux' q hq (m / q) (_ : 0 < m / q) + 1
Tactic:
simp [nat_valuation_aux', nat_valuation_aux''_of_dvd q hq m hm 0 hmq]
Proof state after:
no goals
Theorem: nat_val_aux'_succ
Proof 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]
Proof 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
Theorem: nat_val_aux'_succ
Proof 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
Proof state after:
no goals
Theorem: nat_val_aux'_succ
Proof 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)]
Proof 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
Theorem: nat_val_aux'_succ
Proof 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
Proof state after:
no goals
Theorem: nat_val_aux'_succ
Proof 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]
Proof 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
Theorem: nat_val_aux'_succ
Proof 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
Proof state after:
no goals
Theorem: nat_val_aux_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 1 < p
⊢ nat_valuation_aux p hp 0 = ⊤
Tactic:
simp [nat_valuation_aux]
Proof state after:
no goals
Theorem: nat_val_aux_succ
Proof 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]
Proof 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
Theorem: nat_val_aux_succ
Proof 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
Proof 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
Theorem: nat_val_aux_succ
Proof 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
Proof 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
Theorem: nat_val_aux_succ
Proof 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
Proof state after:
no goals
Theorem: nat_val_aux_succ
Proof 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)
Proof 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
Theorem: nat_val_aux_succ
Proof 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]
Proof 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
Theorem: nat_val_aux_succ
Proof 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
Proof state after:
no goals
Theorem: nat_val_aux_succ
Proof 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
Proof 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)
Theorem: nat_val_aux_succ
Proof 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)
Proof state after:
no goals
Theorem: nat_val_aux_succ
Proof 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]
Proof 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
Theorem: nat_val_aux_succ
Proof 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
Proof state after:
no goals
Theorem: nat_valuation_add_two
Proof 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
Proof 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✝)
Theorem: nat_valuation_add_two
Proof 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
Proof 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✝)
Theorem: nat_valuation_add_two
Proof 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]
Proof state after:
no goals
Theorem: nat_valuation_add_two
Proof 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
Proof state after:
no goals
Theorem: nat_valuation_add_two
Proof 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]
Proof state after:
no goals
Theorem: nat_valuation_of_one_lt
Proof 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
Proof 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
Theorem: nat_valuation_of_one_lt
Proof 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
Proof state after:
no goals
Theorem: nat_valuation_of_one_lt
Proof 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]
Proof state after:
no goals
Theorem: nat_valuation_of_one_lt
Proof 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
Proof state after:
no goals
Theorem: nat_valuation_of_one_lt
Proof 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
Proof 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
Theorem: nat_valuation_of_one_lt
Proof 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
Proof state after:
no goals
Theorem: nat_valuation_of_one_lt
Proof 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]
Proof state after:
no goals
Theorem: nat_valuation_of_one_lt
Proof 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
Proof state after:
no goals
Theorem: nat_valuation_of_one_lt
Proof 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
Proof 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✝)
Theorem: nat_valuation_of_one_lt
Proof 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
Proof 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✝)
Theorem: nat_valuation_of_one_lt
Proof 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]
Proof state after:
no goals
Theorem: nat_valuation_of_one_lt
Proof 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
Proof state after:
no goals
Theorem: nat_valuation_of_one_lt
Proof 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]
Proof state after:
no goals
Theorem: nat_val_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
⊢ nat_valuation p 0 = ⊤
Tactic:
simp [nat_valuation]
Proof state after:
no goals
Theorem: nat_val_succ
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q m : ℕ
⊢ nat_valuation (q + 2) (m + 1) = if (m + 1) % (q + 2) ≠ 0 then 0 else nat_valuation (q + 2) ((m + 1) / (q + 2)) + 1
Tactic:
simp [nat_valuation_add_two, nat_val_aux_succ]
Proof state after:
no goals
Theorem: Int.int_val_uniformizer
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
⊢ int_val p ↑p = 1
Tactic:
simp only [natAbs_cast, int_val]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
⊢ nat_valuation p p = 1