internlm/Lean-Github huggingface dataset:
Theorem: ENatValRing.sub_val_sub_val
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
⊢ ∀ (y : R), sub_val evr n (sub_val evr (Nat.succ m) y) = sub_val evr (Nat.succ m + n) y
Tactic:
intro y
Proof state after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
⊢ sub_val evr n (sub_val evr (Nat.succ m) y) = sub_val evr (Nat.succ m + n) y
Theorem: ENatValRing.sub_val_sub_val
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
⊢ sub_val evr n (sub_val evr (Nat.succ m) y) = sub_val evr (Nat.succ m + n) y
Tactic:
cases @eq_zero_or_pos _ _ (evr.valtn y) with
| inl h' => simp [sub_val_val_zero evr y _ h']
| inr h' =>
  rw [sub_val_val_pos_succ evr y m, Nat.succ_add, sub_val_val_pos_succ evr y _]
  exact ih (evr.decr_val y)
Proof state after:
no goals
Theorem: ENatValRing.sub_val_sub_val
Proof state before:
case succ.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
h' : v evr.valtn y = 0
⊢ sub_val evr n (sub_val evr (Nat.succ m) y) = sub_val evr (Nat.succ m + n) y
Tactic:
simp [sub_val_val_zero evr y _ h']
Proof state after:
no goals
Theorem: ENatValRing.sub_val_sub_val
Proof state before:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
h' : 0 < v evr.valtn y
⊢ sub_val evr n (sub_val evr (Nat.succ m) y) = sub_val evr (Nat.succ m + n) y
Tactic:
rw [sub_val_val_pos_succ evr y m, Nat.succ_add, sub_val_val_pos_succ evr y _]
Proof state after:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
h' : 0 < v evr.valtn y
⊢ sub_val evr n (sub_val evr m (decr_val evr y)) = sub_val evr (m + n) (decr_val evr y)
Theorem: ENatValRing.sub_val_sub_val
Proof state before:
case succ.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
x : R
n m : ℕ
ih : ∀ (y : R), sub_val evr n (sub_val evr m y) = sub_val evr (m + n) y
y : R
h' : 0 < v evr.valtn y
⊢ sub_val evr n (sub_val evr m (decr_val evr y)) = sub_val evr (m + n) (decr_val evr y)
Tactic:
exact ih (evr.decr_val y)
Proof state after:
no goals
Theorem: ENatValRing.val_poly_of_double_root
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
a b c : R
H : has_double_root evr a b c
⊢ v evr.valtn (a * double_root evr a b c ^ 2 + b * double_root evr a b c + c) > 0 ∧
    v evr.valtn (2 * a * double_root evr a b c + b) > 0
Tactic:
sorry
Proof state after:
no goals
Theorem: ENatValRing.pth_root_pos_of_pos
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
⊢ v evr.valtn (pth_root evr r) > 0
Tactic:
suffices 0 < evr.valtn (evr.pth_root r ^ evr.residue_char) by
  . simp at this
    exact this.2
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
Theorem: ENatValRing.pth_root_pos_of_pos
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
Tactic:
have :
  min (SurjVal.v evr.valtn (pth_root evr r ^ evr.residue_char - r)) (SurjVal.v evr.valtn r) > 0 :=
min_rec' (LT.lt 0) (evr.pth_root_spec.resolve_left hchar r) ha
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : min (v evr.valtn (pth_root evr r ^ evr.residue_char - r)) (v evr.valtn r) > 0
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
Theorem: ENatValRing.pth_root_pos_of_pos
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : min (v evr.valtn (pth_root evr r ^ evr.residue_char - r)) (v evr.valtn r) > 0
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
Tactic:
have := this.trans_le (evr.valtn.v_add_ge_min_v (evr.pth_root r ^ evr.residue_char - r) r)
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this✝ : min (v evr.valtn (pth_root evr r ^ evr.residue_char - r)) (v evr.valtn r) > 0
this : 0 < v evr.valtn (pth_root evr r ^ evr.residue_char - r + r)
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
Theorem: ENatValRing.pth_root_pos_of_pos
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this✝ : min (v evr.valtn (pth_root evr r ^ evr.residue_char - r)) (v evr.valtn r) > 0
this : 0 < v evr.valtn (pth_root evr r ^ evr.residue_char - r + r)
⊢ 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
Tactic:
simpa using this
Proof state after:
no goals
Theorem: ENatValRing.pth_root_pos_of_pos
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
⊢ v evr.valtn (pth_root evr r) > 0
Tactic:
. simp at this
  exact this.2
Proof state after:
no goals
Theorem: ENatValRing.pth_root_pos_of_pos
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : 0 < v evr.valtn (pth_root evr r ^ evr.residue_char)
⊢ v evr.valtn (pth_root evr r) > 0
Tactic:
simp at this
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : 0 < evr.residue_char ∧ 0 < v evr.valtn (pth_root evr r)
⊢ v evr.valtn (pth_root evr r) > 0
Theorem: ENatValRing.pth_root_pos_of_pos
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
evr : ENatValRing p
r : R
ha : 0 < v evr.valtn r
hchar : evr.residue_char ≠ 0
this : 0 < evr.residue_char ∧ 0 < v evr.valtn (pth_root evr r)
⊢ v evr.valtn (pth_root evr r) > 0
Tactic:
exact this.2
Proof state after:
no goals
Theorem: ndiv_mul_left
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
⊢ a * b % p ≠ 0 → a % p ≠ 0
Tactic:
intro hab ha
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
hab : a * b % p ≠ 0
ha : a % p = 0
⊢ False
Theorem: ndiv_mul_left
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
hab : a * b % p ≠ 0
ha : a % p = 0
⊢ False
Tactic:
apply hab
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
hab : a * b % p ≠ 0
ha : a % p = 0
⊢ a * b % p = 0
Theorem: ndiv_mul_left
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
hab : a * b % p ≠ 0
ha : a % p = 0
⊢ a * b % p = 0
Tactic:
simp [Nat.mul_mod, ha]
Proof state after:
no goals
Theorem: ndiv_mul_right
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
⊢ a * b % p ≠ 0 → b % p ≠ 0
Tactic:
rw [Nat.mul_comm]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
⊢ b * a % p ≠ 0 → b % p ≠ 0
Theorem: ndiv_mul_right
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b p : ℕ
⊢ b * a % p ≠ 0 → b % p ≠ 0
Tactic:
exact ndiv_mul_left b a p
Proof state after:
no goals
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
⊢ ∀ (M 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
Tactic:
intro M
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
⊢ ∀ (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
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
M : ℕ
⊢ ∀ (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
Tactic:
induction M with
| zero =>
  intro m mle0 hm n hmq
  rw [Nat.le_zero] at mle0
  exact ((ne_of_gt hm) mle0).elim
| succ M IH =>
  intro m m_le_sM hm n hmq
  cases LE.le.lt_or_eq m_le_sM with
  | inl mltsM =>
    exact IH m (Nat.le_of_lt_succ mltsM) hm n hmq
  | inr meqsM =>
    cases em ((m / q) % q == 0) with
    | inl h =>
      rw [nat_valuation_aux'', nat_valuation_aux'', dif_pos h]
      simp only [beq_iff_eq, Nat.cast_succ]
      rw [dif_pos hmq]
      simp only [meqsM]
      rw [meqsM] at hm h hmq
      exact IH (M.succ/q) (Nat.le_of_lt_succ (Nat.div_lt_self hm hq))
        (Nat.div_pos_of_mod hm hq hmq) (n+1) (by simpa using h)
    | inr h =>
      rw [nat_valuation_aux'', nat_valuation_aux'', dif_neg h, dif_pos, nat_valuation_aux'', dif_neg h]
      simp
      . simp only [hmq]
Proof state after:
no goals
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
⊢ ∀ (m : ℕ),
    m ≤ Nat.zero →
      ∀ (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
Tactic:
intro m mle0 hm n hmq
Proof state after:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
mle0 : m ≤ Nat.zero
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
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
mle0 : m ≤ Nat.zero
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
Tactic:
rw [Nat.le_zero] at mle0
Proof state after:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
mle0 : m = 0
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
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hq : 1 < q
m : ℕ
mle0 : m = 0
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
Tactic:
exact ((ne_of_gt hm) mle0).elim
Proof state after:
no goals
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ
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 ≤ Nat.succ 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
Tactic:
intro m m_le_sM hm n hmq
Proof state after:
case succ
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
⊢ nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ
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
⊢ nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
Tactic:
cases LE.le.lt_or_eq m_le_sM with
| inl mltsM =>
  exact IH m (Nat.le_of_lt_succ mltsM) hm n hmq
| inr meqsM =>
  cases em ((m / q) % q == 0) with
  | inl h =>
    rw [nat_valuation_aux'', nat_valuation_aux'', dif_pos h]
    simp only [beq_iff_eq, Nat.cast_succ]
    rw [dif_pos hmq]
    simp only [meqsM]
    rw [meqsM] at hm h hmq
    exact IH (M.succ/q) (Nat.le_of_lt_succ (Nat.div_lt_self hm hq))
      (Nat.div_pos_of_mod hm hq hmq) (n+1) (by simpa using h)
  | inr h =>
    rw [nat_valuation_aux'', nat_valuation_aux'', dif_neg h, dif_pos, nat_valuation_aux'', dif_neg h]
    simp
    . simp only [hmq]
Proof state after:
no goals
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inl
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
mltsM : m < Nat.succ M
⊢ nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
Tactic:
exact IH m (Nat.le_of_lt_succ mltsM) hm n hmq
Proof state after:
no goals
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inr
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
⊢ nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
Tactic:
cases em ((m / q) % q == 0) with
| inl h =>
  rw [nat_valuation_aux'', nat_valuation_aux'', dif_pos h]
  simp only [beq_iff_eq, Nat.cast_succ]
  rw [dif_pos hmq]
  simp only [meqsM]
  rw [meqsM] at hm h hmq
  exact IH (M.succ/q) (Nat.le_of_lt_succ (Nat.div_lt_self hm hq))
    (Nat.div_pos_of_mod hm hq hmq) (n+1) (by simpa using h)
| inr h =>
  rw [nat_valuation_aux'', nat_valuation_aux'', dif_neg h, dif_pos, nat_valuation_aux'', dif_neg h]
  simp
  . simp only [hmq]
Proof state after:
no goals
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inr.inl
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
⊢ nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
Tactic:
rw [nat_valuation_aux'', nat_valuation_aux'', dif_pos h]
Proof state after:
case succ.inr.inl
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
⊢ (if hmq : (m % q == 0) = true then nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) (n + 1) else n) =
    nat_valuation_aux'' q hq (m / q / q) (_ : 0 < m / q / q) (n + 1) + 1
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inr.inl
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
⊢ (if hmq : (m % q == 0) = true then nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) (n + 1) else n) =
    nat_valuation_aux'' q hq (m / q / q) (_ : 0 < m / q / q) (n + 1) + 1
Tactic:
simp only [beq_iff_eq, Nat.cast_succ]
Proof state after:
case succ.inr.inl
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
⊢ (if h : m % q = 0 then nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) (n + 1) else n) =
    nat_valuation_aux'' q hq (m / q / q) (_ : 0 < m / q / q) (n + 1) + 1
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inr.inl
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
⊢ (if h : m % q = 0 then nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) (n + 1) else n) =
    nat_valuation_aux'' q hq (m / q / q) (_ : 0 < m / q / q) (n + 1) + 1
Tactic:
rw [dif_pos hmq]
Proof state after:
case succ.inr.inl
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
⊢ nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) (n + 1) =
    nat_valuation_aux'' q hq (m / q / q) (_ : 0 < m / q / q) (n + 1) + 1
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inr.inl
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
⊢ nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) (n + 1) =
    nat_valuation_aux'' q hq (m / q / q) (_ : 0 < m / q / q) (n + 1) + 1
