Analysis
3.5. Cartesian products

Imports

import Mathlib.Tactic
import Analysis.Section_3_1
import Analysis.Section_3_2
import Analysis.Section_3_4

Analysis I, Section 3.5: Cartesian products

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:

Ordered pairs and n-tuples.
Cartesian products and n-fold products.
Finite choice.
Connections with Mathlib counterparts such as Set.pi and Set.prod.

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]open SetTheory.Set

Definition 3.5.1 (Ordered pair). One could also have used Object × Object to define OrderedPair here.

@[ext]
structure OrderedPair where
  fst: Object
  snd: Object

Chapter3.OrderedPair.ext.{u_1, u_2} {inst✝ : SetTheory} {x y : OrderedPair} (fst : x.fst = y.fst)
  (snd : x.snd = y.snd) : x = y#check OrderedPair.ext

Chapter3.OrderedPair.ext.{u_1, u_2} {inst✝ : SetTheory} {x y : OrderedPair} (fst : x.fst = y.fst)
  (snd : x.snd = y.snd) : x = y

Definition 3.5.1 (Ordered pair)

@[simp]
theorem OrderedPair.eq (x y x' y' : Object) :
    (⟨ x, y ⟩ : OrderedPair) = (⟨ x', y' ⟩ : OrderedPair) ↔ x = x' ∧ y = y' := byinst✝:SetTheoryx:Objecty:Objectx':Objecty':Object⊢ { fst := x, snd := y } = { fst := x', snd := y' } ↔ x = x' ∧ y = y' aesopAll goals completed! 🐙

Helper lemma for Exercise 3.5.1

lemma declaration uses `sorry`SetTheory.Set.pair_eq_singleton_iff {a b c: Object} : {a, b} = ({c}: Set) ↔
    a = c ∧ b = c := byinst✝:SetTheorya:Objectb:Objectc:Object⊢ {a, b} = {c} ↔ a = c ∧ b = c
  sorryAll goals completed! 🐙

Exercise 3.5.1, first part

def declaration uses `sorry`OrderedPair.toObject : OrderedPair ↪ Object where
  toFun p := ({ (({p.fst}:Set):Object), (({p.fst, p.snd}:Set):Object) }:Set)
  inj' := byinst✝:SetTheory⊢ Function.Injective fun p ↦
  SetTheory.set_to_object {SetTheory.set_to_object {p.fst}, SetTheory.set_to_object {p.fst, p.snd}} sorryAll goals completed! 🐙

instance OrderedPair.inst_coeObject : Coe OrderedPair Object where
  coe := toObject

A technical operation, turning a object x and a set Y to a set {x} × Y, needed to define the full Cartesian product

abbrev SetTheory.Set.slice (x:Object) (Y:Set) : Set :=
  Y.replace (P := fun y z ↦ z = (⟨x, y⟩:OrderedPair)) (byinst✝:SetTheoryx:ObjectY:Set⊢ ∀ (x_1 : Y.toSubtype) (y y' : Object),
  (fun y z ↦ z = OrderedPair.toObject { fst := x, snd := ↑y }) x_1 y ∧
      (fun y z ↦ z = OrderedPair.toObject { fst := x, snd := ↑y }) x_1 y' →
    y = y' grindAll goals completed! 🐙)

@[simp]
theorem SetTheory.Set.mem_slice (x z:Object) (Y:Set) :
    z ∈ (SetTheory.Set.slice x Y) ↔ ∃ y:Y, z = (⟨x, y⟩:OrderedPair) := replacement_axiom _ _

Definition 3.5.4 (Cartesian product)

abbrev SetTheory.Set.cartesian (X Y:Set) : Set :=
  union (X.replace (P := fun x z ↦ z = slice x Y) (byinst✝:SetTheoryX:SetY:Set⊢ ∀ (x : X.toSubtype) (y y' : Object),
  (fun x z ↦ z = set_to_object (slice (↑x) Y)) x y ∧ (fun x z ↦ z = set_to_object (slice (↑x) Y)) x y' → y = y' intro _ _inst✝:SetTheoryX:SetY:Setx✝:X.toSubtypey✝:Object⊢ ∀ (y' : Object),
  (fun x z ↦ z = set_to_object (slice (↑x) Y)) x✝ y✝ ∧ (fun x z ↦ z = set_to_object (slice (↑x) Y)) x✝ y' → y✝ = y' _inst✝:SetTheoryX:SetY:Setx✝:X.toSubtypey✝:Objecty'✝:Object⊢ (fun x z ↦ z = set_to_object (slice (↑x) Y)) x✝ y✝ ∧ (fun x z ↦ z = set_to_object (slice (↑x) Y)) x✝ y'✝ → y✝ = y'✝ ⟨h1, h2⟩inst✝:SetTheoryX:SetY:Setx✝:X.toSubtypey✝:Objecty'✝:Objecth1:(fun x z ↦ z = set_to_object (slice (↑x) Y)) x✝ y✝h2:(fun x z ↦ z = set_to_object (slice (↑x) Y)) x✝ y'✝⊢ y✝ = y'✝; exact h1.trans h2.symmAll goals completed! 🐙))

This instance enables the ×ˢ notation for Cartesian product.

instance SetTheory.Set.inst_SProd : SProd Set Set Set where
  sprod := cartesian

              example (X Y:Set) : X ×ˢ Y = SetTheory.Set.cartesian X Y := rfl@[simp]
theorem SetTheory.Set.mem_cartesian (z:Object) (X Y:Set) :
    z ∈ X ×ˢ Y ↔ ∃ x:X, ∃ y:Y, z = (⟨x, y⟩:OrderedPair) := byinst✝:SetTheoryz:ObjectX:SetY:Set⊢ z ∈ X ×ˢ Y ↔ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }
  simp only [SProd.sprod, union_axiom]inst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯) ↔ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }; constructormpinst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯) → ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }mprinst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }) → ∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯
  .mpinst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯) → ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y } intro ⟨ S, hz, hS ⟩mpinst✝:SetTheoryz:ObjectX:SetY:SetS:Sethz:z ∈ ShS:set_to_object S ∈ X.replace ⋯⊢ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }; rw [replacement_axiom] at hSmpinst✝:SetTheoryz:ObjectX:SetY:SetS:Sethz:z ∈ ShS:∃ x, set_to_object S = set_to_object (slice (↑x) Y)⊢ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }; obtain ⟨ x, hx ⟩ := hSmpinst✝:SetTheoryz:ObjectX:SetY:SetS:Sethz:z ∈ Sx:X.toSubtypehx:set_to_object S = set_to_object (slice (↑x) Y)⊢ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }
    use xhinst✝:SetTheoryz:ObjectX:SetY:SetS:Sethz:z ∈ Sx:X.toSubtypehx:set_to_object S = set_to_object (slice (↑x) Y)⊢ ∃ y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }; simp_allAll goals completed! 🐙
  rintro ⟨ x, y, rfl ⟩mprinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ ∃ S, OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ S ∧ set_to_object S ∈ X.replace ⋯; use slice x Yhinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ slice (↑x) Y ∧ set_to_object (slice (↑x) Y) ∈ X.replace ⋯; refine ⟨ byinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ slice (↑x) Y simpAll goals completed! 🐙, ?_ ⟩
  rw [replacement_axiom]hinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ ∃ x_1, set_to_object (slice (↑x) Y) = set_to_object (slice (↑x_1) Y); use xAll goals completed! 🐙noncomputable abbrev SetTheory.Set.fst {X Y:Set} (z:X ×ˢ Y) : X :=
  ((mem_cartesian _ _ _).mp z.property).choosenoncomputable abbrev SetTheory.Set.snd {X Y:Set} (z:X ×ˢ Y) : Y :=
  (exists_comm.mp ((mem_cartesian _ _ _).mp z.property)).choosetheorem SetTheory.Set.pair_eq_fst_snd {X Y:Set} (z:X ×ˢ Y) :
    z.val = (⟨ fst z, snd z ⟩:OrderedPair) := byinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtype⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }
  have := (mem_cartesian _ _ _).mp z.propertyinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypethis:∃ x y, ↑z = OrderedPair.toObject { fst := ↑x, snd := ↑y }⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }
  obtain ⟨ y, hy: z.val = (⟨ fst z, y ⟩:OrderedPair)⟩ := this.choose_specinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypethis:∃ x y, ↑z = OrderedPair.toObject { fst := ↑x, snd := ↑y }y:Y.toSubtypehy:↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑y }⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }
  obtain ⟨ x, hx: z.val = (⟨ x, snd z ⟩:OrderedPair)⟩ := (exists_comm.mp this).choose_specinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypethis:∃ x y, ↑z = OrderedPair.toObject { fst := ↑x, snd := ↑y }y:Y.toSubtypehy:↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑y }x:X.toSubtypehx:↑z = OrderedPair.toObject { fst := ↑x, snd := ↑(snd z) }⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) }
  simp_all [EmbeddingLike.apply_eq_iff_eq]All goals completed! 🐙

