case refine'_1
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c

case refine'_2
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) → 2 < card s
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
⊢ 2 < card s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
refine' ⟨fun h => _, _⟩
case refine'_1.intro
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
case refine'_1
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
obtain ⟨c, hc⟩ := card_pos.mp (pos_of_gt h)
case refine'_1.intro
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
this : 1 < card (erase s c)
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
case refine'_1.intro
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
have : 1 < (s.erase c).card := by rwa [← add_lt_add_iff_right 1, card_erase_add_one hc]
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
this : 1 < card (erase s c)
a b : α
ha : a ∈ erase s c
hb : b ∈ erase s c
hab : a ≠ b
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
case refine'_1.intro
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
this : 1 < card (erase s c)
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
obtain ⟨a, b, ha, hb, hab⟩ := one_lt_card_iff.mp this
no goals
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
this : 1 < card (erase s c)
a b : α
ha : a ∈ erase s c
hb : b ∈ erase s c
hab : a ≠ b
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
exact
  ⟨a, b, c, mem_of_mem_erase ha, mem_of_mem_erase hb, hc, hab, ne_of_mem_erase ha,
    ne_of_mem_erase hb⟩
no goals
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
⊢ 1 < card (erase s c)
rwa [← add_lt_add_iff_right 1, card_erase_add_one hc]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ 2 < card s
case refine'_2
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) → 2 < card s
rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ 2 < card (erase (erase (erase s c) b) a) + 1 + 1 + 1
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ 2 < card s
rw [← card_erase_add_one hc, ← card_erase_add_one (mem_erase_of_ne_of_mem hbc hb), ←
  card_erase_add_one (mem_erase_of_ne_of_mem hab (mem_erase_of_ne_of_mem hac ha))]
no goals
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.56033
s t : Finset α
f : α → β
n : ℕ
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ 2 < card (erase (erase (erase s c) b) a) + 1 + 1 + 1
apply Nat.le_add_left