[GOAL]
α : Type u_1
s✝ t s : Set α
⊢ encard univ = encard s
[PROOFSTEP]
rw [encard, encard, PartENat.card_congr (Equiv.Set.univ ↑s)]
[GOAL]
α✝ : Type ?u.625
s t : Set α✝
α : Type u_1
⊢ encard univ = ↑PartENat.withTopEquiv (PartENat.card α)
[PROOFSTEP]
rw [encard, PartENat.card_congr (Equiv.Set.univ α)]
[GOAL]
α : Type u_1
s t : Set α
h : Set.Finite s
⊢ encard s = ↑(Finset.card (Finite.toFinset h))
[PROOFSTEP]
have := h.fintype
[GOAL]
α : Type u_1
s t : Set α
h : Set.Finite s
this : Fintype ↑s
⊢ encard s = ↑(Finset.card (Finite.toFinset h))
[PROOFSTEP]
rw [encard, PartENat.card_eq_coe_fintype_card, PartENat.withTopEquiv_natCast, toFinite_toFinset, toFinset_card]
[GOAL]
α : Type u_1
s✝ t s : Set α
inst✝ : Fintype ↑s
⊢ encard s = ↑(Finset.card (toFinset s))
[PROOFSTEP]
have h := toFinite s
[GOAL]
α : Type u_1
s✝ t s : Set α
inst✝ : Fintype ↑s
h : Set.Finite s
⊢ encard s = ↑(Finset.card (toFinset s))
[PROOFSTEP]
rw [h.encard_eq_coe_toFinset_card, toFinite_toFinset, toFinset_card]
[GOAL]
α : Type u_1
s✝ t : Set α
s : Finset α
⊢ encard ↑s = ↑(Finset.card s)
[PROOFSTEP]
rw [Finite.encard_eq_coe_toFinset_card (Finset.finite_toSet s)]
[GOAL]
α : Type u_1
s✝ t : Set α
s : Finset α
⊢ ↑(Finset.card (Finite.toFinset (_ : Set.Finite ↑s))) = ↑(Finset.card s)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s✝ t s : Set α
h : Set.Infinite s
⊢ encard s = ⊤
[PROOFSTEP]
have := h.to_subtype
[GOAL]
α : Type u_1
s✝ t s : Set α
h : Set.Infinite s
this : Infinite ↑s
⊢ encard s = ⊤
[PROOFSTEP]
rw [encard, ← PartENat.withTopEquiv.symm.injective.eq_iff, Equiv.symm_apply_apply, PartENat.withTopEquiv_symm_top,
  PartENat.card_eq_top_of_infinite]
[GOAL]
α : Type u_1
s t : Set α
⊢ encard s = 0 ↔ s = ∅
[PROOFSTEP]
rw [encard, ← PartENat.withTopEquiv.symm.injective.eq_iff, Equiv.symm_apply_apply, PartENat.withTopEquiv_symm_zero,
  PartENat.card_eq_zero_iff_empty, isEmpty_subtype, eq_empty_iff_forall_not_mem]
[GOAL]
α : Type u_1
s t : Set α
⊢ encard ∅ = 0
[PROOFSTEP]
rw [encard_eq_zero]
[GOAL]
α : Type u_1
s t : Set α
h : encard s ≠ 0
⊢ Set.Nonempty s
[PROOFSTEP]
rwa [nonempty_iff_ne_empty, Ne.def, ← encard_eq_zero]
[GOAL]
α : Type u_1
s t : Set α
⊢ encard s ≠ 0 ↔ Set.Nonempty s
[PROOFSTEP]
rw [ne_eq, encard_eq_zero, nonempty_iff_ne_empty]
[GOAL]
α : Type u_1
s t : Set α
⊢ 0 < encard s ↔ Set.Nonempty s
[PROOFSTEP]
rw [pos_iff_ne_zero, encard_ne_zero]
[GOAL]
α : Type u_1
s t : Set α
e : α
⊢ encard {e} = 1
[PROOFSTEP]
rw [encard, ← PartENat.withTopEquiv.symm.injective.eq_iff, Equiv.symm_apply_apply, PartENat.card_eq_coe_fintype_card,
  Fintype.card_ofSubsingleton, Nat.cast_one]
[GOAL]
α : Type u_1
s t : Set α
e : α
⊢ 1 = ↑PartENat.withTopEquiv.symm 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ encard (s ∪ t) = encard s + encard t
[PROOFSTEP]
classical
have e := (Equiv.Set.union (by rwa [subset_empty_iff, ← disjoint_iff_inter_eq_empty])).symm
simp [encard, ← PartENat.card_congr e, PartENat.card_sum, PartENat.withTopEquiv]
[GOAL]
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ encard (s ∪ t) = encard s + encard t
[PROOFSTEP]
have e := (Equiv.Set.union (by rwa [subset_empty_iff, ← disjoint_iff_inter_eq_empty])).symm
[GOAL]
α : Type u_1
s t : Set α
h : Disjoint s t
⊢ ?m.6436 ∩ ?m.6437 ⊆ ∅
[PROOFSTEP]
rwa [subset_empty_iff, ← disjoint_iff_inter_eq_empty]
[GOAL]
α : Type u_1
s t : Set α
h : Disjoint s t
e : ↑s ⊕ ↑t ≃ ↑(s ∪ t)
⊢ encard (s ∪ t) = encard s + encard t
[PROOFSTEP]
simp [encard, ← PartENat.card_congr e, PartENat.card_sum, PartENat.withTopEquiv]
[GOAL]
α : Type u_1
s t : Set α
a : α
has : ¬a ∈ s
⊢ encard (insert a s) = encard s + 1
[PROOFSTEP]
rw [← union_singleton, encard_union_eq (by simpa), encard_singleton]
[GOAL]
α : Type u_1
s t : Set α
a : α
has : ¬a ∈ s
⊢ Disjoint s {a}
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
s t : Set α
h : Set.Finite s
⊢ encard s < ⊤
[PROOFSTEP]
refine' h.induction_on (by simpa using WithTop.zero_lt_top) _
[GOAL]
α : Type u_1
s t : Set α
h : Set.Finite s
⊢ encard ∅ < ⊤
[PROOFSTEP]
simpa using WithTop.zero_lt_top
[GOAL]
α : Type u_1
s t : Set α
h : Set.Finite s
⊢ ∀ {a : α} {s : Set α}, ¬a ∈ s → Set.Finite s → encard s < ⊤ → encard (insert a s) < ⊤
[PROOFSTEP]
rintro a t hat _ ht'
[GOAL]
α : Type u_1
s t✝ : Set α
h : Set.Finite s
a : α
t : Set α
hat : ¬a ∈ t
a✝ : Set.Finite t
ht' : encard t < ⊤
⊢ encard (insert a t) < ⊤
[PROOFSTEP]
rw [encard_insert_of_not_mem hat]
[GOAL]
α : Type u_1
s t✝ : Set α
h : Set.Finite s
a : α
t : Set α
hat : ¬a ∈ t
a✝ : Set.Finite t
ht' : encard t < ⊤
⊢ encard t + 1 < ⊤
[PROOFSTEP]
exact lt_tsub_iff_right.1 ht'
[GOAL]
α : Type u_1
s t : Set α
⊢ encard s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
rw [← not_iff_not, ← Ne.def, ← lt_top_iff_ne_top, encard_lt_top_iff, not_infinite]
[GOAL]
α : Type u_1
s t : Set α
⊢ encard s ≠ ⊤ ↔ Set.Finite s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s t : Set α
k : ℕ
h : encard s ≤ ↑k
⊢ Set.Finite s
[PROOFSTEP]
rw [← encard_lt_top_iff]
[GOAL]
α : Type u_1
s t : Set α
k : ℕ
h : encard s ≤ ↑k
⊢ encard s < ⊤
[PROOFSTEP]
exact h.trans_lt (WithTop.coe_lt_top _)
[GOAL]
α : Type u_1
s t : Set α
k : ℕ
h : encard s ≤ ↑k
⊢ ∃ n₀, encard s = ↑n₀ ∧ n₀ ≤ k
[PROOFSTEP]
rwa [ENat.le_coe_iff] at h 
[GOAL]
α : Type u_1
s t : Set α
k : ℕ
x✝ : Set.Finite s ∧ ∃ n₀, encard s = ↑n₀ ∧ n₀ ≤ k
left✝ : Set.Finite s
n₀ : ℕ
hs : encard s = ↑n₀
hle : n₀ ≤ k
⊢ encard s ≤ ↑k
[PROOFSTEP]
rwa [hs, Nat.cast_le]
[GOAL]
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ encard s ≤ encard t
[PROOFSTEP]
rw [← union_diff_cancel h, encard_union_eq disjoint_sdiff_right]
[GOAL]
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ encard s ≤ encard s + encard (t \ s)
[PROOFSTEP]
exact le_self_add
[GOAL]
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ encard (t \ s) + encard s = encard t
[PROOFSTEP]
rw [← encard_union_eq disjoint_sdiff_left, diff_union_self, union_eq_self_of_subset_right h]
[GOAL]
α : Type u_1
s t : Set α
⊢ 1 ≤ encard s ↔ Set.Nonempty s
[PROOFSTEP]
rw [nonempty_iff_ne_empty, Ne.def, ← encard_eq_zero, ENat.one_le_iff_ne_zero]
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
⊢ encard (s \ t) + encard (s ∩ t) = encard s
[PROOFSTEP]
rw [← encard_union_eq (disjoint_of_subset_right (inter_subset_right _ _) disjoint_sdiff_left), diff_union_inter]
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
⊢ encard (s ∪ t) + encard (s ∩ t) = encard s + encard t
[PROOFSTEP]
rw [← diff_union_self, encard_union_eq disjoint_sdiff_left, add_right_comm, encard_diff_add_encard_inter]
[GOAL]
α : Type u_1
s t : Set α
h : Set.Finite (s ∩ t)
⊢ encard s = encard t ↔ encard (s \ t) = encard (t \ s)
[PROOFSTEP]
rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
  WithTop.add_right_cancel_iff h.encard_lt_top.ne]
[GOAL]
α : Type u_1
s t : Set α
h : Set.Finite (s ∩ t)
⊢ encard s ≤ encard t ↔ encard (s \ t) ≤ encard (t \ s)
[PROOFSTEP]
rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
  WithTop.add_le_add_iff_right h.encard_lt_top.ne]
[GOAL]
α : Type u_1
s t : Set α
h : Set.Finite (s ∩ t)
⊢ encard s < encard t ↔ encard (s \ t) < encard (t \ s)
[PROOFSTEP]
rw [← encard_diff_add_encard_inter s t, ← encard_diff_add_encard_inter t s, inter_comm t s,
  WithTop.add_lt_add_iff_right h.encard_lt_top.ne]
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
⊢ encard (s ∪ t) ≤ encard s + encard t
[PROOFSTEP]
rw [← encard_union_add_encard_inter]
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
⊢ encard (s ∪ t) ≤ encard (s ∪ t) + encard (s ∩ t)
[PROOFSTEP]
exact le_self_add
[GOAL]
α : Type u_1
s t : Set α
h : encard s = encard t
⊢ Set.Finite s ↔ Set.Finite t
[PROOFSTEP]
rw [← encard_lt_top_iff, ← encard_lt_top_iff, h]
[GOAL]
α : Type u_1
s t : Set α
h : encard s = encard t
⊢ Set.Infinite s ↔ Set.Infinite t
[PROOFSTEP]
rw [← encard_eq_top_iff, h, encard_eq_top_iff]
[GOAL]
α : Type u_1
s t : Set α
ht : Set.Finite t
hst : s ⊆ t
hts : encard t ≤ encard s
⊢ s = t
[PROOFSTEP]
rw [← zero_add (a := encard s), ← encard_diff_add_encard_of_subset hst] at hts 
[GOAL]
α : Type u_1
s t : Set α
ht : Set.Finite t
hst : s ⊆ t
hts : encard (t \ s) + encard s ≤ 0 + encard s
⊢ s = t
[PROOFSTEP]
have hdiff := WithTop.le_of_add_le_add_right (ht.subset hst).encard_lt_top.ne hts
[GOAL]
α : Type u_1
s t : Set α
ht : Set.Finite t
hst : s ⊆ t
hts : encard (t \ s) + encard s ≤ 0 + encard s
hdiff : encard (t \ s) ≤ 0
⊢ s = t
[PROOFSTEP]
rw [nonpos_iff_eq_zero, encard_eq_zero, diff_eq_empty] at hdiff 
[GOAL]
α : Type u_1
s t : Set α
ht : Set.Finite t
hst : s ⊆ t
hts : encard (t \ s) + encard s ≤ 0 + encard s
hdiff : t ⊆ s
⊢ s = t
[PROOFSTEP]
exact hst.antisymm hdiff
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
⊢ encard (s \ t) + encard t = encard (s ∪ t)
[PROOFSTEP]
rw [← encard_union_eq disjoint_sdiff_left, diff_union_self]
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
⊢ encard s - encard t ≤ encard (s \ t)
[PROOFSTEP]
rw [tsub_le_iff_left, add_comm]
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
⊢ encard s ≤ encard (s \ t) + encard t
[PROOFSTEP]
apply encard_le_encard_diff_add_encard
[GOAL]
α : Type u_1
s✝ t s : Set α
⊢ encard s + encard sᶜ = encard univ
[PROOFSTEP]
rw [← encard_union_eq disjoint_compl_right, union_compl_self]
[GOAL]
α : Type u_1
s✝ t s : Set α
x : α
⊢ encard (insert x s) ≤ encard s + 1
[PROOFSTEP]
rw [← union_singleton, ← encard_singleton x]
[GOAL]
α : Type u_1
s✝ t s : Set α
x : α
⊢ encard (s ∪ {x}) ≤ encard s + encard {x}
[PROOFSTEP]
apply encard_union_le
[GOAL]
α : Type u_1
s✝ t s : Set α
x : α
⊢ encard ({x} ∩ s) ≤ 1
[PROOFSTEP]
rw [← encard_singleton x]
[GOAL]
α : Type u_1
s✝ t s : Set α
x : α
⊢ encard ({x} ∩ s) ≤ encard {x}
[PROOFSTEP]
exact encard_le_of_subset (inter_subset_left _ _)
[GOAL]
α : Type u_1
s t : Set α
a : α
h : a ∈ s
⊢ encard (s \ {a}) + 1 = encard s
[PROOFSTEP]
rw [← encard_insert_of_not_mem (fun h ↦ h.2 rfl), insert_diff_singleton, insert_eq_of_mem h]
[GOAL]
α : Type u_1
s t : Set α
a : α
h : a ∈ s
⊢ encard (s \ {a}) = encard s - 1
[PROOFSTEP]
rw [← encard_diff_singleton_add_one h, ← WithTop.add_right_cancel_iff WithTop.one_ne_top,
  tsub_add_cancel_of_le (self_le_add_left _ _)]
