Theorem: Int.nat_val_aux'_mul_eq_add (ECTate/Algebra/ValuedRing.lean)

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)]
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

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 _)
State after:
no goals

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)]
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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)]
State after:
no goals

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
State after:
no goals

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)]
State after:
no goals

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
State after:
no goals

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)]
State after:
no goals

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 : ℕ
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
q : ℕ
hq : Nat.succ 1 + q = p
⊢ 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:
rw [Nat.add_comm] at hq
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
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
q : ℕ
hq : q + Nat.succ 1 = p
⊢ 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

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 : ℕ
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
q : ℕ
hq : q + Nat.succ 1 = p
⊢ 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:
norm_num at hq
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
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
q : ℕ
hq : q + 2 = p
⊢ 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

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 : ℕ
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
q : ℕ
hq : q + 2 = p
⊢ 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:
have mul_s_s : c.succ * d.succ = (c * d + c + d).succ
State after:
case mul_s_s
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
q : ℕ
hq : q + 2 = p
⊢ Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)

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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
⊢ 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

State before:
case mul_s_s
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
q : ℕ
hq : q + 2 = p
⊢ Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)

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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
⊢ 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:
. simp [Nat.succ_mul, Nat.mul_succ, Nat.add_succ]
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
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
⊢ 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

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 : ℕ
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
⊢ 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:
simp only [←hq, mul_s_s, nat_valuation_add_two, nat_valuation_aux]
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
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
      nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd

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 : ℕ
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
      nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd
Tactic:
simp only [hq, show c * d + c + d + 1 = (c + 1) * (d + 1) by ring]
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
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd

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 : ℕ
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd
Tactic:
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)]
State after:
no goals

State before:
case mul_s_s
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
q : ℕ
hq : q + 2 = p
⊢ Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
Tactic:
simp [Nat.succ_mul, Nat.mul_succ, Nat.add_succ]
State after:
no goals

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 : ℕ
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
⊢ c * d + c + d + 1 = (c + 1) * (d + 1)
Tactic:
ring
State after:
no goals

State before:
case inl
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p = 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd
Tactic:
have hh : (c + 1) % p = 0 ∨ (d + 1) % p = 0 := sorry
State after:
case inl
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p = 0
hh : (c + 1) % p = 0 ∨ (d + 1) % p = 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd

State before:
case inl
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p = 0
hh : (c + 1) % p = 0 ∨ (d + 1) % p = 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd
Tactic:
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
State after:
no goals

State before:
case inl.inl
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p = 0
h' : (c + 1) % p = 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd
Tactic:
subst hq
State after:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
      nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd

State before:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
      nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd
Tactic:
rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
State after:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((c + 1) / (q + 2)) (_ : 0 < (c + 1) / (q + 2)) + 1 +
      nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd

State before:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((c + 1) / (q + 2)) (_ : 0 < (c + 1) / (q + 2)) + 1 +
      nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd
Tactic:
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)
State after:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((c + 1) / (q + 2)) (_ : 0 < (c + 1) / (q + 2)) + 1 +
      nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd

State before:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((c + 1) / (q + 2)) (_ : 0 < (c + 1) / (q + 2)) + 1 +
      nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd
Tactic:
rw [add_assoc _ 1 _, add_comm 1, ← add_assoc]
State after:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((c + 1) / (q + 2)) (_ : 0 < (c + 1) / (q + 2)) +
        nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd +
      1

State before:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((c + 1) / (q + 2)) (_ : 0 < (c + 1) / (q + 2)) +
        nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd +
      1
Tactic:
rw [← ih ((c + 1) / (q + 2)) (d + 1) sorry sorry sum_le_n]
State after:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) hp ((c + 1) / (q + 2) * (d + 1)) (_ : (c + 1) / (q + 2) * (d + 1) > 0) + 1

State before:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) hp ((c + 1) / (q + 2) * (d + 1)) (_ : (c + 1) / (q + 2) * (d + 1) > 0) + 1
Tactic:
have hey := nat_mul_div_assoc' (b := d+1) h'
State after:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
hey : (c + 1) * (d + 1) / (q + 2) = (c + 1) / (q + 2) * (d + 1)
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) hp ((c + 1) / (q + 2) * (d + 1)) (_ : (c + 1) / (q + 2) * (d + 1) > 0) + 1

