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

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

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

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

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

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

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑(-1)
⊢ (-1).val = p - 1
Tactic:
haveI : NeZero p := ⟨hpri.ne_zero⟩
State after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑(-1)
this : NeZero p
⊢ (-1).val = p - 1

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑(-1)
this : NeZero p
⊢ (-1).val = p - 1
Tactic:
haveI : Fact p.Prime := ⟨hpri⟩
State after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑(-1)
this✝ : NeZero p
this : Fact p.Prime
⊢ (-1).val = p - 1

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑(-1)
this✝ : NeZero p
this : Fact p.Prime
⊢ (-1).val = p - 1
Tactic:
haveI : Fact (1 < p) := ⟨hpri.one_lt⟩
State after:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑(-1)
this✝¹ : NeZero p
this✝ : Fact p.Prime
this : Fact (1 < p)
⊢ (-1).val = p - 1

State before:
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑↑k = ↑(-1)
this✝¹ : NeZero p
this✝ : Fact p.Prime
this : Fact (1 < p)
⊢ (-1).val = p - 1
Tactic:
simp [ZMod.neg_val, ZMod.val_one]
State after:
no goals

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