α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
k : ℕ
⊢ Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
⊢ ∀ {k : ℕ}, Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
intro k
case zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
⊢ Part.get (multiplicity p (a ^ zero)) (_ : Finite p (a ^ zero)) = zero * Part.get (multiplicity p a) ha

case succ
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
k : ℕ
hk : Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
⊢ Part.get (multiplicity p (a ^ succ k)) (_ : Finite p (a ^ succ k)) = succ k * Part.get (multiplicity p a) ha
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
k : ℕ
⊢ Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
induction' k with k hk
no goals
case zero
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
⊢ Part.get (multiplicity p (a ^ zero)) (_ : Finite p (a ^ zero)) = zero * Part.get (multiplicity p a) ha
simp [one_right hp.not_unit]
case succ
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
k : ℕ
hk : Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
this : multiplicity p (a ^ (k + 1)) = multiplicity p (a * a ^ k)
⊢ Part.get (multiplicity p (a ^ succ k)) (_ : Finite p (a ^ succ k)) = succ k * Part.get (multiplicity p a) ha
case succ
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
k : ℕ
hk : Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
⊢ Part.get (multiplicity p (a ^ succ k)) (_ : Finite p (a ^ succ k)) = succ k * Part.get (multiplicity p a) ha
have : multiplicity p (a ^ (k + 1)) = multiplicity p (a * a ^ k) := by rw [_root_.pow_succ]
no goals
case succ
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
k : ℕ
hk : Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
this : multiplicity p (a ^ (k + 1)) = multiplicity p (a * a ^ k)
⊢ Part.get (multiplicity p (a ^ succ k)) (_ : Finite p (a ^ succ k)) = succ k * Part.get (multiplicity p a) ha
rw [succ_eq_add_one, get_eq_get_of_eq _ _ this,
  multiplicity.mul' hp, hk, add_mul, one_mul, add_comm]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
ha : Finite p a
k : ℕ
hk : Part.get (multiplicity p (a ^ k)) (_ : Finite p (a ^ k)) = k * Part.get (multiplicity p a) ha
⊢ multiplicity p (a ^ (k + 1)) = multiplicity p (a * a ^ k)
rw [_root_.pow_succ]