-- Mathlib/NumberTheory/Harmonic/Int.lean
theorem padicValRat_two_harmonic (n : ℕ) : padicValRat 2 (harmonic n) = -Nat.log 2 n

Proof state:
case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹
⊢ padicValRat 2 (harmonic n + (↑(n + 1))⁻¹) = -↑(Nat.log 2 (n + 1))

Tactic:
rw [padicValRat.add_eq_min (harmonic_succ n ▸ (harmonic_pos n.succ_ne_zero).ne')
    (harmonic_pos hn).ne' (inv_ne_zero (Nat.cast_ne_zero.mpr n.succ_ne_zero)) key, ih,
    padicValRat.inv, padicValRat.of_nat, min_neg_neg, neg_inj, ← Nat.cast_max, Nat.cast_inj]

Result:
case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹
⊢ Nat.log 2 n ⊔ padicValNat 2 n.succ = Nat.log 2 (n + 1)

Proof state:
case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
⊢ padicValRat 2 (harmonic n + (↑(n + 1))⁻¹) = -↑(Nat.log 2 (n + 1))

Tactic:
have key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹ := by
  rw [ih, padicValRat.inv, padicValRat.of_nat, Ne, neg_inj, Nat.cast_inj]
  exact Nat.log_ne_padicValNat_succ hn

Result:
case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹
⊢ padicValRat 2 (harmonic n + (↑(n + 1))⁻¹) = -↑(Nat.log 2 (n + 1))

Proof state:
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
⊢ ¬Nat.log 2 n = padicValNat 2 (n + 1)

Tactic:
exact Nat.log_ne_padicValNat_succ hn

Result:
no goals

Proof state:
case succ
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
⊢ padicValRat 2 (harmonic (n + 1)) = -↑(Nat.log 2 (n + 1))

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case succ.inl
ih : padicValRat 2 (harmonic 0) = -↑(Nat.log 2 0)
⊢ padicValRat 2 (harmonic (0 + 1)) = -↑(Nat.log 2 (0 + 1))

case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
⊢ padicValRat 2 (harmonic (n + 1)) = -↑(Nat.log 2 (n + 1))

Proof state:
case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹
⊢ Nat.log 2 n ⊔ padicValNat 2 n.succ = Nat.log 2 (n + 1)

Tactic:
exact Nat.max_log_padicValNat_succ_eq_log_succ n

Result:
no goals

Proof state:
case zero

⊢ padicValRat 2 (harmonic 0) = -↑(Nat.log 2 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
⊢ padicValRat 2 (harmonic (n + 1)) = -↑(Nat.log 2 (n + 1))

Tactic:
rw [harmonic_succ]

Result:
case succ.inr
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
⊢ padicValRat 2 (harmonic n + (↑(n + 1))⁻¹) = -↑(Nat.log 2 (n + 1))

Proof state:
case succ.inl
ih : padicValRat 2 (harmonic 0) = -↑(Nat.log 2 0)
⊢ padicValRat 2 (harmonic (0 + 1)) = -↑(Nat.log 2 (0 + 1))

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
⊢ padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹

Tactic:
rw [ih, padicValRat.inv, padicValRat.of_nat, Ne, neg_inj, Nat.cast_inj]

Result:
n : ℕ
ih : padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
hn : n ≠ 0
⊢ ¬Nat.log 2 n = padicValNat 2 (n + 1)