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

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
have h0 : 0 < p := by linarith
State after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
have h1 : 1 < p := by linarith
State after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
let s := ({0, 1, k₁.1, k₂.1} : Finset ℕ)
State after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
have : s.card ≤ 4 := by
  repeat refine' le_trans (card_insert_le _ _) (succ_le_succ _)
  exact rfl.ge
State after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card ≤ 4
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card ≤ 4
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
replace this : s.card < 5 := lt_of_le_of_lt this (by norm_num)
State after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hs : s ⊆ range p := insert_subset_iff.2 ⟨mem_range.2 h0, insert_subset_iff.2
  ⟨mem_range.2 h1, insert_subset_iff.2 ⟨mem_range.2 (Fin.is_lt _),
  singleton_subset_iff.2 (mem_range.2 (Fin.is_lt _))⟩⟩⟩
State after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hcard := card_sdiff hs
State after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).card = (range p).card - s.card
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).card = (range p).card - s.card
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
replace hcard : (range p \ s).Nonempty := by
  rw [← Finset.card_pos, hcard, card_range]
  exact Nat.sub_pos_of_lt (lt_of_lt_of_le this hp5)
State after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).Nonempty
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).Nonempty
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
obtain ⟨i, hi⟩ := hcard
State after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0

State before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
⊢ ∃ i ∈ range p, f a b (↑k₁) (↑k₂) i = 0
Tactic:
refine' ⟨i, sdiff_subset hi, _⟩
State after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
⊢ f a b (↑k₁) (↑k₂) i = 0

State before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
⊢ f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hi0 : i ≠ 0 := fun h => by simp [h, s] at hi
State after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
⊢ f a b (↑k₁) (↑k₂) i = 0

State before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
⊢ f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hi1 : i ≠ 1 := fun h => by simp [h, s] at hi
State after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
⊢ f a b (↑k₁) (↑k₂) i = 0

State before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
⊢ f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hik₁ : i ≠ k₁ := fun h => by simp [h, s] at hi
State after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
hik₁ : i ≠ ↑k₁
⊢ f a b (↑k₁) (↑k₂) i = 0

State before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
hik₁ : i ≠ ↑k₁
⊢ f a b (↑k₁) (↑k₂) i = 0
Tactic:
have hik₂ : i ≠ k₂ := fun h => by simp [h, s] at hi
State after:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
hik₁ : i ≠ ↑k₁
hik₂ : i ≠ ↑k₂
⊢ f a b (↑k₁) (↑k₂) i = 0

State before:
case intro
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
hik₁ : i ≠ ↑k₁
hik₂ : i ≠ ↑k₂
⊢ f a b (↑k₁) (↑k₂) i = 0
Tactic:
simp [f, hi0, hi1, hik₁, hik₂]
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
⊢ 0 < p
Tactic:
linarith
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
⊢ 1 < p
Tactic:
linarith
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ s.card ≤ 4
Tactic:
repeat refine' le_trans (card_insert_le _ _) (succ_le_succ _)
State after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ {↑k₂}.card ≤ 1

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ {↑k₂}.card ≤ 1
Tactic:
exact rfl.ge
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ {↑k₁, ↑k₂}.card ≤ 2
Tactic:
refine' le_trans (card_insert_le _ _) (succ_le_succ _)
State after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
⊢ {↑k₂}.card ≤ 1

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card ≤ 4
⊢ 4 < 5
Tactic:
norm_num
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).card = (range p).card - s.card
⊢ (range p \ s).Nonempty
Tactic:
rw [← Finset.card_pos, hcard, card_range]
State after:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).card = (range p).card - s.card
⊢ 0 < p - s.card

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
hcard : (range p \ s).card = (range p).card - s.card
⊢ 0 < p - s.card
Tactic:
exact Nat.sub_pos_of_lt (lt_of_lt_of_le this hp5)
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
h : i = 0
⊢ False
Tactic:
simp [h, s] at hi
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
h : i = 1
⊢ False
Tactic:
simp [h, s] at hi
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
h : i = ↑k₁
⊢ False
Tactic:
simp [h, s] at hi
State after:
no goals

State before:
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
hik₁ : i ≠ ↑k₁
h : i = ↑k₂
⊢ False
Tactic:
simp [h, s] at hi
State after:
no goals