Theorem: FltRegular.CaseI.aux_cong1k₁ (FltRegular/CaseI/AuxLemmas.lean)

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

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 0 [ZMOD ↑p]
⊢ ↑k = ↑⟨0, ⋯⟩
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 ≡ 0 [ZMOD ↑p]
⊢ (↑↑k).val = ↑⟨0, ⋯⟩

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

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

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

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

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

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