[GOAL]
α : Type u_1
s✝ t s : Set α
x : α
⊢ encard s - 1 ≤ encard (s \ {x})
[PROOFSTEP]
rw [← encard_singleton x]
[GOAL]
α : Type u_1
s✝ t s : Set α
x : α
⊢ encard s - encard {x} ≤ encard (s \ {x})
[PROOFSTEP]
apply tsub_encard_le_encard_diff
[GOAL]
α : Type u_1
s t : Set α
a b : α
ha : ¬a ∈ s
hb : b ∈ s
⊢ encard (insert a (s \ {b})) = encard s
[PROOFSTEP]
rw [encard_insert_of_not_mem, encard_diff_singleton_add_one hb]
[GOAL]
α : Type u_1
s t : Set α
a b : α
ha : ¬a ∈ s
hb : b ∈ s
⊢ ¬a ∈ s \ {b}
[PROOFSTEP]
simp_all only [not_true, mem_diff, mem_singleton_iff, false_and, not_false_eq_true]
[GOAL]
α : Type u_1
s t : Set α
a b : α
ha : ¬a ∈ s
hb : b ∈ s
⊢ encard (insert a s \ {b}) = encard s
[PROOFSTEP]
rw [← insert_diff_singleton_comm (by rintro rfl; exact ha hb), encard_exchange ha hb]
[GOAL]
α : Type u_1
s t : Set α
a b : α
ha : ¬a ∈ s
hb : b ∈ s
⊢ a ≠ b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
s t : Set α
a : α
ha : ¬a ∈ s
hb : a ∈ s
⊢ False
[PROOFSTEP]
exact ha hb
[GOAL]
α : Type u_1
s t : Set α
k : ℕ∞
⊢ encard s = k + 1 ↔ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ encard t = k
[PROOFSTEP]
refine' ⟨fun h ↦ _, _⟩
[GOAL]
case refine'_1
α : Type u_1
s t : Set α
k : ℕ∞
h : encard s = k + 1
⊢ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ encard t = k
[PROOFSTEP]
obtain ⟨a, ha⟩ := nonempty_of_encard_ne_zero (s := s) (by simp [h])
[GOAL]
α : Type u_1
s t : Set α
k : ℕ∞
h : encard s = k + 1
⊢ encard s ≠ 0
[PROOFSTEP]
simp [h]
[GOAL]
case refine'_1.intro
α : Type u_1
s t : Set α
k : ℕ∞
h : encard s = k + 1
a : α
ha : a ∈ s
⊢ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ encard t = k
[PROOFSTEP]
refine' ⟨a, s \ { a }, fun h ↦ h.2 rfl, by rwa [insert_diff_singleton, insert_eq_of_mem], _⟩
[GOAL]
α : Type u_1
s t : Set α
k : ℕ∞
h : encard s = k + 1
a : α
ha : a ∈ s
⊢ insert a (s \ {a}) = s
[PROOFSTEP]
rwa [insert_diff_singleton, insert_eq_of_mem]
[GOAL]
case refine'_1.intro
α : Type u_1
s t : Set α
k : ℕ∞
h : encard s = k + 1
a : α
ha : a ∈ s
⊢ encard (s \ {a}) = k
[PROOFSTEP]
rw [← WithTop.add_right_cancel_iff WithTop.one_ne_top, ← h, encard_diff_singleton_add_one ha]
[GOAL]
case refine'_2
α : Type u_1
s t : Set α
k : ℕ∞
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ encard t = k) → encard s = k + 1
[PROOFSTEP]
rintro ⟨a, t, h, rfl, rfl⟩
[GOAL]
case refine'_2.intro.intro.intro.intro
α : Type u_1
t✝ : Set α
a : α
t : Set α
h : ¬a ∈ t
⊢ encard (insert a t) = encard t + 1
[PROOFSTEP]
rw [encard_insert_of_not_mem h]
[GOAL]
α : Type u_1
s✝ t s : Set α
⊢ s = ∅ ∨ encard s = ⊤ ∨ ∃ a, a ∈ s ∧ encard (s \ {a}) < encard s
[PROOFSTEP]
refine'
  s.eq_empty_or_nonempty.elim Or.inl
    (Or.inr ∘ fun ⟨a, ha⟩ ↦ (s.finite_or_infinite.elim (fun hfin ↦ Or.inr ⟨a, ha, _⟩) (Or.inl ∘ Infinite.encard_eq)))
[GOAL]
α : Type u_1
s✝ t s : Set α
x✝ : Set.Nonempty s
a : α
ha : a ∈ s
hfin : Set.Finite s
⊢ encard (s \ {a}) < encard s
[PROOFSTEP]
rw [← encard_diff_singleton_add_one ha]
[GOAL]
α : Type u_1
s✝ t s : Set α
x✝ : Set.Nonempty s
a : α
ha : a ∈ s
hfin : Set.Finite s
⊢ encard (s \ {a}) < encard (s \ {a}) + 1
[PROOFSTEP]
nth_rw 1 [← add_zero (encard _)]
[GOAL]
α : Type u_1
s✝ t s : Set α
x✝ : Set.Nonempty s
a : α
ha : a ∈ s
hfin : Set.Finite s
⊢ encard (s \ {a}) + 0 < encard (s \ {a}) + 1
[PROOFSTEP]
exact WithTop.add_lt_add_left (hfin.diff _).encard_lt_top.ne zero_lt_one
[GOAL]
α : Type u_1
s t : Set α
x y : α
hne : x ≠ y
⊢ encard {x, y} = 2
[PROOFSTEP]
rw [encard_insert_of_not_mem (by simpa), ← one_add_one_eq_two, WithTop.add_right_cancel_iff WithTop.one_ne_top,
  encard_singleton]
[GOAL]
α : Type u_1
s t : Set α
x y : α
hne : x ≠ y
⊢ ¬x ∈ {y}
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
s t : Set α
⊢ encard s = 1 ↔ ∃ x, s = {x}
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun ⟨x, hx⟩ ↦ by rw [hx, encard_singleton]⟩
[GOAL]
α : Type u_1
s t : Set α
x✝ : ∃ x, s = {x}
x : α
hx : s = {x}
⊢ encard s = 1
[PROOFSTEP]
rw [hx, encard_singleton]
[GOAL]
α : Type u_1
s t : Set α
h : encard s = 1
⊢ ∃ x, s = {x}
[PROOFSTEP]
obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
[GOAL]
α : Type u_1
s t : Set α
h : encard s = 1
⊢ encard s ≠ 0
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
s t : Set α
h : encard s = 1
⊢ 1 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case intro
α : Type u_1
s t : Set α
h : encard s = 1
x : α
hx : x ∈ s
⊢ ∃ x, s = {x}
[PROOFSTEP]
exact ⟨x, ((finite_singleton x).eq_of_subset_of_encard_le' (by simpa) (by simp [h])).symm⟩
[GOAL]
α : Type u_1
s t : Set α
h : encard s = 1
x : α
hx : x ∈ s
⊢ {x} ⊆ s
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
s t : Set α
h : encard s = 1
x : α
hx : x ∈ s
⊢ encard s ≤ encard {x}
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
s t : Set α
⊢ encard s ≤ 1 ↔ s = ∅ ∨ ∃ x, s = {x}
[PROOFSTEP]
rw [le_iff_lt_or_eq, lt_iff_not_le, ENat.one_le_iff_ne_zero, not_not, encard_eq_zero, encard_eq_one]
[GOAL]
α : Type u_1
s t : Set α
⊢ encard s ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
[PROOFSTEP]
rw [encard_le_one_iff_eq, or_iff_not_imp_left, ← Ne.def, ← nonempty_iff_ne_empty]
[GOAL]
α : Type u_1
s t : Set α
⊢ (Set.Nonempty s → ∃ x, s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
[PROOFSTEP]
refine' ⟨fun h a b has hbs ↦ _, fun h ⟨x, hx⟩ ↦ ⟨x, ((singleton_subset_iff.2 hx).antisymm' (fun y hy ↦ h _ _ hy hx))⟩⟩
[GOAL]
α : Type u_1
s t : Set α
h : Set.Nonempty s → ∃ x, s = {x}
a b : α
has : a ∈ s
hbs : b ∈ s
⊢ a = b
[PROOFSTEP]
obtain ⟨x, rfl⟩ := h ⟨_, has⟩
[GOAL]
case intro
α : Type u_1
t : Set α
a b x : α
h : Set.Nonempty {x} → ∃ x_1, {x} = {x_1}
has : a ∈ {x}
hbs : b ∈ {x}
⊢ a = b
[PROOFSTEP]
rw [(has : a = x), (hbs : b = x)]
[GOAL]
α : Type u_1
s t : Set α
⊢ 1 < encard s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
[PROOFSTEP]
rw [← not_iff_not, not_exists, not_lt, encard_le_one_iff]
[GOAL]
α : Type u_1
s t : Set α
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ (x : α), ¬∃ b, x ∈ s ∧ b ∈ s ∧ x ≠ b
[PROOFSTEP]
aesop
[GOAL]
α : Type u_1
s t : Set α
h : 1 < encard s
a : α
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
by_contra' h'
[GOAL]
α : Type u_1
s t : Set α
h : 1 < encard s
a : α
h' : ∀ (b : α), b ∈ s → b = a
⊢ False
[PROOFSTEP]
obtain ⟨b, b', hb, hb', hne⟩ := one_lt_encard_iff.1 h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
s t : Set α
h : 1 < encard s
a : α
h' : ∀ (b : α), b ∈ s → b = a
b b' : α
hb : b ∈ s
hb' : b' ∈ s
hne : b ≠ b'
⊢ False
[PROOFSTEP]
apply hne
[GOAL]
case intro.intro.intro.intro
α : Type u_1
s t : Set α
h : 1 < encard s
a : α
h' : ∀ (b : α), b ∈ s → b = a
b b' : α
hb : b ∈ s
hb' : b' ∈ s
hne : b ≠ b'
⊢ b = b'
[PROOFSTEP]
rw [h' b hb, h' b' hb']
[GOAL]
α : Type u_1
s t : Set α
⊢ encard s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun ⟨x, y, hne, hs⟩ ↦ by rw [hs, encard_pair hne]⟩
[GOAL]
α : Type u_1
s t : Set α
x✝ : ∃ x y, x ≠ y ∧ s = {x, y}
x y : α
hne : x ≠ y
hs : s = {x, y}
⊢ encard s = 2
[PROOFSTEP]
rw [hs, encard_pair hne]
[GOAL]
α : Type u_1
s t : Set α
h : encard s = 2
⊢ ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
[GOAL]
α : Type u_1
s t : Set α
h : encard s = 2
⊢ encard s ≠ 0
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
s t : Set α
h : encard s = 2
⊢ 2 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case intro
α : Type u_1
s t : Set α
h : encard s = 2
x : α
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
rw [← insert_eq_of_mem hx, ← insert_diff_singleton, encard_insert_of_not_mem (fun h ↦ h.2 rfl), ← one_add_one_eq_two,
  WithTop.add_right_cancel_iff (WithTop.one_ne_top), encard_eq_one] at h 
[GOAL]
case intro
α : Type u_1
s t : Set α
x : α
h : ∃ x_1, s \ {x} = {x_1}
hx : x ∈ s
⊢ ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
obtain ⟨y, h⟩ := h
[GOAL]
case intro.intro
α : Type u_1
s t : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
refine' ⟨x, y, by rintro rfl; exact (h.symm.subset rfl).2 rfl, _⟩
[GOAL]
α : Type u_1
s t : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ x ≠ y
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
s t : Set α
x : α
hx : x ∈ s
h : s \ {x} = {x}
⊢ False
[PROOFSTEP]
exact (h.symm.subset rfl).2 rfl
[GOAL]
case intro.intro
α : Type u_1
s t : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ s = {x, y}
[PROOFSTEP]
rw [← h, insert_diff_singleton, insert_eq_of_mem hx]
[GOAL]
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
⊢ encard s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun ⟨x, y, z, hxy, hyz, hxz, hs⟩ ↦ _⟩
[GOAL]
case refine'_1
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
h : encard s = 3
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
[GOAL]
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
h : encard s = 3
⊢ encard s ≠ 0
[PROOFSTEP]
rw [h]
[GOAL]
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
h : encard s = 3
⊢ 3 ≠ 0
[PROOFSTEP]
simp
[GOAL]
case refine'_1.intro
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
h : encard s = 3
x : α
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
rw [← insert_eq_of_mem hx, ← insert_diff_singleton, encard_insert_of_not_mem (fun h ↦ h.2 rfl),
  (by exact rfl : (3 : ℕ∞) = 2 + 1), WithTop.add_right_cancel_iff WithTop.one_ne_top, encard_eq_two] at h 
[GOAL]
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x : α
h : encard (s \ {x}) + 1 = 3
hx : x ∈ s
⊢ 3 = 2 + 1
[PROOFSTEP]
exact rfl
[GOAL]
case refine'_1.intro
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x : α
h : ∃ x_1 y, x_1 ≠ y ∧ s \ {x} = {x_1, y}
hx : x ∈ s
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
obtain ⟨y, z, hne, hs⟩ := h
[GOAL]
case refine'_1.intro.intro.intro.intro
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
refine' ⟨x, y, z, _, _, hne, _⟩
[GOAL]
case refine'_1.intro.intro.intro.intro.refine'_1
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ y
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1.intro.intro.intro.intro.refine'_1
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x : α
hx : x ∈ s
z : α
hne : x ≠ z
hs : s \ {x} = {x, z}
⊢ False
[PROOFSTEP]
exact (hs.symm.subset (Or.inl rfl)).2 rfl
[GOAL]
case refine'_1.intro.intro.intro.intro.refine'_2
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ x ≠ z
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1.intro.intro.intro.intro.refine'_2
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hne : y ≠ x
hs : s \ {x} = {y, x}
⊢ False
[PROOFSTEP]
exact (hs.symm.subset (Or.inr rfl)).2 rfl
[GOAL]
case refine'_1.intro.intro.intro.intro.refine'_3
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = {x, y, z}
[PROOFSTEP]
rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]
[GOAL]
case refine'_2
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ encard s = 3
[PROOFSTEP]
rw [hs, encard_insert_of_not_mem, encard_insert_of_not_mem, encard_singleton]
[GOAL]
case refine'_2
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ 1 + 1 + 1 = 3
[PROOFSTEP]
aesop
[GOAL]
case refine'_2
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ ¬y ∈ {z}
[PROOFSTEP]
aesop
[GOAL]
case refine'_2
α✝ : Type ?u.68373
s✝ t : Set α✝
α : Type u_1
s : Set α
x✝ : ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ ¬x ∈ {y, z}
[PROOFSTEP]
aesop
[GOAL]
α : Type ?u.102702
s t : Set α
k : ℕ
⊢ encard {i | i < k} = ↑k
[PROOFSTEP]
convert encard_coe_eq_coe_finsetCard (Finset.range k) using 1
[GOAL]
case h.e'_2
α : Type ?u.102702
s t : Set α
k : ℕ
⊢ encard {i | i < k} = encard ↑(Finset.range k)
[PROOFSTEP]
rw [Finset.coe_range, Iio_def]
[GOAL]
case h.e'_3
α : Type ?u.102702
s t : Set α
k : ℕ
⊢ ↑k = ↑(Finset.card (Finset.range k))
[PROOFSTEP]
rw [Finset.card_range]
[GOAL]
α : Type u_1
s t : Set α
hs : Set.Finite s
h : s ⊆ t
hst : encard t = encard s + 1
⊢ ∃ a, t = insert a s
[PROOFSTEP]
rw [← encard_diff_add_encard_of_subset h, add_comm, WithTop.add_left_cancel_iff hs.encard_lt_top.ne, encard_eq_one] at
  hst 
