Theorem: Int.Int.ModEq.pow_card_eq_self (ECTate/Algebra/ValuedRing.lean)

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
⊢ n ^ p ≡ n [ZMOD ↑p]
Tactic:
haveI : Fact p.Prime := ⟨hp⟩
State after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this : Fact (Nat.Prime p)
⊢ n ^ p ≡ n [ZMOD ↑p]

State before:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this : Fact (Nat.Prime p)
⊢ n ^ p ≡ n [ZMOD ↑p]
Tactic:
by_cases this : (n : ZMod p) = 0
State after:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ↑n = 0
⊢ n ^ p ≡ n [ZMOD ↑p]

case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ p ≡ n [ZMOD ↑p]

State before:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ p ≡ n [ZMOD ↑p]
Tactic:
conv_lhs =>
  rw [← show p - 1 + 1 = p from Nat.sub_add_cancel hp.one_lt.le]
State after:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1 + 1) ≡ n [ZMOD ↑p]

State before:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1 + 1) ≡ n [ZMOD ↑p]
Tactic:
rw [pow_add, pow_one]
State after:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1) * n ≡ n [ZMOD ↑p]

State before:
case neg
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1) * n ≡ n [ZMOD ↑p]
Tactic:
simp [← ZMod.int_cast_eq_int_cast_iff, ZMod.pow_card_sub_one_eq_one this]
State after:
no goals

State before:
case pos
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this✝ : Fact (Nat.Prime p)
this : ↑n = 0
⊢ n ^ p ≡ n [ZMOD ↑p]
Tactic:
simp [← ZMod.int_cast_eq_int_cast_iff, this]
State after:
no goals