-- Mathlib/NumberTheory/Multiplicity.lean
theorem pow_add_pow (hxy : p ∣ x + y) (hx : ¬p ∣ x) {n : ℕ} (hn : Odd n) :
    padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n

Proof state:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ 0 < x + (y + 1)

Tactic:
simp only [add_pos_iff, Nat.succ_pos', or_true]

Result:
no goals

Proof state:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ padicValNat p (x ^ n + (y + 1) ^ n) = padicValNat p (x + (y + 1)) + padicValNat p n

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), Nat.cast_add]

Result:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ ↑(padicValNat p (x ^ n + (y + 1) ^ n)) = ↑(padicValNat p (x + (y + 1))) + ↑(padicValNat p n)

Proof state:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ 0 < x ^ n + (y + 1) ^ n

Tactic:
exact Nat.lt_add_left _ (pow_pos y.succ_pos _)

Result:
no goals

Proof state:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n

Tactic:
rcases y with - | y

Result:
case zero
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
hxy : p ∣ x + 0
⊢ padicValNat p (x ^ n + 0 ^ n) = padicValNat p (x + 0) + padicValNat p n

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ padicValNat p (x ^ n + (y + 1) ^ n) = padicValNat p (x + (y + 1)) + padicValNat p n

Proof state:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ 0 < n

Tactic:
exact Odd.pos hn

Result:
no goals

Proof state:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + ↑(padicValNat p n)

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ 0 < x + (y + 1)

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ 0 < x ^ n + (y + 1) ^ n

Tactic:
rw [padicValNat_eq_emultiplicity]

Result:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ 0 < n

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ 0 < x + (y + 1)

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ 0 < x ^ n + (y + 1) ^ n

Proof state:
case zero
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
hxy : p ∣ x + 0
⊢ padicValNat p (x ^ n + 0 ^ n) = padicValNat p (x + 0) + padicValNat p n

Tactic:
contradiction

Result:
no goals

Proof state:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ ↑(padicValNat p (x ^ n + (y + 1) ^ n)) = ↑(padicValNat p (x + (y + 1))) + ↑(padicValNat p n)

Tactic:
iterate 3 rw [padicValNat_eq_emultiplicity]

Result:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ 0 < n

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ 0 < x + (y + 1)

case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ 0 < x ^ n + (y + 1) ^ n

Proof state:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ emultiplicity p (x ^ n + (y + 1) ^ n) = emultiplicity p (x + (y + 1)) + emultiplicity p n

Tactic:
exact Nat.emultiplicity_pow_add_pow hp.out hp1 hxy hx hn

Result:
no goals