This equips an OrderedPair with proofs that x ∈ X and y ∈ Y.

def SetTheory.Set.mk_cartesian {X Y:Set} (x:X) (y:Y) : X ×ˢ Y :=
  ⟨(⟨ x, y ⟩:OrderedPair), byinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ X ×ˢ Y simpAll goals completed! 🐙⟩

              @[simp]
theorem SetTheory.Set.fst_of_mk_cartesian {X Y:Set} (x:X) (y:Y) :
    fst (mk_cartesian x y) = x := byinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ fst (mk_cartesian x y) = x
  let z := mk_cartesian x yinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:(X ×ˢ Y).toSubtype := mk_cartesian x y⊢ fst (mk_cartesian x y) = x; have := (mem_cartesian _ _ _).mp z.propertyinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:(X ×ˢ Y).toSubtype := mk_cartesian x ythis:∃ x y, ↑z = OrderedPair.toObject { fst := ↑x, snd := ↑y }⊢ fst (mk_cartesian x y) = x
  obtain ⟨ y', hy: z.val = (⟨ fst z, y' ⟩:OrderedPair) ⟩ := this.choose_specinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:(X ×ˢ Y).toSubtype := mk_cartesian x ythis:∃ x y, ↑z = OrderedPair.toObject { fst := ↑x, snd := ↑y }y':Y.toSubtypehy:↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑y' }⊢ fst (mk_cartesian x y) = x
  simp [z, mk_cartesian, Subtype.val_inj] at *inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:(X ×ˢ Y).toSubtype := mk_cartesian x yy':Y.toSubtypethis:Truehy:x = fst ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩ ∧ y = y'⊢ fst ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩ = x; rw [←hy.1]All goals completed! 🐙@[simp]
theorem SetTheory.Set.snd_of_mk_cartesian {X Y:Set} (x:X) (y:Y) :
    snd (mk_cartesian x y) = y := byinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ snd (mk_cartesian x y) = y
  let z := mk_cartesian x yinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:(X ×ˢ Y).toSubtype := mk_cartesian x y⊢ snd (mk_cartesian x y) = y; have := (mem_cartesian _ _ _).mp z.propertyinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:(X ×ˢ Y).toSubtype := mk_cartesian x ythis:∃ x y, ↑z = OrderedPair.toObject { fst := ↑x, snd := ↑y }⊢ snd (mk_cartesian x y) = y
  obtain ⟨ x', hx: z.val = (⟨ x', snd z ⟩:OrderedPair) ⟩ := (exists_comm.mp this).choose_specinst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:(X ×ˢ Y).toSubtype := mk_cartesian x ythis:∃ x y, ↑z = OrderedPair.toObject { fst := ↑x, snd := ↑y }x':X.toSubtypehx:↑z = OrderedPair.toObject { fst := ↑x', snd := ↑(snd z) }⊢ snd (mk_cartesian x y) = y
  simp [z, mk_cartesian, Subtype.val_inj] at *inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:(X ×ˢ Y).toSubtype := mk_cartesian x yx':X.toSubtypethis:Truehx:x = x' ∧ y = snd ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩⊢ snd ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩ = y; rw [←hx.2]All goals completed! 🐙@[simp]
theorem SetTheory.Set.mk_cartesian_fst_snd_eq {X Y: Set} (z: X ×ˢ Y) :
    (mk_cartesian (fst z) (snd z)) = z := byinst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtype⊢ mk_cartesian (fst z) (snd z) = z
  rw [mk_cartesian, Subtype.mk.injEq, pair_eq_fst_snd]All goals completed! 🐙

Connections with the Mathlib set product, which consists of Lean pairs like (x, y) equipped with a proof that x is in the left set, and y is in the right set. Lean pairs like (x, y) are similar to our OrderedPair, but more general.

noncomputable abbrev SetTheory.Set.prod_equiv_prod (X Y:Set) :
    ((X ×ˢ Y):_root_.Set Object) ≃ (X:_root_.Set Object) ×ˢ (Y:_root_.Set Object) where
  toFun z := ⟨(fst z, snd z), byinst✝:SetTheoryX:SetY:Setz:↑{x | x ∈ X ×ˢ Y}⊢ (↑(fst z), ↑(snd z)) ∈ {x | x ∈ X} ×ˢ {x | x ∈ Y} simpAll goals completed! 🐙⟩
  invFun z := mk_cartesian ⟨z.val.1, z.prop.1⟩ ⟨z.val.2, z.prop.2⟩
  left_inv _ := byinst✝:SetTheoryX:SetY:Setx✝:↑{x | x ∈ X ×ˢ Y}⊢ (fun z ↦ mk_cartesian ⟨(↑z).1, ⋯⟩ ⟨(↑z).2, ⋯⟩) ((fun z ↦ ⟨(↑(fst z), ↑(snd z)), ⋯⟩) x✝) = x✝ simpAll goals completed! 🐙
  right_inv _ := byinst✝:SetTheoryX:SetY:Setx✝:↑({x | x ∈ X} ×ˢ {x | x ∈ Y})⊢ (fun z ↦ ⟨(↑(fst z), ↑(snd z)), ⋯⟩) ((fun z ↦ mk_cartesian ⟨(↑z).1, ⋯⟩ ⟨(↑z).2, ⋯⟩) x✝) = x✝ simpAll goals completed! 🐙

/-- Example 3.5.5 -/
example : ({1, 2}: Set) ×ˢ ({3, 4, 5}: Set) = ({
  ((mk_cartesian (1: Nat) (3: Nat)): Object),
  ((mk_cartesian (1: Nat) (4: Nat)): Object),
  ((mk_cartesian (1: Nat) (5: Nat)): Object),
  ((mk_cartesian (2: Nat) (3: Nat)): Object),
  ((mk_cartesian (2: Nat) (4: Nat)): Object),
  ((mk_cartesian (2: Nat) (5: Nat)): Object)
}: Set) := byinst✝:SetTheory⊢ {1, 2} ×ˢ {3, 4, 5} =
  {↑(mk_cartesian 1 3), ↑(mk_cartesian 1 4), ↑(mk_cartesian 1 5), ↑(mk_cartesian 2 3), ↑(mk_cartesian 2 4),
    ↑(mk_cartesian 2 5)} exthinst✝:SetTheoryx✝:Object⊢ x✝ ∈ {1, 2} ×ˢ {3, 4, 5} ↔
  x✝ ∈
    {↑(mk_cartesian 1 3), ↑(mk_cartesian 1 4), ↑(mk_cartesian 1 5), ↑(mk_cartesian 2 3), ↑(mk_cartesian 2 4),
      ↑(mk_cartesian 2 5)}; aesopAll goals completed! 🐙

Example 3.5.5 / Exercise 3.6.5. There is a bijection between X ×ˢ Y and Y ×ˢ X.

noncomputable abbrev declaration uses `sorry`SetTheory.Set.prod_commutator (X Y:Set) : X ×ˢ Y ≃ Y ×ˢ X where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Example 3.5.5. A function of two variables can be thought of as a function of a pair.