State before:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
hey : (c + 1) * (d + 1) / (q + 2) = (c + 1) / (q + 2) * (d + 1)
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) hp ((c + 1) / (q + 2) * (d + 1)) (_ : (c + 1) / (q + 2) * (d + 1) > 0) + 1
Tactic:
simp only [hey.symm, mul_s_s.symm]
State after:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
hey : (c + 1) * (d + 1) / (q + 2) = (c + 1) / (q + 2) * (d + 1)
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c * Nat.succ d) (_ : 0 < Nat.succ c * Nat.succ d) =
    nat_valuation_aux' (q + 2) hp ((c + 1) * (d + 1) / (q + 2)) (_ : 0 < (c + 1) * (d + 1) / (q + 2)) + 1

State before:
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
hey : (c + 1) * (d + 1) / (q + 2) = (c + 1) / (q + 2) * (d + 1)
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c * Nat.succ d) (_ : 0 < Nat.succ c * Nat.succ d) =
    nat_valuation_aux' (q + 2) hp ((c + 1) * (d + 1) / (q + 2)) (_ : 0 < (c + 1) * (d + 1) / (q + 2)) + 1
Tactic:
apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ (c + 1) / (q + 2) + (d + 1) ≤ n
Tactic:
apply Nat.le_of_lt_succ
State after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ (c + 1) / (q + 2) + (d + 1) < Nat.succ n

State before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ (c + 1) / (q + 2) + (d + 1) < Nat.succ n
Tactic:
apply lt_of_lt_of_le _ h_sum
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ (c + 1) / (q + 2) + (d + 1) < Nat.succ c + Nat.succ d

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ (c + 1) / (q + 2) + (d + 1) < Nat.succ c + Nat.succ d
Tactic:
apply Nat.add_lt_add_right
State after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ (c + 1) / (q + 2) < Nat.succ c

State before:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ (c + 1) / (q + 2) < Nat.succ c
Tactic:
apply Nat.div_lt_self _ prime.one_lt
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ 0 < c + 1

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ 0 < c + 1
Tactic:
rw [Nat.add_comm]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ 0 < 1 + c

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
⊢ 0 < 1 + c
Tactic:
apply Nat.lt_add_right 0 1 c (Nat.lt_succ_self 0)
State after:
no goals

State before:
case inl.inr
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p = 0
h' : (d + 1) % p = 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd
Tactic:
subst hq
State after:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
      nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd

State before:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
      nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd
Tactic:
rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
State after:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
      (nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((d + 1) / (q + 2)) (_ : 0 < (d + 1) / (q + 2)) + 1)

State before:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
      (nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((d + 1) / (q + 2)) (_ : 0 < (d + 1) / (q + 2)) + 1)
Tactic:
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)
State after:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
sum_le_n : c + 1 + (d + 1) / (q + 2) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
      (nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((d + 1) / (q + 2)) (_ : 0 < (d + 1) / (q + 2)) + 1)

State before:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
sum_le_n : c + 1 + (d + 1) / (q + 2) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
      (nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((d + 1) / (q + 2)) (_ : 0 < (d + 1) / (q + 2)) + 1)
Tactic:
rw [← add_assoc]
State after:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
sum_le_n : c + 1 + (d + 1) / (q + 2) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
        nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((d + 1) / (q + 2)) (_ : 0 < (d + 1) / (q + 2)) +
      1

State before:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
sum_le_n : c + 1 + (d + 1) / (q + 2) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c) hc +
        nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((d + 1) / (q + 2)) (_ : 0 < (d + 1) / (q + 2)) +
      1
Tactic:
rw [←ih (c + 1) ((d + 1) / (q + 2)) _ _ sum_le_n]
State after:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
sum_le_n : c + 1 + (d + 1) / (q + 2) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) hp ((c + 1) * ((d + 1) / (q + 2))) (_ : (c + 1) * ((d + 1) / (q + 2)) > 0) + 1

State before:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
sum_le_n : c + 1 + (d + 1) / (q + 2) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) hp ((c + 1) * ((d + 1) / (q + 2))) (_ : (c + 1) * ((d + 1) / (q + 2)) > 0) + 1
Tactic:
have hey := nat_mul_div_assoc (a := c+1) h'
State after:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
sum_le_n : c + 1 + (d + 1) / (q + 2) ≤ n
hey : (c + 1) * (d + 1) / (q + 2) = (c + 1) * ((d + 1) / (q + 2))
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) hp ((c + 1) * ((d + 1) / (q + 2))) (_ : (c + 1) * ((d + 1) / (q + 2)) > 0) + 1

