Theorem: FltRegular.CaseI.aux_cong0k₂ (FltRegular/CaseI/AuxLemmas.lean)

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ k = ⟨1, ⋯⟩
Tactic:
refine' Fin.ext _
State after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ ↑k = ↑⟨1, ⋯⟩

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ ↑k = ↑⟨1, ⋯⟩
Tactic:
rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
State after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ (↑↑k).val = ↑⟨1, ⋯⟩

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ (↑↑k).val = ↑⟨1, ⋯⟩
Tactic:
suffices ((k : ℤ) : ZMod p).val = 1 by simpa
State after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ (↑↑↑k).val = 1

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ (↑↑↑k).val = 1
Tactic:
rw [← ZMod.intCast_eq_intCast_iff] at hcong
State after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
⊢ (↑↑↑k).val = 1

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
⊢ (↑↑↑k).val = 1
Tactic:
rw [hcong, Int.cast_one]
State after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
⊢ ZMod.val 1 = 1

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
⊢ ZMod.val 1 = 1
Tactic:
haveI : Fact p.Prime := ⟨hpri⟩
State after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
this : Fact p.Prime
⊢ ZMod.val 1 = 1

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑1
this : Fact p.Prime
⊢ ZMod.val 1 = 1
Tactic:
simp [ZMod.val_one]
State after:
no goals

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
this : (↑↑↑k).val = 1
⊢ (↑↑k).val = ↑⟨1, ⋯⟩
Tactic:
simpa
State after:
no goals