noncomputable abbrev SetTheory.Set.curry_equiv {X Y Z:Set} : (X → Y → Z) ≃ (X ×ˢ Y → Z) where
  toFun f z := f (fst z) (snd z)
  invFun f x y := f (mk_cartesian x y)
  left_inv _ := byinst✝:SetTheoryX:SetY:SetZ:Setx✝:X.toSubtype → Y.toSubtype → Z.toSubtype⊢ (fun f x y ↦ f (mk_cartesian x y)) ((fun f z ↦ f (fst z) (snd z)) x✝) = x✝ exth.h.ainst✝:SetTheoryX:SetY:SetZ:Setx✝²:X.toSubtype → Y.toSubtype → Z.toSubtypex✝¹:X.toSubtypex✝:Y.toSubtype⊢ ↑((fun f x y ↦ f (mk_cartesian x y)) ((fun f z ↦ f (fst z) (snd z)) x✝²) x✝¹ x✝) = ↑(x✝² x✝¹ x✝); simpAll goals completed! 🐙
  right_inv _ := byinst✝:SetTheoryX:SetY:SetZ:Setx✝:(X ×ˢ Y).toSubtype → Z.toSubtype⊢ (fun f z ↦ f (fst z) (snd z)) ((fun f x y ↦ f (mk_cartesian x y)) x✝) = x✝ simpAll goals completed! 🐙

Definition 3.5.6. The indexing set I plays the role of { i : 1 ≤ i ≤ n } in the text. See Exercise 3.5.10 below for some connections betweeen this concept and the preceding notion of Cartesian product and ordered pair.

abbrev SetTheory.Set.tuple {I:Set} {X: I → Set} (x: ∀ i, X i) : Object :=
  ((fun i ↦ ⟨ x i, byinst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtypei:I.toSubtype⊢ ↑(x i) ∈ I.iUnion X rw [mem_iUnion]inst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtypei:I.toSubtype⊢ ∃ α, ↑(x i) ∈ X α; use ihinst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtypei:I.toSubtype⊢ ↑(x i) ∈ X i; exact (x i).propertyAll goals completed! 🐙 ⟩):I → iUnion I X)

Definition 3.5.6

abbrev SetTheory.Set.iProd {I: Set} (X: I → Set) : Set :=
  ((iUnion I X)^I).specify (fun t ↦ ∃ x : ∀ i, X i, t = tuple x)

Definition 3.5.6

theorem SetTheory.Set.mem_iProd {I: Set} {X: I → Set} (t:Object) :
    t ∈ iProd X ↔ ∃ x: ∀ i, X i, t = tuple x := byinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ t ∈ iProd X ↔ ∃ x, t = tuple x
  simp only [iProd, specification_axiom'']inst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ (_ : t ∈ I.iUnion X ^ I), ∃ x, t = tuple x) ↔ ∃ x, t = tuple x; constructormpinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ (_ : t ∈ I.iUnion X ^ I), ∃ x, t = tuple x) → ∃ x, t = tuple xmprinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ x, t = tuple x) → ∃ (_ : t ∈ I.iUnion X ^ I), ∃ x, t = tuple x
  .mpinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ (_ : t ∈ I.iUnion X ^ I), ∃ x, t = tuple x) → ∃ x, t = tuple x intro ⟨ ht, x, h ⟩mpinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Objectht:t ∈ I.iUnion X ^ Ix:(i : I.toSubtype) → (X i).toSubtypeh:t = tuple x⊢ ∃ x, t = tuple x; use xAll goals completed! 🐙
  intro ⟨ x, hx ⟩mprinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Objectx:(i : I.toSubtype) → (X i).toSubtypehx:t = tuple x⊢ ∃ (_ : t ∈ I.iUnion X ^ I), ∃ x, t = tuple x
  have h : t ∈ (I.iUnion X)^I := byinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ t ∈ iProd X ↔ ∃ x, t = tuple x simp [hx]All goals completed! 🐙
  use h, xAll goals completed! 🐙

theorem SetTheory.Set.tuple_mem_iProd {I: Set} {X: I → Set} (x: ∀ i, X i) :
    tuple x ∈ iProd X := byinst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtype⊢ tuple x ∈ iProd X rw [mem_iProd]inst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtype⊢ ∃ x_1, tuple x = tuple x_1; use xAll goals completed! 🐙

@[simp]
theorem declaration uses `sorry`SetTheory.Set.tuple_inj {I:Set} {X: I → Set} (x y: ∀ i, X i) :
    tuple x = tuple y ↔ x = y := byinst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtypey:(i : I.toSubtype) → (X i).toSubtype⊢ tuple x = tuple y ↔ x = y sorryAll goals completed! 🐙

Example 3.5.8. There is a bijection between (X ×ˢ Y) ×ˢ Z and X ×ˢ (Y ×ˢ Z).

noncomputable abbrev SetTheory.Set.prod_associator (X Y Z:Set) : (X ×ˢ Y) ×ˢ Z ≃ X ×ˢ (Y ×ˢ Z) where
  toFun p := mk_cartesian (fst (fst p)) (mk_cartesian (snd (fst p)) (snd p))
  invFun p := mk_cartesian (mk_cartesian (fst p) (fst (snd p))) (snd (snd p))
  left_inv _ := byinst✝:SetTheoryX:SetY:SetZ:Setx✝:((X ×ˢ Y) ×ˢ Z).toSubtype⊢ (fun p ↦ mk_cartesian (mk_cartesian (fst p) (fst (snd p))) (snd (snd p)))
    ((fun p ↦ mk_cartesian (fst (fst p)) (mk_cartesian (snd (fst p)) (snd p))) x✝) =
  x✝ simpAll goals completed! 🐙
  right_inv _ := byinst✝:SetTheoryX:SetY:SetZ:Setx✝:(X ×ˢ Y ×ˢ Z).toSubtype⊢ (fun p ↦ mk_cartesian (fst (fst p)) (mk_cartesian (snd (fst p)) (snd p)))
    ((fun p ↦ mk_cartesian (mk_cartesian (fst p) (fst (snd p))) (snd (snd p))) x✝) =
  x✝ simpAll goals completed! 🐙

Example 3.5.10. I suspect most of the equivalences will require classical reasoning and only be defined non-computably, but would be happy to learn of counterexamples.

noncomputable abbrev declaration uses `sorry`SetTheory.Set.singleton_iProd_equiv (i:Object) (X:Set) :
    iProd (fun _:({i}:Set) ↦ X) ≃ X where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Example 3.5.10

abbrev declaration uses `sorry`SetTheory.Set.empty_iProd_equiv (X: (∅:Set) → Set) : iProd X ≃ Unit where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Example 3.5.10

noncomputable abbrev declaration uses `sorry`SetTheory.Set.iProd_of_const_equiv (I:Set) (X: Set) :
    iProd (fun _:I ↦ X) ≃ (I → X) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Example 3.5.10

noncomputable abbrev declaration uses `sorry`SetTheory.Set.iProd_equiv_prod (X: ({0,1}:Set) → Set) :
    iProd X ≃ (X ⟨ 0, byinst✝:SetTheoryX:{0, 1}.toSubtype → Set⊢ 0 ∈ {0, 1} simpAll goals completed! 🐙 ⟩) ×ˢ (X ⟨ 1, byinst✝:SetTheoryX:{0, 1}.toSubtype → Set⊢ 1 ∈ {0, 1} simpAll goals completed! 🐙 ⟩) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Example 3.5.10

noncomputable abbrev declaration uses `sorry`SetTheory.Set.iProd_equiv_prod_triple (X: ({0,1,2}:Set) → Set) :
    iProd X ≃ (X ⟨ 0, byinst✝:SetTheoryX:{0, 1, 2}.toSubtype → Set⊢ 0 ∈ {0, 1, 2} simpAll goals completed! 🐙 ⟩) ×ˢ (X ⟨ 1, byinst✝:SetTheoryX:{0, 1, 2}.toSubtype → Set⊢ 1 ∈ {0, 1, 2} simpAll goals completed! 🐙 ⟩) ×ˢ (X ⟨ 2, byinst✝:SetTheoryX:{0, 1, 2}.toSubtype → Set⊢ 2 ∈ {0, 1, 2} simpAll goals completed! 🐙 ⟩) where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Connections with Mathlib's Set.pi

