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
⊢ 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:
have general (n : ℕ) : ∀ c d hc hd, c + d ≤ n → nat_valuation_aux' p hp (c * d) (Nat.mul_pos hc hd) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd := by
  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:
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