[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
⊢ Monotone card
[PROOFSTEP]
apply card_le_of_subset
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
⊢ card ({a} ∩ s) ≤ 1
[PROOFSTEP]
cases' Finset.decidableMem a s with h h
[GOAL]
case isFalse
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card ({a} ∩ s) ≤ 1
[PROOFSTEP]
simp [Finset.singleton_inter_of_not_mem h]
[GOAL]
case isTrue
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card ({a} ∩ s) ≤ 1
[PROOFSTEP]
simp [Finset.singleton_inter_of_mem h]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card (insert a s) = card s + 1
[PROOFSTEP]
rw [← cons_eq_insert _ _ h, card_cons]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card (insert a s) = card s
[PROOFSTEP]
rw [insert_eq_of_mem h]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ card (insert a s) ≤ card s + 1
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ card (insert a s) ≤ card s + 1
[PROOFSTEP]
rw [insert_eq_of_mem h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∈ s
⊢ card s ≤ card s + 1
[PROOFSTEP]
exact Nat.le_succ _
[GOAL]
case neg
α : Type u_1
β : Type u_2
s✝ t : Finset α
a✝ b : α
inst✝ : DecidableEq α
a : α
s : Finset α
h : ¬a ∈ s
⊢ card (insert a s) ≤ card s + 1
[PROOFSTEP]
rw [card_insert_of_not_mem h]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
⊢ card (insert a s) = if a ∈ s then card s else card s + 1
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card (insert a s) = if a ∈ s then card s else card s + 1
[PROOFSTEP]
rw [card_insert_of_mem h, if_pos h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card (insert a s) = if a ∈ s then card s else card s + 1
[PROOFSTEP]
rw [card_insert_of_not_mem h, if_neg h]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ card {a, b} = 2
[PROOFSTEP]
rw [card_insert_of_not_mem (not_mem_singleton.2 h), card_singleton]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
⊢ card s - 1 ≤ card (erase s a)
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ card s - 1 ≤ card (erase s a)
[PROOFSTEP]
exact (card_erase_of_mem h).ge
[GOAL]
case neg
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card s - 1 ≤ card (erase s a)
[PROOFSTEP]
rw [erase_eq_of_not_mem h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
h : ¬a ∈ s
⊢ card s - 1 ≤ card s
[PROOFSTEP]
exact Nat.sub_le _ _
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
s : Finset α
⊢ List.length (toList s) = card s
[PROOFSTEP]
rw [toList, ← Multiset.coe_card, Multiset.coe_toList, card_def]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
⊢ card (image f s) ≤ card s
[PROOFSTEP]
simpa only [card_map] using (s.1.map f).toFinset_card_le
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : Set.InjOn f ↑s
⊢ card (image f s) = card s
[PROOFSTEP]
simp only [card, image_val_of_injOn H, card_map]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : card (image f s) = card s
⊢ Set.InjOn f ↑s
[PROOFSTEP]
rw [card_def, card_def, image, toFinset] at H 
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H :
  ↑Multiset.card { val := dedup (Multiset.map f s.val), nodup := (_ : Nodup (dedup (Multiset.map f s.val))) }.val =
    ↑Multiset.card s.val
⊢ Set.InjOn f ↑s
[PROOFSTEP]
dsimp only at H 
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
⊢ Set.InjOn f ↑s
[PROOFSTEP]
have : (s.1.map f).dedup = s.1.map f :=
  by
  refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
  simp only [H, Multiset.card_map, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
⊢ dedup (Multiset.map f s.val) = Multiset.map f s.val
[PROOFSTEP]
refine Multiset.eq_of_le_of_card_le (Multiset.dedup_le _) ?_
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
⊢ ↑Multiset.card (Multiset.map f s.val) ≤ ↑Multiset.card (dedup (Multiset.map f s.val))
[PROOFSTEP]
simp only [H, Multiset.card_map, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
this : dedup (Multiset.map f s.val) = Multiset.map f s.val
⊢ Set.InjOn f ↑s
[PROOFSTEP]
rw [Multiset.dedup_eq_self] at this 
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq β
H : ↑Multiset.card (dedup (Multiset.map f s.val)) = ↑Multiset.card s.val
this : Nodup (Multiset.map f s.val)
⊢ Set.InjOn f ↑s
[PROOFSTEP]
exact inj_on_of_nodup_map this
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f✝ : α → β
n : ℕ
s : Finset α
f : α → β
inst✝ : DecidableEq β
y : β
⊢ card (filter (fun x => f x = y) s) ≠ 0 ↔ y ∈ image f s
[PROOFSTEP]
rw [← pos_iff_ne_zero, card_pos, fiber_nonempty_iff_mem_image]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ card (Finset.subtype p s) = card (filter p s)
[PROOFSTEP]
simp [Finset.subtype]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝ : DecidablePred p
h : card (filter p s) = card s
x : α
hx : x ∈ s
⊢ p x
[PROOFSTEP]
rw [← eq_of_subset_of_card_le (s.filter_subset p) h.ge, mem_filter] at hx 
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝ : DecidablePred p
h : card (filter p s) = card s
x : α
hx : x ∈ s ∧ p x
⊢ p x
[PROOFSTEP]
exact hx.2
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
⊢ card s = n
[PROOFSTEP]
classical
have : ∀ a : α, a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a := fun a =>
  ⟨fun ha =>
    let ⟨i, hi, eq⟩ := hf a ha
    ⟨i, mem_range.2 hi, eq⟩,
    fun ⟨i, hi, eq⟩ => eq ▸ hf' i (mem_range.1 hi)⟩
have : s = (range n).attach.image fun i => f i.1 (mem_range.1 i.2) := by
  simpa only [ext_iff, mem_image, exists_prop, Subtype.exists, mem_attach, true_and_iff]
calc
  s.card = card ((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
  _ = card (range n).attach :=
    ((card_image_of_injective _) fun ⟨i, hi⟩ ⟨j, hj⟩ eq => Subtype.eq <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq)
  _ = card (range n) := card_attach
  _ = n := card_range n
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
⊢ card s = n
[PROOFSTEP]
have : ∀ a : α, a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a := fun a =>
  ⟨fun ha =>
    let ⟨i, hi, eq⟩ := hf a ha
    ⟨i, mem_range.2 hi, eq⟩,
    fun ⟨i, hi, eq⟩ => eq ▸ hf' i (mem_range.1 hi)⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : ∀ (a : α), a ∈ s ↔ ∃ i hi, f i (_ : i < n) = a
⊢ card s = n
[PROOFSTEP]
have : s = (range n).attach.image fun i => f i.1 (mem_range.1 i.2) := by
  simpa only [ext_iff, mem_image, exists_prop, Subtype.exists, mem_attach, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : ∀ (a : α), a ∈ s ↔ ∃ i hi, f i (_ : i < n) = a
⊢ s = image (fun i => f ↑i (_ : ↑i < n)) (attach (range n))
[PROOFSTEP]
simpa only [ext_iff, mem_image, exists_prop, Subtype.exists, mem_attach, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this✝ : ∀ (a : α), a ∈ s ↔ ∃ i hi, f i (_ : i < n) = a
this : s = image (fun i => f ↑i (_ : ↑i < n)) (attach (range n))
⊢ card s = n
[PROOFSTEP]
calc
  s.card = card ((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
  _ = card (range n).attach :=
    ((card_image_of_injective _) fun ⟨i, hi⟩ ⟨j, hj⟩ eq => Subtype.eq <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq)
  _ = card (range n) := card_attach
  _ = n := card_range n
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ (a : α), a ∈ s → ∃ i h, f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this✝ : ∀ (a : α), a ∈ s ↔ ∃ i hi, f i (_ : i < n) = a
this : s = image (fun i => f ↑i (_ : ↑i < n)) (attach (range n))
⊢ card s = card (image (fun i => f ↑i (_ : ↑i < n)) (attach (range n)))
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
⊢ card s = card t
[PROOFSTEP]
classical calc
  s.card = s.attach.card := card_attach.symm
  _ = (s.attach.image fun a : { a // a ∈ s } => f a.1 a.2).card :=
    (Eq.symm ((card_image_of_injective _) fun a b h => Subtype.eq <| h₂ _ _ _ _ h))
  _ = t.card :=
    congr_arg card
      (Finset.ext fun b =>
        ⟨fun h =>
          let ⟨a, _, ha₂⟩ := mem_image.1 h
          ha₂ ▸ h₁ _ _,
          fun h =>
          let ⟨a, ha₁, ha₂⟩ := h₃ b h
          mem_image.2 ⟨⟨a, ha₁⟩, by simp [ha₂]⟩⟩)
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
⊢ card s = card t
[PROOFSTEP]
calc
  s.card = s.attach.card := card_attach.symm
  _ = (s.attach.image fun a : { a // a ∈ s } => f a.1 a.2).card :=
    (Eq.symm ((card_image_of_injective _) fun a b h => Subtype.eq <| h₂ _ _ _ _ h))
  _ = t.card :=
    congr_arg card
      (Finset.ext fun b =>
        ⟨fun h =>
          let ⟨a, _, ha₂⟩ := mem_image.1 h
          ha₂ ▸ h₁ _ _,
          fun h =>
          let ⟨a, ha₁, ha₂⟩ := h₃ b h
          mem_image.2 ⟨⟨a, ha₁⟩, by simp [ha₂]⟩⟩)
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b
h₃ : ∀ (b : β), b ∈ t → ∃ a ha, f a ha = b
b : β
h : b ∈ t
a : α
ha₁ : a ∈ s
ha₂ : f a ha₁ = b
⊢ { val := a, property := ha₁ } ∈ attach s ∧
    f ↑{ val := a, property := ha₁ } (_ : ↑{ val := a, property := ha₁ } ∈ s) = b
[PROOFSTEP]
simp [ha₂]
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂
⊢ card s ≤ card t
[PROOFSTEP]
classical calc
  s.card = (s.image f).card := (card_image_of_injOn f_inj).symm
  _ ≤ t.card := card_le_of_subset <| image_subset_iff.2 hf
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂
⊢ card s ≤ card t
[PROOFSTEP]
calc
  s.card = (s.image f).card := (card_image_of_injOn f_inj).symm
  _ ≤ t.card := card_le_of_subset <| image_subset_iff.2 hf
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
⊢ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y ∧ f x = f y
[PROOFSTEP]
classical
by_contra' hz
refine' hc.not_le (card_le_card_of_inj_on f hf _)
intro x hx y hy
contrapose
exact hz x hx y hy
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
⊢ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y ∧ f x = f y
[PROOFSTEP]
by_contra' hz
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
⊢ False
[PROOFSTEP]
refine' hc.not_le (card_le_card_of_inj_on f hf _)
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
⊢ ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂
[PROOFSTEP]
intro x hx y hy
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ f x = f y → x = y
[PROOFSTEP]
contrapose
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ¬x = y → ¬f x = f y
[PROOFSTEP]
exact hz x hx y hy
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
⊢ ∀ (a : ℕ), a ∈ range n → f a ∈ s
[PROOFSTEP]
simpa only [mem_range]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f✝ : α → β
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
⊢ ∀ (a₁ : ℕ), a₁ ∈ range n → ∀ (a₂ : ℕ), a₂ ∈ range n → f a₁ = f a₂ → a₁ = a₂
[PROOFSTEP]
simpa only [mem_range]
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
⊢ ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
[PROOFSTEP]
classical
intro b hb
have h : (s.attach.image fun a : { a // a ∈ s } => f a a.prop).card = s.card :=
  @card_attach _ s ▸ card_image_of_injective _ fun ⟨a₁, ha₁⟩ ⟨a₂, ha₂⟩ h => Subtype.eq <| hinj _ _ _ _ h
have h' : image (fun a : { a // a ∈ s } => f a a.prop) s.attach = t :=
  eq_of_subset_of_card_le
    (fun b h =>
      let ⟨a, _, ha₂⟩ := mem_image.1 h
      ha₂ ▸ hf _ _)
    (by simp [hst, h])
rw [← h'] at hb 
obtain ⟨a, _, ha₂⟩ := mem_image.1 hb
exact ⟨a, a.2, ha₂.symm⟩
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
⊢ ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
[PROOFSTEP]
intro b hb
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ t
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
have h : (s.attach.image fun a : { a // a ∈ s } => f a a.prop).card = s.card :=
  @card_attach _ s ▸ card_image_of_injective _ fun ⟨a₁, ha₁⟩ ⟨a₂, ha₂⟩ h => Subtype.eq <| hinj _ _ _ _ h
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ t
h : card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)) = card s
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
have h' : image (fun a : { a // a ∈ s } => f a a.prop) s.attach = t :=
  eq_of_subset_of_card_le
    (fun b h =>
      let ⟨a, _, ha₂⟩ := mem_image.1 h
      ha₂ ▸ hf _ _)
    (by simp [hst, h])
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ t
h : card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)) = card s
⊢ card t ≤ card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s))
[PROOFSTEP]
simp [hst, h]
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ t
h : card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)) = card s
h' : image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s) = t
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
rw [← h'] at hb 
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)
h : card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)) = card s
h' : image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s) = t
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
obtain ⟨a, _, ha₂⟩ := mem_image.1 hb
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : card t ≤ card s
b : β
hb : b ∈ image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)
h : card (image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s)) = card s
h' : image (fun a => f ↑a (_ : ↑a ∈ s)) (attach s) = t
a : { a // a ∈ s }
left✝ : a ∈ attach s
ha₂ : f ↑a (_ : ↑a ∈ s) = b
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
exact ⟨a, a.2, ha₂.symm⟩
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : card s ≤ card t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
this : Inhabited { x // x ∈ s }
f' : { x // x ∈ s } → { x // x ∈ t } := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
g : { x // x ∈ t } → { x // x ∈ s } := surjInv (_ : ∀ (x : { x // x ∈ t }), ∃ a, f' a = x)
hg : Injective g
x : { x // x ∈ s }
⊢ card (attach s) ≤ card (attach t)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ card (s ∪ ∅) + card (s ∩ ∅) = card s + card ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
a : α
r : Finset α
har : ¬a ∈ r
h : card (s ∪ r) + card (s ∩ r) = card s + card r
⊢ card (s ∪ insert a r) + card (s ∩ insert a r) = card s + card (insert a r)
[PROOFSTEP]
by_cases a ∈ s
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
a : α
r : Finset α
har : ¬a ∈ r
h : card (s ∪ r) + card (s ∩ r) = card s + card r
⊢ card (s ∪ insert a r) + card (s ∩ insert a r) = card s + card (insert a r)
[PROOFSTEP]
by_cases a ∈ s
[GOAL]
case pos
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
a : α
r : Finset α
har : ¬a ∈ r
h✝ : card (s ∪ r) + card (s ∩ r) = card s + card r
h : a ∈ s
⊢ card (s ∪ insert a r) + card (s ∩ insert a r) = card s + card (insert a r)
[PROOFSTEP]
simp [*, ← add_assoc, add_right_comm _ 1]
[GOAL]
case neg
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
a : α
r : Finset α
har : ¬a ∈ r
h✝ : card (s ∪ r) + card (s ∩ r) = card s + card r
h : ¬a ∈ s
⊢ card (s ∪ insert a r) + card (s ∩ insert a r) = card s + card (insert a r)
[PROOFSTEP]
simp [*, ← add_assoc, add_right_comm _ 1]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ card (s ∩ t) + card (s ∪ t) = card s + card t
[PROOFSTEP]
rw [add_comm, card_union_add_card_inter]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : _root_.Disjoint s t
⊢ card (s ∪ t) = card s + card t
[PROOFSTEP]
rw [← disjUnion_eq_union s t h, card_disjUnion _ _ _]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : s ⊆ t
⊢ card (t \ s) = card t - card s
[PROOFSTEP]
suffices card (t \ s) = card (t \ s ∪ s) - s.card by rwa [sdiff_union_of_subset h] at this 
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : s ⊆ t
this : card (t \ s) = card (t \ s ∪ s) - card s
⊢ card (t \ s) = card t - card s
[PROOFSTEP]
rwa [sdiff_union_of_subset h] at this 
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : s ⊆ t
⊢ card (t \ s) = card (t \ s ∪ s) - card s
[PROOFSTEP]
rw [card_disjoint_union sdiff_disjoint, add_tsub_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ card (t \ (s ∩ t)) ≤ card (t \ s)
[PROOFSTEP]
rw [sdiff_inter_self_right t s]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card (s \ t) + card t = card (s ∪ t)
[PROOFSTEP]
rw [← card_disjoint_union sdiff_disjoint, sdiff_union_self_eq_union]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ card (filter p s) + card (filter (fun a => ¬p a) s) = card s
[PROOFSTEP]
classical rw [← card_union_eq (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
⊢ card (filter p s) + card (filter (fun a => ¬p a) s) = card s
[PROOFSTEP]
rw [← card_union_eq (disjoint_filter_filter_neg _ _ _), filter_union_filter_neg_eq]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₁ : i + card B ≤ card A
h₂ : B ⊆ A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
classical
rcases Nat.le.dest h₁ with ⟨k, h⟩
clear h₁
induction' k with k ih generalizing A
· exact ⟨A, h₂, Subset.refl _, h.symm⟩
obtain ⟨a, ha⟩ : (A \ B).Nonempty :=
  by
  rw [← card_pos, card_sdiff h₂, ← h, Nat.add_right_comm, add_tsub_cancel_right, Nat.add_succ]
  apply Nat.succ_pos
have z : i + card B + k = card (erase A a) := by
  rw [card_erase_of_mem (mem_sdiff.1 ha).1, ← h, Nat.add_sub_assoc (Nat.one_le_iff_ne_zero.mpr k.succ_ne_zero), ←
    pred_eq_sub_one, k.pred_succ]
have : B ⊆ A.erase a := by
  rintro t th
  apply mem_erase_of_ne_of_mem _ (h₂ th)
  rintro rfl
  exact not_mem_sdiff_of_mem_right th ha
rcases ih this z with ⟨B', hB', B'subA', cards⟩
exact ⟨B', hB', B'subA'.trans (erase_subset _ _), cards⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₁ : i + card B ≤ card A
h₂ : B ⊆ A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
rcases Nat.le.dest h₁ with ⟨k, h⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₁ : i + card B ≤ card A
h₂ : B ⊆ A
k : ℕ
h : i + card B + k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
clear h₁
[GOAL]
case intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₂ : B ⊆ A
k : ℕ
h : i + card B + k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
induction' k with k ih generalizing A
[GOAL]
case intro.zero
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k : ℕ
h✝ : i + card B + k = card A✝
A : Finset α
h₂ : B ⊆ A
h : i + card B + zero = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
exact ⟨A, h₂, Subset.refl _, h.symm⟩
[GOAL]
case intro.succ
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
obtain ⟨a, ha⟩ : (A \ B).Nonempty :=
  by
  rw [← card_pos, card_sdiff h₂, ← h, Nat.add_right_comm, add_tsub_cancel_right, Nat.add_succ]
  apply Nat.succ_pos
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
⊢ Finset.Nonempty (A \ B)
[PROOFSTEP]
rw [← card_pos, card_sdiff h₂, ← h, Nat.add_right_comm, add_tsub_cancel_right, Nat.add_succ]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
⊢ 0 < succ (i + k)
[PROOFSTEP]
apply Nat.succ_pos
[GOAL]
case intro.succ.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
have z : i + card B + k = card (erase A a) := by
  rw [card_erase_of_mem (mem_sdiff.1 ha).1, ← h, Nat.add_sub_assoc (Nat.one_le_iff_ne_zero.mpr k.succ_ne_zero), ←
    pred_eq_sub_one, k.pred_succ]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
⊢ i + card B + k = card (erase A a)
[PROOFSTEP]
rw [card_erase_of_mem (mem_sdiff.1 ha).1, ← h, Nat.add_sub_assoc (Nat.one_le_iff_ne_zero.mpr k.succ_ne_zero), ←
  pred_eq_sub_one, k.pred_succ]
[GOAL]
case intro.succ.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
have : B ⊆ A.erase a := by
  rintro t th
  apply mem_erase_of_ne_of_mem _ (h₂ th)
  rintro rfl
  exact not_mem_sdiff_of_mem_right th ha
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
⊢ B ⊆ erase A a
[PROOFSTEP]
rintro t th
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
t : α
th : t ∈ B
⊢ t ∈ erase A a
[PROOFSTEP]
apply mem_erase_of_ne_of_mem _ (h₂ th)
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
t : α
th : t ∈ B
⊢ t ≠ a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
t : α
th : t ∈ B
ha : t ∈ A \ B
z : i + card B + k = card (erase A t)
⊢ False
[PROOFSTEP]
exact not_mem_sdiff_of_mem_right th ha
[GOAL]
case intro.succ.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
this : B ⊆ erase A a
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
rcases ih this z with ⟨B', hB', B'subA', cards⟩
[GOAL]
case intro.succ.intro.intro.intro.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
this : B ⊆ erase A a
B' : Finset α
hB' : B ⊆ B'
B'subA' : B' ⊆ erase A a
cards : card B' = i + card B
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
[PROOFSTEP]
exact ⟨B', hB', B'subA'.trans (erase_subset _ _), cards⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
A : Finset α
i : ℕ
h₁ : i ≤ card A
⊢ i + card ∅ ≤ card A
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
have h₁ : (X ∩ (Y \ X)).card = 0 := Finset.card_eq_zero.mpr (Finset.inter_sdiff_self X Y)
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
h₁ : card (X ∩ (Y \ X)) = 0
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
have h₂ : (X ∪ Y).card = X.card + (Y \ X).card := by
  rw [← card_union_add_card_inter X (Y \ X), Finset.union_sdiff_self_eq_union, h₁, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
h₁ : card (X ∩ (Y \ X)) = 0
⊢ card (X ∪ Y) = card X + card (Y \ X)
[PROOFSTEP]
rw [← card_union_add_card_inter X (Y \ X), Finset.union_sdiff_self_eq_union, h₁, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : 2 * n < card (X ∪ Y)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
rw [h₂, two_mul] at hXY 
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
rcases lt_or_lt_of_add_lt_add hXY with (h | h)
[GOAL]
case inl
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
h : n < card X
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
exact ⟨X, h, Or.inl (Finset.Subset.refl X)⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n✝ : ℕ
inst✝ : DecidableEq α
X Y : Finset α
n : ℕ
hXY : n + n < card X + card (Y \ X)
h₁ : card (X ∩ (Y \ X)) = 0
h₂ : card (X ∪ Y) = card X + card (Y \ X)
h : n < card (Y \ X)
⊢ ∃ C, n < card C ∧ (C ⊆ X ∨ C ⊆ Y)
[PROOFSTEP]
exact ⟨Y \ X, h, Or.inr (Finset.sdiff_subset Y X)⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ card s = 1 ↔ ∃ a, s = {a}
[PROOFSTEP]
cases s
[GOAL]
case mk
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
val✝ : Multiset α
nodup✝ : Nodup val✝
⊢ card { val := val✝, nodup := nodup✝ } = 1 ↔ ∃ a, { val := val✝, nodup := nodup✝ } = {a}
[PROOFSTEP]
simp only [Multiset.card_eq_one, Finset.card, ← val_inj, singleton_val]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a x, insert a s = t) ↔ s ⊆ t ∧ card s + 1 = card t
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a x, insert a s = t) → s ⊆ t ∧ card s + 1 = card t
[PROOFSTEP]
rintro ⟨a, ha, rfl⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
ha : ¬a ∈ s
⊢ s ⊆ insert a s ∧ card s + 1 = card (insert a s)
[PROOFSTEP]
exact ⟨subset_insert _ _, (card_insert_of_not_mem ha).symm⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊆ t ∧ card s + 1 = card t → ∃ a x, insert a s = t
[PROOFSTEP]
rintro ⟨hst, h⟩
[GOAL]
case mpr.intro
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
⊢ ∃ a x, insert a s = t
[PROOFSTEP]
obtain ⟨a, ha⟩ : ∃ a, t \ s = { a } := card_eq_one.1 (by rw [card_sdiff hst, ← h, add_tsub_cancel_left])
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
⊢ card (t \ s) = 1
[PROOFSTEP]
rw [card_sdiff hst, ← h, add_tsub_cancel_left]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
⊢ ∃ a x, insert a s = t
[PROOFSTEP]
refine' ⟨a, fun hs => (_ : a ∉ { a }) <| mem_singleton_self _, by rw [insert_eq, ← ha, sdiff_union_of_subset hst]⟩
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
⊢ insert a s = t
[PROOFSTEP]
rw [insert_eq, ← ha, sdiff_union_of_subset hst]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ ¬a ∈ {a}
[PROOFSTEP]
rw [← ha]
[GOAL]
case mpr.intro.intro
α : Type u_1
β : Type u_2
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ ¬a ∈ t \ s
[PROOFSTEP]
exact not_mem_sdiff_of_mem_right hs
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ card s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
[PROOFSTEP]
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
[GOAL]
case inl
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
⊢ card ∅ ≤ 1 ↔ ∀ (a : α), a ∈ ∅ → ∀ (b : α), b ∈ ∅ → a = b
[PROOFSTEP]
simp
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ card s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
[PROOFSTEP]
refine' (Nat.succ_le_of_lt (card_pos.2 ⟨x, hx⟩)).le_iff_eq.trans (card_eq_one.trans ⟨_, _⟩)
[GOAL]
case inr.intro.refine'_1
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ (∃ a, s = {a}) → ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
[PROOFSTEP]
rintro ⟨y, rfl⟩
[GOAL]
case inr.intro.refine'_1.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
x y : α
hx : x ∈ {y}
⊢ ∀ (a : α), a ∈ {y} → ∀ (b : α), b ∈ {y} → a = b
[PROOFSTEP]
simp
[GOAL]
case inr.intro.refine'_2
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
x : α
hx : x ∈ s
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b) → ∃ a, s = {a}
[PROOFSTEP]
exact fun h => ⟨x, eq_singleton_iff_unique_mem.2 ⟨hx, fun y hy => h _ hy _ hx⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ card s ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
[PROOFSTEP]
rw [card_le_one]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
⊢ card s ≤ 1 ↔ ∃ x, s ⊆ {x}
[PROOFSTEP]
refine' ⟨fun H => _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card s ≤ 1
⊢ ∃ x, s ⊆ {x}
[PROOFSTEP]
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
[GOAL]
case refine'_1.inl
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card ∅ ≤ 1
⊢ ∃ x, ∅ ⊆ {x}
[PROOFSTEP]
exact ⟨Classical.arbitrary α, empty_subset _⟩
[GOAL]
case refine'_1.inr.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ x, s ⊆ {x}
[PROOFSTEP]
exact ⟨x, fun y hy => by rw [card_le_one.1 H y hy x hx, mem_singleton]⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
H : card s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ y ∈ {x}
[PROOFSTEP]
rw [card_le_one.1 H y hy x hx, mem_singleton]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
⊢ (∃ x, s ⊆ {x}) → card s ≤ 1
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case refine'_2.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ card s ≤ 1
[PROOFSTEP]
rw [← card_singleton x]
[GOAL]
case refine'_2.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : Nonempty α
x : α
hx : s ⊆ {x}
⊢ card s ≤ card {x}
[PROOFSTEP]
exact card_le_of_subset hx
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ 1 < card s ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ ¬1 < card s ↔ ¬∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b
[PROOFSTEP]
push_neg
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ card s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
[PROOFSTEP]
exact card_le_one
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ 1 < card s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
[PROOFSTEP]
rw [one_lt_card]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ (∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
[PROOFSTEP]
simp only [exists_prop, exists_and_left]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ 2 < card s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
classical
refine' ⟨fun h => _, _⟩
· obtain ⟨c, hc⟩ := card_pos.mp (pos_of_gt h)
  have : 1 < (s.erase c).card := by rwa [← add_lt_add_iff_right 1, card_erase_add_one hc]
  obtain ⟨a, b, ha, hb, hab⟩ := one_lt_card_iff.mp this
  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⟩
· rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩
  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))]
  apply Nat.le_add_left
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ 2 < card s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
⊢ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
obtain ⟨c, hc⟩ := card_pos.mp (pos_of_gt h)
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
have : 1 < (s.erase c).card := by rwa [← add_lt_add_iff_right 1, card_erase_add_one hc]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
h : 2 < card s
c : α
hc : c ∈ s
⊢ 1 < card (erase s c)
[PROOFSTEP]
rwa [← add_lt_add_iff_right 1, card_erase_add_one hc]
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
obtain ⟨a, b, ha, hb, hab⟩ := one_lt_card_iff.mp this
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
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⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ (∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) → 2 < card s
[PROOFSTEP]
rintro ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
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))]
[GOAL]
case refine'_2.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
⊢ 2 < card s ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ ∃ c, c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
simp_rw [two_lt_card_iff, exists_and_left]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a : α
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
obtain ⟨x, hx, y, hy, hxy⟩ := Finset.one_lt_card.mp hs
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
by_cases ha : y = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : y = a
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
exact ⟨x, hx, ne_of_ne_of_eq hxy ha⟩
[GOAL]
case neg
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
hs : 1 < card s
a x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
ha : ¬y = a
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
exact ⟨y, hy, ha⟩
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
h : card s = n + 1
a : α
has : a ∈ s
⊢ card (erase s a) = n
[PROOFSTEP]
simp only [h, card_erase_of_mem has, add_tsub_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 2 → ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
rw [card_eq_succ]
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ card t = 1) → ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
simp_rw [card_eq_one]
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ∃ a, t = {a}) → ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
rintro ⟨a, _, hab, rfl, b, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b : α
hab : ¬a ∈ {b}
⊢ ∃ x y, x ≠ y ∧ {a, b} = {x, y}
[PROOFSTEP]
exact ⟨a, b, not_mem_singleton.1 hab, rfl⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → card s = 2
[PROOFSTEP]
rintro ⟨x, y, h, rfl⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
x y : α
h : x ≠ y
⊢ card {x, y} = 2
[PROOFSTEP]
exact card_doubleton h
[GOAL]
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ card s = 3 → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
rw [card_eq_succ]
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ card t = 2) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
simp_rw [card_eq_two]
[GOAL]
case mp
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
rintro ⟨a, _, abc, rfl, b, c, bc, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : ¬a ∈ {b, c}
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}
[PROOFSTEP]
rw [mem_insert, mem_singleton, not_or] at abc 
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
a b c : α
bc : b ≠ c
abc : ¬a = b ∧ ¬a = c
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {a, b, c} = {x, y, z}
[PROOFSTEP]
exact ⟨a, b, c, abc.1, abc.2, bc, rfl⟩
[GOAL]
case mpr
α : Type u_1
β : Type u_2
s t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → card s = 3
[PROOFSTEP]
rintro ⟨x, y, z, xy, xz, yz, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
x y z : α
xy : x ≠ y
xz : x ≠ z
yz : y ≠ z
⊢ card {x, y, z} = 3
[PROOFSTEP]
simp only [xy, xz, yz, mem_insert, card_insert_of_not_mem, not_false_iff, mem_singleton, or_self_iff, card_singleton]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
s : Finset α
⊢ strongInduction H s = H s fun t x => strongInduction H t
[PROOFSTEP]
rw [strongInduction]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ strongInductionOn s H = H s fun t x => strongInductionOn t H
[PROOFSTEP]
dsimp only [strongInductionOn]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ strongInduction H s = H s fun t x => strongInduction H t
[PROOFSTEP]
rw [strongInduction]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
H : (t₁ : Finset α) → ({t₂ : Finset α} → card t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → card t₁ ≤ n → p t₁
s : Finset α
⊢ strongDownwardInduction H s = H s fun {t} ht x => strongDownwardInduction H t ht
[PROOFSTEP]
rw [strongDownwardInduction]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → card t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → card t₁ ≤ n → p t₁
⊢ (fun a => strongDownwardInductionOn s H a) = H s fun {t} ht x => strongDownwardInductionOn t H ht
[PROOFSTEP]
dsimp only [strongDownwardInductionOn]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t : Finset α
f : α → β
n : ℕ
p : Finset α → Sort u_3
s : Finset α
H : (t₁ : Finset α) → ({t₂ : Finset α} → card t₂ ≤ n → t₁ ⊂ t₂ → p t₂) → card t₁ ≤ n → p t₁
⊢ (fun a => strongDownwardInduction H s a) = H s fun {t} ht x => strongDownwardInduction H t ht
[PROOFSTEP]
rw [strongDownwardInduction]