noncomputable abbrev SetTheory.Set.iProd_equiv_pi (I:Set) (X: I → Set) :
    iProd X ≃ Set.pi .univ (fun i:I ↦ ((X i):_root_.Set Object)) where
  toFun t := ⟨fun i ↦ ((mem_iProd _).mp t.property).choose i, byinst✝:SetTheoryI:SetX:I.toSubtype → Sett:(iProd X).toSubtype⊢ (fun i ↦ ↑(⋯.choose i)) ∈ Set.univ.pi fun i ↦ {x | x ∈ X i} simpAll goals completed! 🐙⟩
  invFun x :=
    ⟨tuple fun i ↦ ⟨x.val i, byinst✝:SetTheoryI:SetX:I.toSubtype → Setx:↑(Set.univ.pi fun i ↦ {x | x ∈ X i})i:I.toSubtype⊢ ↑x i ∈ ?m.43 x i have := x.property iinst✝:SetTheoryI:SetX:I.toSubtype → Setx:↑(Set.univ.pi fun i ↦ {x | x ∈ X i})i:I.toSubtypethis:i ∈ Set.univ → ↑x i ∈ (fun i ↦ {x | x ∈ X i}) i⊢ ↑x i ∈ ?m.43 x i; simpaAll goals completed! 🐙⟩, byinst✝:SetTheoryI:SetX:I.toSubtype → Setx:↑(Set.univ.pi fun i ↦ {x | x ∈ X i})⊢ (tuple fun i ↦ ⟨↑x i, ⋯⟩) ∈ iProd X apply tuple_mem_iProdAll goals completed! 🐙⟩
  left_inv t := byinst✝:SetTheoryI:SetX:I.toSubtype → Sett:(iProd X).toSubtype⊢ (fun x ↦ ⟨tuple fun i ↦ ⟨↑x i, ⋯⟩, ⋯⟩) ((fun t ↦ ⟨fun i ↦ ↑(⋯.choose i), ⋯⟩) t) = t extainst✝:SetTheoryI:SetX:I.toSubtype → Sett:(iProd X).toSubtype⊢ ↑((fun x ↦ ⟨tuple fun i ↦ ⟨↑x i, ⋯⟩, ⋯⟩) ((fun t ↦ ⟨fun i ↦ ↑(⋯.choose i), ⋯⟩) t)) = ↑t; rw [((mem_iProd _).mp t.property).choose_spec, tuple_inj]All goals completed! 🐙
  right_inv x := byinst✝:SetTheoryI:SetX:I.toSubtype → Setx:↑(Set.univ.pi fun i ↦ {x | x ∈ X i})⊢ (fun t ↦ ⟨fun i ↦ ↑(⋯.choose i), ⋯⟩) ((fun x ↦ ⟨tuple fun i ↦ ⟨↑x i, ⋯⟩, ⋯⟩) x) = x
    exta.hinst✝:SetTheoryI:SetX:I.toSubtype → Setx:↑(Set.univ.pi fun i ↦ {x | x ∈ X i})x✝:I.toSubtype⊢ ↑((fun t ↦ ⟨fun i ↦ ↑(⋯.choose i), ⋯⟩) ((fun x ↦ ⟨tuple fun i ↦ ⟨↑x i, ⋯⟩, ⋯⟩) x)) x✝ = ↑x x✝; dsimpa.hinst✝:SetTheoryI:SetX:I.toSubtype → Setx:↑(Set.univ.pi fun i ↦ {x | x ∈ X i})x✝:I.toSubtype⊢ ↑(⋯.choose x✝) = ↑x x✝
    generalize_proofs _ ha.hinst✝:SetTheoryI:SetX:I.toSubtype → Setx:↑(Set.univ.pi fun i ↦ {x | x ∈ X i})x✝:I.toSubtypepf✝:∀ (i : I.toSubtype), ↑x i ∈ X ih:∃ x_1, (tuple fun i ↦ ⟨↑x i, ⋯⟩) = tuple x_1⊢ ↑(h.choose x✝) = ↑x x✝
    rw [←(tuple_inj _ _).mp h.choose_spec]All goals completed! 🐙

Here we set up some an analogue of Mathlib Fin n types within the Chapter 3 Set Theory, with rudimentary API.

/-
remark: there are also additional relations between these equivalences, but this begins to drift
into the field of higher order category theory, which we will not pursue here.
-/