State before:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
sum_le_n : c + 1 + (d + 1) / (q + 2) ≤ n
hey : (c + 1) * (d + 1) / (q + 2) = (c + 1) * ((d + 1) / (q + 2))
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) hp ((c + 1) * ((d + 1) / (q + 2))) (_ : (c + 1) * ((d + 1) / (q + 2)) > 0) + 1
Tactic:
simp only [hey.symm, mul_s_s.symm]
State after:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
sum_le_n : c + 1 + (d + 1) / (q + 2) ≤ n
hey : (c + 1) * (d + 1) / (q + 2) = (c + 1) * ((d + 1) / (q + 2))
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c * Nat.succ d) (_ : 0 < Nat.succ c * Nat.succ d) =
    nat_valuation_aux' (q + 2) hp ((c + 1) * (d + 1) / (q + 2)) (_ : 0 < (c + 1) * (d + 1) / (q + 2)) + 1

State before:
case inl.inr
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
sum_le_n : c + 1 + (d + 1) / (q + 2) ≤ n
hey : (c + 1) * (d + 1) / (q + 2) = (c + 1) * ((d + 1) / (q + 2))
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ c * Nat.succ d) (_ : 0 < Nat.succ c * Nat.succ d) =
    nat_valuation_aux' (q + 2) hp ((c + 1) * (d + 1) / (q + 2)) (_ : 0 < (c + 1) * (d + 1) / (q + 2)) + 1
Tactic:
apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
State after:
no goals

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ c + 1 + (d + 1) / (q + 2) ≤ n
Tactic:
apply Nat.le_of_lt_succ
State after:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ c + 1 + (d + 1) / (q + 2) < Nat.succ n

State before:
case a
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ c + 1 + (d + 1) / (q + 2) < Nat.succ n
Tactic:
apply lt_of_lt_of_le _ h_sum
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ c + 1 + (d + 1) / (q + 2) < Nat.succ c + Nat.succ d

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ c + 1 + (d + 1) / (q + 2) < Nat.succ c + Nat.succ d
Tactic:
apply Nat.add_lt_add_left
State after:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ (d + 1) / (q + 2) < Nat.succ d

State before:
case h
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ (d + 1) / (q + 2) < Nat.succ d
Tactic:
apply Nat.div_lt_self _ prime.one_lt
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ 0 < d + 1

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ 0 < d + 1
Tactic:
rw [Nat.add_comm]
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ 0 < 1 + d

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (d + 1) % (q + 2) = 0
⊢ 0 < 1 + d
Tactic:
apply Nat.lt_add_right 0 1 d (Nat.lt_succ_self 0)
State after:
no goals

State before:
case inr
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p > 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd
Tactic:
have hc := ndiv_mul_left _ _ _ (ne_of_gt h)
State after:
case inr
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p > 0
hc : (c + 1) % p ≠ 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc✝ + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd

State before:
case inr
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p > 0
hc : (c + 1) % p ≠ 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc✝ + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd
Tactic:
have hd := ndiv_mul_right _ _ _ (ne_of_gt h)
State after:
case inr
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p > 0
hc : (c + 1) % p ≠ 0
hd : (d + 1) % p ≠ 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc✝ + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd✝

State before:
case inr
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p > 0
hc : (c + 1) % p ≠ 0
hd : (d + 1) % p ≠ 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc✝ + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd✝
Tactic:
simp [nat_valuation_aux'_of_not_dvd _ _ _ _ hc, nat_valuation_aux'_of_not_dvd _ _ _ _ hd]
State after:
case inr
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p > 0
hc : (c + 1) % p ≠ 0
hd : (d + 1) % p ≠ 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) = 0

State before:
case inr
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
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p > 0
hc : (c + 1) % p ≠ 0
hd : (d + 1) % p ≠ 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) = 0
Tactic:
simp [←mul_s_s, nat_valuation_aux'_of_not_dvd _ _ _ _ (ne_of_gt h)]
State after:
no goals