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

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

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
⊢ f0k₁ b p ↑⟨2, ⋯⟩ = 0
Tactic:
have hpred : ((⟨2, two_lt hp5⟩ : Fin p) : ℕ) ≠ p.pred := by
  intro h
  simp only [Fin.ext_iff, Fin.val_mk] at h
  replace h := h.symm
  rw [Nat.pred_eq_sub_one] at h
  omega
State after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
⊢ f0k₁ b p ↑⟨2, ⋯⟩ = 0

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
⊢ f0k₁ b p ↑⟨2, ⋯⟩ = 0
Tactic:
simp only [f0k₁, OfNat.ofNat_ne_one, ite_false, ite_eq_right_iff, neg_eq_zero]
State after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
⊢ 2 = p.pred → b = 0

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
⊢ 2 = p.pred → b = 0
Tactic:
intro h2
State after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ b = 0

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ b = 0
Tactic:
exfalso
State after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ False

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ False
Tactic:
apply hpred
State after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ ↑⟨2, ⋯⟩ = p.pred

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
hpred : ↑⟨2, ⋯⟩ ≠ p.pred
h2 : 2 = p.pred
⊢ ↑⟨2, ⋯⟩ = p.pred
Tactic:
simp [h2]
State after:
no goals

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

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

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : 2 = p.pred
⊢ False
Tactic:
replace h := h.symm
State after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : p.pred = 2
⊢ False

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : p.pred = 2
⊢ False
Tactic:
rw [Nat.pred_eq_sub_one] at h
State after:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
b : ℤ
h : p - 1 = 2
⊢ False

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