abbrev SetTheory.Set.Fin (n:ℕ) : Set := nat.specify (fun m ↦ (m:ℕ) < n)

              theorem SetTheory.Set.mem_Fin (n:ℕ) (x:Object) : x ∈ Fin n ↔ ∃ m, m < n ∧ x = m := byinst✝:SetTheoryn:ℕx:Object⊢ x ∈ Fin n ↔ ∃ m < n, x = ↑m
  rw [specification_axiom'']inst✝:SetTheoryn:ℕx:Object⊢ (∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n) ↔ ∃ m < n, x = ↑m; constructormpinst✝:SetTheoryn:ℕx:Object⊢ (∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n) → ∃ m < n, x = ↑mmprinst✝:SetTheoryn:ℕx:Object⊢ (∃ m < n, x = ↑m) → ∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n
  .mpinst✝:SetTheoryn:ℕx:Object⊢ (∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n) → ∃ m < n, x = ↑m intro ⟨ h1, h2 ⟩mpinst✝:SetTheoryn:ℕx:Objecth1:x ∈ nath2:nat_equiv.symm ⟨x, h1⟩ < n⊢ ∃ m < n, x = ↑m; use ↑(⟨ x, h1 ⟩:nat)hinst✝:SetTheoryn:ℕx:Objecth1:x ∈ nath2:nat_equiv.symm ⟨x, h1⟩ < n⊢ nat_equiv.symm ⟨x, h1⟩ < n ∧ x = ↑(nat_equiv.symm ⟨x, h1⟩); simp [h2]All goals completed! 🐙
  intro ⟨ m, hm, h ⟩mprinst✝:SetTheoryn:ℕx:Objectm:ℕhm:m < nh:x = ↑m⊢ ∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n
  use (byinst✝:SetTheoryn:ℕx:Objectm:ℕhm:m < nh:x = ↑m⊢ x ∈ nat rw [h, ←Object.ofnat_eq]inst✝:SetTheoryn:ℕx:Objectm:ℕhm:m < nh:x = ↑m⊢ ↑↑m ∈ nat; exact (m:nat).propertyAll goals completed! 🐙)
  grind [Object.ofnat_eq''']All goals completed! 🐙abbrev SetTheory.Set.Fin_mk (n m:ℕ) (h: m < n): Fin n := ⟨ m, byinst✝:SetTheoryn:ℕm:ℕh:m < n⊢ ↑m ∈ Fin n rw [mem_Fin]inst✝:SetTheoryn:ℕm:ℕh:m < n⊢ ∃ m_1 < n, ↑m = ↑m_1; use mAll goals completed! 🐙 ⟩theorem SetTheory.Set.mem_Fin' {n:ℕ} (x:Fin n) : ∃ m, ∃ h : m < n, x = Fin_mk n m h := byinst✝:SetTheoryn:ℕx:(Fin n).toSubtype⊢ ∃ m, ∃ (h : m < n), x = Fin_mk n m h
  choose m hm this using (mem_Fin _ _).mp x.propertyinst✝:SetTheoryn:ℕx:(Fin n).toSubtypem:ℕhm:m < nthis:↑x = ↑m⊢ ∃ m, ∃ (h : m < n), x = Fin_mk n m h; use m, hmhinst✝:SetTheoryn:ℕx:(Fin n).toSubtypem:ℕhm:m < nthis:↑x = ↑m⊢ x = Fin_mk n m hm
  simp [Fin_mk, ←Subtype.val_inj, this]All goals completed! 🐙@[coe]
noncomputable abbrev SetTheory.Set.Fin.toNat {n:ℕ} (i: Fin n) : ℕ := (mem_Fin' i).choosenoncomputable instance SetTheory.Set.Fin.inst_coeNat {n:ℕ} : CoeOut (Fin n) ℕ where
  coe := toNattheorem SetTheory.Set.Fin.toNat_spec {n:ℕ} (i: Fin n) :
    ∃ h : i < n, i = Fin_mk n i h := (mem_Fin' i).choose_spectheorem SetTheory.Set.Fin.toNat_lt {n:ℕ} (i: Fin n) : i < n := (toNat_spec i).choose@[simp]
theorem SetTheory.Set.Fin.coe_toNat {n:ℕ} (i: Fin n) : ((i:ℕ):Object) = (i:Object) := byinst✝:SetTheoryn:ℕi:(Fin n).toSubtype⊢ ↑↑i = ↑i
  set j := (i:ℕ)inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ := ↑i⊢ ↑j = ↑i; obtain ⟨ h, h':i = Fin_mk n j h ⟩ := toNat_spec iinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ := ↑ih:↑i < nh':i = Fin_mk n j h⊢ ↑j = ↑i; rw [h']All goals completed! 🐙@[simp low]
lemma SetTheory.Set.Fin.coe_inj {n:ℕ} {i j: Fin n} : i = j ↔ (i:ℕ) = (j:ℕ) := byinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:(Fin n).toSubtype⊢ i = j ↔ ↑i = ↑j
  constructormpinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:(Fin n).toSubtype⊢ i = j → ↑i = ↑jmprinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:(Fin n).toSubtype⊢ ↑i = ↑j → i = j
  ·mpinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:(Fin n).toSubtype⊢ i = j → ↑i = ↑j simp_allAll goals completed! 🐙
  obtain ⟨_, hi⟩ := toNat_spec imprinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:(Fin n).toSubtypew✝:↑i < nhi:i = Fin_mk n (↑i) w✝⊢ ↑i = ↑j → i = j
  obtain ⟨_, hj⟩ := toNat_spec jmprinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:(Fin n).toSubtypew✝¹:↑i < nhi:i = Fin_mk n (↑i) w✝w✝:↑j < nhj:j = Fin_mk n (↑j) w✝⊢ ↑i = ↑j → i = j
  grindAll goals completed! 🐙@[simp]
theorem SetTheory.Set.Fin.coe_eq_iff {n:ℕ} (i: Fin n) {j:ℕ} : (i:Object) = (j:Object) ↔ i = j := byinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ⊢ ↑i = ↑j ↔ ↑i = j
  constructormpinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ⊢ ↑i = ↑j → ↑i = jmprinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ⊢ ↑i = j → ↑i = ↑j
  ·mpinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ⊢ ↑i = ↑j → ↑i = j intro hmpinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕh:↑i = ↑j⊢ ↑i = j
    rw [Subtype.coe_eq_iff] at hmpinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕh:∃ (h : ↑j ∈ Fin n), i = ⟨↑j, h⟩⊢ ↑i = j
    obtain ⟨_, rfl⟩ := hmpinst✝:SetTheoryn:ℕj:ℕw✝:↑j ∈ Fin n⊢ ↑⟨↑j, w✝⟩ = j
    simp [←Object.natCast_inj]All goals completed! 🐙
  aesopAll goals completed! 🐙@[simp]
theorem SetTheory.Set.Fin.coe_eq_iff' {n m:ℕ} (i: Fin n) (hi : ↑i ∈ Fin m) : ((⟨i, hi⟩ : Fin m):ℕ) = (i:ℕ) := byinst✝:SetTheoryn:ℕm:ℕi:(Fin n).toSubtypehi:↑i ∈ Fin m⊢ ↑⟨↑i, hi⟩ = ↑i
  obtain ⟨val, property⟩ := iinst✝:SetTheoryn:ℕm:ℕval:Objectproperty:val ∈ Fin nhi:↑⟨val, property⟩ ∈ Fin m⊢ ↑⟨↑⟨val, property⟩, hi⟩ = ↑⟨val, property⟩
  simp only [toNat, Subtype.mk.injEq, exists_prop]inst✝:SetTheoryn:ℕm:ℕval:Objectproperty:val ∈ Fin nhi:↑⟨val, property⟩ ∈ Fin m⊢ ⋯.choose = ⋯.choose
  generalize_proofs h1 h2inst✝:SetTheoryn:ℕm:ℕval:Objectproperty:val ∈ Fin nhi:↑⟨val, property⟩ ∈ Fin mh1:∃ m_1 < m, val = ↑m_1h2:∃ m < n, val = ↑m⊢ h1.choose = h2.choose
  suffices : (h1.choose: Object) = h2.chooseinst✝:SetTheoryn:ℕm:ℕval:Objectproperty:val ∈ Fin nhi:↑⟨val, property⟩ ∈ Fin mh1:∃ m_1 < m, val = ↑m_1h2:∃ m < n, val = ↑mthis:↑h1.choose = ↑h2.choose⊢ h1.choose = h2.choosethisinst✝:SetTheoryn:ℕm:ℕval:Objectproperty:val ∈ Fin nhi:↑⟨val, property⟩ ∈ Fin mh1:∃ m_1 < m, val = ↑m_1h2:∃ m < n, val = ↑m⊢ ↑h1.choose = ↑h2.choose
  ·inst✝:SetTheoryn:ℕm:ℕval:Objectproperty:val ∈ Fin nhi:↑⟨val, property⟩ ∈ Fin mh1:∃ m_1 < m, val = ↑m_1h2:∃ m < n, val = ↑mthis:↑h1.choose = ↑h2.choose⊢ h1.choose = h2.choose aesopAll goals completed! 🐙
  have := h1.choose_specthisinst✝:SetTheoryn:ℕm:ℕval:Objectproperty:val ∈ Fin nhi:↑⟨val, property⟩ ∈ Fin mh1:∃ m_1 < m, val = ↑m_1h2:∃ m < n, val = ↑mthis:h1.choose < m ∧ val = ↑h1.choose⊢ ↑h1.choose = ↑h2.choose
  have := h2.choose_specthisinst✝:SetTheoryn:ℕm:ℕval:Objectproperty:val ∈ Fin nhi:↑⟨val, property⟩ ∈ Fin mh1:∃ m_1 < m, val = ↑m_1h2:∃ m < n, val = ↑mthis✝:h1.choose < m ∧ val = ↑h1.choosethis:h2.choose < n ∧ val = ↑h2.choose⊢ ↑h1.choose = ↑h2.choose
  grindAll goals completed! 🐙@[simp]
theorem SetTheory.Set.Fin.toNat_mk {n:ℕ} (m:ℕ) (h: m < n) : (Fin_mk n m h : ℕ) = m := byinst✝:SetTheoryn:ℕm:ℕh:m < n⊢ ↑(Fin_mk n m h) = m
  have := coe_toNat (Fin_mk n m h)inst✝:SetTheoryn:ℕm:ℕh:m < nthis:↑↑(Fin_mk n m h) = ↑(Fin_mk n m h)⊢ ↑(Fin_mk n m h) = m
  rwa [Object.natCast_inj]inst✝:SetTheoryn:ℕm:ℕh:m < nthis:↑(Fin_mk n m h) = m⊢ ↑(Fin_mk n m h) = m at thisabbrev SetTheory.Set.Fin_embed (n N:ℕ) (h: n ≤ N) (i: Fin n) : Fin N := ⟨ i.val, byinst✝:SetTheoryn:ℕN:ℕh:n ≤ Ni:(Fin n).toSubtype⊢ ↑i ∈ Fin N
  have := i.propertyinst✝:SetTheoryn:ℕN:ℕh:n ≤ Ni:(Fin n).toSubtypethis:↑i ∈ Fin n⊢ ↑i ∈ Fin N; rw [mem_Fin] at *inst✝:SetTheoryn:ℕN:ℕh:n ≤ Ni:(Fin n).toSubtypethis:∃ m < n, ↑i = ↑m⊢ ∃ m < N, ↑i = ↑m; grindAll goals completed! 🐙
⟩

Connections with Mathlib's Fin n

noncomputable abbrev SetTheory.Set.Fin.Fin_equiv_Fin (n:ℕ) : Fin n ≃ _root_.Fin n where
  toFun m := _root_.Fin.mk m (toNat_lt m)
  invFun m := Fin_mk n m.val m.isLt
  left_inv m := (toNat_spec m).2.symm
  right_inv m := byinst✝:SetTheoryn:ℕm:_root_.Fin n⊢ (fun m ↦ ⟨↑m, ⋯⟩) ((fun m ↦ Fin_mk n ↑m ⋯) m) = m simpAll goals completed! 🐙

Lemma 3.5.11 (finite choice)

theorem SetTheory.Set.finite_choice {n:ℕ} {X: Fin n → Set} (h: ∀ i, X i ≠ ∅) : iProd X ≠ ∅ := byinst✝:SetTheoryn:ℕX:(Fin n).toSubtype → Seth:∀ (i : (Fin n).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅
  -- This proof broadly follows the one in the text
  -- (although it is more convenient to induct from 0 rather than 1)
  induction' n with n hnzeroinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅succinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅
  .zeroinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅ have : Fin 0 = ∅ := byinst✝:SetTheoryn:ℕX:(Fin n).toSubtype → Seth:∀ (i : (Fin n).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅
      rw [eq_empty_iff_forall_notMem]inst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅⊢ ∀ (x : Object), x ∉ Fin 0
      grind [specification_axiom'']All goals completed! 🐙
    have empty (i:Fin 0) : X i := False.elim (byinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:Fin 0 = ∅i:(Fin 0).toSubtype⊢ False rw [this] at iinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:Fin 0 = ∅i:∅.toSubtype⊢ False; exact not_mem_empty i i.propertyAll goals completed! 🐙)
    apply nonempty_of_inhabited (x := tuple empty)zeroinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:Fin 0 = ∅empty:(i : (Fin 0).toSubtype) → (X i).toSubtype⊢ tuple empty ∈ iProd X; rw [mem_iProd]zeroinst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:Fin 0 = ∅empty:(i : (Fin 0).toSubtype) → (X i).toSubtype⊢ ∃ x, tuple empty = tuple x; use emptyAll goals completed! 🐙
  set X' : Fin n → Set := fun i ↦ X (Fin_embed n (n+1) (byinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅i:(Fin n).toSubtype⊢ n ≤ n + 1 linarithAll goals completed! 🐙) i)
  have hX' (i: Fin n) : X' i ≠ ∅ := h _succinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i ↦ X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅⊢ iProd X ≠ ∅
  choose x'_obj hx' using nonempty_def (hn hX')succinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i ↦ X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅x'_obj:Objecthx':x'_obj ∈ iProd X'⊢ iProd X ≠ ∅
  rw [mem_iProd] at hx'succinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i ↦ X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅x'_obj:Objecthx':∃ x, x'_obj = tuple x⊢ iProd X ≠ ∅; obtain ⟨ x', rfl ⟩ := hx'succinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i ↦ X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtype⊢ iProd X ≠ ∅
  set last : Fin (n+1) := Fin_mk (n+1) n (byinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i ↦ X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtype⊢ n < n + 1 linarithAll goals completed! 🐙)
  choose a ha using nonempty_def (h last)succinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i ↦ X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X last⊢ iProd X ≠ ∅
  have x : ∀ i, X i := fun i =>
    if h : i = n then
      have : i = last := byinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth✝:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i ↦ X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeh:↑i = n⊢ i = last extainst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth✝:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i ↦ X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeh:↑i = n⊢ ↑i = ↑last; simpa [←Fin.coe_toNat, last]All goals completed! 🐙
      ⟨a, byinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth✝:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i ↦ X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeh:↑i = nthis:i = last⊢ a ∈ X i grindAll goals completed! 🐙⟩
    else
      have : i < n := lt_of_le_of_ne (Nat.lt_succ_iff.mp (Fin.toNat_lt i)) h
      let i' := Fin_mk n i this
      have : X i = X' i' := byinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth✝:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i ↦ X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeh:¬↑i = nthis:↑i < ni':(Fin n).toSubtype := Fin_mk n (↑i) this⊢ X i = X' i' simp [X', i', Fin_embed]All goals completed! 🐙
      ⟨x' i', byinst✝:SetTheoryn:ℕhn:∀ {X : (Fin n).toSubtype → Set}, (∀ (i : (Fin n).toSubtype), X i ≠ ∅) → iProd X ≠ ∅X:(Fin (n + 1)).toSubtype → Seth✝:∀ (i : (Fin (n + 1)).toSubtype), X i ≠ ∅X':(Fin n).toSubtype → Set := fun i ↦ X (Fin_embed n (n + 1) ⋯ i)hX':∀ (i : (Fin n).toSubtype), X' i ≠ ∅x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Fin (n + 1)).toSubtype := Fin_mk (n + 1) n ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeh:¬↑i = nthis✝:↑i < ni':(Fin n).toSubtype := Fin_mk n (↑i) thisthis:X i = X' i'⊢ ↑(x' i') ∈ X i grindAll goals completed! 🐙⟩
  exact nonempty_of_inhabited (tuple_mem_iProd x)All goals completed! 🐙

Exercise 3.5.1, second part (requires axiom of regularity)

abbrev declaration uses `sorry`OrderedPair.toObject' : OrderedPair ↪ Object where
  toFun p := ({ p.fst, (({p.fst, p.snd}:Set):Object) }:Set)
  inj' := byinst✝:SetTheory⊢ Function.Injective fun p ↦ SetTheory.set_to_object {p.fst, SetTheory.set_to_object {p.fst, p.snd}} sorryAll goals completed! 🐙

An alternate definition of a tuple, used in Exercise 3.5.2

structure SetTheory.Set.Tuple (n:ℕ) where
  X: Set
  x: Fin n → X
  surj: Function.Surjective x

Custom extensionality lemma for Exercise 3.5.2. Placing @[ext] on the structure would generate a lemma requiring proof of t.x = t'.x, but these functions have different types when t.X ≠ t'.X. This lemma handles that part.

@[ext]
lemma SetTheory.Set.Tuple.ext {n:ℕ} {t t':Tuple n}
    (hX : t.X = t'.X)
    (hx : ∀ n : Fin n, ((t.x n):Object) = ((t'.x n):Object)) :
    t = t' := byinst✝:SetTheoryn:ℕt:Tuple nt':Tuple nhX:t.X = t'.Xhx:∀ (n_1 : (Fin n).toSubtype), ↑(t.x n_1) = ↑(t'.x n_1)⊢ t = t'
  have ⟨_, _, _⟩ := tinst✝:SetTheoryn:ℕt:Tuple nt':Tuple nX✝:Setx✝:(Fin n).toSubtype → X✝.toSubtypesurj✝:Function.Surjective x✝hX:{ X := X✝, x := x✝, surj := surj✝ }.X = t'.Xhx:∀ (n_1 : (Fin n).toSubtype), ↑({ X := X✝, x := x✝, surj := surj✝ }.x n_1) = ↑(t'.x n_1)⊢ { X := X✝, x := x✝, surj := surj✝ } = t'; have ⟨_, _, _⟩ := t'inst✝:SetTheoryn:ℕt:Tuple nt':Tuple nX✝¹:Setx✝¹:(Fin n).toSubtype → X✝.toSubtypesurj✝¹:Function.Surjective x✝X✝:Setx✝:(Fin n).toSubtype → X✝.toSubtypesurj✝:Function.Surjective x✝hX:{ X := X✝¹, x := x✝¹, surj := surj✝¹ }.X = { X := X✝, x := x✝, surj := surj✝ }.Xhx:∀ (n_1 : (Fin n).toSubtype),
  ↑({ X := X✝¹, x := x✝¹, surj := surj✝¹ }.x n_1) = ↑({ X := X✝, x := x✝, surj := surj✝ }.x n_1)⊢ { X := X✝¹, x := x✝¹, surj := surj✝¹ } = { X := X✝, x := x✝, surj := surj✝ }; subst hXinst✝:SetTheoryn:ℕt:Tuple nt':Tuple nX✝:Setx✝¹:(Fin n).toSubtype → X✝.toSubtypesurj✝¹:Function.Surjective x✝x✝:(Fin n).toSubtype → { X := X✝, x := x✝¹, surj := surj✝¹ }.X.toSubtypesurj✝:Function.Surjective x✝hx:∀ (n_1 : (Fin n).toSubtype),
  ↑({ X := X✝, x := x✝¹, surj := surj✝¹ }.x n_1) =
    ↑({ X := { X := X✝, x := x✝¹, surj := surj✝¹ }.X, x := x✝, surj := surj✝ }.x n_1)⊢ { X := X✝, x := x✝¹, surj := surj✝¹ } = { X := { X := X✝, x := x✝¹, surj := surj✝¹ }.X, x := x✝, surj := surj✝ }; congre_xinst✝:SetTheoryn:ℕt:Tuple nt':Tuple nX✝:Setx✝¹:(Fin n).toSubtype → X✝.toSubtypesurj✝¹:Function.Surjective x✝x✝:(Fin n).toSubtype → { X := X✝, x := x✝¹, surj := surj✝¹ }.X.toSubtypesurj✝:Function.Surjective x✝hx:∀ (n_1 : (Fin n).toSubtype),
  ↑({ X := X✝, x := x✝¹, surj := surj✝¹ }.x n_1) =
    ↑({ X := { X := X✝, x := x✝¹, surj := surj✝¹ }.X, x := x✝, surj := surj✝ }.x n_1)⊢ x✝¹ = x✝; exte_x.h.ainst✝:SetTheoryn:ℕt:Tuple nt':Tuple nX✝:Setx✝²:(Fin n).toSubtype → X✝.toSubtypesurj✝¹:Function.Surjective x✝x✝¹:(Fin n).toSubtype → { X := X✝, x := x✝¹, surj := surj✝¹ }.X.toSubtypesurj✝:Function.Surjective x✝hx:∀ (n_1 : (Fin n).toSubtype),
  ↑({ X := X✝, x := x✝¹, surj := surj✝¹ }.x n_1) =
    ↑({ X := { X := X✝, x := x✝¹, surj := surj✝¹ }.X, x := x✝, surj := surj✝ }.x n_1)x✝:(Fin n).toSubtype⊢ ↑(x✝² x✝) = ↑(x✝¹ x✝); grindAll goals completed! 🐙

Exercise 3.5.2

theorem declaration uses `sorry`SetTheory.Set.Tuple.eq {n:ℕ} (t t':Tuple n) :
    t = t' ↔ ∀ n : Fin n, ((t.x n):Object) = ((t'.x n):Object) := byinst✝:SetTheoryn:ℕt:Tuple nt':Tuple n⊢ t = t' ↔ ∀ (n_1 : (Fin n).toSubtype), ↑(t.x n_1) = ↑(t'.x n_1) sorryAll goals completed! 🐙

noncomputable abbrev declaration uses `sorry`SetTheory.Set.iProd_equiv_tuples (n:ℕ) (X: Fin n → Set) :
    iProd X ≃ { t:Tuple n // ∀ i, (t.x i:Object) ∈ X i } where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Exercise 3.5.3. The spirit here is to avoid direct rewrites (which make all of these claims trivial), and instead use OrderedPair.eq or SetTheory.Set.tuple_inj

theorem declaration uses `sorry`OrderedPair.refl (p: OrderedPair) : p = p := byinst✝:SetTheoryp:OrderedPair⊢ p = p sorryAll goals completed! 🐙

              theorem declaration uses `sorry`OrderedPair.symm (p q: OrderedPair) : p = q ↔ q = p := byinst✝:SetTheoryp:OrderedPairq:OrderedPair⊢ p = q ↔ q = p sorryAll goals completed! 🐙theorem declaration uses `sorry`OrderedPair.trans {p q r: OrderedPair} (hpq: p=q) (hqr: q=r) : p=r := byinst✝:SetTheoryp:OrderedPairq:OrderedPairr:OrderedPairhpq:p = qhqr:q = r⊢ p = r sorryAll goals completed! 🐙theorem declaration uses `sorry`SetTheory.Set.tuple_refl {I:Set} {X: I → Set} (a: ∀ i, X i) :
    tuple a = tuple a := byinst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtype⊢ tuple a = tuple a sorryAll goals completed! 🐙theorem declaration uses `sorry`SetTheory.Set.tuple_symm {I:Set} {X: I → Set} (a b: ∀ i, X i) :
    tuple a = tuple b ↔ tuple b = tuple a := byinst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtypeb:(i : I.toSubtype) → (X i).toSubtype⊢ tuple a = tuple b ↔ tuple b = tuple a sorryAll goals completed! 🐙theorem declaration uses `sorry`SetTheory.Set.tuple_trans {I:Set} {X: I → Set} {a b c: ∀ i, X i}
  (hab: tuple a = tuple b) (hbc : tuple b = tuple c) :
    tuple a = tuple c := byinst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtypeb:(i : I.toSubtype) → (X i).toSubtypec:(i : I.toSubtype) → (X i).toSubtypehab:tuple a = tuple bhbc:tuple b = tuple c⊢ tuple a = tuple c sorryAll goals completed! 🐙

Exercise 3.5.4

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

Exercise 3.5.4

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

Exercise 3.5.4

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

Exercise 3.5.4

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

Exercise 3.5.4

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

Exercise 3.5.4

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

Exercise 3.5.5

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

/- Exercise 3.5.5 -/
def declaration uses `sorry`SetTheory.Set.union_of_prod :
  Decidable (∀ (A B C D:Set), (A ×ˢ B) ∪ (C ×ˢ D) = (A ∪ C) ×ˢ (B ∪ D)) := byinst✝:SetTheory⊢ Decidable (∀ (A B C D : Set), A ×ˢ B ∪ C ×ˢ D = (A ∪ C) ×ˢ (B ∪ D))
  -- the first line of this construction should be `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

/- Exercise 3.5.5 -/
def declaration uses `sorry`SetTheory.Set.diff_of_prod :
  Decidable (∀ (A B C D:Set), (A ×ˢ B) \ (C ×ˢ D) = (A \ C) ×ˢ (B \ D)) := byinst✝:SetTheory⊢ Decidable (∀ (A B C D : Set), A ×ˢ B \ C ×ˢ D = (A \ C) ×ˢ (B \ D))
  -- the first line of this construction should be `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

Exercise 3.5.6.

theorem declaration uses `sorry`SetTheory.Set.prod_subset_prod {A B C D:Set}
  (hA: A ≠ ∅) (hB: B ≠ ∅) (hC: C ≠ ∅) (hD: D ≠ ∅) :
    A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D := byinst✝:SetTheoryA:SetB:SetC:SetD:SethA:A ≠ ∅hB:B ≠ ∅hC:C ≠ ∅hD:D ≠ ∅⊢ A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D sorryAll goals completed! 🐙

def declaration uses `sorry`SetTheory.Set.prod_subset_prod' :
  Decidable (∀ (A B C D:Set), A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D) := byinst✝:SetTheory⊢ Decidable (∀ (A B C D : Set), A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D)
  -- the first line of this construction should be `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

Exercise 3.5.7

theorem declaration uses `sorry`SetTheory.Set.direct_sum {X Y Z:Set} (f: Z → X) (g: Z → Y) :
    ∃! h: Z → X ×ˢ Y, fst ∘ h = f ∧ snd ∘ h = g := byinst✝:SetTheoryX:SetY:SetZ:Setf:Z.toSubtype → X.toSubtypeg:Z.toSubtype → Y.toSubtype⊢ ∃! h, fst ∘ h = f ∧ snd ∘ h = g sorryAll goals completed! 🐙

Exercise 3.5.8

@[simp]
theorem declaration uses `sorry`SetTheory.Set.iProd_empty_iff {n:ℕ} {X: Fin n → Set} :
    iProd X = ∅ ↔ ∃ i, X i = ∅ := byinst✝:SetTheoryn:ℕX:(Fin n).toSubtype → Set⊢ iProd X = ∅ ↔ ∃ i, X i = ∅ sorryAll goals completed! 🐙

Exercise 3.5.9

theorem declaration uses `sorry`SetTheory.Set.iUnion_inter_iUnion {I J: Set} (A: I → Set) (B: J → Set) :
    (iUnion I A) ∩ (iUnion J B) = iUnion (I ×ˢ J) (fun p ↦ (A (fst p)) ∩ (B (snd p))) := byinst✝:SetTheoryI:SetJ:SetA:I.toSubtype → SetB:J.toSubtype → Set⊢ I.iUnion A ∩ J.iUnion B = (I ×ˢ J).iUnion fun p ↦ A (fst p) ∩ B (snd p) sorryAll goals completed! 🐙

abbrev SetTheory.Set.graph {X Y:Set} (f: X → Y) : Set :=
  (X ×ˢ Y).specify (fun p ↦ (f (fst p) = snd p))

Exercise 3.5.10

theorem declaration uses `sorry`SetTheory.Set.graph_inj {X Y:Set} (f f': X → Y) :
    graph f = graph f' ↔ f = f' := byinst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypef':X.toSubtype → Y.toSubtype⊢ graph f = graph f' ↔ f = f' sorryAll goals completed! 🐙

theorem declaration uses `sorry`SetTheory.Set.is_graph {X Y G:Set} (hG: G ⊆ X ×ˢ Y)
  (hvert: ∀ x:X, ∃! y:Y, ((⟨x,y⟩:OrderedPair):Object) ∈ G) :
    ∃! f: X → Y, G = graph f := byinst✝:SetTheoryX:SetY:SetG:SethG:G ⊆ X ×ˢ Yhvert:∀ (x : X.toSubtype), ∃! y, OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ G⊢ ∃! f, G = graph f sorryAll goals completed! 🐙

Exercise 3.5.11. This trivially follows from SetTheory.Set.powerset_axiom, but the exercise is to derive it from SetTheory.Set.exists_powerset instead.

theorem declaration uses `sorry`SetTheory.Set.powerset_axiom' (X Y:Set) :
    ∃! S:Set, ∀(F:Object), F ∈ S ↔ ∃ f: Y → X, f = F := sorry

Exercise 3.5.12, with errata from web site incorporated

theorem declaration uses `sorry`SetTheory.Set.recursion (X: Set) (f: nat → X → X) (c:X) :
    ∃! a: nat → X, a 0 = c ∧ ∀ n, a (n + 1:ℕ) = f n (a n) := byinst✝:SetTheoryX:Setf:nat.toSubtype → X.toSubtype → X.toSubtypec:X.toSubtype⊢ ∃! a, a 0 = c ∧ ∀ (n : ℕ), a ↑(n + 1) = f (↑n) (a ↑n) sorryAll goals completed! 🐙

Exercise 3.5.13

theorem declaration uses `sorry`SetTheory.Set.nat_unique (nat':Set) (zero:nat') (succ:nat' → nat')
  (succ_ne: ∀ n:nat', succ n ≠ zero) (succ_of_ne: ∀ n m:nat', n ≠ m → succ n ≠ succ m)
  (ind: ∀ P: nat' → Prop, P zero → (∀ n, P n → P (succ n)) → ∀ n, P n) :
    ∃! f : nat → nat', Function.Bijective f ∧ f 0 = zero
    ∧ ∀ (n:nat) (n':nat'), f n = n' ↔ f (n+1:ℕ) = succ n' := byinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P n⊢ ∃! f,
  Function.Bijective f ∧
    f 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), f n = n' ↔ f ↑(nat_equiv.symm n + 1) = succ n'
  have nat_coe_eq {m:nat} {n} : (m:ℕ) = n → m = n := byinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P n⊢ ∃! f,
  Function.Bijective f ∧
    f 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), f n = n' ↔ f ↑(nat_equiv.symm n + 1) = succ n' aesopAll goals completed! 🐙
  have nat_coe_eq_zero {m:nat} : (m:ℕ) = 0 → m = 0 := nat_coe_eqinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0⊢ ∃! f,
  Function.Bijective f ∧
    f 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), f n = n' ↔ f ↑(nat_equiv.symm n + 1) = succ n'
  obtain ⟨f, hf⟩ := recursion nat' sorry sorryinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = f⊢ ∃! f,
  Function.Bijective f ∧
    f 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), f n = n' ↔ f ↑(nat_equiv.symm n + 1) = succ n'
  apply existsUnique_of_exists_of_uniquehexinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = f⊢ ∃ x,
  Function.Bijective x ∧
    x 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), x n = n' ↔ x ↑(nat_equiv.symm n + 1) = succ n'huniqueinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = f⊢ ∀ (y₁ y₂ : nat.toSubtype → nat'.toSubtype),
  (Function.Bijective y₁ ∧
      y₁ 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), y₁ n = n' ↔ y₁ ↑(nat_equiv.symm n + 1) = succ n') →
    (Function.Bijective y₂ ∧
        y₂ 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), y₂ n = n' ↔ y₂ ↑(nat_equiv.symm n + 1) = succ n') →
      y₁ = y₂
  ·hexinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = f⊢ ∃ x,
  Function.Bijective x ∧
    x 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), x n = n' ↔ x ↑(nat_equiv.symm n + 1) = succ n' use fhinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = f⊢ Function.Bijective f ∧
  f 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), f n = n' ↔ f ↑(nat_equiv.symm n + 1) = succ n'
    constructorh.leftinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = f⊢ Function.Bijective fh.rightinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = f⊢ f 0 = zero ∧ ∀ (n : nat.toSubtype) (n' : nat'.toSubtype), f n = n' ↔ f ↑(nat_equiv.symm n + 1) = succ n'
    ·h.leftinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = f⊢ Function.Bijective f constructorh.left.leftinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = f⊢ Function.Injective fh.left.rightinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = f⊢ Function.Surjective f
      ·h.left.leftinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = f⊢ Function.Injective f intro x1 x2h.left.leftinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = fx1:nat.toSubtypex2:nat.toSubtype⊢ f x1 = f x2 → x1 = x2 heqh.left.leftinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = fx1:nat.toSubtypex2:nat.toSubtypeheq:f x1 = f x2⊢ x1 = x2
        induction' hx1: (x1:ℕ) with i ih generalizing x1 x2h.left.left.zeroinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = fx1:nat.toSubtypex2:nat.toSubtypeheq:f x1 = f x2hx1:nat_equiv.symm x1 = 0⊢ x1 = x2h.left.left.succinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = fi:ℕih:∀ ⦃x1 x2 : nat.toSubtype⦄, f x1 = f x2 → nat_equiv.symm x1 = i → x1 = x2x1:nat.toSubtypex2:nat.toSubtypeheq:f x1 = f x2hx1:nat_equiv.symm x1 = i + 1⊢ x1 = x2
        ·h.left.left.zeroinst✝:SetTheorynat':Setzero:nat'.toSubtypesucc:nat'.toSubtype → nat'.toSubtypesucc_ne:∀ (n : nat'.toSubtype), succ n ≠ zerosucc_of_ne:∀ (n m : nat'.toSubtype), n ≠ m → succ n ≠ succ mind:∀ (P : nat'.toSubtype → Prop), P zero → (∀ (n : nat'.toSubtype), P n → P (succ n)) → ∀ (n : nat'.toSubtype), P nnat_coe_eq:∀ {m : nat.toSubtype} {n : ℕ}, nat_equiv.symm m = n → m = ↑nnat_coe_eq_zero:∀ {m : nat.toSubtype}, nat_equiv.symm m = 0 → m = 0f:nat.toSubtype → nat'.toSubtypehf:(fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) f ∧
  ∀ (y : nat.toSubtype → nat'.toSubtype), (fun a ↦ a 0 = sorry ∧ ∀ (n : ℕ), a ↑(n + 1) = sorry (↑n) (a ↑n)) y → y = fx1:nat.toSubtypex2:nat.toSubtypeheq:f x1 = f x2hx1:nat_equiv.symm x1 = 0⊢ x1 = x2 sorryAll goals completed! 🐙
        sorryAll goals completed! 🐙
      sorryAll goals completed! 🐙
    sorryAll goals completed! 🐙
  sorryAll goals completed! 🐙

end Chapter3