Cardinality of sets

Analysis I, Section 3.6: Cardinality of sets

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Cardinality of a set
Finite and infinite sets
Connections with Mathlib equivalents

After this section, these notions will be deprecated in favor of their Mathlib equivalents.

Tips from past users

Users of the companion who have completed the exercises in this section are welcome to send their tips for future users in this section as PRs.

(Add tip here)

namespace Chapter3export SetTheory (Set Object nat)variable [SetTheory]

Definition 3.6.1 (Equal cardinality)

abbrev SetTheory.Set.EqualCard (X Y:Set) : Prop := ∃ f : X → Y, Function.Bijective f

Example 3.6.2

theorem SetTheory.Set.Example_3_6_2 : EqualCard {0,1,2} {3,4,5} := byinst✝:SetTheory⊢ {0, 1, 2}.EqualCard {3, 4, 5}
  use open Classical in fun x ↦
    ⟨if x.val = 0 then 3 else if x.val = 1 then 4 else 5, byinst✝:SetTheoryx:{0, 1, 2}.toSubtype⊢ (if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5) ∈ {3, 4, 5} aesopAll goals completed! 🐙⟩
  constructorh.leftinst✝:SetTheory⊢ Function.Injective fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩h.rightinst✝:SetTheory⊢ Function.Surjective fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩
  ·h.leftinst✝:SetTheory⊢ Function.Injective fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩ introh.leftinst✝:SetTheorya₁✝:{0, 1, 2}.toSubtype⊢ ∀ ⦃a₂ : {0, 1, 2}.toSubtype⦄,
  (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a₁✝ =
      (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a₂ →
    a₁✝ = a₂; aesopAll goals completed! 🐙
  intro yh.rightinst✝:SetTheoryy:{3, 4, 5}.toSubtype⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = y
  have : y = (3: Object) ∨ y = (4: Object) ∨ y = (5: Object) := byinst✝:SetTheory⊢ {0, 1, 2}.EqualCard {3, 4, 5}
    have := y.propertyinst✝:SetTheoryy:{3, 4, 5}.toSubtypethis:↑y ∈ {3, 4, 5} := y.property⊢ ↑y = 3 ∨ ↑y = 4 ∨ ↑y = 5
    aesopAll goals completed! 🐙
  rcases this with (_ | _ | _)h.right.inlinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 3⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = yh.right.inr.inlinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 4⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = yh.right.inr.inrinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 5⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = y
  ·h.right.inlinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 3⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = y use ⟨0, byinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 3⊢ 0 ∈ {0, 1, 2} simpAll goals completed! 🐙⟩; aesopAll goals completed! 🐙
  ·h.right.inr.inlinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 4⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = y use ⟨1, byinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 4⊢ 1 ∈ {0, 1, 2} simpAll goals completed! 🐙⟩; aesopAll goals completed! 🐙
  ·h.right.inr.inrinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 5⊢ ∃ a, (fun x => ⟨if ↑x = 0 then 3 else if ↑x = 1 then 4 else 5, ⋯⟩) a = y use ⟨2, byinst✝:SetTheoryy:{3, 4, 5}.toSubtypeh✝:↑y = 5⊢ 2 ∈ {0, 1, 2} simpAll goals completed! 🐙⟩; aesopAll goals completed! 🐙

Example 3.6.3

theorem declaration uses `sorry`SetTheory.Set.Example_3_6_3 : EqualCard nat (nat.specify (fun x ↦ Even (x:ℕ))) := byinst✝:SetTheory⊢ nat.EqualCard (nat.specify fun x => Even (nat_equiv.symm x)) sorryAll goals completed! 🐙

@[refl]
theorem declaration uses `sorry`SetTheory.Set.EqualCard.refl (X:Set) : EqualCard X X := byinst✝:SetTheoryX:Set⊢ X.EqualCard X
  sorryAll goals completed! 🐙

@[symm]
theorem declaration uses `sorry`SetTheory.Set.EqualCard.symm {X Y:Set} (h: EqualCard X Y) : EqualCard Y X := byinst✝:SetTheoryX:SetY:Seth:X.EqualCard Y⊢ Y.EqualCard X
  sorryAll goals completed! 🐙

@[trans]
theorem declaration uses `sorry`SetTheory.Set.EqualCard.trans {X Y Z:Set} (h1: EqualCard X Y) (h2: EqualCard Y Z) : EqualCard X Z := byinst✝:SetTheoryX:SetY:SetZ:Seth1:X.EqualCard Yh2:Y.EqualCard Z⊢ X.EqualCard Z
  sorryAll goals completed! 🐙

Proposition 3.6.4 / Exercise 3.6.1

instance SetTheory.Set.EqualCard.inst_setoid : Setoid SetTheory.Set := ⟨ EqualCard, {refl, symm, trans} ⟩

Definition 3.6.5

abbrev SetTheory.Set.has_card (X:Set) (n:ℕ) : Prop := X ≈ Fin n

theorem SetTheory.Set.has_card_iff (X:Set) (n:ℕ) :
    X.has_card n ↔ ∃ f: X → Fin n, Function.Bijective f := byinst✝:SetTheoryX:Setn:ℕ⊢ X.has_card n ↔ ∃ f, Function.Bijective f
  simp [has_card, HasEquiv.Equiv, instHasEquivOfSetoid, Setoid.r, EqualCard]All goals completed! 🐙

Remark 3.6.6

theorem declaration uses `sorry`SetTheory.Set.Remark_3_6_6 (n:ℕ) :
    (nat.specify (fun x ↦ 1 ≤ (x:ℕ) ∧ (x:ℕ) ≤ n)).has_card n := byinst✝:SetTheoryn:ℕ⊢ (nat.specify fun x => 1 ≤ nat_equiv.symm x ∧ nat_equiv.symm x ≤ n).has_card n sorryAll goals completed! 🐙

Example 3.6.7

theorem SetTheory.Set.Example_3_6_7a (a:Object) : ({a}:Set).has_card 1 := byinst✝:SetTheorya:Object⊢ {a}.has_card 1
  rw [has_card_iff]inst✝:SetTheorya:Object⊢ ∃ f, Function.Bijective f
  use fun _ ↦ Fin_mk _ 0 (byinst✝:SetTheorya:Objectx✝:{a}.toSubtype⊢ 0 < 1 simpAll goals completed! 🐙)
  constructorh.leftinst✝:SetTheorya:Object⊢ Function.Injective fun x => Fin_mk 1 0 ⋯h.rightinst✝:SetTheorya:Object⊢ Function.Surjective fun x => Fin_mk 1 0 ⋯
  ·h.leftinst✝:SetTheorya:Object⊢ Function.Injective fun x => Fin_mk 1 0 ⋯ intro x1 x2h.leftinst✝:SetTheorya:Objectx1:{a}.toSubtypex2:{a}.toSubtype⊢ (fun x => Fin_mk 1 0 ⋯) x1 = (fun x => Fin_mk 1 0 ⋯) x2 → x1 = x2 hfh.leftinst✝:SetTheorya:Objectx1:{a}.toSubtypex2:{a}.toSubtypehf:(fun x => Fin_mk 1 0 ⋯) x1 = (fun x => Fin_mk 1 0 ⋯) x2⊢ x1 = x2; aesopAll goals completed! 🐙
  intro yh.rightinst✝:SetTheorya:Objecty:(Fin 1).toSubtype⊢ ∃ a_1, (fun x => Fin_mk 1 0 ⋯) a_1 = y
  use ⟨a, byinst✝:SetTheorya:Objecty:(Fin 1).toSubtype⊢ a ∈ {a} simpAll goals completed! 🐙⟩
  have := Fin.toNat_lt yhinst✝:SetTheorya:Objecty:(Fin 1).toSubtypethis:↑y < 1 := Fin.toNat_lt y⊢ (fun x => Fin_mk 1 0 ⋯) ⟨a, ⋯⟩ = y
  simp_allAll goals completed! 🐙

theorem SetTheory.Set.Example_3_6_7b {a b c d:Object} (hab: a ≠ b) (hac: a ≠ c) (had: a ≠ d)
    (hbc: b ≠ c) (hbd: b ≠ d) (hcd: c ≠ d) : ({a,b,c,d}:Set).has_card 4 := byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ {a, b, c, d}.has_card 4
  rw [has_card_iff]inst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ ∃ f, Function.Bijective f
  use open Classical in fun x ↦ Fin_mk _ (
    if x.val = a then 0 else if x.val = b then 1 else if x.val = c then 2 else 3
  ) (byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dx:{a, b, c, d}.toSubtype⊢ (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) < 4 aesopAll goals completed! 🐙)
  constructorh.leftinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ Function.Injective fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯h.rightinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ Function.Surjective fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯
  ·h.leftinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ Function.Injective fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯ intro x1 x2h.leftinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dx1:{a, b, c, d}.toSubtypex2:{a, b, c, d}.toSubtype⊢ (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) x1 =
    (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) x2 →
  x1 = x2 hfh.leftinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dx1:{a, b, c, d}.toSubtypex2:{a, b, c, d}.toSubtypehf:(fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) x1 =
  (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) x2⊢ x1 = x2; aesopAll goals completed! 🐙
  intro yh.rightinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtype⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y
  have : y = (0:ℕ) ∨ y = (1:ℕ) ∨ y = (2:ℕ) ∨ y = (3:ℕ) := byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ d⊢ {a, b, c, d}.has_card 4
    have := Fin.toNat_lt yinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypethis:↑y < 4 := Fin.toNat_lt y⊢ ↑y = 0 ∨ ↑y = 1 ∨ ↑y = 2 ∨ ↑y = 3
    omegaAll goals completed! 🐙
  rcases this with (_ | _ | _ | _)h.right.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 0⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = yh.right.inr.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 1⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = yh.right.inr.inr.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 2⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = yh.right.inr.inr.inrinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 3⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y
  ·h.right.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 0⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y use ⟨a, byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 0⊢ a ∈ {a, b, c, d} aesopAll goals completed! 🐙⟩; aesopAll goals completed! 🐙
  ·h.right.inr.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 1⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y use ⟨b, byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 1⊢ b ∈ {a, b, c, d} aesopAll goals completed! 🐙⟩; aesopAll goals completed! 🐙
  ·h.right.inr.inr.inlinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 2⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y use ⟨c, byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 2⊢ c ∈ {a, b, c, d} aesopAll goals completed! 🐙⟩; aesopAll goals completed! 🐙
  ·h.right.inr.inr.inrinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 3⊢ ∃ a_1, (fun x => Fin_mk 4 (if ↑x = a then 0 else if ↑x = b then 1 else if ↑x = c then 2 else 3) ⋯) a_1 = y use ⟨d, byinst✝:SetTheorya:Objectb:Objectc:Objectd:Objecthab:a ≠ bhac:a ≠ chad:a ≠ dhbc:b ≠ chbd:b ≠ dhcd:c ≠ dy:(Fin 4).toSubtypeh✝:↑y = 3⊢ d ∈ {a, b, c, d} aesopAll goals completed! 🐙⟩; aesopAll goals completed! 🐙

Lemma 3.6.9

theorem declaration uses `sorry`SetTheory.Set.pos_card_nonempty {n:ℕ} (h: n ≥ 1) {X:Set} (hX: X.has_card n) : X ≠ ∅ := byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card n⊢ X ≠ ∅
  -- This proof is written to follow the structure of the original text.
  by_contra! thisinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nthis:X = ∅⊢ False
  have hnon : Fin n ≠ ∅ := byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card n⊢ X ≠ ∅
    apply nonempty_of_inhabited (x := 0)inst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nthis:X = ∅⊢ 0 ∈ Fin n; rw [mem_Fin]inst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nthis:X = ∅⊢ ∃ m < n, 0 = ↑m; use 0, (byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nthis:X = ∅⊢ 0 < n omegaAll goals completed! 🐙); rflAll goals completed! 🐙
  rw [has_card_iff] at hXinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:∃ f, Function.Bijective fthis:X = ∅hnon:Fin n ≠ ∅⊢ False
  choose f hf using hXinst✝:SetTheoryn:ℕh:n ≥ 1X:Setthis:X = ∅hnon:Fin n ≠ ∅f:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective f⊢ False
  sorryAll goals completed! 🐙

-- obtain a contradiction from the fact that `f` is a bijection from the empty set to a
  -- non-empty set.

Exercise 3.6.2a

theorem declaration uses `sorry`SetTheory.Set.has_card_zero {X:Set} : X.has_card 0 ↔ X = ∅ := byinst✝:SetTheoryX:Set⊢ X.has_card 0 ↔ X = ∅ sorryAll goals completed! 🐙

Lemma 3.6.9

theorem declaration uses `sorry`SetTheory.Set.card_erase {n:ℕ} (h: n ≥ 1) {X:Set} (hX: X.has_card n) (x:X) :
    (X \ {x.val}).has_card (n-1) := byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nx:X.toSubtype⊢ (X \ {↑x}).has_card (n - 1)
  -- This proof has been rewritten from the original text to try to make it friendlier to
  -- formalize in Lean.
  rw [has_card_iff] at hXinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:∃ f, Function.Bijective fx:X.toSubtype⊢ (X \ {↑x}).has_card (n - 1); choose f hf using hXinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective f⊢ (X \ {↑x}).has_card (n - 1)
  set X' : Set := X \ {x.val}inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}⊢ X'.has_card (n - 1)
  set ι : X' → X := fun ⟨y, hy⟩ ↦ ⟨ y, byinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}x✝:X'.toSubtypey:Objecthy:y ∈ X'⊢ y ∈ X aesopAll goals completed! 🐙 ⟩
  observe hι : ∀ x:X', (ι x:Object) = xinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑x⊢ X'.has_card (n - 1)
  choose m₀ hm₀ hm₀f using (mem_Fin _ _).mp (f x).propertyinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑xm₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀⊢ X'.has_card (n - 1)
  set g : X' → Fin (n-1) := fun x' ↦
    let := Fin.toNat_lt (f (ι x'))
    let : (f (ι x'):ℕ) ≠ m₀ := byinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑xm₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis:↑(f (ι x')) < n := Fin.toNat_lt (f (ι x'))⊢ ↑(f (ι x')) ≠ m₀
      by_contra!inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑xm₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis✝:↑(f (ι x')) < n := Fin.toNat_lt (f (ι x'))this:↑(f (ι x')) = m₀⊢ False; simp [←this, Subtype.val_inj, hf.1.eq_iff, ι] at hm₀finst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑xm₀:ℕhm₀:m₀ < nx':X'.toSubtypethis✝:↑(f (ι x')) < n := Fin.toNat_lt (f (ι x'))this:↑(f (ι x')) = m₀hm₀f:x = ⟨↑x', ⋯⟩⊢ False
      have := x'.propertyinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑xm₀:ℕhm₀:m₀ < nx':X'.toSubtypethis✝¹:↑(f (ι x')) < n := Fin.toNat_lt (f (ι x'))this✝:↑(f (ι x')) = m₀hm₀f:x = ⟨↑x', ⋯⟩this:↑x' ∈ X' := x'.property⊢ False; aesopAll goals completed! 🐙
    if h' : f (ι x') < m₀ then Fin_mk _ (f (ι x')) (byinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑xm₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis✝:↑(f (ι x')) < n := Fin.toNat_lt (f (ι x'))this:↑(f (ι x')) ≠ m₀ := 
  id fun h =>
    have this := x'.property;
    Eq.ndrec (motive := fun m₀ => m₀ < n → False)
      (fun hm₀ =>
        False.elim
          (Eq.mp
            (Eq.trans
              (Eq.trans
                (congrFun'
                  (congrArg Membership.mem
                    (congrArg (sdiff X)
                      (congrArg Singleton.singleton
                        (congrArg Subtype.val
                          (id
                            (id
                              (Eq.mp
                                (Eq.trans
                                  (Eq.trans
                                    (congrArg (Eq ↑(f x))
                                      (Eq.trans (congrArg Nat.cast (Eq.symm h))
                                        (Fin.coe_toNat
                                          (f
                                            ⟨↑x',
                                              (id
                                                  (Eq.mp
                                                    (Eq.trans (mem_sdiff._simp_1 (↑x') X {↑x})
                                                      (congrArg (And (↑x' ∈ X))
                                                        (congrArg Not (mem_singleton._simp_1 ↑x' ↑x))))
                                                    x'.property)).1⟩))))
                                    card_erase._simp_2)
                                  ((fun x_0 x_1 => propext ((fun x_0 x_1 => Function.Injective.eq_iff hf.left) x_0 x_1)) x
                                    ⟨↑x',
                                      (id
                                          (Eq.mp
                                            (Eq.trans (mem_sdiff._simp_1 (↑x') X {↑x})
                                              (congrArg (And (↑x' ∈ X)) (congrArg Not (mem_singleton._simp_1 ↑x' ↑x))))
                                            x'.property)).1⟩))
                                hm₀f)))))))
                  ↑x')
                (mem_sdiff._simp_1 (↑x') X {↑x'}))
              (Eq.trans
                (congrArg (And (↑x' ∈ X))
                  (Eq.trans (congrArg Not (Eq.trans (mem_singleton._simp_1 ↑x' ↑x') (eq_self ↑x'))) not_true_eq_false))
                (and_false (↑x' ∈ X))))
            this))
      h hm₀h':↑(f (ι x')) < m₀⊢ ↑(f (ι x')) < n - 1 omegaAll goals completed! 🐙)
    else Fin_mk _ (f (ι x') - 1) (byinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑xm₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis✝:↑(f (ι x')) < n := Fin.toNat_lt (f (ι x'))this:↑(f (ι x')) ≠ m₀ := 
  id fun h =>
    have this := x'.property;
    Eq.ndrec (motive := fun m₀ => m₀ < n → False)
      (fun hm₀ =>
        False.elim
          (Eq.mp
            (Eq.trans
              (Eq.trans
                (congrFun'
                  (congrArg Membership.mem
                    (congrArg (sdiff X)
                      (congrArg Singleton.singleton
                        (congrArg Subtype.val
                          (id
                            (id
                              (Eq.mp
                                (Eq.trans
                                  (Eq.trans
                                    (congrArg (Eq ↑(f x))
                                      (Eq.trans (congrArg Nat.cast (Eq.symm h))
                                        (Fin.coe_toNat
                                          (f
                                            ⟨↑x',
                                              (id
                                                  (Eq.mp
                                                    (Eq.trans (mem_sdiff._simp_1 (↑x') X {↑x})
                                                      (congrArg (And (↑x' ∈ X))
                                                        (congrArg Not (mem_singleton._simp_1 ↑x' ↑x))))
                                                    x'.property)).1⟩))))
                                    card_erase._simp_2)
                                  ((fun x_0 x_1 => propext ((fun x_0 x_1 => Function.Injective.eq_iff hf.left) x_0 x_1)) x
                                    ⟨↑x',
                                      (id
                                          (Eq.mp
                                            (Eq.trans (mem_sdiff._simp_1 (↑x') X {↑x})
                                              (congrArg (And (↑x' ∈ X)) (congrArg Not (mem_singleton._simp_1 ↑x' ↑x))))
                                            x'.property)).1⟩))
                                hm₀f)))))))
                  ↑x')
                (mem_sdiff._simp_1 (↑x') X {↑x'}))
              (Eq.trans
                (congrArg (And (↑x' ∈ X))
                  (Eq.trans (congrArg Not (Eq.trans (mem_singleton._simp_1 ↑x' ↑x') (eq_self ↑x'))) not_true_eq_false))
                (and_false (↑x' ∈ X))))
            this))
      h hm₀h':¬↑(f (ι x')) < m₀⊢ ↑(f (ι x')) - 1 < n - 1 omegaAll goals completed! 🐙)
  have hg_def (x':X') : if (f (ι x'):ℕ) < m₀ then (g x':ℕ) = f (ι x') else (g x':ℕ) = f (ι x') - 1 := byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nx:X.toSubtype⊢ (X \ {↑x}).has_card (n - 1)
    split_ifs with h'posinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑xm₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:X'.toSubtype → (Fin (n - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(f (ι x')) < m₀ then Fin_mk (n - 1) ↑(f (ι x')) ⋯ else Fin_mk (n - 1) (↑(f (ι x')) - 1) ⋯x':X'.toSubtypeh':↑(f (ι x')) < m₀⊢ ↑(g x') = ↑(f (ι x'))neginst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑xm₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:X'.toSubtype → (Fin (n - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(f (ι x')) < m₀ then Fin_mk (n - 1) ↑(f (ι x')) ⋯ else Fin_mk (n - 1) (↑(f (ι x')) - 1) ⋯x':X'.toSubtypeh':¬↑(f (ι x')) < m₀⊢ ↑(g x') = ↑(f (ι x')) - 1 <;>posinst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑xm₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:X'.toSubtype → (Fin (n - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(f (ι x')) < m₀ then Fin_mk (n - 1) ↑(f (ι x')) ⋯ else Fin_mk (n - 1) (↑(f (ι x')) - 1) ⋯x':X'.toSubtypeh':↑(f (ι x')) < m₀⊢ ↑(g x') = ↑(f (ι x'))neginst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Set := X \ {↑x}ι:X'.toSubtype → X.toSubtype := 
  fun x_1 =>
    match x_1 with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (x : X'.toSubtype), ↑(ι x) = ↑xm₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:X'.toSubtype → (Fin (n - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(f (ι x')) < m₀ then Fin_mk (n - 1) ↑(f (ι x')) ⋯ else Fin_mk (n - 1) (↑(f (ι x')) - 1) ⋯x':X'.toSubtypeh':¬↑(f (ι x')) < m₀⊢ ↑(g x') = ↑(f (ι x')) - 1 simp [g,h']All goals completed! 🐙
  have hg : Function.Bijective g := byinst✝:SetTheoryn:ℕh:n ≥ 1X:SethX:X.has_card nx:X.toSubtype⊢ (X \ {↑x}).has_card (n - 1) sorryAll goals completed! 🐙
  use gAll goals completed! 🐙

Proposition 3.6.8 (Uniqueness of cardinality)

theorem SetTheory.Set.card_uniq {X:Set} {n m:ℕ} (h1: X.has_card n) (h2: X.has_card m) : n = m := byinst✝:SetTheoryX:Setn:ℕm:ℕh1:X.has_card nh2:X.has_card m⊢ n = m
  -- This proof is written to follow the structure of the original text.
  revert X minst✝:SetTheoryn:ℕ⊢ ∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = m; induction' n with n hnzeroinst✝:SetTheory⊢ ∀ {X : Set} {m : ℕ}, X.has_card 0 → X.has_card m → 0 = msuccinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = m⊢ ∀ {X : Set} {m : ℕ}, X.has_card (n + 1) → X.has_card m → n + 1 = m
  .zeroinst✝:SetTheory⊢ ∀ {X : Set} {m : ℕ}, X.has_card 0 → X.has_card m → 0 = m intro _ _zeroinst✝:SetTheoryX✝:Setm✝:ℕ⊢ X✝.has_card 0 → X✝.has_card m✝ → 0 = m✝ h1zeroinst✝:SetTheoryX✝:Setm✝:ℕh1:X✝.has_card 0⊢ X✝.has_card m✝ → 0 = m✝ h2zeroinst✝:SetTheoryX✝:Setm✝:ℕh1:X✝.has_card 0h2:X✝.has_card m✝⊢ 0 = m✝; rw [has_card_zero] at h1zeroinst✝:SetTheoryX✝:Setm✝:ℕh1:X✝ = ∅h2:X✝.has_card m✝⊢ 0 = m✝; contrapose! h1zeroinst✝:SetTheoryX✝:Setm✝:ℕh2:X✝.has_card m✝h1:0 ≠ m✝⊢ X✝ ≠ ∅
    apply pos_card_nonempty _ h2inst✝:SetTheoryX✝:Setm✝:ℕh2:X✝.has_card m✝h1:0 ≠ m✝⊢ m✝ ≥ 1; omegaAll goals completed! 🐙
  intro X msuccinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕ⊢ X.has_card (n + 1) → X.has_card m → n + 1 = m h1succinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)⊢ X.has_card m → n + 1 = m h2succinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card m⊢ n + 1 = m
  have : X ≠ ∅ := pos_card_nonempty (byinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card m⊢ n + 1 ≥ 1 omegaAll goals completed! 🐙) h1
  choose x hx using nonempty_def thissuccinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis:X ≠ ∅ := pos_card_nonempty (Decidable.byContradiction fun a => card_uniq._proof_2 n a) h1x:Objecthx:x ∈ X⊢ n + 1 = m
  have : m ≠ 0 := byinst✝:SetTheoryX:Setn:ℕm:ℕh1:X.has_card nh2:X.has_card m⊢ n = m contrapose! thisinst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mx:Objecthx:x ∈ Xthis:m = 0⊢ X = ∅; simpa [has_card_zero, this] using h2All goals completed! 🐙
  specialize hn (card_erase ?_ h1 ⟨ _, hx ⟩) (card_erase ?_ h2 ⟨ _, hx ⟩)succ.specialize_1inst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:X ≠ ∅ := pos_card_nonempty (Decidable.byContradiction fun a => card_uniq._proof_2 n a) h1x:Objecthx:x ∈ Xthis:m ≠ 0 := 
  Mathlib.Tactic.Contrapose.contrapose₄ (fun this => Eq.mp (Eq.trans (congrArg X.has_card this) card_uniq._simp_2) h2)
    this✝⊢ n + 1 ≥ 1succ.specialize_2inst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:X ≠ ∅ := pos_card_nonempty (Decidable.byContradiction fun a => card_uniq._proof_2 n a) h1x:Objecthx:x ∈ Xthis:m ≠ 0 := 
  Mathlib.Tactic.Contrapose.contrapose₄ (fun this => Eq.mp (Eq.trans (congrArg X.has_card this) card_uniq._simp_2) h2)
    this✝⊢ m ≥ 1succinst✝:SetTheoryn:ℕX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:X ≠ ∅ := pos_card_nonempty (Decidable.byContradiction fun a => card_uniq._proof_2 n a) h1x:Objecthx:x ∈ Xthis:m ≠ 0 := 
  Mathlib.Tactic.Contrapose.contrapose₄ (fun this => Eq.mp (Eq.trans (congrArg X.has_card this) card_uniq._simp_2) h2)
    this✝hn:n = m - 1⊢ n + 1 = m <;>succ.specialize_1inst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:X ≠ ∅ := pos_card_nonempty (Decidable.byContradiction fun a => card_uniq._proof_2 n a) h1x:Objecthx:x ∈ Xthis:m ≠ 0 := 
  Mathlib.Tactic.Contrapose.contrapose₄ (fun this => Eq.mp (Eq.trans (congrArg X.has_card this) card_uniq._simp_2) h2)
    this✝⊢ n + 1 ≥ 1succ.specialize_2inst✝:SetTheoryn:ℕhn:∀ {X : Set} {m : ℕ}, X.has_card n → X.has_card m → n = mX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:X ≠ ∅ := pos_card_nonempty (Decidable.byContradiction fun a => card_uniq._proof_2 n a) h1x:Objecthx:x ∈ Xthis:m ≠ 0 := 
  Mathlib.Tactic.Contrapose.contrapose₄ (fun this => Eq.mp (Eq.trans (congrArg X.has_card this) card_uniq._simp_2) h2)
    this✝⊢ m ≥ 1succinst✝:SetTheoryn:ℕX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:X ≠ ∅ := pos_card_nonempty (Decidable.byContradiction fun a => card_uniq._proof_2 n a) h1x:Objecthx:x ∈ Xthis:m ≠ 0 := 
  Mathlib.Tactic.Contrapose.contrapose₄ (fun this => Eq.mp (Eq.trans (congrArg X.has_card this) card_uniq._simp_2) h2)
    this✝hn:n = m - 1⊢ n + 1 = m omegaAll goals completed! 🐙

lemma SetTheory.Set.Example_3_6_8_a: ({0,1,2}:Set).has_card 3 := byinst✝:SetTheory⊢ {0, 1, 2}.has_card 3
  rw [has_card_iff]inst✝:SetTheory⊢ ∃ f, Function.Bijective f
  have : ({0, 1, 2}: Set) = SetTheory.Set.Fin 3 := byinst✝:SetTheory⊢ {0, 1, 2}.has_card 3
    ext xhinst✝:SetTheoryx:Object⊢ x ∈ {0, 1, 2} ↔ x ∈ Fin 3
    simp only [mem_insert, mem_singleton, mem_Fin]hinst✝:SetTheoryx:Object⊢ x = 0 ∨ x = 1 ∨ x = 2 ↔ ∃ m < 3, x = ↑m
    constructorh.mpinst✝:SetTheoryx:Object⊢ x = 0 ∨ x = 1 ∨ x = 2 → ∃ m < 3, x = ↑mh.mprinst✝:SetTheoryx:Object⊢ (∃ m < 3, x = ↑m) → x = 0 ∨ x = 1 ∨ x = 2
    ·h.mpinst✝:SetTheoryx:Object⊢ x = 0 ∨ x = 1 ∨ x = 2 → ∃ m < 3, x = ↑m aesopAll goals completed! 🐙
    rintro ⟨x, ⟨_, rfl⟩⟩h.mprinst✝:SetTheoryx:ℕleft✝:x < 3⊢ ↑x = 0 ∨ ↑x = 1 ∨ ↑x = 2
    simp only [nat_coe_eq_iff]h.mprinst✝:SetTheoryx:ℕleft✝:x < 3⊢ x = 0 ∨ x = 1 ∨ x = 2
    omegaAll goals completed! 🐙
  rw [this]inst✝:SetTheorythis:{0, 1, 2} = Fin 3 := 
  ext fun x =>
    Eq.mpr
      (id
        (congr
          (congrArg Iff
            (Eq.trans (Example_3_6_8_a._simp_1 x 0 {1, 2})
              (congrArg (Or (x = 0))
                (Eq.trans (Example_3_6_8_a._simp_1 x 1 {2}) (congrArg (Or (x = 1)) (Example_3_6_8_a._simp_2 x 2))))))
          (Example_3_6_8_a._simp_3 3 x)))
      {
        mp := fun a =>
          Or.casesOn a (fun h => Eq.symm h ▸ Exists.intro 0 ⟨id (of_eq_true Nat.ofNat_pos._simp_1), Eq.refl 0⟩) fun h_1 =>
            Or.casesOn h_1 (fun h => Eq.symm h ▸ Exists.intro 1 ⟨id (of_eq_true Nat.one_lt_ofNat._simp_1), Eq.refl 1⟩)
              fun h_2 => Eq.symm h_2 ▸ Exists.intro 2 ⟨id (of_eq_true (Nat.lt_add_one._simp_1 2)), Eq.refl 2⟩,
        mpr := fun a =>
          Exists.casesOn a fun x_1 h =>
            And.casesOn h fun left right =>
              Eq.symm right ▸
                Eq.mpr
                  (id
                    (congr (congrArg Or Example_3_6_8_a._simp_4)
                      (congr (congrArg Or Example_3_6_8_a._simp_4) Example_3_6_8_a._simp_4)))
                  (Decidable.byContradiction fun a => Example_3_6_8_a._proof_4 x_1 left a) }⊢ ∃ f, Function.Bijective f
  use idhinst✝:SetTheorythis:{0, 1, 2} = Fin 3 := 
  ext fun x =>
    Eq.mpr
      (id
        (congr
          (congrArg Iff
            (Eq.trans (Example_3_6_8_a._simp_1 x 0 {1, 2})
              (congrArg (Or (x = 0))
                (Eq.trans (Example_3_6_8_a._simp_1 x 1 {2}) (congrArg (Or (x = 1)) (Example_3_6_8_a._simp_2 x 2))))))
          (Example_3_6_8_a._simp_3 3 x)))
      {
        mp := fun a =>
          Or.casesOn a (fun h => Eq.symm h ▸ Exists.intro 0 ⟨id (of_eq_true Nat.ofNat_pos._simp_1), Eq.refl 0⟩) fun h_1 =>
            Or.casesOn h_1 (fun h => Eq.symm h ▸ Exists.intro 1 ⟨id (of_eq_true Nat.one_lt_ofNat._simp_1), Eq.refl 1⟩)
              fun h_2 => Eq.symm h_2 ▸ Exists.intro 2 ⟨id (of_eq_true (Nat.lt_add_one._simp_1 2)), Eq.refl 2⟩,
        mpr := fun a =>
          Exists.casesOn a fun x_1 h =>
            And.casesOn h fun left right =>
              Eq.symm right ▸
                Eq.mpr
                  (id
                    (congr (congrArg Or Example_3_6_8_a._simp_4)
                      (congr (congrArg Or Example_3_6_8_a._simp_4) Example_3_6_8_a._simp_4)))
                  (Decidable.byContradiction fun a => Example_3_6_8_a._proof_4 x_1 left a) }⊢ Function.Bijective id
  exact Function.bijective_idAll goals completed! 🐙

lemma SetTheory.Set.Example_3_6_8_b: ({3,4}:Set).has_card 2 := byinst✝:SetTheory⊢ {3, 4}.has_card 2
  rw [has_card_iff]inst✝:SetTheory⊢ ∃ f, Function.Bijective f
  use open Classical in fun x ↦ Fin_mk _ (if x = (3:Object) then 0 else 1) (byinst✝:SetTheoryx:{3, 4}.toSubtype⊢ (if ↑x = 3 then 0 else 1) < 2 aesopAll goals completed! 🐙)
  constructorh.leftinst✝:SetTheory⊢ Function.Injective fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯h.rightinst✝:SetTheory⊢ Function.Surjective fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯
  ·h.leftinst✝:SetTheory⊢ Function.Injective fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯ intro x1 x2h.leftinst✝:SetTheoryx1:{3, 4}.toSubtypex2:{3, 4}.toSubtype⊢ (fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯) x1 = (fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯) x2 → x1 = x2
    aesopAll goals completed! 🐙
  intro yh.rightinst✝:SetTheoryy:(Fin 2).toSubtype⊢ ∃ a, (fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯) a = y
  have := Fin.toNat_lt yh.rightinst✝:SetTheoryy:(Fin 2).toSubtypethis:↑y < 2 := Fin.toNat_lt y⊢ ∃ a, (fun x => Fin_mk 2 (if ↑x = 3 then 0 else 1) ⋯) a = y
  have : y = (0:ℕ) ∨ y = (1:ℕ) := byinst✝:SetTheory⊢ {3, 4}.has_card 2 omegaAll goals completed! 🐙
  aesopAll goals completed! 🐙

lemma SetTheory.Set.Example_3_6_8_c : ¬({0,1,2}:Set) ≈ ({3,4}:Set) := byinst✝:SetTheory⊢ ¬{0, 1, 2} ≈ {3, 4}
  by_contra hinst✝:SetTheoryh:{0, 1, 2} ≈ {3, 4}⊢ False
  have h1 : Fin 3 ≈ Fin 2 := (Example_3_6_8_a.symm.trans h).trans Example_3_6_8_binst✝:SetTheoryh:{0, 1, 2} ≈ {3, 4}h1:Fin 3 ≈ Fin 2 := EqualCard.trans (EqualCard.trans (EqualCard.symm Example_3_6_8_a) h) Example_3_6_8_b⊢ False
  have h2 : Fin 3 ≈ Fin 3 := byinst✝:SetTheory⊢ ¬{0, 1, 2} ≈ {3, 4} rflAll goals completed! 🐙
  have := card_uniq h1 h2inst✝:SetTheoryh:{0, 1, 2} ≈ {3, 4}h1:Fin 3 ≈ Fin 2 := EqualCard.trans (EqualCard.trans (EqualCard.symm Example_3_6_8_a) h) Example_3_6_8_bh2:Fin 3 ≈ Fin 3 := Setoid.refl (Fin 3)this:2 = 3 := card_uniq h1 h2⊢ False
  contradictionAll goals completed! 🐙

abbrev SetTheory.Set.finite (X:Set) : Prop := ∃ n:ℕ, X.has_card nabbrev SetTheory.Set.infinite (X:Set) : Prop := ¬ finite X

Exercise 3.6.3, phrased using Mathlib natural numbers

theorem declaration uses `sorry`SetTheory.Set.bounded_on_finite {n:ℕ} (f: Fin n → nat) : ∃ M, ∀ i, (f i:ℕ) ≤ M := byinst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtype⊢ ∃ M, ∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ M sorryAll goals completed! 🐙

Theorem 3.6.12

theorem SetTheory.Set.nat_infinite : infinite nat := byinst✝:SetTheory⊢ nat.infinite
  -- This proof is written to follow the structure of the original text.
  by_contra thisinst✝:SetTheorythis:nat.finite⊢ False; choose n hn using thisinst✝:SetTheoryn:ℕhn:nat.has_card n⊢ False
  simp [has_card] at hninst✝:SetTheoryn:ℕhn:nat ≈ Fin n⊢ False; symm at hninst✝:SetTheoryn:ℕhn:Fin n ≈ nat⊢ False; simp [HasEquiv.Equiv] at hninst✝:SetTheoryn:ℕhn:instHasEquivOfSetoid.1 (Fin n) nat⊢ False
  choose f hf using hninst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypehf:Function.Bijective f⊢ False; choose M hM using bounded_on_finite finst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypehf:Function.Bijective fM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ M⊢ False
  replace hf := hf.surjective ↑(M+1)inst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypeM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ Mhf:∃ a, f a = ↑(M + 1) := Function.Bijective.surjective _fvar.339277 ↑(M + 1)⊢ False; contrapose! hfinst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypeM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ Mhf:True⊢ ∀ (a : (Fin n).toSubtype), f a ≠ ↑(M + 1)
  peel hM with hihinst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypeM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ Mhf:Truea✝:(Fin n).toSubtypehi:nat_equiv.symm (f a✝) ≤ M⊢ f a✝ ≠ ↑(M + 1); contrapose! hihinst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypeM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ Mhf:Truea✝:(Fin n).toSubtypehi:f a✝ = ↑(M + 1)⊢ M < nat_equiv.symm (f a✝)
  apply_fun nat_equiv.symm at hihinst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypeM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ Mhf:Truea✝:(Fin n).toSubtypehi:nat_equiv.symm (f a✝) = nat_equiv.symm ↑(M + 1)⊢ M < nat_equiv.symm (f a✝); simp_allAll goals completed! 🐙

open Classical in
/-- It is convenient for Lean purposes to give infinite sets the ``junk`` cardinality of zero. -/
noncomputable def SetTheory.Set.card (X:Set) : ℕ := if h:X.finite then h.choose else 0

theorem SetTheory.Set.has_card_card {X:Set} (hX: X.finite) : X.has_card (SetTheory.Set.card X) := byinst✝:SetTheoryX:SethX:X.finite⊢ X.has_card X.card
  simp [card, hX, hX.choose_spec]All goals completed! 🐙

theorem SetTheory.Set.has_card_to_card {X:Set} {n: ℕ}: X.has_card n → X.card = n := byinst✝:SetTheoryX:Setn:ℕ⊢ X.has_card n → X.card = n
  intro hinst✝:SetTheoryX:Setn:ℕh:X.has_card n⊢ X.card = n; simp [card, card_uniq (⟨ n, h ⟩:X.finite).choose_spec h]inst✝:SetTheoryX:Setn:ℕh:X.has_card n⊢ (∀ (x : ℕ), ¬X.has_card x) → 0 = n; aesopAll goals completed! 🐙

theorem SetTheory.Set.card_to_has_card {X:Set} {n: ℕ} (hn: n ≠ 0): X.card = n → X.has_card n
  := byinst✝:SetTheoryX:Setn:ℕhn:n ≠ 0⊢ X.card = n → X.has_card n grind [card, has_card_card]All goals completed! 🐙

theorem SetTheory.Set.card_fin_eq (n:ℕ): (Fin n).has_card n := (has_card_iff _ _).mp ⟨ id, Function.bijective_id ⟩theorem SetTheory.Set.Fin_card (n:ℕ): (Fin n).card = n := has_card_to_card (card_fin_eq n)theorem SetTheory.Set.Fin_finite (n:ℕ): (Fin n).finite := ⟨n, card_fin_eq n⟩

theorem SetTheory.Set.EquivCard_to_has_card_eq {X Y:Set} {n: ℕ} (h: X ≈ Y): X.has_card n ↔ Y.has_card n := byinst✝:SetTheoryX:SetY:Setn:ℕh:X ≈ Y⊢ X.has_card n ↔ Y.has_card n
  choose f hf using hinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective f⊢ X.has_card n ↔ Y.has_card n; let e := Equiv.ofBijective f hfinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hf⊢ X.has_card n ↔ Y.has_card n
  constructormpinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hf⊢ X.has_card n → Y.has_card nmprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hf⊢ Y.has_card n → X.has_card n <;>mpinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hf⊢ X.has_card n → Y.has_card nmprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hf⊢ Y.has_card n → X.has_card n (intro h'mprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hfh':Y.has_card n⊢ X.has_card n; rw [has_card_iff] at *mprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hfh':∃ f, Function.Bijective f⊢ ∃ f, Function.Bijective f; choose g hg using h'mprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hfg:Y.toSubtype → (Fin n).toSubtypehg:Function.Bijective g⊢ ∃ f, Function.Bijective f)
  .mpinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hfg:X.toSubtype → (Fin n).toSubtypehg:Function.Bijective g⊢ ∃ f, Function.Bijective f use e.symm.trans (.ofBijective _ hg)hinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hfg:X.toSubtype → (Fin n).toSubtypehg:Function.Bijective g⊢ Function.Bijective ⇑(e.symm.trans (Equiv.ofBijective g hg)); apply Equiv.bijectiveAll goals completed! 🐙
  .mprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hfg:Y.toSubtype → (Fin n).toSubtypehg:Function.Bijective g⊢ ∃ f, Function.Bijective f use e.trans (.ofBijective _ hg)hinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:X.toSubtype ≃ Y.toSubtype := Equiv.ofBijective f hfg:Y.toSubtype → (Fin n).toSubtypehg:Function.Bijective g⊢ Function.Bijective ⇑(e.trans (Equiv.ofBijective g hg)); apply Equiv.bijectiveAll goals completed! 🐙

theorem SetTheory.Set.EquivCard_to_card_eq {X Y:Set} (h: X ≈ Y): X.card = Y.card := byinst✝:SetTheoryX:SetY:Seth:X ≈ Y⊢ X.card = Y.card
  by_cases hX: X.finiteposinst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finite⊢ X.card = Y.cardneginst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finite⊢ X.card = Y.card <;>posinst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finite⊢ X.card = Y.cardneginst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finite⊢ X.card = Y.card by_cases hY: Y.finiteposinst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:Y.finite⊢ X.card = Y.cardneginst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:¬Y.finite⊢ X.card = Y.card <;>posinst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finitehY:Y.finite⊢ X.card = Y.cardneginst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finitehY:¬Y.finite⊢ X.card = Y.cardposinst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:Y.finite⊢ X.card = Y.cardneginst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:¬Y.finite⊢ X.card = Y.card try rw [finite] at hX hYneginst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬∃ n, X.has_card nhY:¬∃ n, Y.has_card n⊢ X.card = Y.card
  .posinst✝:SetTheoryX:SetY:Seth:X ≈ YhX:∃ n, X.has_card nhY:∃ n, Y.has_card n⊢ X.card = Y.card choose nX hXn using hXposinst✝:SetTheoryX:SetY:Seth:X ≈ YhY:∃ n, Y.has_card nnX:ℕhXn:X.has_card nX⊢ X.card = Y.card; choose nY hYn using hYposinst✝:SetTheoryX:SetY:Seth:X ≈ YnX:ℕhXn:X.has_card nXnY:ℕhYn:Y.has_card nY⊢ X.card = Y.card
    simp [has_card_to_card hXn, has_card_to_card hYn, EquivCard_to_has_card_eq h] at *posinst✝:SetTheoryX:SetY:Seth:X ≈ YnX:ℕnY:ℕhYn:Y.has_card nYhXn:Y.has_card nX⊢ nX = nY
    solve_by_elim [card_uniq]All goals completed! 🐙
  .neginst✝:SetTheoryX:SetY:Seth:X ≈ YhX:∃ n, X.has_card nhY:¬∃ n, Y.has_card n⊢ X.card = Y.card choose nX hXn using hXneginst✝:SetTheoryX:SetY:Seth:X ≈ YhY:¬∃ n, Y.has_card nnX:ℕhXn:X.has_card nX⊢ X.card = Y.card; rw [EquivCard_to_has_card_eq h] at hXnneginst✝:SetTheoryX:SetY:Seth:X ≈ YhY:¬∃ n, Y.has_card nnX:ℕhXn:Y.has_card nX⊢ X.card = Y.card; tautoAll goals completed! 🐙
  .posinst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬∃ n, X.has_card nhY:∃ n, Y.has_card n⊢ X.card = Y.card choose nY hYn using hYposinst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬∃ n, X.has_card nnY:ℕhYn:Y.has_card nY⊢ X.card = Y.card; rw [←EquivCard_to_has_card_eq h] at hYnposinst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬∃ n, X.has_card nnY:ℕhYn:X.has_card nY⊢ X.card = Y.card; tautoAll goals completed! 🐙
  simp [card, hX, hY]All goals completed! 🐙

Exercise 3.6.2

theorem declaration uses `sorry`SetTheory.Set.empty_iff_card_eq_zero {X:Set} : X = ∅ ↔ X.finite ∧ X.card = 0 := byinst✝:SetTheoryX:Set⊢ X = ∅ ↔ X.finite ∧ X.card = 0
  sorryAll goals completed! 🐙

lemma SetTheory.Set.empty_of_card_eq_zero {X:Set} (hX : X.finite) : X.card = 0 → X = ∅ := byinst✝:SetTheoryX:SethX:X.finite⊢ X.card = 0 → X = ∅
  intro hinst✝:SetTheoryX:SethX:X.finiteh:X.card = 0⊢ X = ∅
  rw [empty_iff_card_eq_zero]inst✝:SetTheoryX:SethX:X.finiteh:X.card = 0⊢ X.finite ∧ X.card = 0
  exact ⟨hX, h⟩All goals completed! 🐙

lemma SetTheory.Set.finite_of_empty {X:Set} : X = ∅ → X.finite := byinst✝:SetTheoryX:Set⊢ X = ∅ → X.finite
  intro hinst✝:SetTheoryX:Seth:X = ∅⊢ X.finite
  rw [empty_iff_card_eq_zero] at hinst✝:SetTheoryX:Seth:X.finite ∧ X.card = 0⊢ X.finite
  exact h.1All goals completed! 🐙

lemma SetTheory.Set.card_eq_zero_of_empty {X:Set} : X = ∅ → X.card = 0 := byinst✝:SetTheoryX:Set⊢ X = ∅ → X.card = 0
  intro hinst✝:SetTheoryX:Seth:X = ∅⊢ X.card = 0
  rw [empty_iff_card_eq_zero] at hinst✝:SetTheoryX:Seth:X.finite ∧ X.card = 0⊢ X.card = 0
  exact h.2All goals completed! 🐙

@[simp]
lemma SetTheory.Set.empty_finite : (∅: Set).finite := finite_of_empty rfl

@[simp]
lemma SetTheory.Set.empty_card_eq_zero : (∅: Set).card = 0 := card_eq_zero_of_empty rfl

Proposition 3.6.14 (a) / Exercise 3.6.4

theorem declaration uses `sorry`SetTheory.Set.card_insert {X:Set} (hX: X.finite) {x:Object} (hx: x ∉ X) :
    (X ∪ {x}).finite ∧ (X ∪ {x}).card = X.card + 1 := byinst✝:SetTheoryX:SethX:X.finitex:Objecthx:x ∉ X⊢ (X ∪ {x}).finite ∧ (X ∪ {x}).card = X.card + 1 sorryAll goals completed! 🐙

Proposition 3.6.14 (b) / Exercise 3.6.4

theorem declaration uses `sorry`SetTheory.Set.card_union {X Y:Set} (hX: X.finite) (hY: Y.finite) :
    (X ∪ Y).finite ∧ (X ∪ Y).card ≤ X.card + Y.card := byinst✝:SetTheoryX:SetY:SethX:X.finitehY:Y.finite⊢ (X ∪ Y).finite ∧ (X ∪ Y).card ≤ X.card + Y.card sorryAll goals completed! 🐙

Proposition 3.6.14 (b) / Exercise 3.6.4

theorem declaration uses `sorry`SetTheory.Set.card_union_disjoint {X Y:Set} (hX: X.finite) (hY: Y.finite)
  (hdisj: Disjoint X Y) : (X ∪ Y).card = X.card + Y.card := byinst✝:SetTheoryX:SetY:SethX:X.finitehY:Y.finitehdisj:Disjoint X Y⊢ (X ∪ Y).card = X.card + Y.card sorryAll goals completed! 🐙

Proposition 3.6.14 (c) / Exercise 3.6.4

theorem declaration uses `sorry`SetTheory.Set.card_subset {X Y:Set} (hX: X.finite) (hY: Y ⊆ X) :
    Y.finite ∧ Y.card ≤ X.card := byinst✝:SetTheoryX:SetY:SethX:X.finitehY:Y ⊆ X⊢ Y.finite ∧ Y.card ≤ X.card sorryAll goals completed! 🐙

Proposition 3.6.14 (c) / Exercise 3.6.4

theorem declaration uses `sorry`SetTheory.Set.card_ssubset {X Y:Set} (hX: X.finite) (hY: Y ⊂ X) :
    Y.card < X.card := byinst✝:SetTheoryX:SetY:SethX:X.finitehY:Y ⊂ X⊢ Y.card < X.card sorryAll goals completed! 🐙

Proposition 3.6.14 (d) / Exercise 3.6.4

theorem declaration uses `sorry`SetTheory.Set.card_image {X Y:Set} (hX: X.finite) (f: X → Y) :
    (image f X).finite ∧ (image f X).card ≤ X.card := byinst✝:SetTheoryX:SetY:SethX:X.finitef:X.toSubtype → Y.toSubtype⊢ (image f X).finite ∧ (image f X).card ≤ X.card sorryAll goals completed! 🐙

Proposition 3.6.14 (d) / Exercise 3.6.4

theorem declaration uses `sorry`SetTheory.Set.card_image_inj {X Y:Set} (hX: X.finite) {f: X → Y}
  (hf: Function.Injective f) : (image f X).card = X.card := byinst✝:SetTheoryX:SetY:SethX:X.finitef:X.toSubtype → Y.toSubtypehf:Function.Injective f⊢ (image f X).card = X.card sorryAll goals completed! 🐙

Proposition 3.6.14 (e) / Exercise 3.6.4

theorem declaration uses `sorry`SetTheory.Set.card_prod {X Y:Set} (hX: X.finite) (hY: Y.finite) :
    (X ×ˢ Y).finite ∧ (X ×ˢ Y).card = X.card * Y.card := byinst✝:SetTheoryX:SetY:SethX:X.finitehY:Y.finite⊢ (X ×ˢ Y).finite ∧ (X ×ˢ Y).card = X.card * Y.card sorryAll goals completed! 🐙

noncomputable def declaration uses `sorry`declaration uses `sorry`declaration uses `sorry`SetTheory.Set.pow_fun_equiv {A B : Set} : ↑(A ^ B) ≃ (B → A) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

lemma SetTheory.Set.pow_fun_eq_iff {A B : Set} (x y : ↑(A ^ B)) : x = y ↔ pow_fun_equiv x = pow_fun_equiv y := byinst✝:SetTheoryA:SetB:Setx:(A ^ B).toSubtypey:(A ^ B).toSubtype⊢ x = y ↔ pow_fun_equiv x = pow_fun_equiv y
  rw [←pow_fun_equiv.apply_eq_iff_eq]All goals completed! 🐙

Proposition 3.6.14 (f) / Exercise 3.6.4

theorem declaration uses `sorry`SetTheory.Set.card_pow {X Y:Set} (hY: Y.finite) (hX: X.finite) :
    (Y ^ X).finite ∧ (Y ^ X).card = Y.card ^ X.card := byinst✝:SetTheoryX:SetY:SethY:Y.finitehX:X.finite⊢ (Y ^ X).finite ∧ (Y ^ X).card = Y.card ^ X.card sorryAll goals completed! 🐙

Exercise 3.6.5. You might find Chapter3.SetTheory.Set.prod_commutator.{u_1, u_2} [SetTheory] (X Y : Set) : (X ×ˢ Y).toSubtype ≃ (Y ×ˢ X).toSubtypeSetTheory.Set.prod_commutator useful.

theorem declaration uses `sorry`SetTheory.Set.prod_EqualCard_prod (A B:Set) :
    EqualCard (A ×ˢ B) (B ×ˢ A) := byinst✝:SetTheoryA:SetB:Set⊢ (A ×ˢ B).EqualCard (B ×ˢ A) sorryAll goals completed! 🐙

noncomputable abbrev SetTheory.Set.pow_fun_equiv' (A B : Set) : ↑(A ^ B) ≃ (B → A) :=
  pow_fun_equiv (A:=A) (B:=B)

Exercise 3.6.6. You may find Chapter3.SetTheory.Set.curry_equiv.{u_1, u_2} [SetTheory] {X Y Z : Set} : (X.toSubtype → Y.toSubtype → Z.toSubtype) ≃ ((X ×ˢ Y).toSubtype → Z.toSubtype)SetTheory.Set.curry_equiv useful.

theorem declaration uses `sorry`SetTheory.Set.pow_pow_EqualCard_pow_prod (A B C:Set) :
    EqualCard ((A ^ B) ^ C) (A ^ (B ×ˢ C)) := byinst✝:SetTheoryA:SetB:SetC:Set⊢ ((A ^ B) ^ C).EqualCard (A ^ B ×ˢ C) sorryAll goals completed! 🐙

theorem declaration uses `sorry`SetTheory.Set.pow_pow_eq_pow_mul (a b c:ℕ): (a^b)^c = a^(b*c) := byinst✝:SetTheorya:ℕb:ℕc:ℕ⊢ (a ^ b) ^ c = a ^ (b * c) sorryAll goals completed! 🐙

theorem declaration uses `sorry`SetTheory.Set.pow_prod_pow_EqualCard_pow_union (A B C:Set) (hd: Disjoint B C) :
    EqualCard ((A ^ B) ×ˢ (A ^ C)) (A ^ (B ∪ C)) := byinst✝:SetTheoryA:SetB:SetC:Sethd:Disjoint B C⊢ ((A ^ B) ×ˢ (A ^ C)).EqualCard (A ^ (B ∪ C)) sorryAll goals completed! 🐙

theorem declaration uses `sorry`SetTheory.Set.pow_mul_pow_eq_pow_add (a b c:ℕ): (a^b) * a^c = a^(b+c) := byinst✝:SetTheorya:ℕb:ℕc:ℕ⊢ a ^ b * a ^ c = a ^ (b + c) sorryAll goals completed! 🐙

Exercise 3.6.7

theorem declaration uses `sorry`SetTheory.Set.injection_iff_card_le {A B:Set} (hA: A.finite) (hB: B.finite) :
    (∃ f:A → B, Function.Injective f) ↔ A.card ≤ B.card := sorry

Exercise 3.6.8

theorem declaration uses `sorry`SetTheory.Set.surjection_from_injection {A B:Set} (hA: A ≠ ∅) (f: A → B)
  (hf: Function.Injective f) : ∃ g:B → A, Function.Surjective g := byinst✝:SetTheoryA:SetB:SethA:A ≠ ∅f:A.toSubtype → B.toSubtypehf:Function.Injective f⊢ ∃ g, Function.Surjective g sorryAll goals completed! 🐙

Exercise 3.6.9

theorem declaration uses `sorry`SetTheory.Set.card_union_add_card_inter {A B:Set} (hA: A.finite) (hB: B.finite) :
    A.card + B.card = (A ∪ B).card + (A ∩ B).card := byinst✝:SetTheoryA:SetB:SethA:A.finitehB:B.finite⊢ A.card + B.card = (A ∪ B).card + (A ∩ B).card  sorryAll goals completed! 🐙

Exercise 3.6.10

theorem declaration uses `sorry`SetTheory.Set.pigeonhole_principle {n:ℕ} {A: Fin n → Set}
  (hA: ∀ i, (A i).finite) (hAcard: (iUnion _ A).card > n) : ∃ i, (A i).card ≥ 2 := byinst✝:SetTheoryn:ℕA:(Fin n).toSubtype → SethA:∀ (i : (Fin n).toSubtype), (A i).finitehAcard:((Fin n).iUnion A).card > n⊢ ∃ i, (A i).card ≥ 2 sorryAll goals completed! 🐙

Exercise 3.6.11

theorem declaration uses `sorry`SetTheory.Set.two_to_two_iff {X Y:Set} (f: X → Y): Function.Injective f ↔
    ∀ S ⊆ X, S.card = 2 → (image f S).card = 2 := byinst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtype⊢ Function.Injective f ↔ ∀ S ⊆ X, S.card = 2 → (image f S).card = 2 sorryAll goals completed! 🐙

Exercise 3.6.12

def SetTheory.Set.Permutations (n: ℕ): Set := (Fin n ^ Fin n).specify (fun F ↦
    Function.Bijective (pow_fun_equiv F))

Exercise 3.6.12 (i), first part

theorem declaration uses `sorry`SetTheory.Set.Permutations_finite (n: ℕ): (Permutations n).finite := byinst✝:SetTheoryn:ℕ⊢ (Permutations n).finite sorryAll goals completed! 🐙

/- To continue Exercise 3.6.12 (i), we'll first develop some theory about `Permutations` and `Fin`. -/

noncomputable def SetTheory.Set.Permutations_toFun {n: ℕ} (p: Permutations n) : (Fin n) → (Fin n) := byinst✝:SetTheoryn:ℕp:(Permutations n).toSubtype⊢ (Fin n).toSubtype → (Fin n).toSubtype
  have := p.propertyinst✝:SetTheoryn:ℕp:(Permutations n).toSubtypethis:↑p ∈ Permutations n := p.property⊢ (Fin n).toSubtype → (Fin n).toSubtype
  simp only [Permutations, specification_axiom'', powerset_axiom] at thisinst✝:SetTheoryn:ℕp:(Permutations n).toSubtypethis:∃ (h : ∃ f, ↑f = ↑p), Function.Bijective (pow_fun_equiv ⟨↑p, ⋯⟩)⊢ (Fin n).toSubtype → (Fin n).toSubtype
  exact this.choose.chooseAll goals completed! 🐙

theorem declaration uses `sorry`SetTheory.Set.Permutations_bijective {n: ℕ} (p: Permutations n) :
    Function.Bijective (Permutations_toFun p) := byinst✝:SetTheoryn:ℕp:(Permutations n).toSubtype⊢ Function.Bijective (Permutations_toFun p) sorryAll goals completed! 🐙

theorem declaration uses `sorry`SetTheory.Set.Permutations_inj {n: ℕ} (p1 p2: Permutations n) :
    Permutations_toFun p1 = Permutations_toFun p2 ↔ p1 = p2 := byinst✝:SetTheoryn:ℕp1:(Permutations n).toSubtypep2:(Permutations n).toSubtype⊢ Permutations_toFun p1 = Permutations_toFun p2 ↔ p1 = p2 sorryAll goals completed! 🐙

This connects our concept of a permutation with Mathlib's Equiv.{u_1, u_2} (α : Sort u_1) (β : Sort u_2) : Sort (max (max 1 u_1) u_2)Equiv between Fin sorry : TypeFin Unknown identifier `n`n and Fin sorry : TypeFin Unknown identifier `n`n.

noncomputable def declaration uses `sorry`declaration uses `sorry`declaration uses `sorry`SetTheory.Set.perm_equiv_equiv {n : ℕ} : Permutations n ≃ (Fin n ≃ Fin n) := {
  toFun := fun p => Equiv.ofBijective (Permutations_toFun p) (Permutations_bijective p)
  invFun := sorry
  left_inv := sorry
  right_inv := sorry
}

/- Exercise 3.6.12 involves a lot of moving between `Fin n` and `Fin (n + 1)` so let's add some conveniences. -/

Any Fin sorry : TypeFin Unknown identifier `n`n can be cast to Fin (sorry + 1) : TypeFin (Unknown identifier `n`n + 1). Compare to Mathlib Fin.castSucc {n : ℕ} : Fin n → Fin (n + 1)Fin.castSucc.

def SetTheory.Set.Fin.castSucc {n} (x : Fin n) : Fin (n + 1) :=
  Fin_embed _ _ (byinst✝:SetTheoryn:ℕx:(Fin n).toSubtype⊢ n ≤ n + 1 omegaAll goals completed! 🐙) x

@[simp]
lemma declaration uses `sorry`SetTheory.Set.Fin.castSucc_inj {n} {x y : Fin n} : castSucc x = castSucc y ↔ x = y := byinst✝:SetTheoryn:ℕx:(Fin n).toSubtypey:(Fin n).toSubtype⊢ castSucc x = castSucc y ↔ x = y sorryAll goals completed! 🐙

@[simp]
theorem declaration uses `sorry`SetTheory.Set.Fin.castSucc_ne {n} (x : Fin n) : castSucc x ≠ n := byinst✝:SetTheoryn:ℕx:(Fin n).toSubtype⊢ ↑(castSucc x) ≠ n sorryAll goals completed! 🐙

Any Fin (sorry + 1) : TypeFin (Unknown identifier `n`n + 1) except Unknown identifier `n`n can be cast to Fin sorry : TypeFin Unknown identifier `n`n. Compare to Mathlib Fin.castPred {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n) : Fin nFin.castPred.

noncomputable def SetTheory.Set.Fin.castPred {n} (x : Fin (n + 1)) (h : (x : ℕ) ≠ n) : Fin n :=
  Fin_mk _ (x : ℕ) (byinst✝:SetTheoryn:ℕx:(Fin (n + 1)).toSubtypeh:↑x ≠ n⊢ ↑x < n have := Fin.toNat_lt xinst✝:SetTheoryn:ℕx:(Fin (n + 1)).toSubtypeh:↑x ≠ nthis:↑x < n + 1 := toNat_lt x⊢ ↑x < n; omegaAll goals completed! 🐙)

@[simp]
theorem declaration uses `sorry`SetTheory.Set.Fin.castSucc_castPred {n} (x : Fin (n + 1)) (h : (x : ℕ) ≠ n) :
    castSucc (castPred x h) = x := byinst✝:SetTheoryn:ℕx:(Fin (n + 1)).toSubtypeh:↑x ≠ n⊢ castSucc (castPred x h) = x sorryAll goals completed! 🐙

@[simp]
theorem declaration uses `sorry`SetTheory.Set.Fin.castPred_castSucc {n} (x : Fin n) (h : ((castSucc x : Fin (n + 1)) : ℕ) ≠ n) :
    castPred (castSucc x) h = x := byinst✝:SetTheoryn:ℕx:(Fin n).toSubtypeh:↑(castSucc x) ≠ n⊢ castPred (castSucc x) h = x sorryAll goals completed! 🐙

Any natural Unknown identifier `n`n can be cast to Fin (sorry + 1) : TypeFin (Unknown identifier `n`n + 1). Compare to Mathlib Fin.last (n : ℕ) : Fin (n + 1)Fin.last.

def SetTheory.Set.Fin.last (n : ℕ) : Fin (n + 1) := Fin_mk _ n (byinst✝:SetTheoryn:ℕ⊢ n < n + 1 omegaAll goals completed! 🐙)

Now is a good time to prove this result, which will be useful for completing Exercise 3.6.12 (i).

theorem declaration uses `sorry`SetTheory.Set.card_iUnion_card_disjoint {n m: ℕ} {S : Fin n → Set}
    (hSc : ∀ i, (S i).has_card m)
    (hSd : Pairwise fun i j => Disjoint (S i) (S j)) :
    ((Fin n).iUnion S).finite ∧ ((Fin n).iUnion S).card = n * m := byinst✝:SetTheoryn:ℕm:ℕS:(Fin n).toSubtype → SethSc:∀ (i : (Fin n).toSubtype), (S i).has_card mhSd:Pairwise fun i j => Disjoint (S i) (S j)⊢ ((Fin n).iUnion S).finite ∧ ((Fin n).iUnion S).card = n * m sorryAll goals completed! 🐙

/- Finally, we'll set up a way to shrink `Fin (n + 1)` into `Fin n` (or expand the latter) by making a hole. -/

If some is never equal to Unknown identifier `i`i, we can shrink it into Fin sorry : TypeFin Unknown identifier `n`n by shifting all Unknown identifier `x`sorry > sorry : Propx > Unknown identifier `i`i down by one. Compare to Mathlib Fin.predAbove {n : ℕ} (p : Fin n) (i : Fin (n + 1)) : Fin nFin.predAbove.

noncomputable def declaration uses `sorry`declaration uses `sorry`SetTheory.Set.Fin.predAbove {n} (i : Fin (n + 1)) (x : Fin (n + 1)) (h : x ≠ i) : Fin n :=
  if hx : (x:ℕ) < i then
    Fin_mk _ (x:ℕ) (byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin (n + 1)).toSubtypeh:x ≠ ihx:↑x < ↑i⊢ ↑x < n sorryAll goals completed! 🐙)
  else
    Fin_mk _ ((x:ℕ) - 1) (byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin (n + 1)).toSubtypeh:x ≠ ihx:¬↑x < ↑i⊢ ↑x - 1 < n sorryAll goals completed! 🐙)

We can expand into Fin (sorry + 1) : TypeFin (Unknown identifier `n`n + 1) by shifting all Unknown identifier `x`sorry ≥ sorry : Propx ≥ Unknown identifier `i`i up by one. The output is never Unknown identifier `i`i, so it forms an inverse to the shrinking done by Unknown identifier `predAbove`predAbove. Compare to Mathlib Fin.succAbove {n : ℕ} (p : Fin (n + 1)) (i : Fin n) : Fin (n + 1)Fin.succAbove.

noncomputable def declaration uses `sorry`declaration uses `sorry`SetTheory.Set.Fin.succAbove {n} (i : Fin (n + 1)) (x : Fin n) : Fin (n + 1) :=
  if (x:ℕ) < i then
    Fin_embed _ _ (byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin n).toSubtype⊢ n ≤ n + 1 sorryAll goals completed! 🐙) x
  else
    Fin_mk _ ((x:ℕ) + 1) (byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin n).toSubtype⊢ ↑x + 1 < n + 1 sorryAll goals completed! 🐙)

@[simp]
theorem declaration uses `sorry`SetTheory.Set.Fin.succAbove_ne {n} (i : Fin (n + 1)) (x : Fin n) : succAbove i x ≠ i := byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin n).toSubtype⊢ succAbove i x ≠ i sorryAll goals completed! 🐙

@[simp]
theorem declaration uses `sorry`SetTheory.Set.Fin.succAbove_predAbove {n} (i : Fin (n + 1)) (x : Fin (n + 1)) (h : x ≠ i) :
    (succAbove i) (predAbove i x h) = x := byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin (n + 1)).toSubtypeh:x ≠ i⊢ succAbove i (predAbove i x h) = x sorryAll goals completed! 🐙

@[simp]
theorem declaration uses `sorry`SetTheory.Set.Fin.predAbove_succAbove {n} (i : Fin (n + 1)) (x : Fin n) :
    (predAbove i) (succAbove i x) (succAbove_ne i x) = x := byinst✝:SetTheoryn:ℕi:(Fin (n + 1)).toSubtypex:(Fin n).toSubtype⊢ predAbove i (succAbove i x) ⋯ = x sorryAll goals completed! 🐙

Exercise 3.6.12 (i), second part

theorem declaration uses `sorry`SetTheory.Set.Permutations_ih (n: ℕ):
    (Permutations (n + 1)).card = (n + 1) * (Permutations n).card := byinst✝:SetTheoryn:ℕ⊢ (Permutations (n + 1)).card = (n + 1) * (Permutations n).card
  let S i := (Permutations (n + 1)).specify (fun p ↦ perm_equiv_equiv p (Fin.last n) = i)inst✝:SetTheoryn:ℕS:(Fin (n + 1)).toSubtype → Set := fun i => (Permutations (n + 1)).specify fun p => (perm_equiv_equiv p) (Fin.last n) = i⊢ (Permutations (n + 1)).card = (n + 1) * (Permutations n).card

  have hSe : ∀ i, S i ≈ Permutations n := byinst✝:SetTheoryn:ℕ⊢ (Permutations (n + 1)).card = (n + 1) * (Permutations n).card
    intro iinst✝:SetTheoryn:ℕS:(Fin (n + 1)).toSubtype → Set := fun i => (Permutations (n + 1)).specify fun p => (perm_equiv_equiv p) (Fin.last n) = ii:(Fin (n + 1)).toSubtype⊢ S i ≈ Permutations n
    -- Hint: you might find `perm_equiv_equiv`, `Fin.succAbove`, and `Fin.predAbove` useful.
    have equiv : S i ≃ Permutations n := sorryinst✝:SetTheoryn:ℕS:(Fin (n + 1)).toSubtype → Set := fun i => (Permutations (n + 1)).specify fun p => (perm_equiv_equiv p) (Fin.last n) = ii:(Fin (n + 1)).toSubtypeequiv:(S i).toSubtype ≃ (Permutations n).toSubtype := sorry⊢ S i ≈ Permutations n
    use equiv, equiv.injective, equiv.surjectiveAll goals completed! 🐙

  -- Hint: you might find `card_iUnion_card_disjoint` and `Permutations_finite` useful.
  sorryAll goals completed! 🐙

Exercise 3.6.12 (ii)

theorem declaration uses `sorry`SetTheory.Set.Permutations_card (n: ℕ):
    (Permutations n).card = n.factorial := byinst✝:SetTheoryn:ℕ⊢ (Permutations n).card = n.factorial sorryAll goals completed! 🐙

Connections with Mathlib's Finite.{u_3} (α : Sort u_3) : PropFinite

theorem SetTheory.Set.finite_iff_finite {X:Set} : X.finite ↔ Finite X := byinst✝:SetTheoryX:Set⊢ X.finite ↔ Finite X.toSubtype
  rw [finite_iff_exists_equiv_fin, finite]inst✝:SetTheoryX:Set⊢ (∃ n, X.has_card n) ↔ ∃ n, Nonempty (X.toSubtype ≃ _root_.Fin n)
  constructormpinst✝:SetTheoryX:Set⊢ (∃ n, X.has_card n) → ∃ n, Nonempty (X.toSubtype ≃ _root_.Fin n)mprinst✝:SetTheoryX:Set⊢ (∃ n, Nonempty (X.toSubtype ≃ _root_.Fin n)) → ∃ n, X.has_card n
  ·mpinst✝:SetTheoryX:Set⊢ (∃ n, X.has_card n) → ∃ n, Nonempty (X.toSubtype ≃ _root_.Fin n) rintro ⟨n, hn⟩mpinst✝:SetTheoryX:Setn:ℕhn:X.has_card n⊢ ∃ n, Nonempty (X.toSubtype ≃ _root_.Fin n)
    use nhinst✝:SetTheoryX:Setn:ℕhn:X.has_card n⊢ Nonempty (X.toSubtype ≃ _root_.Fin n)
    obtain ⟨f, hf⟩ := hnhinst✝:SetTheoryX:Setn:ℕf:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective f⊢ Nonempty (X.toSubtype ≃ _root_.Fin n)
    have eq := (Equiv.ofBijective f hf).trans (Fin.Fin_equiv_Fin n)hinst✝:SetTheoryX:Setn:ℕf:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective feq:X.toSubtype ≃ _root_.Fin n := (Equiv.ofBijective f hf).trans (Fin.Fin_equiv_Fin n)⊢ Nonempty (X.toSubtype ≃ _root_.Fin n)
    exact ⟨eq⟩All goals completed! 🐙
  rintro ⟨n, hn⟩mprinst✝:SetTheoryX:Setn:ℕhn:Nonempty (X.toSubtype ≃ _root_.Fin n)⊢ ∃ n, X.has_card n
  use nhinst✝:SetTheoryX:Setn:ℕhn:Nonempty (X.toSubtype ≃ _root_.Fin n)⊢ X.has_card n
  have eq := hn.some.trans (Fin.Fin_equiv_Fin n).symmhinst✝:SetTheoryX:Setn:ℕhn:Nonempty (X.toSubtype ≃ _root_.Fin n)eq:X.toSubtype ≃ (Fin n).toSubtype := hn.some.trans (Fin.Fin_equiv_Fin n).symm⊢ X.has_card n
  exact ⟨eq, eq.bijective⟩All goals completed! 🐙

Connections with Mathlib's Set.Finite.{u} {α : Type u} (s : _root_.Set α) : PropSet.Finite

theorem SetTheory.Set.finite_iff_set_finite {X:Set} :
    X.finite ↔ (X :_root_.Set Object).Finite := byinst✝:SetTheoryX:Set⊢ X.finite ↔ {x | x ∈ X}.Finite
  rw [finite_iff_finite]inst✝:SetTheoryX:Set⊢ Finite X.toSubtype ↔ {x | x ∈ X}.Finite
  rflAll goals completed! 🐙

Connections with Mathlib's Nat.card.{u_3} (α : Type u_3) : ℕNat.card

theorem SetTheory.Set.card_eq_nat_card {X:Set} : X.card = Nat.card X := byinst✝:SetTheoryX:Set⊢ X.card = Nat.card X.toSubtype
  by_cases hf : X.finiteposinst✝:SetTheoryX:Sethf:X.finite⊢ X.card = Nat.card X.toSubtypeneginst✝:SetTheoryX:Sethf:¬X.finite⊢ X.card = Nat.card X.toSubtype
  ·posinst✝:SetTheoryX:Sethf:X.finite⊢ X.card = Nat.card X.toSubtype by_cases hz : X.card = 0posinst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ X.card = Nat.card X.toSubtypeneginst✝:SetTheoryX:Sethf:X.finitehz:¬X.card = 0⊢ X.card = Nat.card X.toSubtype
    ·posinst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ X.card = Nat.card X.toSubtype rw [hz]posinst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ 0 = Nat.card X.toSubtype; symmposinst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ Nat.card X.toSubtype = 0
      have : X = ∅ := empty_of_card_eq_zero hf hzposinst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0this:X = ∅ := empty_of_card_eq_zero hf hz⊢ Nat.card X.toSubtype = 0
      rw [this, Nat.card_eq_zero, isEmpty_iff]posinst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0this:X = ∅ := empty_of_card_eq_zero hf hz⊢ (∀ (a : ∅.toSubtype), False) ∨ Infinite ∅.toSubtype
      aesopAll goals completed! 🐙
    symmneginst✝:SetTheoryX:Sethf:X.finitehz:¬X.card = 0⊢ Nat.card X.toSubtype = X.card
    have hc := has_card_card hfneginst✝:SetTheoryX:Sethf:X.finitehz:¬X.card = 0hc:X.has_card X.card := has_card_card hf⊢ Nat.card X.toSubtype = X.card
    obtain ⟨f, hf⟩ := hcneginst✝:SetTheoryX:Sethf✝:X.finitehz:¬X.card = 0f:X.toSubtype → (Fin X.card).toSubtypehf:Function.Bijective f⊢ Nat.card X.toSubtype = X.card
    apply Nat.card_eq_of_equiv_finneg.finst✝:SetTheoryX:Sethf✝:X.finitehz:¬X.card = 0f:X.toSubtype → (Fin X.card).toSubtypehf:Function.Bijective f⊢ X.toSubtype ≃ _root_.Fin X.card
    exact (Equiv.ofBijective f hf).trans (Fin.Fin_equiv_Fin X.card)All goals completed! 🐙
  simp only [card, hf, ↓reduceDIte]neginst✝:SetTheoryX:Sethf:¬X.finite⊢ 0 = Nat.card X.toSubtype; symmneginst✝:SetTheoryX:Sethf:¬X.finite⊢ Nat.card X.toSubtype = 0
  rw [Nat.card_eq_zero, ←not_finite_iff_infinite]neginst✝:SetTheoryX:Sethf:¬X.finite⊢ IsEmpty X.toSubtype ∨ ¬Finite X.toSubtype
  rightneg.hinst✝:SetTheoryX:Sethf:¬X.finite⊢ ¬Finite X.toSubtype
  rwa [finite_iff_set_finite]neg.hinst✝:SetTheoryX:Sethf:¬{x | x ∈ X}.Finite⊢ ¬Finite X.toSubtype at hf

Connections with Mathlib's Set.ncard.{u_1} {α : Type u_1} (s : _root_.Set α) : ℕSet.ncard

theorem SetTheory.Set.card_eq_ncard {X:Set} : X.card = (X: _root_.Set Object).ncard := byinst✝:SetTheoryX:Set⊢ X.card = {x | x ∈ X}.ncard
  rw [card_eq_nat_card]inst✝:SetTheoryX:Set⊢ Nat.card X.toSubtype = {x | x ∈ X}.ncard
  rflAll goals completed! 🐙

end Chapter3