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

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

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

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

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

State before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑↑↑k).val = 2
Tactic:
rw [hcong]
State after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑(1 + 1)).val = 2

State before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑(1 + 1)).val = 2
Tactic:
simp only [Int.cast_add, algebraMap.coe_one]
State after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑1 + ↑1).val = 2

State before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑1 + ↑1).val = 2
Tactic:
haveI : Fact p.Prime := ⟨hpri⟩
State after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this : Fact p.Prime
⊢ (↑1 + ↑1).val = 2

State before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this : Fact p.Prime
⊢ (↑1 + ↑1).val = 2
Tactic:
have := congr_arg Nat.succ (Nat.succ_pred_eq_of_pos hpri.pred_pos)
State after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p.pred.succ
⊢ (↑1 + ↑1).val = 2

State before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p.pred.succ
⊢ (↑1 + ↑1).val = 2
Tactic:
rw [succ_pred_prime hpri] at this
State after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p
⊢ (↑1 + ↑1).val = 2

State before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p
⊢ (↑1 + ↑1).val = 2
Tactic:
rw [ZMod.val_add, Int.cast_one, ZMod.val_one, ← Nat.mod_add_mod, ← this, one_mod, this,
  Nat.mod_eq_of_lt]
State after:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p
⊢ 1 + 1 < p

State before:
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p
⊢ 1 + 1 < p
Tactic:
linarith
State after:
no goals

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