[GOAL]
α : Type u_1
s t : Set α
hs : Set.Finite s
h : s ⊆ t
hst : ∃ x, t \ s = {x}
⊢ ∃ a, t = insert a s
[PROOFSTEP]
obtain ⟨x, hx⟩ := hst
[GOAL]
case intro
α : Type u_1
s t : Set α
hs : Set.Finite s
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ ∃ a, t = insert a s
[PROOFSTEP]
use x
[GOAL]
case h
α : Type u_1
s t : Set α
hs : Set.Finite s
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ t = insert x s
[PROOFSTEP]
rw [← diff_union_of_subset h, hx, singleton_union]
[GOAL]
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
hk : k ≤ encard s
⊢ ∃ t, t ⊆ s ∧ encard t = k
[PROOFSTEP]
revert hk
[GOAL]
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
⊢ k ≤ encard s → ∃ t, t ⊆ s ∧ encard t = k
[PROOFSTEP]
refine' ENat.nat_induction k (fun _ ↦ ⟨∅, empty_subset _, by simp⟩) (fun n IH hle ↦ _) _
[GOAL]
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
x✝ : 0 ≤ encard s
⊢ encard ∅ = 0
[PROOFSTEP]
simp
[GOAL]
case refine'_1
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
n : ℕ
IH : ↑n ≤ encard s → ∃ t, t ⊆ s ∧ encard t = ↑n
hle : ↑(Nat.succ n) ≤ encard s
⊢ ∃ t, t ⊆ s ∧ encard t = ↑(Nat.succ n)
[PROOFSTEP]
obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hle)
[GOAL]
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
n : ℕ
IH : ↑n ≤ encard s → ∃ t, t ⊆ s ∧ encard t = ↑n
hle : ↑(Nat.succ n) ≤ encard s
⊢ ↑n ≤ ↑(Nat.succ n)
[PROOFSTEP]
simp
[GOAL]
case refine'_1.intro.intro
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
n : ℕ
IH : ↑n ≤ encard s → ∃ t, t ⊆ s ∧ encard t = ↑n
hle : ↑(Nat.succ n) ≤ encard s
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : encard t₀ = ↑n
⊢ ∃ t, t ⊆ s ∧ encard t = ↑(Nat.succ n)
[PROOFSTEP]
simp only [Nat.cast_succ] at *
[GOAL]
case refine'_1.intro.intro
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
n : ℕ
IH : ↑n ≤ encard s → ∃ t, t ⊆ s ∧ encard t = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : encard t₀ = ↑n
hle : ↑n + 1 ≤ encard s
⊢ ∃ t, t ⊆ s ∧ encard t = ↑n + 1
[PROOFSTEP]
have hne : t₀ ≠ s
[GOAL]
case hne
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
n : ℕ
IH : ↑n ≤ encard s → ∃ t, t ⊆ s ∧ encard t = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : encard t₀ = ↑n
hle : ↑n + 1 ≤ encard s
⊢ t₀ ≠ s
[PROOFSTEP]
rintro rfl
[GOAL]
case hne
α : Type u_1
t : Set α
n : ℕ
t₀ : Set α
ht₀ : encard t₀ = ↑n
k : ℕ∞
IH : ↑n ≤ encard t₀ → ∃ t, t ⊆ t₀ ∧ encard t = ↑n
ht₀s : t₀ ⊆ t₀
hle : ↑n + 1 ≤ encard t₀
⊢ False
[PROOFSTEP]
rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hle 
[GOAL]
case hne
α : Type u_1
t : Set α
n : ℕ
t₀ : Set α
ht₀ : encard t₀ = ↑n
k : ℕ∞
IH : ↑n ≤ encard t₀ → ∃ t, t ⊆ t₀ ∧ encard t = ↑n
ht₀s : t₀ ⊆ t₀
hle : n + 1 ≤ n
⊢ False
[PROOFSTEP]
simp at hle 
[GOAL]
case refine'_1.intro.intro
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
n : ℕ
IH : ↑n ≤ encard s → ∃ t, t ⊆ s ∧ encard t = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : encard t₀ = ↑n
hle : ↑n + 1 ≤ encard s
hne : t₀ ≠ s
⊢ ∃ t, t ⊆ s ∧ encard t = ↑n + 1
[PROOFSTEP]
obtain ⟨x, hx⟩ := exists_of_ssubset (ht₀s.ssubset_of_ne hne)
[GOAL]
case refine'_1.intro.intro.intro
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
n : ℕ
IH : ↑n ≤ encard s → ∃ t, t ⊆ s ∧ encard t = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : encard t₀ = ↑n
hle : ↑n + 1 ≤ encard s
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ ¬x ∈ t₀
⊢ ∃ t, t ⊆ s ∧ encard t = ↑n + 1
[PROOFSTEP]
exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_not_mem hx.2, ht₀]⟩
[GOAL]
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
n : ℕ
IH : ↑n ≤ encard s → ∃ t, t ⊆ s ∧ encard t = ↑n
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : encard t₀ = ↑n
hle : ↑n + 1 ≤ encard s
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ ¬x ∈ t₀
⊢ encard (insert x t₀) = ↑n + 1
[PROOFSTEP]
rw [encard_insert_of_not_mem hx.2, ht₀]
[GOAL]
case refine'_2
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
⊢ (∀ (n : ℕ), ↑n ≤ encard s → ∃ t, t ⊆ s ∧ encard t = ↑n) → ⊤ ≤ encard s → ∃ t, t ⊆ s ∧ encard t = ⊤
[PROOFSTEP]
simp only [top_le_iff, encard_eq_top_iff]
[GOAL]
case refine'_2
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
⊢ (∀ (n : ℕ), ↑n ≤ encard s → ∃ t, t ⊆ s ∧ encard t = ↑n) → Set.Infinite s → ∃ t, t ⊆ s ∧ Set.Infinite t
[PROOFSTEP]
exact fun _ hi ↦ ⟨s, Subset.rfl, hi⟩
[GOAL]
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
hst : s ⊆ t
hsk : encard s ≤ k
hkt : k ≤ encard t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ encard r = k
[PROOFSTEP]
obtain (hs | hs) := eq_or_ne s.encard ⊤
[GOAL]
case inl
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
hst : s ⊆ t
hsk : encard s ≤ k
hkt : k ≤ encard t
hs : encard s = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ encard r = k
[PROOFSTEP]
rw [hs, top_le_iff] at hsk 
[GOAL]
case inl
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
hst : s ⊆ t
hsk : k = ⊤
hkt : k ≤ encard t
hs : encard s = ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ encard r = k
[PROOFSTEP]
subst hsk
[GOAL]
case inl
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : encard s = ⊤
hkt : ⊤ ≤ encard t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ encard r = ⊤
[PROOFSTEP]
exact ⟨s, Subset.rfl, hst, hs⟩
[GOAL]
case inr
α : Type u_1
s t : Set α
k : (fun x => ℕ∞) (PartENat.card ↑s)
hst : s ⊆ t
hsk : encard s ≤ k
hkt : k ≤ encard t
hs : encard s ≠ ⊤
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ encard r = k
[PROOFSTEP]
obtain ⟨k, rfl⟩ := exists_add_of_le hsk
[GOAL]
case inr.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : encard s ≠ ⊤
k : ℕ∞
hsk : encard s ≤ encard s + k
hkt : encard s + k ≤ encard t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ encard r = encard s + k
[PROOFSTEP]
obtain ⟨k', hk'⟩ := exists_add_of_le hkt
[GOAL]
case inr.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : encard s ≠ ⊤
k : ℕ∞
hsk : encard s ≤ encard s + k
hkt : encard s + k ≤ encard t
k' : ℕ∞
hk' : encard t = encard s + k + k'
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ encard r = encard s + k
[PROOFSTEP]
have hk : k ≤ encard (t \ s)
[GOAL]
case hk
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : encard s ≠ ⊤
k : ℕ∞
hsk : encard s ≤ encard s + k
hkt : encard s + k ≤ encard t
k' : ℕ∞
hk' : encard t = encard s + k + k'
⊢ k ≤ encard (t \ s)
[PROOFSTEP]
rw [← encard_diff_add_encard_of_subset hst, add_comm] at hkt 
[GOAL]
case hk
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : encard s ≠ ⊤
k : ℕ∞
hsk : encard s ≤ encard s + k
hkt : k + encard s ≤ encard (t \ s) + encard s
k' : ℕ∞
hk' : encard t = encard s + k + k'
⊢ k ≤ encard (t \ s)
[PROOFSTEP]
exact WithTop.le_of_add_le_add_right hs hkt
[GOAL]
case inr.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : encard s ≠ ⊤
k : ℕ∞
hsk : encard s ≤ encard s + k
hkt : encard s + k ≤ encard t
k' : ℕ∞
hk' : encard t = encard s + k + k'
hk : k ≤ encard (t \ s)
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ encard r = encard s + k
[PROOFSTEP]
obtain ⟨r', hr', rfl⟩ := exists_subset_encard_eq hk
[GOAL]
case inr.intro.intro.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : encard s ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : encard s ≤ encard s + encard r'
hkt : encard s + encard r' ≤ encard t
hk' : encard t = encard s + encard r' + k'
hk : encard r' ≤ encard (t \ s)
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ encard r = encard s + encard r'
[PROOFSTEP]
refine' ⟨s ∪ r', subset_union_left _ _, union_subset hst (hr'.trans (diff_subset _ _)), _⟩
[GOAL]
case inr.intro.intro.intro.intro
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : encard s ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : encard s ≤ encard s + encard r'
hkt : encard s + encard r' ≤ encard t
hk' : encard t = encard s + encard r' + k'
hk : encard r' ≤ encard (t \ s)
⊢ encard (s ∪ r') = encard s + encard r'
[PROOFSTEP]
rw [encard_union_eq (disjoint_of_subset_right hr' disjoint_sdiff_right)]
[GOAL]
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f : α → β
h : InjOn f s
⊢ encard (f '' s) = encard s
[PROOFSTEP]
rw [encard, PartENat.card_image_of_injOn h, encard]
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ s : Set α
t : Set β
f : α → β
e : ↑s ≃ ↑t
⊢ encard s = encard t
[PROOFSTEP]
rw [← encard_univ_coe, ← encard_univ_coe t, encard_univ, encard_univ, PartENat.card_congr e]
[GOAL]
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f : α → β
e : ↑s ↪ ↑t
⊢ encard s ≤ encard t
[PROOFSTEP]
rw [← encard_univ_coe, ← e.injective.encard_image, ← Subtype.coe_injective.encard_image]
[GOAL]
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f : α → β
e : ↑s ↪ ↑t
⊢ encard ((fun a => ↑a) '' (↑e '' univ)) ≤ encard t
[PROOFSTEP]
exact encard_mono (by simp)
[GOAL]
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f : α → β
e : ↑s ↪ ↑t
⊢ (fun a => ↑a) '' (↑e '' univ) ≤ t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
s✝¹ t✝ s✝ : Set α
t : Set β
f✝ f : α → β
s : Set α
⊢ encard (f '' s) ≤ encard s
[PROOFSTEP]
obtain (h | h) := isEmpty_or_nonempty α
[GOAL]
case inl
α : Type u_1
β : Type u_2
s✝¹ t✝ s✝ : Set α
t : Set β
f✝ f : α → β
s : Set α
h : IsEmpty α
⊢ encard (f '' s) ≤ encard s
[PROOFSTEP]
rw [s.eq_empty_of_isEmpty]
[GOAL]
case inl
α : Type u_1
β : Type u_2
s✝¹ t✝ s✝ : Set α
t : Set β
f✝ f : α → β
s : Set α
h : IsEmpty α
⊢ encard (f '' ∅) ≤ encard ∅
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
s✝¹ t✝ s✝ : Set α
t : Set β
f✝ f : α → β
s : Set α
h : Nonempty α
⊢ encard (f '' s) ≤ encard s
[PROOFSTEP]
rw [← (f.invFunOn_injOn_image s).encard_image]
[GOAL]
case inr
α : Type u_1
β : Type u_2
s✝¹ t✝ s✝ : Set α
t : Set β
f✝ f : α → β
s : Set α
h : Nonempty α
⊢ encard (Function.invFunOn f s '' (f '' s)) ≤ encard s
[PROOFSTEP]
apply encard_le_of_subset
[GOAL]
case inr.h
α : Type u_1
β : Type u_2
s✝¹ t✝ s✝ : Set α
t : Set β
f✝ f : α → β
s : Set α
h : Nonempty α
⊢ Function.invFunOn f s '' (f '' s) ⊆ s
[PROOFSTEP]
exact f.invFunOn_image_image_subset s
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ s : Set α
t : Set β
f : α → β
hs : Set.Finite s
h : encard (f '' s) = encard s
⊢ InjOn f s
[PROOFSTEP]
obtain (h' | hne) := isEmpty_or_nonempty α
[GOAL]
case inl
α : Type u_1
β : Type u_2
s✝ t✝ s : Set α
t : Set β
f : α → β
hs : Set.Finite s
h : encard (f '' s) = encard s
h' : IsEmpty α
⊢ InjOn f s
[PROOFSTEP]
rw [s.eq_empty_of_isEmpty]
[GOAL]
case inl
α : Type u_1
β : Type u_2
s✝ t✝ s : Set α
t : Set β
f : α → β
hs : Set.Finite s
h : encard (f '' s) = encard s
h' : IsEmpty α
⊢ InjOn f ∅
[PROOFSTEP]
simp
[GOAL]
case inr
α : Type u_1
β : Type u_2
s✝ t✝ s : Set α
t : Set β
f : α → β
hs : Set.Finite s
h : encard (f '' s) = encard s
hne : Nonempty α
⊢ InjOn f s
[PROOFSTEP]
rw [← (f.invFunOn_injOn_image s).encard_image] at h 
[GOAL]
case inr
α : Type u_1
β : Type u_2
s✝ t✝ s : Set α
t : Set β
f : α → β
hs : Set.Finite s
hne : Nonempty α
h : encard (Function.invFunOn f s '' (f '' s)) = encard s
⊢ InjOn f s
[PROOFSTEP]
rw [injOn_iff_invFunOn_image_image_eq_self]
[GOAL]
case inr
α : Type u_1
β : Type u_2
s✝ t✝ s : Set α
t : Set β
f : α → β
hs : Set.Finite s
hne : Nonempty α
h : encard (Function.invFunOn f s '' (f '' s)) = encard s
⊢ Function.invFunOn f s '' (f '' s) = s
[PROOFSTEP]
exact hs.eq_of_subset_of_encard_le (f.invFunOn_image_image_subset s) h.symm.le
[GOAL]
α : Type u_1
β : Type u_2
s✝ t✝ s : Set α
t : Set β
f : α → β
hf : Function.Injective f
ht : t ⊆ range f
⊢ encard (f ⁻¹' t) = encard t
[PROOFSTEP]
rw [← hf.encard_image, image_preimage_eq_inter_range, inter_eq_self_of_subset_left ht]
[GOAL]
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ encard s ≤ encard t
[PROOFSTEP]
rw [← f_inj.encard_image]
[GOAL]
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ encard (f '' s) ≤ encard t
[PROOFSTEP]
apply encard_le_of_subset
[GOAL]
case h
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
⊢ f '' s ⊆ t
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case h.intro.intro
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
x : α
hx : x ∈ s
⊢ f x ∈ t
[PROOFSTEP]
exact hf hx
[GOAL]
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
[PROOFSTEP]
classical
obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
· simp
· exact (encard_ne_top_iff.mpr hs h).elim
obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
have hle' : (s \ { a }).encard ≤ (t \ { b }).encard
·
  rwa [← WithTop.add_le_add_iff_right WithTop.one_ne_top, encard_diff_singleton_add_one has,
    encard_diff_singleton_add_one hbt]
obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le (hs.diff { a }) hle'
simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s 
use Function.update f₀ a b
rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
simp only [mem_diff, mem_singleton_iff, not_true, and_false, insert_diff_singleton, subset_def, mem_insert_iff,
  mem_preimage, ne_eq, Function.update_apply, forall_eq_or_imp, ite_true, and_imp, mem_image, ite_eq_left_iff,
  not_exists, not_and, not_forall, exists_prop, and_iff_right hbt]
refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
· rintro x hx; split_ifs with h; assumption; exact (hf₀s x hx h).1
exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_noteq])
[GOAL]
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
[PROOFSTEP]
obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
[GOAL]
case inl
α : Type u_2
β : Type u_1
s✝ t✝¹ s : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
t : Set β
hs : Set.Finite ∅
hle : encard ∅ ≤ encard t
⊢ ∃ f, ∅ ⊆ f ⁻¹' t ∧ InjOn f ∅
[PROOFSTEP]
simp
[GOAL]
case inr.inl
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
h : encard s = ⊤
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
[PROOFSTEP]
exact (encard_ne_top_iff.mpr hs h).elim
[GOAL]
case inr.inr.intro.intro
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
[PROOFSTEP]
obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
[GOAL]
case inr.inr.intro.intro.intro
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
[PROOFSTEP]
have hle' : (s \ { a }).encard ≤ (t \ { b }).encard
[GOAL]
case hle'
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
⊢ encard (s \ {a}) ≤ encard (t \ {b})
[PROOFSTEP]
rwa [← WithTop.add_le_add_iff_right WithTop.one_ne_top, encard_diff_singleton_add_one has,
  encard_diff_singleton_add_one hbt]
[GOAL]
case inr.inr.intro.intro.intro
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
[PROOFSTEP]
obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le (hs.diff { a }) hle'
[GOAL]
case inr.inr.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hf₀s : s \ {a} ⊆ f₀ ⁻¹' (t \ {b})
hinj : InjOn f₀ (s \ {a})
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
[PROOFSTEP]
simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s 
[GOAL]
case inr.inr.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ (x : α), x ∈ s → ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ ∃ f, s ⊆ f ⁻¹' t ∧ InjOn f s
[PROOFSTEP]
use Function.update f₀ a b
[GOAL]
case h
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ (x : α), x ∈ s → ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ s ⊆ Function.update f₀ a b ⁻¹' t ∧ InjOn (Function.update f₀ a b) s
[PROOFSTEP]
rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
[GOAL]
case h
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ (x : α), x ∈ s → ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ insert a (s \ {a}) ⊆ Function.update f₀ a b ⁻¹' t ∧
    InjOn (Function.update f₀ a b) (s \ {a}) ∧ ¬Function.update f₀ a b a ∈ Function.update f₀ a b '' (s \ {a})
[PROOFSTEP]
simp only [mem_diff, mem_singleton_iff, not_true, and_false, insert_diff_singleton, subset_def, mem_insert_iff,
  mem_preimage, ne_eq, Function.update_apply, forall_eq_or_imp, ite_true, and_imp, mem_image, ite_eq_left_iff,
  not_exists, not_and, not_forall, exists_prop, and_iff_right hbt]
[GOAL]
case h
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ (x : α), x ∈ s → ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ (∀ (a_1 : α), a_1 ∈ s → (if a_1 = a then b else f₀ a_1) ∈ t) ∧
    InjOn (Function.update f₀ a b) (s \ {a}) ∧ ∀ (x : α), x ∈ s → ¬x = a → ¬x = a ∧ ¬f₀ x = b
[PROOFSTEP]
refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
[GOAL]
case h.refine_1
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ (x : α), x ∈ s → ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ ∀ (a_1 : α), a_1 ∈ s → (if a_1 = a then b else f₀ a_1) ∈ t
[PROOFSTEP]
rintro x hx
[GOAL]
case h.refine_1
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ (x : α), x ∈ s → ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
⊢ (if x = a then b else f₀ x) ∈ t
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ (x : α), x ∈ s → ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
h : x = a
⊢ b ∈ t
case neg
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ (x : α), x ∈ s → ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
h : ¬x = a
⊢ f₀ x ∈ t
[PROOFSTEP]
assumption
[GOAL]
case neg
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ (x : α), x ∈ s → ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
h : ¬x = a
⊢ f₀ x ∈ t
[PROOFSTEP]
exact (hf₀s x hx h).1
[GOAL]
case h.refine_2
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ (x : α), x ∈ s → ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ InjOn (Function.update f₀ a b) (s \ {a})
[PROOFSTEP]
exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_noteq])
[GOAL]
α : Type u_2
β : Type u_1
s✝¹ t✝¹ s✝ : Set α
t✝ : Set β
f : α → β
inst✝ : Nonempty β
s : Set α
t : Set β
hs : Set.Finite s
hle : encard s ≤ encard t
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : encard (s \ {a}) ≤ encard (t \ {b})
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ (x : α), x ∈ s → ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
x✝ : x ∈ s \ {a}
left✝ : x ∈ s
hxa : ¬x ∈ {a}
⊢ f₀ x = Function.update f₀ a b x
[PROOFSTEP]
rwa [Function.update_noteq]
[GOAL]
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f : α → β
inst✝ : Nonempty β
hs : Set.Finite s
h : encard s = encard t
⊢ ∃ f, BijOn f s t
[PROOFSTEP]
obtain ⟨f, hf, hinj⟩ := hs.exists_injOn_of_encard_le h.le
[GOAL]
case intro.intro
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f✝ : α → β
inst✝ : Nonempty β
hs : Set.Finite s
h : encard s = encard t
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ ∃ f, BijOn f s t
[PROOFSTEP]
use f
[GOAL]
case h
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f✝ : α → β
inst✝ : Nonempty β
hs : Set.Finite s
h : encard s = encard t
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ BijOn f s t
[PROOFSTEP]
convert hinj.bijOn_image
[GOAL]
case h.e'_5
α : Type u_2
β : Type u_1
s✝ t✝ s : Set α
t : Set β
f✝ : α → β
inst✝ : Nonempty β
hs : Set.Finite s
h : encard s = encard t
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ t = f '' s
[PROOFSTEP]
rw [(hs.image f).eq_of_subset_of_encard_le' (image_subset_iff.mpr hf) (h.symm.trans hinj.encard_image.symm).le]
[GOAL]
α : Type u_1
s t : Set α
hs : Set.Finite s
⊢ ↑(ncard s) = encard s
[PROOFSTEP]
rwa [ncard, ENat.coe_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]
[GOAL]
α : Type u_1
s✝ t s : Set α
⊢ Nat.card ↑s = ncard s
[PROOFSTEP]
obtain (h | h) := s.finite_or_infinite
[GOAL]
case inl
α : Type u_1
s✝ t s : Set α
h : Set.Finite s
⊢ Nat.card ↑s = ncard s
[PROOFSTEP]
have := h.fintype
[GOAL]
case inl
α : Type u_1
s✝ t s : Set α
h : Set.Finite s
this : Fintype ↑s
⊢ Nat.card ↑s = ncard s
[PROOFSTEP]
rw [ncard, h.encard_eq_coe_toFinset_card, Nat.card_eq_fintype_card, toFinite_toFinset, toFinset_card, ENat.toNat_coe]
[GOAL]
case inr
α : Type u_1
s✝ t s : Set α
h : Set.Infinite s
⊢ Nat.card ↑s = ncard s
[PROOFSTEP]
have := infinite_coe_iff.2 h
[GOAL]
case inr
α : Type u_1
s✝ t s : Set α
h : Set.Infinite s
this : Infinite ↑s
⊢ Nat.card ↑s = ncard s
[PROOFSTEP]
rw [ncard, h.encard_eq, Nat.card_eq_zero_of_infinite, ENat.toNat_top]
[GOAL]
α : Type u_1
s✝ t s : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s = Finset.card (Finite.toFinset hs)
[PROOFSTEP]
rw [← Nat.card_coe_set_eq, @Nat.card_eq_fintype_card _ hs.fintype, @Finite.card_toFinset _ _ hs.fintype hs]
[GOAL]
α : Type u_1
s✝ t s : Set α
inst✝ : Fintype ↑s
⊢ ncard s = Finset.card (toFinset s)
[PROOFSTEP]
simp [← Nat.card_coe_set_eq, Nat.card_eq_fintype_card]
[GOAL]
α : Type u_1
s t : Set α
k : ℕ
⊢ encard s ≤ ↑k ↔ Set.Finite s ∧ ncard s ≤ k
[PROOFSTEP]
rw [encard_le_coe_iff, and_congr_right_iff]
[GOAL]
α : Type u_1
s t : Set α
k : ℕ
⊢ Set.Finite s → ((∃ n₀, encard s = ↑n₀ ∧ n₀ ≤ k) ↔ ncard s ≤ k)
[PROOFSTEP]
exact fun hfin ↦
  ⟨fun ⟨n₀, hn₀, hle⟩ ↦ by rwa [ncard_def, hn₀, ENat.toNat_coe], fun h ↦ ⟨s.ncard, by rw [hfin.cast_ncard_eq], h⟩⟩
[GOAL]
α : Type u_1
s t : Set α
k : ℕ
hfin : Set.Finite s
x✝ : ∃ n₀, encard s = ↑n₀ ∧ n₀ ≤ k
n₀ : ℕ
hn₀ : encard s = ↑n₀
hle : n₀ ≤ k
⊢ ncard s ≤ k
[PROOFSTEP]
rwa [ncard_def, hn₀, ENat.toNat_coe]
[GOAL]
α : Type u_1
s t : Set α
k : ℕ
hfin : Set.Finite s
h : ncard s ≤ k
⊢ encard s = ↑(ncard s)
[PROOFSTEP]
rw [hfin.cast_ncard_eq]
[GOAL]
α : Type u_1
s t : Set α
hs : Set.Infinite s
⊢ Set.ncard s = 0
[PROOFSTEP]
rw [← Nat.card_coe_set_eq, @Nat.card_eq_zero_of_infinite _ hs.to_subtype]
[GOAL]
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard s ≤ ncard t
[PROOFSTEP]
rw [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset hst).cast_ncard_eq]
[GOAL]
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ encard s ≤ encard t
[PROOFSTEP]
exact encard_mono hst
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s = 0 ↔ s = ∅
[PROOFSTEP]
rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, Nat.cast_zero, encard_eq_zero]
[GOAL]
α : Type u_1
s✝ t : Set α
s : Finset α
⊢ ncard ↑s = Finset.card s
[PROOFSTEP]
rw [ncard_eq_toFinset_card _, Finset.finite_toSet_toFinset]
[GOAL]
α✝ : Type ?u.175384
s t : Set α✝
α : Type u_1
⊢ ncard univ = Nat.card α
[PROOFSTEP]
cases' finite_or_infinite α with h h
[GOAL]
case inl
α✝ : Type ?u.175384
s t : Set α✝
α : Type u_1
h : Finite α
⊢ ncard univ = Nat.card α
[PROOFSTEP]
have hft := Fintype.ofFinite α
[GOAL]
case inl
α✝ : Type ?u.175384
s t : Set α✝
α : Type u_1
h : Finite α
hft : Fintype α
⊢ ncard univ = Nat.card α
[PROOFSTEP]
rw [ncard_eq_toFinset_card, Finite.toFinset_univ, Finset.card_univ, Nat.card_eq_fintype_card]
[GOAL]
case inr
α✝ : Type ?u.175384
s t : Set α✝
α : Type u_1
h : Infinite α
⊢ ncard univ = Nat.card α
[PROOFSTEP]
rw [Nat.card_eq_zero_of_infinite, Infinite.ncard]
[GOAL]
case inr
α✝ : Type ?u.175384
s t : Set α✝
α : Type u_1
h : Infinite α
⊢ Set.Infinite univ
[PROOFSTEP]
exact infinite_univ
[GOAL]
α✝ : Type ?u.176860
s t : Set α✝
α : Type u_1
⊢ ncard ∅ = 0
[PROOFSTEP]
rw [ncard_eq_zero]
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ 0 < ncard s ↔ Set.Nonempty s
[PROOFSTEP]
rw [pos_iff_ne_zero, Ne.def, ncard_eq_zero hs, nonempty_iff_ne_empty]
[GOAL]
α : Type u_1
s t : Set α
hs : ncard s ≠ 0
⊢ Set.Nonempty s
[PROOFSTEP]
rw [nonempty_iff_ne_empty]
[GOAL]
α : Type u_1
s t : Set α
hs : ncard s ≠ 0
⊢ s ≠ ∅
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
t : Set α
hs : ncard ∅ ≠ 0
⊢ False
[PROOFSTEP]
simp at hs 
[GOAL]
α : Type u_1
s t : Set α
a : α
⊢ ncard {a} = 1
[PROOFSTEP]
simp [ncard_eq_toFinset_card]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
s : Set α
⊢ ncard ({a} ∩ s) ≤ 1
[PROOFSTEP]
rw [← Nat.cast_le (α := ℕ∞), (toFinite _).cast_ncard_eq, Nat.cast_one]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
s : Set α
⊢ encard ({a} ∩ s) ≤ 1
[PROOFSTEP]
apply encard_singleton_inter
[GOAL]
α : Type u_1
s t : Set α
a : α
h : ¬a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (insert a s) = ncard s + 1
[PROOFSTEP]
rw [← Nat.cast_inj (R := ℕ∞), (hs.insert a).cast_ncard_eq, Nat.cast_add, Nat.cast_one, hs.cast_ncard_eq,
  encard_insert_of_not_mem h]
[GOAL]
α : Type u_1
s t : Set α
a : α
h : a ∈ s
⊢ ncard (insert a s) = ncard s
[PROOFSTEP]
rw [insert_eq_of_mem h]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
s : Set α
⊢ ncard (insert a s) ≤ ncard s + 1
[PROOFSTEP]
obtain hs | hs := s.finite_or_infinite
[GOAL]
case inl
α : Type u_1
s✝ t : Set α
a : α
s : Set α
hs : Set.Finite s
⊢ ncard (insert a s) ≤ ncard s + 1
[PROOFSTEP]
to_encard_tac
[GOAL]
case inl
α : Type u_1
s✝ t : Set α
a : α
s : Set α
hs : Set.Finite s
⊢ ↑(ncard (insert a s)) ≤ ↑(ncard s) + 1
[PROOFSTEP]
rw [hs.cast_ncard_eq, (hs.insert _).cast_ncard_eq]
[GOAL]
case inl
α : Type u_1
s✝ t : Set α
a : α
s : Set α
hs : Set.Finite s
⊢ encard (insert a s) ≤ encard s + 1
[PROOFSTEP]
apply encard_insert_le
[GOAL]
case inr
α : Type u_1
s✝ t : Set α
a : α
s : Set α
hs : Set.Infinite s
⊢ ncard (insert a s) ≤ ncard s + 1
[PROOFSTEP]
rw [(hs.mono (subset_insert a s)).ncard]
[GOAL]
case inr
α : Type u_1
s✝ t : Set α
a : α
s : Set α
hs : Set.Infinite s
⊢ 0 ≤ ncard s + 1
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
α : Type u_1
s t : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (insert a s) = if a ∈ s then ncard s else ncard s + 1
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
s t : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : autoParam (Set.Finite s) _auto✝
h : a ∈ s
⊢ ncard (insert a s) = if a ∈ s then ncard s else ncard s + 1
[PROOFSTEP]
rw [ncard_insert_of_mem h, if_pos h]
[GOAL]
case neg
α : Type u_1
s t : Set α
a : α
inst✝ : Decidable (a ∈ s)
hs : autoParam (Set.Finite s) _auto✝
h : ¬a ∈ s
⊢ ncard (insert a s) = if a ∈ s then ncard s else ncard s + 1
[PROOFSTEP]
rw [ncard_insert_of_not_mem h hs, if_neg h]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
s : Set α
⊢ ncard s ≤ ncard (insert a s)
[PROOFSTEP]
classical
refine' s.finite_or_infinite.elim (fun h ↦ _) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))
rw [ncard_insert_eq_ite h]; split_ifs <;> simp
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
s : Set α
⊢ ncard s ≤ ncard (insert a s)
[PROOFSTEP]
refine' s.finite_or_infinite.elim (fun h ↦ _) (fun h ↦ by (rw [h.ncard]; exact Nat.zero_le _))
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
s : Set α
h : Set.Infinite s
⊢ ncard s ≤ ncard (insert a s)
[PROOFSTEP]
rw [h.ncard]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
s : Set α
h : Set.Infinite s
⊢ 0 ≤ ncard (insert a s)
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
s : Set α
h : Set.Finite s
⊢ ncard s ≤ ncard (insert a s)
[PROOFSTEP]
rw [ncard_insert_eq_ite h]
[GOAL]
α : Type u_1
s✝ t : Set α
a : α
s : Set α
h : Set.Finite s
⊢ ncard s ≤ if a ∈ s then ncard s else ncard s + 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
s✝ t : Set α
a : α
s : Set α
h : Set.Finite s
h✝ : a ∈ s
⊢ ncard s ≤ ncard s
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
s✝ t : Set α
a : α
s : Set α
h : Set.Finite s
h✝ : ¬a ∈ s
⊢ ncard s ≤ ncard s + 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s t : Set α
a b : α
h : a ≠ b
⊢ ncard {a, b} = 2
[PROOFSTEP]
rw [ncard_insert_of_not_mem, ncard_singleton]
[GOAL]
α : Type u_1
s t : Set α
a b : α
h : a ≠ b
⊢ ¬a ∈ {b}
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
s t : Set α
a : α
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (s \ {a}) + 1 = ncard s
[PROOFSTEP]
to_encard_tac
[GOAL]
α : Type u_1
s t : Set α
a : α
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ↑(ncard (s \ {a})) + 1 = ↑(ncard s)
[PROOFSTEP]
rw [hs.cast_ncard_eq, (hs.diff _).cast_ncard_eq, encard_diff_singleton_add_one h]
[GOAL]
α : Type u_1
s t : Set α
a : α
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (s \ {a}) < ncard s
[PROOFSTEP]
rw [← ncard_diff_singleton_add_one h hs]
[GOAL]
α : Type u_1
s t : Set α
a : α
h : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (s \ {a}) < ncard (s \ {a}) + 1
[PROOFSTEP]
apply lt_add_one
[GOAL]
α : Type u_1
s✝ t s : Set α
a : α
⊢ ncard (s \ {a}) ≤ ncard s
[PROOFSTEP]
obtain hs | hs := s.finite_or_infinite
[GOAL]
case inl
α : Type u_1
s✝ t s : Set α
a : α
hs : Set.Finite s
⊢ ncard (s \ {a}) ≤ ncard s
[PROOFSTEP]
apply ncard_le_of_subset (diff_subset _ _) hs
[GOAL]
case inr
α : Type u_1
s✝ t s : Set α
a : α
hs : Set.Infinite s
⊢ ncard (s \ {a}) ≤ ncard s
[PROOFSTEP]
convert @zero_le ℕ _ _
[GOAL]
case h.e'_3
α : Type u_1
s✝ t s : Set α
a : α
hs : Set.Infinite s
⊢ ncard (s \ {a}) = 0
[PROOFSTEP]
exact (hs.diff (by simp : Set.Finite { a })).ncard
[GOAL]
α : Type u_1
s✝ t s : Set α
a : α
hs : Set.Infinite s
⊢ Set.Finite {a}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s✝ t s : Set α
a : α
⊢ ncard s - 1 ≤ ncard (s \ {a})
[PROOFSTEP]
cases' s.finite_or_infinite with hs hs
[GOAL]
case inl
α : Type u_1
s✝ t s : Set α
a : α
hs : Set.Finite s
⊢ ncard s - 1 ≤ ncard (s \ {a})
[PROOFSTEP]
by_cases h : a ∈ s
[GOAL]
case pos
α : Type u_1
s✝ t s : Set α
a : α
hs : Set.Finite s
h : a ∈ s
⊢ ncard s - 1 ≤ ncard (s \ {a})
[PROOFSTEP]
rw [ncard_diff_singleton_of_mem h hs]
[GOAL]
case neg
α : Type u_1
s✝ t s : Set α
a : α
hs : Set.Finite s
h : ¬a ∈ s
⊢ ncard s - 1 ≤ ncard (s \ {a})
[PROOFSTEP]
rw [diff_singleton_eq_self h]
[GOAL]
case neg
α : Type u_1
s✝ t s : Set α
a : α
hs : Set.Finite s
h : ¬a ∈ s
⊢ ncard s - 1 ≤ ncard s
[PROOFSTEP]
apply Nat.pred_le
[GOAL]
case inr
α : Type u_1
s✝ t s : Set α
a : α
hs : Set.Infinite s
⊢ ncard s - 1 ≤ ncard (s \ {a})
[PROOFSTEP]
convert Nat.zero_le _
[GOAL]
case h.e'_3
α : Type u_1
s✝ t s : Set α
a : α
hs : Set.Infinite s
⊢ ncard s - 1 = 0
[PROOFSTEP]
rw [hs.ncard]
[GOAL]
α : Type u_1
s t : Set α
a b : α
ha : ¬a ∈ s
hb : b ∈ s
⊢ ncard (insert a s \ {b}) = ncard s
[PROOFSTEP]
rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_diff_distrib,
  @diff_singleton_eq_self _ b { a } fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])]
