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

State before:
p : ℕ
hpri : p.Prime
a : ℤ
⊢ ∃ i, f1k₂ a ↑i = 0
Tactic:
refine' ⟨⟨1, hpri.one_lt⟩, _⟩
State after:
p : ℕ
hpri : p.Prime
a : ℤ
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0

State before:
p : ℕ
hpri : p.Prime
a : ℤ
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0
Tactic:
have h2 : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 2 :=
  by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h; contradiction
State after:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0

State before:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0
Tactic:
have hzero : ((⟨1, hpri.one_lt⟩ : Fin p) : ℕ) ≠ 0 :=
  by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h
State after:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
hzero : ↑⟨1, ⋯⟩ ≠ 0
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0

State before:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
hzero : ↑⟨1, ⋯⟩ ≠ 0
⊢ f1k₂ a ↑⟨1, ⋯⟩ = 0
Tactic:
simp only [f1k₂, h2, if_false, hzero, one_lt_two.ne]
State after:
no goals

State before:
p : ℕ
hpri : p.Prime
a : ℤ
⊢ ↑⟨1, ⋯⟩ ≠ 2
Tactic:
intro h
State after:
p : ℕ
hpri : p.Prime
a : ℤ
h : ↑⟨1, ⋯⟩ = 2
⊢ False

State before:
p : ℕ
hpri : p.Prime
a : ℤ
h : ↑⟨1, ⋯⟩ = 2
⊢ False
Tactic:
simp only [Fin.ext_iff, Fin.val_mk] at h
State after:
p : ℕ
hpri : p.Prime
a : ℤ
h : 1 = 2
⊢ False

State before:
p : ℕ
hpri : p.Prime
a : ℤ
h : 1 = 2
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
⊢ ↑⟨1, ⋯⟩ ≠ 0
Tactic:
intro h
State after:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
h : ↑⟨1, ⋯⟩ = 0
⊢ False

State before:
p : ℕ
hpri : p.Prime
a : ℤ
h2 : ↑⟨1, ⋯⟩ ≠ 2
h : ↑⟨1, ⋯⟩ = 0
⊢ False
Tactic:
simp only [Fin.ext_iff, Fin.val_mk] at h
State after:
no goals