Tactic:
simp only [meqsM]
Proof state after:
case succ.inr.inl
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
⊢ nat_valuation_aux'' q hq (Nat.succ M / q) (_ : 0 < Nat.succ M / q) (n + 1) =
    nat_valuation_aux'' q hq (Nat.succ M / q / q) (_ : 0 < Nat.succ M / q / q) (n + 1) + 1
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inr.inl
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
⊢ nat_valuation_aux'' q hq (Nat.succ M / q) (_ : 0 < Nat.succ M / q) (n + 1) =
    nat_valuation_aux'' q hq (Nat.succ M / q / q) (_ : 0 < Nat.succ M / q / q) (n + 1) + 1
Tactic:
rw [meqsM] at hm h hmq
Proof state after:
case succ.inr.inl
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
hm : 0 < Nat.succ M
n : ℕ
hmq✝ : m % q = 0
hmq : Nat.succ M % q = 0
meqsM : m = Nat.succ M
h✝ : (m / q % q == 0) = true
h : (Nat.succ M / q % q == 0) = true
⊢ nat_valuation_aux'' q hq (Nat.succ M / q) (_ : 0 < Nat.succ M / q) (n + 1) =
    nat_valuation_aux'' q hq (Nat.succ M / q / q) (_ : 0 < Nat.succ M / q / q) (n + 1) + 1
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inr.inl
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
hm : 0 < Nat.succ M
n : ℕ
hmq✝ : m % q = 0
hmq : Nat.succ M % q = 0
meqsM : m = Nat.succ M
h✝ : (m / q % q == 0) = true
h : (Nat.succ M / q % q == 0) = true
⊢ nat_valuation_aux'' q hq (Nat.succ M / q) (_ : 0 < Nat.succ M / q) (n + 1) =
    nat_valuation_aux'' q hq (Nat.succ M / q / q) (_ : 0 < Nat.succ M / q / q) (n + 1) + 1
Tactic:
exact IH (M.succ/q) (Nat.le_of_lt_succ (Nat.div_lt_self hm hq))
  (Nat.div_pos_of_mod hm hq hmq) (n+1) (by simpa using h)
Proof state after:
no goals
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
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
hm : 0 < Nat.succ M
n : ℕ
hmq✝ : m % q = 0
hmq : Nat.succ M % q = 0
meqsM : m = Nat.succ M
h✝ : (m / q % q == 0) = true
h : (Nat.succ M / q % q == 0) = true
⊢ Nat.succ M / q % q = 0
Tactic:
simpa using h
Proof state after:
no goals
Theorem: nat_valuation_aux''_of_dvd_induction
Proof state before:
case succ.inr.inr
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
⊢ nat_valuation_aux'' q hq m hm n = nat_valuation_aux'' q hq (m / q) (_ : 0 < m / q) n + 1
Tactic:
rw [nat_valuation_aux'', nat_valuation_aux'', dif_neg h, dif_pos, nat_valuation_aux'', dif_neg h]
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) = 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