[GOAL]
α : Type u_1
s t : Set α
a b : α
ha : ¬a ∈ s
hb : b ∈ s
h : b ∈ {a}
⊢ a ∈ s
[PROOFSTEP]
rwa [← mem_singleton_iff.mp h]
[GOAL]
α : Type u_2
s t : Set α
α✝ : Type u_1
f : α → α✝
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (f '' s) ≤ ncard s
[PROOFSTEP]
to_encard_tac
[GOAL]
α : Type u_2
s t : Set α
α✝ : Type u_1
f : α → α✝
hs : autoParam (Set.Finite s) _auto✝
⊢ ↑(ncard (f '' s)) ≤ ↑(ncard s)
[PROOFSTEP]
rw [hs.cast_ncard_eq, (hs.image _).cast_ncard_eq]
[GOAL]
α : Type u_2
s t : Set α
α✝ : Type u_1
f : α → α✝
hs : autoParam (Set.Finite s) _auto✝
⊢ encard (f '' s) ≤ encard s
[PROOFSTEP]
apply encard_image_le
[GOAL]
α : Type u_2
s t : Set α
α✝ : Type u_1
f : α → α✝
h : ncard (f '' s) = ncard s
hs : autoParam (Set.Finite s) _auto✝
⊢ InjOn f s
[PROOFSTEP]
rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, (hs.image _).cast_ncard_eq] at h 
[GOAL]
α : Type u_2
s t : Set α
α✝ : Type u_1
f : α → α✝
h : encard (f '' s) = encard s
hs : autoParam (Set.Finite s) _auto✝
⊢ InjOn f s
[PROOFSTEP]
exact hs.injOn_of_encard_image_eq h
[GOAL]
α : Type ?u.212510
s✝ t : Set α
β : Type u_1
α✝ : Type u_2
f : α✝ → β
s : Set β
H : Function.Injective f
hs : s ⊆ range f
⊢ ncard (f ⁻¹' s) = ncard s
[PROOFSTEP]
rw [← ncard_image_of_injective _ H, image_preimage_eq_iff.mpr hs]
[GOAL]
α : Type u_2
s t : Set α
β : Type u_1
f : α → β
y : β
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard {x | x ∈ s ∧ f x = y} ≠ 0 ↔ y ∈ f '' s
[PROOFSTEP]
refine' ⟨nonempty_of_ncard_ne_zero, _⟩
[GOAL]
α : Type u_2
s t : Set α
β : Type u_1
f : α → β
y : β
hs : autoParam (Set.Finite s) _auto✝
⊢ y ∈ f '' s → ncard {x | x ∈ s ∧ f x = y} ≠ 0
[PROOFSTEP]
rintro ⟨z, hz, rfl⟩
[GOAL]
case intro.intro
α : Type u_2
s t : Set α
β : Type u_1
f : α → β
hs : autoParam (Set.Finite s) _auto✝
z : α
hz : z ∈ s
⊢ ncard {x | x ∈ s ∧ f x = f z} ≠ 0
[PROOFSTEP]
exact @ncard_ne_zero_of_mem _ ({x ∈ s | f x = f z}) z (mem_sep hz rfl) (hs.subset (sep_subset _ _))
[GOAL]
α : Type u_1
s✝ t : Set α
P : α → Prop
s : Set α
⊢ ncard {x | ↑x ∈ s} = ncard (s ∩ setOf P)
[PROOFSTEP]
convert (ncard_image_of_injective _ (@Subtype.coe_injective _ P)).symm
[GOAL]
case h.e'_3.h.e'_2
α : Type u_1
s✝ t : Set α
P : α → Prop
s : Set α
⊢ s ∩ setOf P = (fun a => ↑a) '' {x | ↑x ∈ s}
[PROOFSTEP]
ext x
[GOAL]
case h.e'_3.h.e'_2.h
α : Type u_1
s✝ t : Set α
P : α → Prop
s : Set α
x : α
⊢ x ∈ s ∩ setOf P ↔ x ∈ (fun a => ↑a) '' {x | ↑x ∈ s}
[PROOFSTEP]
simp [← and_assoc, exists_eq_right]
[GOAL]
α : Type u_1
s t : Set α
h : s ⊆ t
h' : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
⊢ encard t ≤ encard s
[PROOFSTEP]
rwa [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq] at h' 
[GOAL]
α : Type u_1
s t : Set α
a : α
P : α → Prop
h : ncard {x | x ∈ s ∧ P x} = ncard s
ha : a ∈ s
hs : autoParam (Set.Finite s) _auto✝
⊢ {x | x ∈ s ∧ P x} ⊆ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s t : Set α
h : s ⊂ t
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard s < ncard t
[PROOFSTEP]
rw [← Nat.cast_lt (α := ℕ∞), ht.cast_ncard_eq, (ht.subset h.subset).cast_ncard_eq]
[GOAL]
α : Type u_1
s t : Set α
h : s ⊂ t
ht : autoParam (Set.Finite t) _auto✝
⊢ encard s < encard t
[PROOFSTEP]
exact ht.encard_lt_encard h
[GOAL]
α : Type u_1
s t : Set α
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
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s = n
[PROOFSTEP]
rw [ncard_eq_toFinset_card _ hs]
[GOAL]
α : Type u_1
s t : Set α
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
hs : autoParam (Set.Finite s) _auto✝
⊢ Finset.card (Finite.toFinset hs) = n
[PROOFSTEP]
apply Finset.card_eq_of_bijective
[GOAL]
case hf
α : Type u_1
s t : Set α
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
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (a : α), a ∈ Finite.toFinset hs → ∃ i h, ?f i h = a
case hf'
α : Type u_1
s t : Set α
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
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (i : ℕ) (h : i < n), ?f i h ∈ Finite.toFinset hs
case f_inj
α : Type u_1
s t : Set α
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
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (i j : ℕ) (hi : i < n) (hj : j < n), ?f i hi = ?f j hj → i = j
case f
α : Type u_1
s t : Set α
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
hs : autoParam (Set.Finite s) _auto✝
⊢ (i : ℕ) → i < n → α
[PROOFSTEP]
all_goals simpa
[GOAL]
case hf
α : Type u_1
s t : Set α
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
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (a : α), a ∈ Finite.toFinset hs → ∃ i h, ?f i h = a
[PROOFSTEP]
simpa
[GOAL]
case hf'
α : Type u_1
s t : Set α
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
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (i : ℕ) (h : i < n), f i h ∈ Finite.toFinset hs
[PROOFSTEP]
simpa
[GOAL]
case f_inj
α : Type u_1
s t : Set α
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
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
[PROOFSTEP]
simpa
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
⊢ ncard s = ncard t
[PROOFSTEP]
set f' : s → t := fun x ↦ ⟨f x.1 x.2, h₁ _ _⟩
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ ncard s = ncard t
[PROOFSTEP]
have hbij : f'.Bijective := by
  constructor
  · rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
    simp only [Subtype.mk.injEq] at hxy ⊢
    exact h₂ _ _ hx hy hxy
  rintro ⟨y, hy⟩
  obtain ⟨a, ha, rfl⟩ := h₃ y hy
  simp only [Subtype.mk.injEq, Subtype.exists]
  exact ⟨_, ha, rfl⟩
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ Function.Bijective f'
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ Function.Injective f'
[PROOFSTEP]
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
[GOAL]
case left.mk.mk
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f' { val := x, property := hx } = f' { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
[PROOFSTEP]
simp only [Subtype.mk.injEq] at hxy ⊢
[GOAL]
case left.mk.mk
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x (_ : ↑{ val := x, property := hx } ∈ s) = f y (_ : ↑{ val := y, property := hy } ∈ s)
⊢ x = y
[PROOFSTEP]
exact h₂ _ _ hx hy hxy
[GOAL]
case right
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ Function.Surjective f'
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case right.mk
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
y : β
hy : y ∈ t
⊢ ∃ a, f' a = { val := y, property := hy }
[PROOFSTEP]
obtain ⟨a, ha, rfl⟩ := h₃ y hy
[GOAL]
case right.mk.intro.intro
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, f' a_1 = { val := f a ha, property := hy }
[PROOFSTEP]
simp only [Subtype.mk.injEq, Subtype.exists]
[GOAL]
case right.mk.intro.intro
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1 h, f a_1 (_ : ↑{ val := a_1, property := (_ : a_1 ∈ s) } ∈ s) = f a ha
[PROOFSTEP]
exact ⟨_, ha, rfl⟩
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hbij : Function.Bijective f'
⊢ ncard s = ncard t
[PROOFSTEP]
simp_rw [← Nat.card_coe_set_eq]
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hbij : Function.Bijective f'
⊢ Nat.card ↑s = Nat.card ↑t
[PROOFSTEP]
exact Nat.card_congr (Equiv.ofBijective f' hbij)
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard s ≤ ncard t
[PROOFSTEP]
have hle := encard_le_encard_of_injOn hf f_inj
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
hle : encard s ≤ encard t
⊢ ncard s ≤ ncard t
[PROOFSTEP]
to_encard_tac
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
f_inj : InjOn f s
ht : autoParam (Set.Finite t) _auto✝
hle : encard s ≤ encard t
⊢ ↑(ncard s) ≤ ↑(ncard t)
[PROOFSTEP]
rwa [ht.cast_ncard_eq, (ht.finite_of_encard_le hle).cast_ncard_eq]
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
hc : ncard t < ncard s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : autoParam (Set.Finite t) _auto✝
⊢ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y ∧ f x = f y
[PROOFSTEP]
by_contra h'
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
hc : ncard t < ncard s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : autoParam (Set.Finite t) _auto✝
h' : ¬∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y ∧ f x = f y
⊢ False
[PROOFSTEP]
simp only [Ne.def, exists_prop, not_exists, not_and, not_imp_not] at h' 
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
hc : ncard t < ncard s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : autoParam (Set.Finite t) _auto✝
h' : ∀ (x : α), x ∈ s → ∀ (x_1 : α), x_1 ∈ s → f x = f x_1 → x = x_1
⊢ False
[PROOFSTEP]
exact (ncard_le_ncard_of_injOn f hf h' ht).not_lt hc
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ n ≤ ncard s
[PROOFSTEP]
rw [ncard_eq_toFinset_card _ hs]
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ n ≤ Finset.card (Finite.toFinset hs)
[PROOFSTEP]
apply Finset.le_card_of_inj_on_range
[GOAL]
case hf
α : Type u_1
s t : Set α
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (i : ℕ), i < n → ?f i ∈ Finite.toFinset hs
[PROOFSTEP]
simpa
[GOAL]
case f_inj
α : Type u_1
s t : Set α
n : ℕ
f : ℕ → α
hf : ∀ (i : ℕ), i < n → f i ∈ s
f_inj : ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
hs : autoParam (Set.Finite s) _auto✝
⊢ ∀ (i : ℕ), i < n → ∀ (j : ℕ), j < n → f i = f j → i = j
[PROOFSTEP]
simpa
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
⊢ ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
[PROOFSTEP]
intro b hb
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
set f' : s → t := fun x ↦ ⟨f x.1 x.2, hf _ _⟩
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
have finj : f'.Injective := by
  rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
  simp only [Subtype.mk.injEq] at hxy ⊢
  apply hinj _ _ hx hy hxy
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ Function.Injective f'
[PROOFSTEP]
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
[GOAL]
case mk.mk
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f' { val := x, property := hx } = f' { val := y, property := hy }
⊢ { val := x, property := hx } = { val := y, property := hy }
[PROOFSTEP]
simp only [Subtype.mk.injEq] at hxy ⊢
[GOAL]
case mk.mk
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : f x (_ : ↑{ val := x, property := hx } ∈ s) = f y (_ : ↑{ val := y, property := hy } ∈ s)
⊢ x = y
[PROOFSTEP]
apply hinj _ _ hx hy hxy
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
have hft := ht.fintype
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
have hft' := Fintype.ofInjective f' finj
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h)
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
a : α
h : a ∈ toFinset s
⊢ a ∈ s
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ∃ a ha, b = f a ha
[PROOFSTEP]
convert @Finset.surj_on_of_inj_on_of_card_le _ _ _ t.toFinset f'' _ _ _ _ (by simpa)
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ?m.261721 ∈ toFinset t
[PROOFSTEP]
simpa
[GOAL]
case h.e'_2.h.h.e'_1.a
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
x✝ : α
⊢ x✝ ∈ s ↔ x✝ ∈ toFinset s
[PROOFSTEP]
simp
[GOAL]
case convert_1
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ∀ (a : α) (ha : a ∈ toFinset s), f'' a ha ∈ toFinset t
[PROOFSTEP]
simp [hf]
[GOAL]
case convert_2
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ toFinset s) (ha₂ : a₂ ∈ toFinset s), f'' a₁ ha₁ = f'' a₂ ha₂ → a₁ = a₂
[PROOFSTEP]
intros a₁ a₂ ha₁ ha₂ h
[GOAL]
case convert_2
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
a₁ a₂ : α
ha₁ : a₁ ∈ toFinset s
ha₂ : a₂ ∈ toFinset s
h : f'' a₁ ha₁ = f'' a₂ ha₂
⊢ a₁ = a₂
[PROOFSTEP]
rw [mem_toFinset] at ha₁ ha₂ 
[GOAL]
case convert_2
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
a₁ a₂ : α
ha₁✝ : a₁ ∈ toFinset s
ha₁ : a₁ ∈ s
ha₂✝ : a₂ ∈ toFinset s
ha₂ : a₂ ∈ s
h : f'' a₁ ha₁✝ = f'' a₂ ha₂✝
⊢ a₁ = a₂
[PROOFSTEP]
exact hinj _ _ ha₁ ha₂ h
[GOAL]
case convert_3
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
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 : ncard t ≤ ncard s
ht : autoParam (Set.Finite t) _auto✝
b : β
hb : b ∈ t
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
finj : Function.Injective f'
hft : Fintype ↑t
hft' : Fintype ↑s
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ Finset.card (toFinset t) ≤ Finset.card (toFinset s)
[PROOFSTEP]
rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card']
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
⊢ a₁ = a₂
[PROOFSTEP]
classical
set f' : s → t := fun x ↦ ⟨f x.1 x.2, hf _ _⟩
have hsurj : f'.Surjective := by
  rintro ⟨y, hy⟩
  obtain ⟨a, ha, rfl⟩ := hsurj y hy
  simp only [Subtype.mk.injEq, Subtype.exists]
  exact ⟨_, ha, rfl⟩
haveI := hs.fintype
haveI := Fintype.ofSurjective _ hsurj
set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h)
exact
  @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f''
    (fun a ha ↦ by {rw [mem_toFinset] at ha ⊢; exact hf a ha
    })
    (by simpa)
    (by {rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card']
    })
    a₁ a₂ (by simpa) (by simpa) (by simpa)
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
⊢ a₁ = a₂
[PROOFSTEP]
set f' : s → t := fun x ↦ ⟨f x.1 x.2, hf _ _⟩
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ a₁ = a₂
[PROOFSTEP]
have hsurj : f'.Surjective := by
  rintro ⟨y, hy⟩
  obtain ⟨a, ha, rfl⟩ := hsurj y hy
  simp only [Subtype.mk.injEq, Subtype.exists]
  exact ⟨_, ha, rfl⟩
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
⊢ Function.Surjective f'
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case mk
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
y : β
hy : y ∈ t
⊢ ∃ a, f' a = { val := y, property := hy }
[PROOFSTEP]
obtain ⟨a, ha, rfl⟩ := hsurj y hy
[GOAL]
case mk.intro.intro
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1, f' a_1 = { val := f a ha, property := hy }
[PROOFSTEP]
simp only [Subtype.mk.injEq, Subtype.exists]
[GOAL]
case mk.intro.intro
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
a : α
ha : a ∈ s
hy : f a ha ∈ t
⊢ ∃ a_1 h, f a_1 (_ : ↑{ val := a_1, property := (_ : a_1 ∈ s) } ∈ s) = f a ha
[PROOFSTEP]
exact ⟨_, ha, rfl⟩
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
⊢ a₁ = a₂
[PROOFSTEP]
haveI := hs.fintype
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this : Fintype ↑s
⊢ a₁ = a₂
[PROOFSTEP]
haveI := Fintype.ofSurjective _ hsurj
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
⊢ a₁ = a₂
[PROOFSTEP]
set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h)
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
a : α
h : a ∈ toFinset s
⊢ a ∈ s
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ a₁ = a₂
[PROOFSTEP]
exact
  @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f''
    (fun a ha ↦ by {rw [mem_toFinset] at ha ⊢; exact hf a ha
    })
    (by simpa)
    (by {rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card']
    })
    a₁ a₂ (by simpa) (by simpa) (by simpa)
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
a : α
ha : a ∈ toFinset s
⊢ f'' a ha ∈ toFinset t
[PROOFSTEP]
{rw [mem_toFinset] at ha ⊢; exact hf a ha
}
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
a : α
ha : a ∈ toFinset s
⊢ f'' a ha ∈ toFinset t
[PROOFSTEP]
rw [mem_toFinset] at ha ⊢
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
a : α
ha✝ : a ∈ toFinset s
ha : a ∈ s
⊢ f'' a ha✝ ∈ t
[PROOFSTEP]
exact hf a ha
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ ∀ (b : β), b ∈ toFinset t → ∃ a ha, b = f'' a ha
[PROOFSTEP]
simpa
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ Finset.card (toFinset s) ≤ Finset.card (toFinset t)
[PROOFSTEP]
{rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card']
}
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ Finset.card (toFinset s) ≤ Finset.card (toFinset t)
[PROOFSTEP]
rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card']
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ a₁ ∈ toFinset s
[PROOFSTEP]
simpa
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ a₂ ∈ toFinset s
[PROOFSTEP]
simpa
[GOAL]
α : Type u_2
s t✝ : Set α
β : Type u_1
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj✝ : ∀ (b : β), b ∈ t → ∃ a ha, b = f a ha
hst : ncard s ≤ ncard t
a₁ a₂ : α
ha₁ : a₁ ∈ s
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : autoParam (Set.Finite s) _auto✝
f' : ↑s → ↑t := fun x => { val := f ↑x (_ : ↑x ∈ s), property := (_ : f ↑x (_ : ↑x ∈ s) ∈ t) }
hsurj : Function.Surjective f'
this✝ : Fintype ↑s
this : Fintype ↑t
f'' : (a : α) → a ∈ toFinset s → β := fun a h => f a (_ : a ∈ s)
⊢ f'' a₁ (_ : a₁ ∈ toFinset s) = f'' a₂ (_ : a₂ ∈ toFinset s)
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (s ∪ t) + ncard (s ∩ t) = ncard s + ncard t
[PROOFSTEP]
to_encard_tac
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ↑(ncard (s ∪ t)) + ↑(ncard (s ∩ t)) = ↑(ncard s) + ↑(ncard t)
[PROOFSTEP]
rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq, (hs.subset (inter_subset_left _ _)).cast_ncard_eq,
  encard_union_add_encard_inter]
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (s ∩ t) + ncard (s ∪ t) = ncard s + ncard t
[PROOFSTEP]
rw [add_comm, ncard_union_add_ncard_inter _ _ hs ht]
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
[PROOFSTEP]
obtain (h | h) := (s ∪ t).finite_or_infinite
[GOAL]
case inl
α : Type u_1
s✝ t✝ s t : Set α
h : Set.Finite (s ∪ t)
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
[PROOFSTEP]
to_encard_tac
[GOAL]
case inl
α : Type u_1
s✝ t✝ s t : Set α
h : Set.Finite (s ∪ t)
⊢ ↑(ncard (s ∪ t)) ≤ ↑(ncard s) + ↑(ncard t)
[PROOFSTEP]
rw [h.cast_ncard_eq, (h.subset (subset_union_left _ _)).cast_ncard_eq,
  (h.subset (subset_union_right _ _)).cast_ncard_eq]
