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:?_mvar.79743 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑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, 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 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:?_mvar.134821 := Chapter3.SetTheory.Set.Fin.toNat_lt _fvar.134684⊢ (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 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:?_mvar.233132 := Chapter3.SetTheory.Set.Fin.toNat_lt _fvar.215234⊢ ↑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':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)⊢ 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':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)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':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑a⊢ 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':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕ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':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))⊢ ↑(f (ι x')) ≠ m₀
      by_contra!inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis✝:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))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':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nx':X'.toSubtypethis✝:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))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':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nx':X'.toSubtypethis✝¹:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))this✝:↑(f (ι x')) = m₀hm₀f:x = ⟨↑x', ⋯⟩this:?_mvar.282467 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ 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':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis✝:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))this:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) ≠ _fvar.275218 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)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':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀x':X'.toSubtypethis✝:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) < _fvar.271942 := Chapter3.SetTheory.Set.Fin.toNat_lt (@_fvar.271986 (@_fvar.274488 _fvar.275348))this:↑(@_fvar.271986 (@_fvar.274488 _fvar.275348)) ≠ _fvar.275218 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)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'pos._@._hyg.2592inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → (Chapter3.SetTheory.Set.Fin (_fvar.271942 - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(@_fvar.271986 (@_fvar.274488 x')) < _fvar.275218 then
      Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) ↑(@_fvar.271986 (@_fvar.274488 x')) ⋯
    else Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) (↑(@_fvar.271986 (@_fvar.274488 x')) - 1) ⋯x':X'.toSubtypeh':↑(f (ι x')) < m₀⊢ ↑(g x') = ↑(f (ι x'))neg._@._hyg.2592inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → (Chapter3.SetTheory.Set.Fin (_fvar.271942 - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(@_fvar.271986 (@_fvar.274488 x')) < _fvar.275218 then
      Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) ↑(@_fvar.271986 (@_fvar.274488 x')) ⋯
    else Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) (↑(@_fvar.271986 (@_fvar.274488 x')) - 1) ⋯x':X'.toSubtypeh':¬↑(f (ι x')) < m₀⊢ ↑(g x') = ↑(f (ι x')) - 1 <;>pos._@._hyg.2592inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → (Chapter3.SetTheory.Set.Fin (_fvar.271942 - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(@_fvar.271986 (@_fvar.274488 x')) < _fvar.275218 then
      Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) ↑(@_fvar.271986 (@_fvar.274488 x')) ⋯
    else Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) (↑(@_fvar.271986 (@_fvar.274488 x')) - 1) ⋯x':X'.toSubtypeh':↑(f (ι x')) < m₀⊢ ↑(g x') = ↑(f (ι x'))neg._@._hyg.2592inst✝:SetTheoryn:ℕh:n ≥ 1X:Setx:X.toSubtypef:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective fX':Chapter3.Set := 
  @sdiff Chapter3.Set Chapter3.SetTheory.Set.instSDiff _fvar.271944
    (@singleton Chapter3.Object Chapter3.Set Chapter3.SetTheory.Set.instSingleton ↑_fvar.271972)ι:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → Chapter3.SetTheory.Set.toSubtype _fvar.271944 := 
  fun x =>
    match x with
    | ⟨y, hy⟩ => ⟨y, ⋯⟩hι:∀ (a : X'.toSubtype), ↑(ι a) = ↑am₀:ℕhm₀:m₀ < nhm₀f:↑(f x) = ↑m₀g:Chapter3.SetTheory.Set.toSubtype _fvar.272097 → (Chapter3.SetTheory.Set.Fin (_fvar.271942 - 1)).toSubtype := 
  fun x' =>
    let this := ⋯;
    let this := ⋯;
    if h' : ↑(@_fvar.271986 (@_fvar.274488 x')) < _fvar.275218 then
      Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) ↑(@_fvar.271986 (@_fvar.274488 x')) ⋯
    else Chapter3.SetTheory.Set.Fin_mk (_fvar.271942 - 1) (↑(@_fvar.271986 (@_fvar.274488 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 _ _ h1 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 m h1 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:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x: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✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519⊢ 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✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519⊢ m ≥ 1succinst✝:SetTheoryn:ℕX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519hn: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✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519⊢ 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✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519⊢ m ≥ 1succinst✝:SetTheoryn:ℕX:Setm:ℕh1:X.has_card (n + 1)h2:X.has_card mthis✝:_fvar.301234 ≠ ∅ := Chapter3.SetTheory.Set.pos_card_nonempty ?_mvar.301360 _fvar.301240x:Objecthx:x ∈ Xthis:_fvar.301237 ≠ 0 := ?_mvar.301519hn: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.mpr.intro.introinst✝:SetTheoryx:ℕleft✝:x < 3⊢ ↑x = 0 ∨ ↑x = 1 ∨ ↑x = 2
    simp only [nat_coe_eq_iff]h.mpr.intro.introinst✝:SetTheoryx:ℕleft✝:x < 3⊢ x = 0 ∨ x = 1 ∨ x = 2
    omegaAll goals completed! 🐙
  rw [this]inst✝:SetTheorythis:{0, 1, 2} = Chapter3.SetTheory.Set.Fin 3 := ?_mvar.302860⊢ ∃ f, Function.Bijective f
  use idhinst✝:SetTheorythis:{0, 1, 2} = Chapter3.SetTheory.Set.Fin 3 := ?_mvar.302860⊢ 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:?_mvar.328400 := Chapter3.SetTheory.Set.Fin.toNat_lt _fvar.328396⊢ ∃ 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:Chapter3.SetTheory.Set.Fin 3 ≈ Chapter3.SetTheory.Set.Fin 2 := 
  Chapter3.SetTheory.Set.EqualCard.trans
    (Chapter3.SetTheory.Set.EqualCard.trans (Chapter3.SetTheory.Set.EqualCard.symm Chapter3.SetTheory.Set.Example_3_6_8_a)
      _fvar.373641)
    Chapter3.SetTheory.Set.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:Chapter3.SetTheory.Set.Fin 3 ≈ Chapter3.SetTheory.Set.Fin 2 := 
  Chapter3.SetTheory.Set.EqualCard.trans
    (Chapter3.SetTheory.Set.EqualCard.trans (Chapter3.SetTheory.Set.EqualCard.symm Chapter3.SetTheory.Set.Example_3_6_8_a)
      _fvar.373641)
    Chapter3.SetTheory.Set.Example_3_6_8_bh2:Chapter3.SetTheory.Set.Fin 3 ≈ Chapter3.SetTheory.Set.Fin 3 := ?_mvar.373795this:?_mvar.373823 := Chapter3.SetTheory.Set.card_uniq _fvar.373755 _fvar.373796⊢ 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, Setoid.r, EqualCard] at hninst✝:SetTheoryn:ℕhn:∃ f, Function.Bijective f⊢ 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:?_mvar.381182 := Function.Bijective.surjective _fvar.381158 ↑(_fvar.381174 + 1)⊢ False; contrapose! hfinst✝:SetTheoryn:ℕf:(Fin n).toSubtype → nat.toSubtypeM:ℕhM:∀ (i : (Fin n).toSubtype), nat_equiv.symm (f i) ≤ Mhf:¬False⊢ ∀ (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:¬Falsea✝:(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:¬Falsea✝:(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:¬Falsea✝:(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:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071⊢ X.has_card n ↔ Y.has_card n
  constructormpinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071⊢ X.has_card n → Y.has_card nmprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071⊢ Y.has_card n → X.has_card n <;>mpinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071⊢ X.has_card n → Y.has_card nmprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071⊢ Y.has_card n → X.has_card n (intro h'mprinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071h':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:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071h':∃ 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:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071g:Y.toSubtype → (Fin n).toSubtypehg:Function.Bijective g⊢ ∃ f, Function.Bijective f)
  .mpinst✝:SetTheoryX:SetY:Setn:ℕf:X.toSubtype → Y.toSubtypehf:Function.Bijective fe:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071g: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:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071g: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:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071g: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:?_mvar.421075 := Equiv.ofBijective _fvar.421066 _fvar.421071g: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.finitepos._@._hyg.4279inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finite⊢ X.card = Y.cardneg._@._hyg.4279inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finite⊢ X.card = Y.card <;>pos._@._hyg.4279inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finite⊢ X.card = Y.cardneg._@._hyg.4279inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finite⊢ X.card = Y.card by_cases hY: Y.finitepos._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:Y.finite⊢ X.card = Y.cardneg._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:¬Y.finite⊢ X.card = Y.card <;>pos._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finitehY:Y.finite⊢ X.card = Y.cardneg._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:X.finitehY:¬Y.finite⊢ X.card = Y.cardpos._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:Y.finite⊢ X.card = Y.cardneg._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬X.finitehY:¬Y.finite⊢ X.card = Y.card try rw [finite] at hX hYneg._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬∃ n, X.has_card nhY:¬∃ n, Y.has_card n⊢ X.card = Y.card
  .pos._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:∃ n, X.has_card nhY:∃ n, Y.has_card n⊢ X.card = Y.card choose nX hXn using hXpos._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhY:∃ n, Y.has_card nnX:ℕhXn:X.has_card nX⊢ X.card = Y.card; choose nY hYn using hYpos._@._hyg.4308inst✝: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 *pos._@._hyg.4308inst✝: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! 🐙
  .neg._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:∃ n, X.has_card nhY:¬∃ n, Y.has_card n⊢ X.card = Y.card choose nX hXn using hXneg._@._hyg.4308inst✝: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 hXnneg._@._hyg.4308inst✝:SetTheoryX:SetY:Seth:X ≈ YhY:¬∃ n, Y.has_card nnX:ℕhXn:Y.has_card nX⊢ X.card = Y.card; tautoAll goals completed! 🐙
  .pos._@._hyg.4334inst✝:SetTheoryX:SetY:Seth:X ≈ YhX:¬∃ n, X.has_card nhY:∃ n, Y.has_card n⊢ X.card = Y.card choose nY hYn using hYpos._@._hyg.4334inst✝: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 hYnpos._@._hyg.4334inst✝: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:?_mvar.431578 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ (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:?_mvar.438826 := Chapter3.SetTheory.Set.Fin.toNat_lt _fvar.438609⊢ ↑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'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:(@Chapter3.SetTheory.Set.Fin _fvar.443015 (_fvar.443242 + 1)).toSubtype → Chapter3.Set := 
  fun i =>
    @Chapter3.SetTheory.Set.specify _fvar.443015 (@Chapter3.SetTheory.Set.Permutations _fvar.443015 (_fvar.443242 + 1))
      fun p => (Chapter3.SetTheory.Set.perm_equiv_equiv p) (Chapter3.SetTheory.Set.Fin.last _fvar.443242) = 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:(@Chapter3.SetTheory.Set.Fin _fvar.443015 (_fvar.443242 + 1)).toSubtype → Chapter3.Set := 
  fun i =>
    @Chapter3.SetTheory.Set.specify _fvar.443015 (@Chapter3.SetTheory.Set.Permutations _fvar.443015 (_fvar.443242 + 1))
      fun p => (Chapter3.SetTheory.Set.perm_equiv_equiv p) (Chapter3.SetTheory.Set.Fin.last _fvar.443242) = 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:(@Chapter3.SetTheory.Set.Fin _fvar.443015 (_fvar.443242 + 1)).toSubtype → Chapter3.Set := 
  fun i =>
    @Chapter3.SetTheory.Set.specify _fvar.443015 (@Chapter3.SetTheory.Set.Permutations _fvar.443015 (_fvar.443242 + 1))
      fun p => (Chapter3.SetTheory.Set.perm_equiv_equiv p) (Chapter3.SetTheory.Set.Fin.last _fvar.443242) = ii:(Fin (n + 1)).toSubtypeequiv:Chapter3.SetTheory.Set.toSubtype (@_fvar.443511 _fvar.443566) ≃
  (@Chapter3.SetTheory.Set.Permutations _fvar.443015 _fvar.443242).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⟩mp.introinst✝: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⟩ := hnh.introinst✝: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)h.introinst✝:SetTheoryX:Setn:ℕf:X.toSubtype → (Fin n).toSubtypehf:Function.Bijective feq:?_mvar.444529 := (Equiv.ofBijective _fvar.444523 _fvar.444524).trans (Chapter3.SetTheory.Set.Fin.Fin_equiv_Fin _fvar.444468)⊢ Nonempty (X.toSubtype ≃ _root_.Fin n)
    exact ⟨eq⟩All goals completed! 🐙
  rintro ⟨n, hn⟩mpr.introinst✝: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:?_mvar.444627 := Equiv.trans (Nonempty.some _fvar.444590) (Chapter3.SetTheory.Set.Fin.Fin_equiv_Fin _fvar.444589).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.finitepos._@._hyg.7309inst✝:SetTheoryX:Sethf:X.finite⊢ X.card = Nat.card X.toSubtypeneg._@._hyg.7309inst✝:SetTheoryX:Sethf:¬X.finite⊢ X.card = Nat.card X.toSubtype
  ·pos._@._hyg.7309inst✝:SetTheoryX:Sethf:X.finite⊢ X.card = Nat.card X.toSubtype by_cases hz : X.card = 0pos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ X.card = Nat.card X.toSubtypeneg._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:¬X.card = 0⊢ X.card = Nat.card X.toSubtype
    ·pos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ X.card = Nat.card X.toSubtype rw [hz]pos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ 0 = Nat.card X.toSubtype; symmpos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0⊢ Nat.card X.toSubtype = 0
      have : X = ∅ := empty_of_card_eq_zero hf hzpos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0this:_fvar.445131 = ∅ := Chapter3.SetTheory.Set.empty_of_card_eq_zero _fvar.445470 _fvar.445550⊢ Nat.card X.toSubtype = 0
      rw [this, Nat.card_eq_zero, isEmpty_iff]pos._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:X.card = 0this:_fvar.445131 = ∅ := Chapter3.SetTheory.Set.empty_of_card_eq_zero _fvar.445470 _fvar.445550⊢ (∀ (a : ∅.toSubtype), False) ∨ Infinite ∅.toSubtype
      aesopAll goals completed! 🐙
    symmneg._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:¬X.card = 0⊢ Nat.card X.toSubtype = X.card
    have hc := has_card_card hfneg._@._hyg.7336inst✝:SetTheoryX:Sethf:X.finitehz:¬X.card = 0hc:?_mvar.454775 := Chapter3.SetTheory.Set.has_card_card _fvar.445470⊢ Nat.card X.toSubtype = X.card
    obtain ⟨f, hf⟩ := hcneg.intro._@._hyg.7336inst✝: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.intro.f._@._hyg.7336inst✝: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]neg._@._hyg.7309inst✝:SetTheoryX:Sethf:¬X.finite⊢ 0 = Nat.card X.toSubtype; symmneg._@._hyg.7309inst✝:SetTheoryX:Sethf:¬X.finite⊢ Nat.card X.toSubtype = 0
  rw [Nat.card_eq_zero, ←not_finite_iff_infinite]neg._@._hyg.7309inst✝:SetTheoryX:Sethf:¬X.finite⊢ IsEmpty X.toSubtype ∨ ¬Finite X.toSubtype
  rightneg.h._@._hyg.7309inst✝:SetTheoryX:Sethf:¬X.finite⊢ ¬Finite X.toSubtype
  rwa [finite_iff_set_finite]neg.h._@._hyg.7309inst✝: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