Theorem: BrownCs22.Int.ModEq.pow (BrownCs22/Library/ModEq/Lemmas.lean)

State before:
n a b : ℤ
k : ℕ
h : a ≡ b [ZMOD n]
⊢ a ^ k ≡ b ^ k [ZMOD n]
Tactic:
induction k
State after:
case zero
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ Nat.zero ≡ b ^ Nat.zero [ZMOD n]

case succ
n a b : ℤ
h : a ≡ b [ZMOD n]
n✝ : ℕ
n_ih✝ : a ^ n✝ ≡ b ^ n✝ [ZMOD n]
⊢ a ^ Nat.succ n✝ ≡ b ^ Nat.succ n✝ [ZMOD n]

State before:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ Nat.zero ≡ b ^ Nat.zero [ZMOD n]
Tactic:
case zero => exact Int.ModEq.refl _
State after:
no goals

State before:
n a b : ℤ
h : a ≡ b [ZMOD n]
k : ℕ
hk : a ^ k ≡ b ^ k [ZMOD n]
⊢ a ^ Nat.succ k ≡ b ^ Nat.succ k [ZMOD n]
Tactic:
case succ k hk => exact Int.ModEq.mul hk h
State after:
no goals

State before:
n a b : ℤ
h : a ≡ b [ZMOD n]
⊢ a ^ Nat.zero ≡ b ^ Nat.zero [ZMOD n]
Tactic:
exact Int.ModEq.refl _
State after:
no goals

State before:
n a b : ℤ
h : a ≡ b [ZMOD n]
k : ℕ
hk : a ^ k ≡ b ^ k [ZMOD n]
⊢ a ^ Nat.succ k ≡ b ^ Nat.succ k [ZMOD n]
Tactic:
exact Int.ModEq.mul hk h
State after:
no goals