internlm/Lean-Github huggingface dataset:
Theorem: Int.int_val_uniformizer
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < p
⊢ nat_valuation p p = 1
Tactic:
match p with
| 0 =>
  apply False.elim
  apply Nat.not_lt_zero 1
  assumption
| Nat.succ 0 =>
  apply False.elim
  apply Nat.lt_irrefl 1
  assumption
| q+2 =>
  rw [nat_val_succ, Nat.mod_self, if_neg _]
  rw [Nat.div_self, nat_val_succ, if_pos, zero_add]
  rw [Nat.mod_eq_of_lt]
  exact Nat.succ_ne_zero 0
  assumption
  exact lt_trans (Nat.lt_succ_self 0) gt1
  exact Ne.irrefl
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 < 0
⊢ nat_valuation 0 0 = 1
Tactic:
apply False.elim
Proof state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < 0
⊢ False
Theorem: Int.int_val_uniformizer
Proof state before:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < 0
⊢ False
Tactic:
apply Nat.not_lt_zero 1
Proof state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < 0
⊢ 1 < 0
Theorem: Int.int_val_uniformizer
Proof state before:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < 0
⊢ 1 < 0
Tactic:
assumption
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 < Nat.succ 0
⊢ nat_valuation (Nat.succ 0) (Nat.succ 0) = 1
Tactic:
apply False.elim
Proof state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.succ 0
⊢ False
Theorem: Int.int_val_uniformizer
Proof state before:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.succ 0
⊢ False
Tactic:
apply Nat.lt_irrefl 1
Proof state after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.succ 0
⊢ 1 < 1
Theorem: Int.int_val_uniformizer
Proof state before:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
gt1 : 1 < Nat.succ 0
⊢ 1 < 1
Tactic:
assumption
Proof state after:
no goals
Theorem: Int.int_val_uniformizer
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ nat_valuation (q + 2) (q + 2) = 1
Tactic:
rw [nat_val_succ, Nat.mod_self, if_neg _]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ nat_valuation (q + 2) ((q + 1 + 1) / (q + 2)) + 1 = 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Theorem: Int.int_val_uniformizer
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ nat_valuation (q + 2) ((q + 1 + 1) / (q + 2)) + 1 = 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
rw [Nat.div_self, nat_val_succ, if_pos, zero_add]
Proof state after:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ (0 + 1) % (q + 2) ≠ 0

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Theorem: Int.int_val_uniformizer
Proof state before:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ (0 + 1) % (q + 2) ≠ 0

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
rw [Nat.mod_eq_of_lt]
Proof state after:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 ≠ 0

case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 < q + 2

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Theorem: Int.int_val_uniformizer
Proof state before:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 ≠ 0

case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 < q + 2

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
exact Nat.succ_ne_zero 0
Proof state after:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 < q + 2

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Theorem: Int.int_val_uniformizer
Proof state before:
case hc
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 + 1 < q + 2

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
assumption
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Theorem: Int.int_val_uniformizer
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ 0 < q + 1 + 1