[GOAL]
case inl
α : Type u_1
s✝ t✝ s t : Set α
h : Set.Finite (s ∪ t)
⊢ encard (s ∪ t) ≤ encard s + encard t
[PROOFSTEP]
apply encard_union_le
[GOAL]
case inr
α : Type u_1
s✝ t✝ s t : Set α
h : Set.Infinite (s ∪ t)
⊢ ncard (s ∪ t) ≤ ncard s + ncard t
[PROOFSTEP]
rw [h.ncard]
[GOAL]
case inr
α : Type u_1
s✝ t✝ s t : Set α
h : Set.Infinite (s ∪ t)
⊢ 0 ≤ ncard s + ncard t
[PROOFSTEP]
apply zero_le
[GOAL]
α : Type u_1
s t : Set α
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (s ∪ t) = ncard s + ncard t
[PROOFSTEP]
to_encard_tac
[GOAL]
α : Type u_1
s t : Set α
h : Disjoint s t
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ↑(ncard (s ∪ t)) = ↑(ncard s) + ↑(ncard t)
[PROOFSTEP]
rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq, encard_union_eq h]
[GOAL]
α : Type u_1
s t : Set α
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (t \ s) + ncard s = ncard t
[PROOFSTEP]
to_encard_tac
[GOAL]
α : Type u_1
s t : Set α
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ ↑(ncard (t \ s)) + ↑(ncard s) = ↑(ncard t)
[PROOFSTEP]
rw [ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq, (ht.diff _).cast_ncard_eq, encard_diff_add_encard_of_subset h]
[GOAL]
α : Type u_1
s t : Set α
h : s ⊆ t
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (t \ s) = ncard t - ncard s
[PROOFSTEP]
rw [← ncard_diff_add_ncard_of_subset h ht, add_tsub_cancel_right]
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard s ≤ ncard (s \ t) + ncard t
[PROOFSTEP]
cases' s.finite_or_infinite with hs hs
[GOAL]
case inl
α : Type u_1
s✝ t✝ s t : Set α
ht : autoParam (Set.Finite t) _auto✝
hs : Set.Finite s
⊢ ncard s ≤ ncard (s \ t) + ncard t
[PROOFSTEP]
to_encard_tac
[GOAL]
case inl
α : Type u_1
s✝ t✝ s t : Set α
ht : autoParam (Set.Finite t) _auto✝
hs : Set.Finite s
⊢ ↑(ncard s) ≤ ↑(ncard (s \ t)) + ↑(ncard t)
[PROOFSTEP]
rw [ht.cast_ncard_eq, hs.cast_ncard_eq, (hs.diff _).cast_ncard_eq]
[GOAL]
case inl
α : Type u_1
s✝ t✝ s t : Set α
ht : autoParam (Set.Finite t) _auto✝
hs : Set.Finite s
⊢ encard s ≤ encard (s \ t) + encard t
[PROOFSTEP]
apply encard_le_encard_diff_add_encard
[GOAL]
case inr
α : Type u_1
s✝ t✝ s t : Set α
ht : autoParam (Set.Finite t) _auto✝
hs : Set.Infinite s
⊢ ncard s ≤ ncard (s \ t) + ncard t
[PROOFSTEP]
convert Nat.zero_le _
[GOAL]
case h.e'_3
α : Type u_1
s✝ t✝ s t : Set α
ht : autoParam (Set.Finite t) _auto✝
hs : Set.Infinite s
⊢ ncard s = 0
[PROOFSTEP]
rw [hs.ncard]
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard t ≤ ncard s + ncard (t \ s)
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard t ≤ ncard (t \ s) + ncard s
[PROOFSTEP]
apply ncard_le_ncard_diff_add_ncard _ _ hs
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard (s \ t) + ncard t = ncard (s ∪ t)
[PROOFSTEP]
rw [← ncard_union_eq disjoint_sdiff_left (hs.diff _) ht, diff_union_self]
[GOAL]
α : Type u_1
s t : Set α
h : ncard s < ncard t
hs : autoParam (Set.Finite s) _auto✝
⊢ Set.Nonempty (t \ s)
[PROOFSTEP]
rw [Set.nonempty_iff_ne_empty, Ne.def, diff_eq_empty]
[GOAL]
α : Type u_1
s t : Set α
h : ncard s < ncard t
hs : autoParam (Set.Finite s) _auto✝
⊢ ¬t ⊆ s
[PROOFSTEP]
exact fun h' ↦ h.not_le (ncard_le_of_subset h' hs)
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard (s ∩ t) + ncard (s \ t) = ncard s
[PROOFSTEP]
rw [←
  ncard_union_eq (disjoint_of_subset_left (inter_subset_right _ _) disjoint_sdiff_right) (hs.inter_of_left _)
    (hs.diff _),
  union_comm, diff_union_inter]
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard s = ncard t ↔ ncard (s \ t) = ncard (t \ s)
[PROOFSTEP]
rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht, inter_comm,
  add_right_inj]
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard s ≤ ncard t ↔ ncard (s \ t) ≤ ncard (t \ s)
[PROOFSTEP]
rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht, inter_comm,
  add_le_add_iff_left]
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : autoParam (Set.Finite t) _auto✝
⊢ ncard s < ncard t ↔ ncard (s \ t) < ncard (t \ s)
[PROOFSTEP]
rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht, inter_comm,
  add_lt_add_iff_left]
