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

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
⊢ ∃ i, f0k₂ a b ↑i = 0
Tactic:
refine' ⟨⟨2, two_lt hp5⟩, _⟩
State after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0

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

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h1 : ↑⟨2, ⋯⟩ ≠ 1
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0
Tactic:
have hzero : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ 0 := by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h
State after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h1 : ↑⟨2, ⋯⟩ ≠ 1
hzero : ↑⟨2, ⋯⟩ ≠ 0
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
a b : ℤ
h1 : ↑⟨2, ⋯⟩ ≠ 1
hzero : ↑⟨2, ⋯⟩ ≠ 0
⊢ f0k₂ a b ↑⟨2, ⋯⟩ = 0
Tactic:
simp only [f0k₂, h1, if_false, hzero, one_lt_two.ne']
State after:
no goals

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

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

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

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

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