Theorem: FltRegular.auxf (FltRegular/CaseI/Statement.lean)

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
⊢ ∃ i, f a b ↑k₁ ↑k₂ ↑i = 0
Tactic:
obtain ⟨i, hrange, hi⟩ := auxf' hp5 a b k₁ k₂
State after:
case intro.intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
i : ℕ
hrange : i ∈ range p
hi : f a b (↑k₁) (↑k₂) i = 0
⊢ ∃ i, f a b ↑k₁ ↑k₂ ↑i = 0

State before:
case intro.intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
i : ℕ
hrange : i ∈ range p
hi : f a b (↑k₁) (↑k₂) i = 0
⊢ ∃ i, f a b ↑k₁ ↑k₂ ↑i = 0
Tactic:
exact ⟨⟨i, mem_range.1 hrange⟩, hi⟩
State after:
no goals