[GOAL]
α : Type u_1
s✝ t s : Set α
hs : autoParam (Set.Finite s) _auto✝
hsc : autoParam (Set.Finite sᶜ) _auto✝
⊢ ncard s + ncard sᶜ = Nat.card α
[PROOFSTEP]
rw [← ncard_univ, ← ncard_union_eq (@disjoint_compl_right _ _ s) hs hsc, union_compl_self]
[GOAL]
α : Type u_1
s t : Set α
i : ℕ
h₁ : i + ncard s ≤ ncard t
h₂ : s ⊆ t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
[PROOFSTEP]
cases' t.finite_or_infinite with ht ht
[GOAL]
case inl
α : Type u_1
s t : Set α
i : ℕ
h₁ : i + ncard s ≤ ncard t
h₂ : s ⊆ t
ht : Set.Finite t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
[PROOFSTEP]
rw [ncard_eq_toFinset_card _ (ht.subset h₂)] at h₁ ⊢
[GOAL]
case inl
α : Type u_1
s t : Set α
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ ncard t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
[PROOFSTEP]
rw [ncard_eq_toFinset_card t ht] at h₁ 
[GOAL]
case inl
α : Type u_1
s t : Set α
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
[PROOFSTEP]
obtain ⟨r', hsr', hr't, hr'⟩ := Finset.exists_intermediate_set _ h₁ (by simpa)
[GOAL]
α : Type u_1
s t : Set α
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
⊢ Finite.toFinset (_ : Set.Finite s) ⊆ Finite.toFinset ht
[PROOFSTEP]
simpa
[GOAL]
case inl.intro.intro.intro
α : Type u_1
s t : Set α
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
r' : Finset α
hsr' : Finite.toFinset (_ : Set.Finite s) ⊆ r'
hr't : r' ⊆ Finite.toFinset ht
hr' : Finset.card r' = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
[PROOFSTEP]
exact ⟨r', by simpa using hsr', by simpa using hr't, by rw [← hr', ncard_coe_Finset]⟩
[GOAL]
α : Type u_1
s t : Set α
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
r' : Finset α
hsr' : Finite.toFinset (_ : Set.Finite s) ⊆ r'
hr't : r' ⊆ Finite.toFinset ht
hr' : Finset.card r' = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
⊢ s ⊆ ↑r'
[PROOFSTEP]
simpa using hsr'
[GOAL]
α : Type u_1
s t : Set α
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
r' : Finset α
hsr' : Finite.toFinset (_ : Set.Finite s) ⊆ r'
hr't : r' ⊆ Finite.toFinset ht
hr' : Finset.card r' = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
⊢ ↑r' ⊆ t
[PROOFSTEP]
simpa using hr't
[GOAL]
α : Type u_1
s t : Set α
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
r' : Finset α
hsr' : Finite.toFinset (_ : Set.Finite s) ⊆ r'
hr't : r' ⊆ Finite.toFinset ht
hr' : Finset.card r' = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
⊢ ncard ↑r' = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
[PROOFSTEP]
rw [← hr', ncard_coe_Finset]
[GOAL]
case inr
α : Type u_1
s t : Set α
i : ℕ
h₁ : i + ncard s ≤ ncard t
h₂ : s ⊆ t
ht : Set.Infinite t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
[PROOFSTEP]
rw [ht.ncard] at h₁ 
[GOAL]
case inr
α : Type u_1
s t : Set α
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
[PROOFSTEP]
have h₁' := Nat.eq_zero_of_le_zero h₁
[GOAL]
case inr
α : Type u_1
s t : Set α
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
h₁' : i + ncard s = 0
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
[PROOFSTEP]
rw [add_eq_zero_iff] at h₁' 
[GOAL]
case inr
α : Type u_1
s t : Set α
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
h₁' : i = 0 ∧ ncard s = 0
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
[PROOFSTEP]
refine' ⟨t, h₂, rfl.subset, _⟩
[GOAL]
case inr
α : Type u_1
s t : Set α
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
h₁' : i = 0 ∧ ncard s = 0
⊢ ncard t = i + ncard s
[PROOFSTEP]
rw [h₁'.2, h₁'.1, ht.ncard, add_zero]
[GOAL]
α : Type u_1
s t : Set α
m : ℕ
hs : ncard s ≤ m
ht : m ≤ ncard t
h : s ⊆ t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = m
[PROOFSTEP]
obtain ⟨r, hsr, hrt, hc⟩ := exists_intermediate_Set (m - s.ncard) (by rwa [tsub_add_cancel_of_le hs]) h
[GOAL]
α : Type u_1
s t : Set α
m : ℕ
hs : ncard s ≤ m
ht : m ≤ ncard t
h : s ⊆ t
⊢ m - ncard s + ncard s ≤ ncard t
[PROOFSTEP]
rwa [tsub_add_cancel_of_le hs]
[GOAL]
case intro.intro.intro
α : Type u_1
s t : Set α
m : ℕ
hs : ncard s ≤ m
ht : m ≤ ncard t
h : s ⊆ t
r : Set α
hsr : s ⊆ r
hrt : r ⊆ t
hc : ncard r = m - ncard s + ncard s
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = m
[PROOFSTEP]
rw [tsub_add_cancel_of_le hs] at hc 
[GOAL]
case intro.intro.intro
α : Type u_1
s t : Set α
m : ℕ
hs : ncard s ≤ m
ht : m ≤ ncard t
h : s ⊆ t
r : Set α
hsr : s ⊆ r
hrt : r ⊆ t
hc : ncard r = m
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = m
[PROOFSTEP]
exact ⟨r, hsr, hrt, hc⟩
[GOAL]
α : Type u_1
s✝ t s : Set α
i : ℕ
h₁ : i ≤ ncard s
⊢ i + ncard ∅ ≤ ncard s
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
s✝ t✝ s : Set α
i : ℕ
h₁ : i ≤ ncard s
t : Set α
ht : ∅ ⊆ t ∧ t ⊆ s ∧ ncard t = i + ncard ∅
⊢ ncard t = i
[PROOFSTEP]
simpa using ht.2.2
[GOAL]
α : Type u_1
s✝ t s : Set α
hs : Set.Infinite s
k : ℕ
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ Set.ncard t = k
[PROOFSTEP]
have := hs.to_subtype
[GOAL]
α : Type u_1
s✝ t s : Set α
hs : Set.Infinite s
k : ℕ
this : Infinite ↑s
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ Set.ncard t = k
[PROOFSTEP]
obtain ⟨t', -, rfl⟩ := @Infinite.exists_subset_card_eq s univ infinite_univ k
[GOAL]
case intro.intro
α : Type u_1
s✝ t s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ ∃ t, t ⊆ s ∧ Set.Finite t ∧ Set.ncard t = Finset.card t'
[PROOFSTEP]
refine' ⟨Subtype.val '' (t' : Set s), by simp, Finite.image _ (by simp), _⟩
[GOAL]
α : Type u_1
s✝ t s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ Subtype.val '' ↑t' ⊆ s
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s✝ t s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ Set.Finite ↑t'
[PROOFSTEP]
simp
[GOAL]
case intro.intro
α : Type u_1
s✝ t s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ Set.ncard (Subtype.val '' ↑t') = Finset.card t'
[PROOFSTEP]
rw [ncard_image_of_injective _ Subtype.coe_injective]
[GOAL]
case intro.intro
α : Type u_1
s✝ t s : Set α
hs : Set.Infinite s
this : Infinite ↑s
t' : Finset ↑s
⊢ Set.ncard ↑t' = Finset.card t'
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s✝ t✝ s t : Set α
ht : Set.Infinite t
hst : s ⊆ t
hs : Set.Finite s
k : ℕ
hsk : Set.ncard s ≤ k
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ Set.ncard s' = k
[PROOFSTEP]
obtain ⟨s₁, hs₁, hs₁fin, hs₁card⟩ := (ht.diff hs).exists_subset_ncard_eq (k - s.ncard)
[GOAL]
case intro.intro.intro
α : Type u_1
s✝ t✝ s t : Set α
ht : Set.Infinite t
hst : s ⊆ t
hs : Set.Finite s
k : ℕ
hsk : Set.ncard s ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : Set.Finite s₁
hs₁card : Set.ncard s₁ = k - Set.ncard s
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ t ∧ Set.ncard s' = k
[PROOFSTEP]
refine' ⟨s ∪ s₁, subset_union_left _ _, union_subset hst (hs₁.trans (diff_subset _ _)), _⟩
[GOAL]
case intro.intro.intro
α : Type u_1
s✝ t✝ s t : Set α
ht : Set.Infinite t
hst : s ⊆ t
hs : Set.Finite s
k : ℕ
hsk : Set.ncard s ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : Set.Finite s₁
hs₁card : Set.ncard s₁ = k - Set.ncard s
⊢ Set.ncard (s ∪ s₁) = k
[PROOFSTEP]
rwa [ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin, hs₁card, add_tsub_cancel_of_le]
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < ncard (s ∪ t)
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
[PROOFSTEP]
classical
have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
rw [ncard_eq_toFinset_card _ hu,
  Finite.toFinset_union (hu.subset (subset_union_left _ _)) (hu.subset (subset_union_right _ _))] at hst 
obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
exact ⟨r', by simpa, by simpa using hr'⟩
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < ncard (s ∪ t)
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
[PROOFSTEP]
have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < ncard (s ∪ t)
hu : Set.Finite (s ∪ t)
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
[PROOFSTEP]
rw [ncard_eq_toFinset_card _ hu,
  Finite.toFinset_union (hu.subset (subset_union_left _ _)) (hu.subset (subset_union_right _ _))] at hst 
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
hu : Set.Finite (s ∪ t)
hst : 2 * n < Finset.card (Finite.toFinset (_ : Set.Finite s) ∪ Finite.toFinset (_ : Set.Finite t))
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
[PROOFSTEP]
obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
[GOAL]
case intro.intro
α : Type u_1
s t : Set α
n : ℕ
hu : Set.Finite (s ∪ t)
hst : 2 * n < Finset.card (Finite.toFinset (_ : Set.Finite s) ∪ Finite.toFinset (_ : Set.Finite t))
r' : Finset α
hnr' : n < Finset.card r'
hr' : r' ⊆ Finite.toFinset (_ : Set.Finite s) ∨ r' ⊆ Finite.toFinset (_ : Set.Finite t)
⊢ ∃ r, n < ncard r ∧ (r ⊆ s ∨ r ⊆ t)
[PROOFSTEP]
exact ⟨r', by simpa, by simpa using hr'⟩
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
hu : Set.Finite (s ∪ t)
hst : 2 * n < Finset.card (Finite.toFinset (_ : Set.Finite s) ∪ Finite.toFinset (_ : Set.Finite t))
r' : Finset α
hnr' : n < Finset.card r'
hr' : r' ⊆ Finite.toFinset (_ : Set.Finite s) ∨ r' ⊆ Finite.toFinset (_ : Set.Finite t)
⊢ n < ncard ↑r'
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
hu : Set.Finite (s ∪ t)
hst : 2 * n < Finset.card (Finite.toFinset (_ : Set.Finite s) ∪ Finite.toFinset (_ : Set.Finite t))
r' : Finset α
hnr' : n < Finset.card r'
hr' : r' ⊆ Finite.toFinset (_ : Set.Finite s) ∨ r' ⊆ Finite.toFinset (_ : Set.Finite t)
⊢ ↑r' ⊆ s ∨ ↑r' ⊆ t
[PROOFSTEP]
simpa using hr'
[GOAL]
α : Type u_1
s t : Set α
⊢ ncard s = 1 ↔ ∃ a, s = {a}
[PROOFSTEP]
refine' ⟨fun h ↦ _, by rintro ⟨a, rfl⟩; rw [ncard_singleton]⟩
[GOAL]
α : Type u_1
s t : Set α
⊢ (∃ a, s = {a}) → ncard s = 1
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro
α : Type u_1
t : Set α
a : α
⊢ ncard {a} = 1
[PROOFSTEP]
rw [ncard_singleton]
[GOAL]
α : Type u_1
s t : Set α
h : ncard s = 1
⊢ ∃ a, s = {a}
[PROOFSTEP]
have hft := (finite_of_ncard_ne_zero (ne_zero_of_eq_one h)).fintype
[GOAL]
α : Type u_1
s t : Set α
h : ncard s = 1
hft : Fintype ↑s
⊢ ∃ a, s = {a}
[PROOFSTEP]
simp_rw [ncard_eq_toFinset_card', @Finset.card_eq_one _ (toFinset s)] at h 
[GOAL]
α : Type u_1
s t : Set α
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
⊢ ∃ a, s = {a}
[PROOFSTEP]
refine' h.imp fun a ha ↦ _
[GOAL]
α : Type u_1
s t : Set α
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
a : α
ha : toFinset s = {a}
⊢ s = {a}
[PROOFSTEP]
simp_rw [Set.ext_iff, mem_singleton_iff]
[GOAL]
α : Type u_1
s t : Set α
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
a : α
ha : toFinset s = {a}
⊢ ∀ (x : α), x ∈ s ↔ x = a
[PROOFSTEP]
simp only [Finset.ext_iff, mem_toFinset, Finset.mem_singleton] at ha 
[GOAL]
α : Type u_1
s t : Set α
hft : Fintype ↑s
h : ∃ a, toFinset s = {a}
a : α
ha : ∀ (a_1 : α), a_1 ∈ s ↔ a_1 = a
⊢ ∀ (x : α), x ∈ s ↔ x = a
[PROOFSTEP]
exact ha
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ (∃ a x, insert a s = t) ↔ s ⊆ t ∧ ncard s + 1 = ncard t
[PROOFSTEP]
classical
cases' t.finite_or_infinite with ht ht
· rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht, ← @Finite.toFinset_subset_toFinset _ _ _ hs ht, ←
    Finset.exists_eq_insert_iff]
  convert Iff.rfl using 2; simp
  ext x
  simp [Finset.ext_iff, Set.ext_iff]
simp only [ht.ncard, exists_prop, add_eq_zero, and_false, iff_false, not_exists, not_and]
rintro x - rfl
exact ht (hs.insert x)
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ (∃ a x, insert a s = t) ↔ s ⊆ t ∧ ncard s + 1 = ncard t
[PROOFSTEP]
cases' t.finite_or_infinite with ht ht
[GOAL]
case inl
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : Set.Finite t
⊢ (∃ a x, insert a s = t) ↔ s ⊆ t ∧ ncard s + 1 = ncard t
[PROOFSTEP]
rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht, ← @Finite.toFinset_subset_toFinset _ _ _ hs ht, ←
  Finset.exists_eq_insert_iff]
