case zero
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ Nat.zero ≡ b ^ Nat.zero [ZMOD n]

case succ
m n a b c d✝ : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ Nat.succ d ≡ b ^ Nat.succ d [ZMOD n]
m✝ n a b c d : ℤ
m : ℕ
h : a ≡ b [ZMOD n]
⊢ a ^ m ≡ b ^ m [ZMOD n]
induction' m with d hd
case succ
m n a b c d✝ : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a * a ^ d ≡ b * b ^ d [ZMOD n]
case succ
m n a b c d✝ : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a ^ Nat.succ d ≡ b ^ Nat.succ d [ZMOD n]
rw [pow_succ, pow_succ]
no goals
case succ
m n a b c d✝ : ℤ
h : a ≡ b [ZMOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [ZMOD n]
⊢ a * a ^ d ≡ b * b ^ d [ZMOD n]
exact h.mul hd
no goals
case zero
m n a b c d : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ Nat.zero ≡ b ^ Nat.zero [ZMOD n]
rfl