Theorem: FltRegular.CaseI.auxk₁k₂ (FltRegular/CaseI/AuxLemmas.lean)

State before:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
⊢ ↑k₁ ≠ ↑k₂
Tactic:
haveI := (⟨hpri⟩ : Fact p.Prime)
State after:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
this : Fact p.Prime
⊢ ↑k₁ ≠ ↑k₂

State before:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
this : Fact p.Prime
⊢ ↑k₁ ≠ ↑k₂
Tactic:
intro habs
State after:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
this : Fact p.Prime
habs : ↑k₁ = ↑k₂
⊢ False

State before:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
this : Fact p.Prime
habs : ↑k₁ = ↑k₂
⊢ False
Tactic:
rw [habs, ← ZMod.intCast_eq_intCast_iff, Int.cast_sub, ← sub_eq_zero] at hcong
State after:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
this : Fact p.Prime
hcong : ↑↑↑k₂ - (↑↑↑k₂ - ↑1) = 0
habs : ↑k₁ = ↑k₂
⊢ False

State before:
p : ℕ
hpri✝ : p.Prime
k₁ k₂ : Fin p
hpri : p.Prime
this : Fact p.Prime
hcong : ↑↑↑k₂ - (↑↑↑k₂ - ↑1) = 0
habs : ↑k₁ = ↑k₂
⊢ False
Tactic:
simp at hcong
State after:
no goals