internlm/Lean-Github huggingface dataset:
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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]
Proof 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
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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'
Proof 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
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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]
Proof 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
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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
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
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
Proof 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
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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
Proof 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
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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
Proof 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
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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
Proof 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
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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]
Proof 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
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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)
Proof state after:
no goals
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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)
Proof 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
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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)
Proof 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✝
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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]
Proof 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
Theorem: Int.nat_val_aux'_mul_eq_add
Proof 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)]
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 : ℕ
⊢ nat_valuation_aux p hp (a * b) = nat_valuation_aux p hp a + nat_valuation_aux p hp b
Tactic:
cases a with
  | zero => simp [nat_valuation_aux]
  | succ a => cases b with
    | zero => simp [nat_valuation_aux]
    | succ b =>
      exact nat_val_aux'_mul_eq_add p prime prime.one_lt a.succ b.succ _ _
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)
b : ℕ
⊢ nat_valuation_aux p hp (Nat.zero * b) = nat_valuation_aux p hp Nat.zero + nat_valuation_aux p hp b
Tactic:
simp [nat_valuation_aux]
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)
b a : ℕ
⊢ nat_valuation_aux p hp (Nat.succ a * b) = nat_valuation_aux p hp (Nat.succ a) + nat_valuation_aux p hp b
Tactic:
cases b with
| zero => simp [nat_valuation_aux]
| succ b =>
exact nat_val_aux'_mul_eq_add p prime prime.one_lt a.succ b.succ _ _
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 : ℕ
⊢ nat_valuation_aux p hp (Nat.succ a * Nat.zero) = nat_valuation_aux p hp (Nat.succ a) + nat_valuation_aux p hp Nat.zero
Tactic:
simp [nat_valuation_aux]
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 : ℕ
⊢ nat_valuation_aux p hp (Nat.succ a * Nat.succ b) =
    nat_valuation_aux p hp (Nat.succ a) + nat_valuation_aux p hp (Nat.succ b)
Tactic:
exact nat_val_aux'_mul_eq_add p prime prime.one_lt a.succ b.succ _ _
Proof state after:
no goals
Theorem: Int.nat_val_mul_eq_add
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
a b : ℕ
⊢ nat_valuation p (a * b) = nat_valuation p a + nat_valuation p b
Tactic:
convert nat_val_aux_mul_eq_add p prime prime.one_lt a b <;>
ext <;>
rw [(nat_valuation_of_one_lt p _ prime.one_lt)]
Proof state after:
no goals
Theorem: Int.int_val_mul_eq_add
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
a b : ℤ
⊢ int_val p (a * b) = int_val p a + int_val p b
Tactic:
simp [int_val, natAbs_mul]
Proof state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
a b : ℤ
⊢ nat_valuation p (natAbs a * natAbs b) = nat_valuation p (natAbs a) + nat_valuation p (natAbs b)
Theorem: Int.int_val_mul_eq_add
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
a b : ℤ
⊢ nat_valuation p (natAbs a * natAbs b) = nat_valuation p (natAbs a) + nat_valuation p (natAbs b)
Tactic:
exact nat_val_mul_eq_add p prime (natAbs a) (natAbs b)
Proof state after:
no goals
Theorem: Int.nat_val_add_eq_min
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
h : nat_valuation p a < nat_valuation p b
⊢ nat_valuation p (a + b) = nat_valuation p a
Tactic:
sorry
Proof state after:
no goals
Theorem: Int.nat_val_add_ge_min
Proof state before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p a b : ℕ
⊢ min (nat_valuation p a) (nat_valuation p b) ≤ nat_valuation p (a + b)
Tactic:
cases lt_trichotomy (nat_valuation p a) (nat_valuation p b) with | inl h =>
  simp only [min, if_pos (le_of_lt h)]
  apply le_of_eq
  rw [nat_val_add_eq_min p a b h]
  rw [inf_eq_left]
  exact h.le
| inr h => cases h with
  | inl h =>
    simp only [min, if_pos (le_of_eq h)]
    sorry
  | inr h =>
    simp only [add_comm a b, min, if_neg (not_le_of_lt h)]
    apply le_of_eq
    rw [nat_val_add_eq_min p b a h]
    simp
    exact h.le
Proof state after:
no goals