[GOAL]
case inl
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : Set.Finite t
⊢ (∃ a x, insert a s = t) ↔ ∃ a x, insert a (Finite.toFinset hs) = Finite.toFinset ht
[PROOFSTEP]
convert Iff.rfl using 2
[GOAL]
case h.e'_2.h.e'_2
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : Set.Finite t
⊢ (fun a => ∃ x, insert a (Finite.toFinset hs) = Finite.toFinset ht) = fun a => ∃ x, insert a s = t
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h.e'_2
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : Set.Finite t
⊢ (fun a => ¬a ∈ s ∧ insert a (Finite.toFinset hs) = Finite.toFinset ht) = fun a => ¬a ∈ s ∧ insert a s = t
[PROOFSTEP]
ext x
[GOAL]
case h.e'_2.h.e'_2.h.a
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : Set.Finite t
x : α
⊢ ¬x ∈ s ∧ insert x (Finite.toFinset hs) = Finite.toFinset ht ↔ ¬x ∈ s ∧ insert x s = t
[PROOFSTEP]
simp [Finset.ext_iff, Set.ext_iff]
[GOAL]
case inr
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : Set.Infinite t
⊢ (∃ a x, insert a s = t) ↔ s ⊆ t ∧ ncard s + 1 = ncard t
[PROOFSTEP]
simp only [ht.ncard, exists_prop, add_eq_zero, and_false, iff_false, not_exists, not_and]
[GOAL]
case inr
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
ht : Set.Infinite t
⊢ ∀ (x : α), ¬x ∈ s → ¬insert x s = t
[PROOFSTEP]
rintro x - rfl
[GOAL]
case inr
α : Type u_1
s : Set α
hs : autoParam (Set.Finite s) _auto✝
x : α
ht : Set.Infinite (insert x s)
⊢ False
[PROOFSTEP]
exact ht (hs.insert x)
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s ≤ 1 ↔ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b
[PROOFSTEP]
simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one, Finite.mem_toFinset]
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
[PROOFSTEP]
rw [ncard_le_one hs]
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a = b) ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}
[PROOFSTEP]
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
[GOAL]
case inl
α : Type u_1
t : Set α
hs : autoParam (Set.Finite ∅) _auto✝
⊢ ncard ∅ ≤ 1 ↔ ∅ = ∅ ∨ ∃ a, ∅ = {a}
[PROOFSTEP]
exact iff_of_true (by simp) (Or.inl rfl)
[GOAL]
α : Type u_1
t : Set α
hs : autoParam (Set.Finite ∅) _auto✝
⊢ ncard ∅ ≤ 1
[PROOFSTEP]
simp
[GOAL]
case inr.intro
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
x : α
hx : x ∈ s
⊢ ncard s ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}
[PROOFSTEP]
rw [ncard_le_one_iff hs]
[GOAL]
case inr.intro
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
x : α
hx : x ∈ s
⊢ (∀ {a b : α}, a ∈ s → b ∈ s → a = b) ↔ s = ∅ ∨ ∃ a, s = {a}
[PROOFSTEP]
refine' ⟨fun h ↦ Or.inr ⟨x, (singleton_subset_iff.mpr hx).antisymm' fun y hy ↦ h hy hx⟩, _⟩
[GOAL]
case inr.intro
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
x : α
hx : x ∈ s
⊢ (s = ∅ ∨ ∃ a, s = {a}) → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
[PROOFSTEP]
rintro (rfl | ⟨a, rfl⟩)
[GOAL]
case inr.intro.inl
α : Type u_1
t : Set α
x : α
hs : autoParam (Set.Finite ∅) _auto✝
hx : x ∈ ∅
⊢ ∀ {a b : α}, a ∈ ∅ → b ∈ ∅ → a = b
[PROOFSTEP]
exact (not_mem_empty _ hx).elim
[GOAL]
case inr.intro.inr.intro
α : Type u_1
t : Set α
x a : α
hs : autoParam (Set.Finite {a}) _auto✝
hx : x ∈ {a}
⊢ ∀ {a_1 b : α}, a_1 ∈ {a} → b ∈ {a} → a_1 = b
[PROOFSTEP]
simp_rw [mem_singleton_iff] at hx ⊢
[GOAL]
case inr.intro.inr.intro
α : Type u_1
t : Set α
x a : α
hs : autoParam (Set.Finite {a}) _auto✝
hx : x = a
⊢ ∀ {a_1 b : α}, a_1 = a → b = a → a_1 = b
[PROOFSTEP]
subst hx
[GOAL]
case inr.intro.inr.intro
α : Type u_1
t : Set α
x : α
hs : autoParam (Set.Finite {x}) _auto✝
⊢ ∀ {a b : α}, a = x → b = x → a = b
[PROOFSTEP]
simp only [forall_eq_apply_imp_iff', imp_self, implies_true]
[GOAL]
α : Type u_1
s t : Set α
inst✝ : Nonempty α
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s ≤ 1 ↔ ∃ x, s ⊆ {x}
[PROOFSTEP]
simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one_iff_subset_singleton, Finite.toFinset_subset,
  Finset.coe_singleton]