R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
exact lt_trans (Nat.lt_succ_self 0) gt1
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Theorem: Int.int_val_uniformizer
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : ℕ
gt1 : 1 < q + 2
⊢ ¬0 ≠ 0
Tactic:
exact Ne.irrefl
Proof state after:
no goals
Theorem: Int.int_val_zero
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
⊢ int_val p 0 = ⊤
Tactic:
simp [natAbs_cast, int_val]
Proof state after:
no goals
Theorem: Int.mod_mul
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
h : a % c = 0
⊢ a * b % c = 0
Tactic:
rw [Nat.mul_mod, h, zero_mul, Nat.zero_mod]
Proof state after:
no goals
Theorem: Int.nat_mul_div_assoc
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
⊢ b % c = 0 → a * b / c = a * (b / c)
Tactic:
intro hmod
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : b % c = 0
⊢ a * b / c = a * (b / c)
Theorem: Int.nat_mul_div_assoc
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : b % c = 0
⊢ a * b / c = a * (b / c)
Tactic:
rw [Nat.mul_div_assoc]
Proof state after:
case H
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : b % c = 0
⊢ c ∣ b
Theorem: Int.nat_mul_div_assoc
Proof state before:
case H
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : b % c = 0
⊢ c ∣ b
Tactic:
rwa [← Nat.modEq_zero_iff_dvd]
Proof state after:
no goals
Theorem: Int.nat_mul_div_assoc'
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
⊢ a % c = 0 → a * b / c = a / c * b
Tactic:
intro hmod
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : a % c = 0
⊢ a * b / c = a / c * b
Theorem: Int.nat_mul_div_assoc'
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c : ℕ
hmod : a % c = 0
⊢ a * b / c = a / c * b
Tactic:
rw [Nat.mul_comm, nat_mul_div_assoc hmod, Nat.mul_comm]
Proof state after:
no goals
Theorem: Int.nat_val_aux'_mul_eq_add
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
general :
  ∀ (n c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
⊢ nat_valuation_aux' p hp (a * b) (_ : a * b > 0) = nat_valuation_aux' p hp a ha + nat_valuation_aux' p hp b hb
Tactic:
apply general (a + b) a b ha hb (le_refl _)
Proof state after:
no goals
Theorem: Int.nat_val_aux'_mul_eq_add
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
n : ℕ
⊢ ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
Tactic:
induction n with
| zero =>
  intro c d hc hd h_sum
  rw [Nat.eq_zero_of_add_eq_zero_right (Nat.eq_zero_of_le_zero h_sum)] at hc
  exact (lt_irrefl 0 hc).elim
| succ n ih =>
  intro c d hc hd h_sum
  cases c with
  | zero => cases hc
  | succ c => cases d with
    | zero => cases hd
    | succ d =>
      match Nat.le.dest (Nat.succ_le_of_lt prime.one_lt) with
      | ⟨q, hq⟩ =>
        rw [Nat.add_comm] at hq
        norm_num at hq have mul_s_s : c.succ * d.succ = (c * d + c + d).succ
        . simp [Nat.succ_mul, Nat.mul_succ, Nat.add_succ]
        simp only [←hq, mul_s_s, nat_valuation_add_two, nat_valuation_aux]
        simp only [hq, show c * d + c + d + 1 = (c + 1) * (d + 1) by ring]
        cases Nat.eq_zero_or_pos ((c + 1) * (d + 1) % p) with
        | inl h =>
          have hh : (c + 1) % p = 0 ∨ (d + 1) % p = 0 := sorry
          cases hh with
          | inl h' =>
            subst hq
            rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
            have sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n := by
              apply Nat.le_of_lt_succ
              apply lt_of_lt_of_le _ h_sum
              apply Nat.add_lt_add_right
              apply Nat.div_lt_self _ prime.one_lt
              rw [Nat.add_comm]
              apply Nat.lt_add_right 0 1 c (Nat.lt_succ_self 0)
            rw [add_assoc _ 1 _, add_comm 1, ← add_assoc]
            rw [← ih ((c + 1) / (q + 2)) (d + 1) sorry sorry sum_le_n]
            have hey := nat_mul_div_assoc' (b := d+1) h'
            simp only [hey.symm, mul_s_s.symm]
            apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
          | inr h' =>
            subst hq
            rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
            have sum_le_n : (c + 1) + (d + 1) / (q + 2) ≤ n := by
              apply Nat.le_of_lt_succ
              apply lt_of_lt_of_le _ h_sum
              apply Nat.add_lt_add_left
              apply Nat.div_lt_self _ prime.one_lt
              rw [Nat.add_comm]
              apply Nat.lt_add_right 0 1 d (Nat.lt_succ_self 0)
            rw [← add_assoc]
            rw [←ih (c + 1) ((d + 1) / (q + 2)) _ _ sum_le_n]
            have hey := nat_mul_div_assoc (a := c+1) h'
            simp only [hey.symm, mul_s_s.symm]
            apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
        | inr h =>
          have hc := ndiv_mul_left _ _ _ (ne_of_gt h)
          have hd := ndiv_mul_right _ _ _ (ne_of_gt h)
          simp [nat_valuation_aux'_of_not_dvd _ _ _ _ hc, nat_valuation_aux'_of_not_dvd _ _ _ _ hd]
          simp [←mul_s_s, nat_valuation_aux'_of_not_dvd _ _ _ _ (ne_of_gt h)]
Proof state after:
no goals
Theorem: Int.nat_val_aux'_mul_eq_add
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
⊢ ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ Nat.zero →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
Tactic:
intro c d hc hd h_sum
Proof state after:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
c d : ℕ
hc : c > 0
hd : d > 0
h_sum : c + d ≤ Nat.zero
⊢ nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
Theorem: Int.nat_val_aux'_mul_eq_add
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
c d : ℕ
hc : c > 0
hd : d > 0
h_sum : c + d ≤ Nat.zero
⊢ nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
Tactic:
rw [Nat.eq_zero_of_add_eq_zero_right (Nat.eq_zero_of_le_zero h_sum)] at hc
Proof state after:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
c d : ℕ
hc✝ : c > 0
hc : 0 > 0
hd : d > 0
h_sum : c + d ≤ Nat.zero
⊢ nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc✝ + nat_valuation_aux' p hp d hd
Theorem: Int.nat_val_aux'_mul_eq_add
Proof state before:
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
c d : ℕ
hc✝ : c > 0
hc : 0 > 0
hd : d > 0
h_sum : c + d ≤ Nat.zero
⊢ nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc✝ + nat_valuation_aux' p hp d hd
Tactic:
exact (lt_irrefl 0 hc).elim
Proof state after:
no goals
Theorem: Int.nat_val_aux'_mul_eq_add
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
n : ℕ
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
⊢ ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ Nat.succ n →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
Tactic:
intro c d hc hd h_sum
Proof state after:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
n : ℕ
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
c d : ℕ
hc : c > 0
hd : d > 0
h_sum : c + d ≤ Nat.succ n
⊢ nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
Theorem: Int.nat_val_aux'_mul_eq_add
Proof state before:
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
n : ℕ
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
c d : ℕ
hc : c > 0
hd : d > 0
h_sum : c + d ≤ Nat.succ n
⊢ nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
Tactic:
cases c with
| zero => cases hc
| succ c => cases d with
  | zero => cases hd
  | succ d =>
    match Nat.le.dest (Nat.succ_le_of_lt prime.one_lt) with
    | ⟨q, hq⟩ =>
      rw [Nat.add_comm] at hq
      norm_num at hq have mul_s_s : c.succ * d.succ = (c * d + c + d).succ
      . simp [Nat.succ_mul, Nat.mul_succ, Nat.add_succ]
      simp only [←hq, mul_s_s, nat_valuation_add_two, nat_valuation_aux]
      simp only [hq, show c * d + c + d + 1 = (c + 1) * (d + 1) by ring]
      cases Nat.eq_zero_or_pos ((c + 1) * (d + 1) % p) with
      | inl h =>
        have hh : (c + 1) % p = 0 ∨ (d + 1) % p = 0 := sorry
        cases hh with
        | inl h' =>
          subst hq
          rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
          have sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n := by
            apply Nat.le_of_lt_succ
            apply lt_of_lt_of_le _ h_sum
            apply Nat.add_lt_add_right
            apply Nat.div_lt_self _ prime.one_lt
            rw [Nat.add_comm]
            apply Nat.lt_add_right 0 1 c (Nat.lt_succ_self 0)
          rw [add_assoc _ 1 _, add_comm 1, ← add_assoc]
          rw [← ih ((c + 1) / (q + 2)) (d + 1) sorry sorry sum_le_n]
          have hey := nat_mul_div_assoc' (b := d+1) h'
          simp only [hey.symm, mul_s_s.symm]
          apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
        | inr h' =>
          subst hq
          rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
          have sum_le_n : (c + 1) + (d + 1) / (q + 2) ≤ n := by
            apply Nat.le_of_lt_succ
            apply lt_of_lt_of_le _ h_sum
            apply Nat.add_lt_add_left
            apply Nat.div_lt_self _ prime.one_lt
            rw [Nat.add_comm]
            apply Nat.lt_add_right 0 1 d (Nat.lt_succ_self 0)
          rw [← add_assoc]
          rw [←ih (c + 1) ((d + 1) / (q + 2)) _ _ sum_le_n]
          have hey := nat_mul_div_assoc (a := c+1) h'
          simp only [hey.symm, mul_s_s.symm]
          apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
      | inr h =>
        have hc := ndiv_mul_left _ _ _ (ne_of_gt h)
        have hd := ndiv_mul_right _ _ _ (ne_of_gt h)
        simp [nat_valuation_aux'_of_not_dvd _ _ _ _ hc, nat_valuation_aux'_of_not_dvd _ _ _ _ hd]
        simp [←mul_s_s, nat_valuation_aux'_of_not_dvd _ _ _ _ (ne_of_gt h)]
Proof state after:
no goals
Theorem: Int.nat_val_aux'_mul_eq_add
Proof state before:
case succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
n : ℕ
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
d : ℕ
hd : d > 0
hc : Nat.zero > 0
h_sum : Nat.zero + d ≤ Nat.succ n
⊢ nat_valuation_aux' p hp (Nat.zero * d) (_ : Nat.zero * d > 0) =
    nat_valuation_aux' p hp Nat.zero hc + nat_valuation_aux' p hp d hd
Tactic:
cases hc
Proof state after:
no goals
Theorem: Int.nat_val_aux'_mul_eq_add
Proof state before:
case succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
n : ℕ
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
d : ℕ
hd : d > 0
c : ℕ
hc : Nat.succ c > 0
h_sum : Nat.succ c + d ≤ Nat.succ n
⊢ nat_valuation_aux' p hp (Nat.succ c * d) (_ : Nat.succ c * d > 0) =
    nat_valuation_aux' p hp (Nat.succ c) hc + nat_valuation_aux' p hp d hd
Tactic:
cases d with
| zero => cases hd
| succ d =>
match Nat.le.dest (Nat.succ_le_of_lt prime.one_lt) with
| ⟨q, hq⟩ =>
rw [Nat.add_comm] at hq
norm_num at hq have mul_s_s : c.succ * d.succ = (c * d + c + d).succ
. simp [Nat.succ_mul, Nat.mul_succ, Nat.add_succ]
simp only [←hq, mul_s_s, nat_valuation_add_two, nat_valuation_aux]
simp only [hq, show c * d + c + d + 1 = (c + 1) * (d + 1) by ring]
cases Nat.eq_zero_or_pos ((c + 1) * (d + 1) % p) with
| inl h =>
have hh : (c + 1) % p = 0 ∨ (d + 1) % p = 0 := sorry
cases hh with
| inl h' =>
subst hq
rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
have sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n := by
apply Nat.le_of_lt_succ
apply lt_of_lt_of_le _ h_sum
apply Nat.add_lt_add_right
apply Nat.div_lt_self _ prime.one_lt
rw [Nat.add_comm]
apply Nat.lt_add_right 0 1 c (Nat.lt_succ_self 0)
rw [add_assoc _ 1 _, add_comm 1, ← add_assoc]
rw [← ih ((c + 1) / (q + 2)) (d + 1) sorry sorry sum_le_n]
have hey := nat_mul_div_assoc' (b := d+1) h'
simp only [hey.symm, mul_s_s.symm]
apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
| inr h' =>
subst hq
rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
have sum_le_n : (c + 1) + (d + 1) / (q + 2) ≤ n := by
apply Nat.le_of_lt_succ
apply lt_of_lt_of_le _ h_sum
apply Nat.add_lt_add_left
apply Nat.div_lt_self _ prime.one_lt
rw [Nat.add_comm]
apply Nat.lt_add_right 0 1 d (Nat.lt_succ_self 0)
rw [← add_assoc]
rw [←ih (c + 1) ((d + 1) / (q + 2)) _ _ sum_le_n]
have hey := nat_mul_div_assoc (a := c+1) h'
simp only [hey.symm, mul_s_s.symm]
apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
| inr h =>
have hc := ndiv_mul_left _ _ _ (ne_of_gt h)
have hd := ndiv_mul_right _ _ _ (ne_of_gt h)
simp [nat_valuation_aux'_of_not_dvd _ _ _ _ hc, nat_valuation_aux'_of_not_dvd _ _ _ _ hd]
simp [←mul_s_s, nat_valuation_aux'_of_not_dvd _ _ _ _ (ne_of_gt h)]
Proof state after:
no goals
Theorem: Int.nat_val_aux'_mul_eq_add
Proof state before:
case succ.succ.zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
n : ℕ
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
c : ℕ
hc : Nat.succ c > 0
hd : Nat.zero > 0
h_sum : Nat.succ c + Nat.zero ≤ Nat.succ n
⊢ nat_valuation_aux' p hp (Nat.succ c * Nat.zero) (_ : Nat.succ c * Nat.zero > 0) =
    nat_valuation_aux' p hp (Nat.succ c) hc + nat_valuation_aux' p hp Nat.zero hd
Tactic:
cases hd
Proof state after:
no goals
Theorem: Int.nat_val_aux'_mul_eq_add
Proof state before:
case succ.succ.succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
n : ℕ
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
⊢ nat_valuation_aux' p hp (Nat.succ c * Nat.succ d) (_ : Nat.succ c * Nat.succ d > 0) =
    nat_valuation_aux' p hp (Nat.succ c) hc + nat_valuation_aux' p hp (Nat.succ d) hd
Tactic:
match Nat.le.dest (Nat.succ_le_of_lt prime.one_lt) with
| ⟨q, hq⟩ =>
  rw [Nat.add_comm] at hq
  norm_num at hq have mul_s_s : c.succ * d.succ = (c * d + c + d).succ
  . simp [Nat.succ_mul, Nat.mul_succ, Nat.add_succ]
  simp only [←hq, mul_s_s, nat_valuation_add_two, nat_valuation_aux]
  simp only [hq, show c * d + c + d + 1 = (c + 1) * (d + 1) by ring]
  cases Nat.eq_zero_or_pos ((c + 1) * (d + 1) % p) with
  | inl h =>
    have hh : (c + 1) % p = 0 ∨ (d + 1) % p = 0 := sorry
    cases hh with
    | inl h' =>
      subst hq
      rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
      have sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n := by
        apply Nat.le_of_lt_succ
        apply lt_of_lt_of_le _ h_sum
        apply Nat.add_lt_add_right
        apply Nat.div_lt_self _ prime.one_lt
        rw [Nat.add_comm]
        apply Nat.lt_add_right 0 1 c (Nat.lt_succ_self 0)
      rw [add_assoc _ 1 _, add_comm 1, ← add_assoc]
      rw [← ih ((c + 1) / (q + 2)) (d + 1) sorry sorry sum_le_n]
      have hey := nat_mul_div_assoc' (b := d+1) h'
      simp only [hey.symm, mul_s_s.symm]
      apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
    | inr h' =>
      subst hq
      rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
      have sum_le_n : (c + 1) + (d + 1) / (q + 2) ≤ n := by
        apply Nat.le_of_lt_succ
        apply lt_of_lt_of_le _ h_sum
        apply Nat.add_lt_add_left
        apply Nat.div_lt_self _ prime.one_lt
        rw [Nat.add_comm]
        apply Nat.lt_add_right 0 1 d (Nat.lt_succ_self 0)
      rw [← add_assoc]
      rw [←ih (c + 1) ((d + 1) / (q + 2)) _ _ sum_le_n]
      have hey := nat_mul_div_assoc (a := c+1) h'
      simp only [hey.symm, mul_s_s.symm]
      apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
  | inr h =>
    have hc := ndiv_mul_left _ _ _ (ne_of_gt h)
    have hd := ndiv_mul_right _ _ _ (ne_of_gt h)
    simp [nat_valuation_aux'_of_not_dvd _ _ _ _ hc, nat_valuation_aux'_of_not_dvd _ _ _ _ hd]
    simp [←mul_s_s, nat_valuation_aux'_of_not_dvd _ _ _ _ (ne_of_gt h)]
Proof state after:
no goals