[GOAL]
α : Type u_1
s✝ t : Set α
inst✝ : Subsingleton α
s : Set α
⊢ ncard s ≤ 1
[PROOFSTEP]
rw [ncard_eq_toFinset_card]
[GOAL]
α : Type u_1
s✝ t : Set α
inst✝ : Subsingleton α
s : Set α
⊢ Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ 1
[PROOFSTEP]
exact Finset.card_le_one_of_subsingleton _
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ 1 < ncard s ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ a ≠ b
[PROOFSTEP]
simp_rw [ncard_eq_toFinset_card _ hs, Finset.one_lt_card, Finite.mem_toFinset]
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ 1 < ncard s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
[PROOFSTEP]
rw [one_lt_ncard hs]
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ (∃ 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
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ 2 < ncard s ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
simp_rw [ncard_eq_toFinset_card _ hs, Finset.two_lt_card_iff, Finite.mem_toFinset]
[GOAL]
α : Type u_1
s t : Set α
hs : autoParam (Set.Finite s) _auto✝
⊢ 2 < ncard s ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ s ∧ ∃ c, c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
[PROOFSTEP]
simp only [two_lt_ncard_iff hs, exists_and_left, exists_prop]
[GOAL]
α : Type u_1
s t : Set α
hs : 1 < ncard s
a : α
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
have hsf := (finite_of_ncard_ne_zero (zero_lt_one.trans hs).ne.symm)
[GOAL]
α : Type u_1
s t : Set α
hs : 1 < ncard s
a : α
hsf : Set.Finite s
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
rw [ncard_eq_toFinset_card _ hsf] at hs 
[GOAL]
α : Type u_1
s t : Set α
a : α
hsf : Set.Finite s
hs : 1 < Finset.card (Finite.toFinset hsf)
⊢ ∃ b, b ∈ s ∧ b ≠ a
[PROOFSTEP]
simpa only [Finite.mem_toFinset] using Finset.exists_ne_of_one_lt_card hs a
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
h : ncard s = n + 1
⊢ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ncard t = n
[PROOFSTEP]
classical
have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h 
obtain ⟨a, t, hat, hts, rfl⟩ := h
simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts 
refine' ⟨a, t, hat, _, _⟩
· simp only [Finset.mem_coe, ext_iff, mem_insert_iff]
  tauto
simp
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
h : ncard s = n + 1
⊢ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ncard t = n
[PROOFSTEP]
have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
h : ncard s = n + 1
hsf : Set.Finite s
⊢ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ncard t = n
[PROOFSTEP]
rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h 
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
hsf : Set.Finite s
h✝ : Finset.card (Finite.toFinset hsf) = n + 1
h : ∃ a t, ¬a ∈ t ∧ insert a t = Finite.toFinset hsf ∧ Finset.card t = n
⊢ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ncard t = n
[PROOFSTEP]
obtain ⟨a, t, hat, hts, rfl⟩ := h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
s t✝ : Set α
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
hts : insert a t = Finite.toFinset hsf
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
⊢ ∃ a t_1, ¬a ∈ t_1 ∧ insert a t_1 = s ∧ ncard t_1 = Finset.card t
[PROOFSTEP]
simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts 
[GOAL]
case intro.intro.intro.intro
α : Type u_1
s t✝ : Set α
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ∃ a t_1, ¬a ∈ t_1 ∧ insert a t_1 = s ∧ ncard t_1 = Finset.card t
[PROOFSTEP]
refine' ⟨a, t, hat, _, _⟩
[GOAL]
case intro.intro.intro.intro.refine'_1
α : Type u_1
s t✝ : Set α
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ insert a ↑t = s
[PROOFSTEP]
simp only [Finset.mem_coe, ext_iff, mem_insert_iff]
[GOAL]
case intro.intro.intro.intro.refine'_1
α : Type u_1
s t✝ : Set α
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ∀ (x : α), x = a ∨ x ∈ t ↔ x ∈ s
[PROOFSTEP]
tauto
[GOAL]
case intro.intro.intro.intro.refine'_2
α : Type u_1
s t✝ : Set α
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ncard ↑t = Finset.card t
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
hs : autoParam (Set.Finite s) _auto✝
⊢ ncard s = n + 1 ↔ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ncard t = n
[PROOFSTEP]
refine' ⟨eq_insert_of_ncard_eq_succ, _⟩
[GOAL]
α : Type u_1
s t : Set α
n : ℕ
hs : autoParam (Set.Finite s) _auto✝
⊢ (∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ncard t = n) → ncard s = n + 1
[PROOFSTEP]
rintro ⟨a, t, hat, h, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
s t✝ : Set α
hs : autoParam (Set.Finite s) _auto✝
a : α
t : Set α
hat : ¬a ∈ t
h : insert a t = s
⊢ ncard s = ncard t + 1
[PROOFSTEP]
rw [← h, ncard_insert_of_not_mem hat (hs.subset ((subset_insert a t).trans_eq h))]
[GOAL]
α : Type u_1
s t : Set α
⊢ ncard s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
[PROOFSTEP]
rw [← encard_eq_two, ncard_def, ← Nat.cast_inj (R := ℕ∞), Nat.cast_ofNat]
[GOAL]
α : Type u_1
s t : Set α
⊢ ↑(↑ENat.toNat (encard s)) = 2 ↔ encard s = 2
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun h ↦ _⟩
[GOAL]
case refine'_1
α : Type u_1
s t : Set α
h : ↑(↑ENat.toNat (encard s)) = 2
⊢ encard s = 2
[PROOFSTEP]
rwa [ENat.coe_toNat] at h 
[GOAL]
case refine'_1
α : Type u_1
s t : Set α
h : ↑(↑ENat.toNat (encard s)) = 2
⊢ encard s ≠ ⊤
[PROOFSTEP]
rintro h'
[GOAL]
case refine'_1
α : Type u_1
s t : Set α
h : ↑(↑ENat.toNat (encard s)) = 2
h' : encard s = ⊤
⊢ False
[PROOFSTEP]
simp [h'] at h 
[GOAL]
case refine'_2
α : Type u_1
s t : Set α
h : encard s = 2
⊢ ↑(↑ENat.toNat (encard s)) = 2
[PROOFSTEP]
simp [h]
[GOAL]
case refine'_2
α : Type u_1
s t : Set α
h : encard s = 2
⊢ ¬2 = ⊤
[PROOFSTEP]
exact Iff.mp ENat.coe_toNat_eq_self rfl
[GOAL]
α : Type u_1
s t : Set α
⊢ ncard s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
[PROOFSTEP]
rw [← encard_eq_three, ncard_def, ← Nat.cast_inj (R := ℕ∞), Nat.cast_ofNat]
[GOAL]
α : Type u_1
s t : Set α
⊢ ↑(↑ENat.toNat (encard s)) = 3 ↔ encard s = 3
[PROOFSTEP]
refine' ⟨fun h ↦ _, fun h ↦ _⟩
[GOAL]
case refine'_1
α : Type u_1
s t : Set α
h : ↑(↑ENat.toNat (encard s)) = 3
⊢ encard s = 3
[PROOFSTEP]
rwa [ENat.coe_toNat] at h 
[GOAL]
case refine'_1
α : Type u_1
s t : Set α
h : ↑(↑ENat.toNat (encard s)) = 3
⊢ encard s ≠ ⊤
[PROOFSTEP]
rintro h'
[GOAL]
case refine'_1
α : Type u_1
s t : Set α
h : ↑(↑ENat.toNat (encard s)) = 3
h' : encard s = ⊤
⊢ False
[PROOFSTEP]
simp [h'] at h 
[GOAL]
case refine'_2
α : Type u_1
s t : Set α
h : encard s = 3
⊢ ↑(↑ENat.toNat (encard s)) = 3
[PROOFSTEP]
simp [h]
[GOAL]
case refine'_2
α : Type u_1
s t : Set α
h : encard s = 3
⊢ ¬3 = ⊤
[PROOFSTEP]
exact Iff.mp ENat.coe_toNat_eq_self rfl
