Cartesian products

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.{u_1, u_2} {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) (t : (i : ι) → Set (α i)) : Set ((i : ι) → α i)Set.pi and Set.prod.{u, v} {α : Type u} {β : Type v} (s : Set α) (t : Set β) : Set (α × β)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 : Type u_1Object × Object to define Chapter3.OrderedPair.{u_1, u_2} [SetTheory] : Type u_2OrderedPair 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

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' := inst✝:SetTheoryx:Objecty:Objectx':Objecty':Object⊢ { fst := x, snd := y } = { fst := x', snd := y' } ↔ x = x' ∧ y = y' All 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 := inst✝:SetTheorya:Objectb:Objectc:Object⊢ {a, b} = {c} ↔ a = c ∧ b = c All 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' := inst✝:SetTheory⊢ Function.Injective fun p => SetTheory.set_to_object {SetTheory.set_to_object {p.fst}, SetTheory.set_to_object {p.fst, p.snd}} All goals completed! 🐙
instance OrderedPair.inst_coeObject : Coe OrderedPair Object where coe := toObject

A technical operation, turning a object Unknown identifier `x`x and a set Unknown identifier `Y`Y to a set overloaded, errors 1:1 Unknown identifier `x` invalid {...} notation, expected type is not of the form (C ...) Type ?u.436364sorry × sorry : Type (max u_1 u_2){x} × Unknown identifier `Y`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)) (inst✝: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' All 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) (inst✝: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' All 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) := inst✝:SetTheoryz:ObjectX:SetY:Set⊢ z ∈ X ×ˢ Y ↔ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y } inst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯) ↔ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }; inst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯) → ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }inst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }) → ∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯ inst✝:SetTheoryz:ObjectX:SetY:Set⊢ (∃ S, z ∈ S ∧ set_to_object S ∈ X.replace ⋯) → ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y } inst✝:SetTheoryz:ObjectX:SetY:SetS:Sethz:z ∈ ShS:set_to_object S ∈ X.replace ⋯⊢ ∃ x y, z = OrderedPair.toObject { fst := ↑x, snd := ↑y }; inst✝: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 }; inst✝: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 } inst✝: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 }; All goals completed! 🐙 inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ ∃ S, OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ S ∧ set_to_object S ∈ X.replace ⋯; inst✝: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 ⟨ inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ slice (↑x) Y All goals completed! 🐙, ?_ ⟩ inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ ∃ x_1, set_to_object (slice (↑x) Y) = set_to_object (slice (↑x_1) Y); All 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) := inst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtype⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) } inst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypethis:?_mvar.39162 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) } inst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypethis:?_mvar.39162 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)y:Y.toSubtypehy:↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑y }⊢ ↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑(snd z) } inst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtypethis:?_mvar.39162 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)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) } All goals completed! 🐙

This equips an Chapter3.OrderedPair.{u_1, u_2} [SetTheory] : Type u_2OrderedPair with proofs that Unknown identifier `x`sorry ∈ sorry : Propx ∈ Unknown identifier `X`X and Unknown identifier `y`sorry ∈ sorry : Propy ∈ Unknown identifier `Y`Y.

def SetTheory.Set.mk_cartesian {X Y:Set} (x:X) (y:Y) : X ×ˢ Y := ⟨(⟨ x, y ⟩:OrderedPair), inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ X ×ˢ Y All goals completed! 🐙⟩
@[simp] theorem SetTheory.Set.fst_of_mk_cartesian {X Y:Set} (x:X) (y:Y) : fst (mk_cartesian x y) = x := inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ fst (mk_cartesian x y) = x inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:?_mvar.74682 := Chapter3.SetTheory.Set.mk_cartesian _fvar.74678 _fvar.74679⊢ fst (mk_cartesian x y) = x; inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:?_mvar.74682 := Chapter3.SetTheory.Set.mk_cartesian _fvar.74678 _fvar.74679this:?_mvar.74696 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ fst (mk_cartesian x y) = x inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:?_mvar.74682 := Chapter3.SetTheory.Set.mk_cartesian _fvar.74678 _fvar.74679this:?_mvar.74696 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)y':Y.toSubtypehy:↑z = OrderedPair.toObject { fst := ↑(fst z), snd := ↑y' }⊢ fst (mk_cartesian x y) = x inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:?_mvar.74682 := Chapter3.SetTheory.Set.mk_cartesian _fvar.74678 _fvar.74679y':Y.toSubtypethis:Truehy:x = fst ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩ ∧ y = y'⊢ fst ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩ = x; All goals completed! 🐙@[simp] theorem SetTheory.Set.snd_of_mk_cartesian {X Y:Set} (x:X) (y:Y) : snd (mk_cartesian x y) = y := inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtype⊢ snd (mk_cartesian x y) = y inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:?_mvar.91139 := Chapter3.SetTheory.Set.mk_cartesian _fvar.91135 _fvar.91136⊢ snd (mk_cartesian x y) = y; inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:?_mvar.91139 := Chapter3.SetTheory.Set.mk_cartesian _fvar.91135 _fvar.91136this:?_mvar.91153 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ snd (mk_cartesian x y) = y inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:?_mvar.91139 := Chapter3.SetTheory.Set.mk_cartesian _fvar.91135 _fvar.91136this:?_mvar.91153 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)x':X.toSubtypehx:↑z = OrderedPair.toObject { fst := ↑x', snd := ↑(snd z) }⊢ snd (mk_cartesian x y) = y inst✝:SetTheoryX:SetY:Setx:X.toSubtypey:Y.toSubtypez:?_mvar.91139 := Chapter3.SetTheory.Set.mk_cartesian _fvar.91135 _fvar.91136x':X.toSubtypethis:Truehx:x = x' ∧ y = snd ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩⊢ snd ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩ = y; 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 := inst✝:SetTheoryX:SetY:Setz:(X ×ˢ Y).toSubtype⊢ mk_cartesian (fst z) (snd z) = z All goals completed! 🐙

Connections with the Mathlib set product, which consists of Lean pairs like (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x`x, Unknown identifier `y`y) equipped with a proof that Unknown identifier `x`x is in the left set, and Unknown identifier `y`y is in the right set. Lean pairs like (sorry, sorry) : ?m.1 × ?m.2(Unknown identifier `x`x, Unknown identifier `y`y) are similar to our Chapter3.OrderedPair.{u_1, u_2} [SetTheory] : Type u_2OrderedPair, 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), inst✝:SetTheoryX:SetY:Setz:↑{x | x ∈ X ×ˢ Y}⊢ (↑(fst z), ↑(snd z)) ∈ {x | x ∈ X} ×ˢ {x | x ∈ Y} All goals completed! 🐙⟩ invFun z := mk_cartesian ⟨z.val.1, z.prop.1⟩ ⟨z.val.2, z.prop.2⟩ left_inv _ := inst✝:SetTheoryX:SetY:Setx✝:↑{x | x ∈ X ×ˢ Y}⊢ (fun z => mk_cartesian ⟨(↑z).1, ⋯⟩ ⟨(↑z).2, ⋯⟩) ((fun z => ⟨(↑(fst z), ↑(snd z)), ⋯⟩) x✝) = x✝ All goals completed! 🐙 right_inv _ := inst✝: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✝ All 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) := inst✝: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)} inst✝: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)}; All goals completed! 🐙

Example 3.5.5 / Exercise 3.6.5. There is a bijection between Unknown identifier `X`sorry ×ˢ sorry : _root_.Set (?α × ?β)X ×ˢ Unknown identifier `Y`Y and Unknown identifier `Y`sorry ×ˢ sorry : _root_.Set (?α × ?β)Y ×ˢ Unknown identifier `X`X.

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'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 ⟨ (⟨ x, y ⟩:OrderedPair), inst✝:SetTheoryX:SetY:SetZ:Setf:(X ×ˢ Y).toSubtype → Z.toSubtypex:X.toSubtypey:Y.toSubtype⊢ OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ X ×ˢ Y All goals completed! 🐙 ⟩ left_inv _ := inst✝:SetTheoryX:SetY:SetZ:Setx✝:X.toSubtype → Y.toSubtype → Z.toSubtype⊢ (fun f x y => f ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩) ((fun f z => f (fst z) (snd z)) x✝) = x✝ All goals completed! 🐙 right_inv _ := inst✝:SetTheoryX:SetY:SetZ:Setx✝:(X ×ˢ Y).toSubtype → Z.toSubtype⊢ (fun f z => f (fst z) (snd z)) ((fun f x y => f ⟨OrderedPair.toObject { fst := ↑x, snd := ↑y }, ⋯⟩) x✝) = x✝ All goals completed! 🐙

Definition 3.5.6. The indexing set Unknown identifier `I`I plays the role of 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, inst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtypei:I.toSubtype⊢ ↑(x i) ∈ I.iUnion X inst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtypei:I.toSubtype⊢ ∃ α, ↑(x i) ∈ X α; inst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtypei:I.toSubtype⊢ ↑(x i) ∈ X i; All 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 := inst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ t ∈ iProd X ↔ ∃ x, t = tuple x inst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ (_ : t ∈ I.iUnion X ^ I), ∃ x, t = tuple x) ↔ ∃ x, t = tuple x; inst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ (_ : t ∈ I.iUnion X ^ I), ∃ x, t = tuple x) → ∃ x, t = tuple xinst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ x, t = tuple x) → ∃ (_ : t ∈ I.iUnion X ^ I), ∃ x, t = tuple x inst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ (∃ (_ : t ∈ I.iUnion X ^ I), ∃ x, t = tuple x) → ∃ x, t = tuple x inst✝:SetTheoryI:SetX:I.toSubtype → Sett:Objectht:t ∈ I.iUnion X ^ Ix:(i : I.toSubtype) → (X i).toSubtypeh:t = tuple x⊢ ∃ x, t = tuple x; All goals completed! 🐙 inst✝: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 := inst✝:SetTheoryI:SetX:I.toSubtype → Sett:Object⊢ t ∈ iProd X ↔ ∃ x, t = tuple x All goals completed! 🐙 All goals completed! 🐙
theorem SetTheory.Set.tuple_mem_iProd {I: Set} {X: I → Set} (x: ∀ i, X i) : tuple x ∈ iProd X := inst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtype⊢ tuple x ∈ iProd X inst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtype⊢ ∃ x_1, tuple x = tuple x_1; All 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 := inst✝:SetTheoryI:SetX:I.toSubtype → Setx:(i : I.toSubtype) → (X i).toSubtypey:(i : I.toSubtype) → (X i).toSubtype⊢ tuple x = tuple y ↔ x = y All goals completed! 🐙

Example 3.5.8. There is a bijection between (sorry ×ˢ sorry) ×ˢ sorry : _root_.Set ((?α × ?β) × ?β)(Unknown identifier `X`X ×ˢ Unknown identifier `Y`Y) ×ˢ Unknown identifier `Z`Z and Unknown identifier `X`sorry ×ˢ sorry ×ˢ sorry : _root_.Set (?α × ?α × ?β)X ×ˢ (Unknown identifier `Y`Y ×ˢ Unknown identifier `Z`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 _ := inst✝: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✝ All goals completed! 🐙 right_inv _ := inst✝: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✝ All 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'declaration uses 'sorry'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'declaration uses 'sorry'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'declaration uses 'sorry'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'declaration uses 'sorry'declaration uses 'sorry'SetTheory.Set.iProd_equiv_prod (X: ({0,1}:Set) → Set) : iProd X ≃ (X ⟨ 0, inst✝:SetTheoryX:{0, 1}.toSubtype → Set⊢ 0 ∈ {0, 1} All goals completed! 🐙 ⟩) ×ˢ (X ⟨ 1, inst✝:SetTheoryX:{0, 1}.toSubtype → Set⊢ 1 ∈ {0, 1} All goals completed! 🐙 ⟩) where toFun := sorry invFun := sorry left_inv := sorry right_inv := sorry

Example 3.5.10

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

Connections with Mathlib's Set.pi.{u_1, u_2} {ι : Type u_1} {α : ι → Type u_2} (s : _root_.Set ι) (t : (i : ι) → _root_.Set (α i)) : _root_.Set ((i : ι) → α i)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, inst✝:SetTheoryI:SetX:I.toSubtype → Sett:(iProd X).toSubtype⊢ (fun i => ↑(⋯.choose i)) ∈ Set.univ.pi fun i => {x | x ∈ X i} All goals completed! 🐙⟩ invFun x := ⟨tuple fun i ↦ ⟨x.val i, inst✝:SetTheoryI:SetX:I.toSubtype → Setx:↑(Set.univ.pi fun i => {x | x ∈ X i})i:I.toSubtype⊢ ↑x i ∈ ?m.43 x i inst✝:SetTheoryI:SetX:I.toSubtype → Setx:↑(Set.univ.pi fun i => {x | x ∈ X i})i:I.toSubtypethis:?_mvar.239441 := @Subtype.property ?_mvar.239443 ?_mvar.239444 _fvar.238568 _fvar.238586⊢ ↑x i ∈ ?m.43 x i; All goals completed! 🐙⟩, inst✝:SetTheoryI:SetX:I.toSubtype → Setx:↑(Set.univ.pi fun i => {x | x ∈ X i})⊢ (tuple fun i => ⟨↑x i, ⋯⟩) ∈ iProd X All goals completed! 🐙⟩ left_inv t := inst✝:SetTheoryI:SetX:I.toSubtype → Sett:(iProd X).toSubtype⊢ (fun x => ⟨tuple fun i => ⟨↑x i, ⋯⟩, ⋯⟩) ((fun t => ⟨fun i => ↑(⋯.choose i), ⋯⟩) t) = t inst✝:SetTheoryI:SetX:I.toSubtype → Sett:(iProd X).toSubtype⊢ ↑((fun x => ⟨tuple fun i => ⟨↑x i, ⋯⟩, ⋯⟩) ((fun t => ⟨fun i => ↑(⋯.choose i), ⋯⟩) t)) = ↑t; All goals completed! 🐙 right_inv x := inst✝: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 inst✝: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✝; inst✝:SetTheoryI:SetX:I.toSubtype → Setx:↑(Set.univ.pi fun i => {x | x ∈ X i})x✝:I.toSubtype⊢ ↑(⋯.choose x✝) = ↑x x✝ inst✝: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✝ All goals completed! 🐙
/- 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. -/

Here we set up some an analogue of Mathlib overloaded, errors 1:4 Unknown identifier `n` 1:4 Unknown identifier `n`Fin n types within the Chapter 3 Set Theory, with rudimentary API.

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 := inst✝:SetTheoryn:ℕx:Object⊢ x ∈ Fin n ↔ ∃ m < n, x = ↑m inst✝:SetTheoryn:ℕx:Object⊢ (∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n) ↔ ∃ m < n, x = ↑m; inst✝:SetTheoryn:ℕx:Object⊢ (∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n) → ∃ m < n, x = ↑minst✝:SetTheoryn:ℕx:Object⊢ (∃ m < n, x = ↑m) → ∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n inst✝:SetTheoryn:ℕx:Object⊢ (∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n) → ∃ m < n, x = ↑m inst✝:SetTheoryn:ℕx:Objecth1:x ∈ nath2:nat_equiv.symm ⟨x, h1⟩ < n⊢ ∃ m < n, x = ↑m; inst✝:SetTheoryn:ℕx:Objecth1:x ∈ nath2:nat_equiv.symm ⟨x, h1⟩ < n⊢ nat_equiv.symm ⟨x, h1⟩ < n ∧ x = ↑(nat_equiv.symm ⟨x, h1⟩); All goals completed! 🐙 inst✝:SetTheoryn:ℕx:Objectm:ℕhm:m < nh:x = ↑m⊢ ∃ (h : x ∈ nat), nat_equiv.symm ⟨x, h⟩ < n use (inst✝:SetTheoryn:ℕx:Objectm:ℕhm:m < nh:x = ↑m⊢ x ∈ nat inst✝:SetTheoryn:ℕx:Objectm:ℕhm:m < nh:x = ↑m⊢ ↑↑m ∈ nat; All goals completed! 🐙) All goals completed! 🐙abbrev SetTheory.Set.Fin_mk (n m:ℕ) (h: m < n): Fin n := ⟨ m, inst✝:SetTheoryn:ℕm:ℕh:m < n⊢ ↑m ∈ Fin n inst✝:SetTheoryn:ℕm:ℕh:m < n⊢ ∃ m_1 < n, ↑m = ↑m_1; All goals completed! 🐙 ⟩theorem SetTheory.Set.mem_Fin' {n:ℕ} (x:Fin n) : ∃ m, ∃ h : m < n, x = Fin_mk n m h := inst✝:SetTheoryn:ℕx:(Fin n).toSubtype⊢ ∃ m, ∃ (h : m < n), x = Fin_mk n m h inst✝:SetTheoryn:ℕx:(Fin n).toSubtypem:ℕhm:m < nthis:↑x = ↑m⊢ ∃ m, ∃ (h : m < n), x = Fin_mk n m h; inst✝:SetTheoryn:ℕx:(Fin n).toSubtypem:ℕhm:m < nthis:↑x = ↑m⊢ x = Fin_mk n m hm 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) := inst✝:SetTheoryn:ℕi:(Fin n).toSubtype⊢ ↑↑i = ↑i inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ := ↑_fvar.256476⊢ ↑j = ↑i; inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ := ↑_fvar.256476h:↑i < nh':i = Fin_mk n j h⊢ ↑j = ↑i; All goals completed! 🐙@[simp low] lemma SetTheory.Set.Fin.coe_inj {n:ℕ} {i j: Fin n} : i = j ↔ (i:ℕ) = (j:ℕ) := inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:(Fin n).toSubtype⊢ i = j ↔ ↑i = ↑j inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:(Fin n).toSubtype⊢ i = j → ↑i = ↑jinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:(Fin n).toSubtype⊢ ↑i = ↑j → i = j inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:(Fin n).toSubtype⊢ i = j → ↑i = ↑j All goals completed! 🐙 inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:(Fin n).toSubtypew✝:↑i < nhi:i = Fin_mk n (↑i) w✝⊢ ↑i = ↑j → i = j inst✝: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 All goals completed! 🐙@[simp] theorem SetTheory.Set.Fin.coe_eq_iff {n:ℕ} (i: Fin n) {j:ℕ} : (i:Object) = (j:Object) ↔ i = j := inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ⊢ ↑i = ↑j ↔ ↑i = j inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ⊢ ↑i = ↑j → ↑i = jinst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ⊢ ↑i = j → ↑i = ↑j inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕ⊢ ↑i = ↑j → ↑i = j inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕh:↑i = ↑j⊢ ↑i = j inst✝:SetTheoryn:ℕi:(Fin n).toSubtypej:ℕh:∃ (h : ↑j ∈ Fin n), i = ⟨↑j, h⟩⊢ ↑i = j inst✝:SetTheoryn:ℕj:ℕw✝:↑j ∈ Fin n⊢ ↑⟨↑j, w✝⟩ = j All goals completed! 🐙 All goals completed! 🐙@[simp] theorem SetTheory.Set.Fin.coe_eq_iff' {n m:ℕ} (i: Fin n) (hi : ↑i ∈ Fin m) : ((⟨i, hi⟩ : Fin m):ℕ) = (i:ℕ) := inst✝:SetTheoryn:ℕm:ℕi:(Fin n).toSubtypehi:↑i ∈ Fin m⊢ ↑⟨↑i, hi⟩ = ↑i inst✝:SetTheoryn:ℕm:ℕval:Objectproperty:val ∈ Fin nhi:↑⟨val, property⟩ ∈ Fin m⊢ ↑⟨↑⟨val, property⟩, hi⟩ = ↑⟨val, property⟩ inst✝:SetTheoryn:ℕm:ℕval:Objectproperty:val ∈ Fin nhi:↑⟨val, property⟩ ∈ Fin m⊢ ⋯.choose = ⋯.choose inst✝: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.chooseinst✝: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 All goals completed! 🐙 inst✝:SetTheoryn:ℕm:ℕval:Objectproperty:val ∈ Fin nhi:↑⟨val, property⟩ ∈ Fin mh1:∃ m_1 < m, val = ↑m_1h2:∃ m < n, val = ↑mthis:?_mvar.271371 := Exists.choose_spec _fvar.267727⊢ ↑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✝:?_mvar.271371 := Exists.choose_spec _fvar.267727this:?_mvar.271389 := Exists.choose_spec _fvar.267728⊢ ↑h1.choose = ↑h2.choose All goals completed! 🐙@[simp] theorem SetTheory.Set.Fin.toNat_mk {n:ℕ} (m:ℕ) (h: m < n) : (Fin_mk n m h : ℕ) = m := inst✝:SetTheoryn:ℕm:ℕh:m < n⊢ ↑(Fin_mk n m h) = m inst✝:SetTheoryn:ℕm:ℕh:m < nthis:?_mvar.273420 := Chapter3.SetTheory.Set.Fin.coe_toNat (Chapter3.SetTheory.Set.Fin_mk _fvar.273415 _fvar.273416 _fvar.273417)⊢ ↑(Fin_mk n m h) = m rwa [Object.natCast_injinst✝: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, inst✝:SetTheoryn:ℕN:ℕh:n ≤ Ni:(Fin n).toSubtype⊢ ↑i ∈ Fin N inst✝:SetTheoryn:ℕN:ℕh:n ≤ Ni:(Fin n).toSubtypethis:?_mvar.273573 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ↑i ∈ Fin N; inst✝:SetTheoryn:ℕN:ℕh:n ≤ Ni:(Fin n).toSubtypethis:∃ m < n, ↑i = ↑m⊢ ∃ m < N, ↑i = ↑m; All goals completed! 🐙 ⟩

Connections with Mathlib's overloaded, errors 1:4 Unknown identifier `n` 1:4 Unknown identifier `n`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 := inst✝:SetTheoryn:ℕm:_root_.Fin n⊢ (fun m => ⟨↑m, ⋯⟩) ((fun m => Fin_mk n ↑m ⋯) m) = m All goals completed! 🐙

Lemma 3.5.11 (finite choice)

theorem SetTheory.Set.finite_choice {n:ℕ} {X: Fin n → Set} (h: ∀ i, X i ≠ ∅) : iProd X ≠ ∅ := inst✝: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) inst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅inst✝: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 ≠ ∅ inst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅ have : Fin 0 = ∅ := inst✝:SetTheoryn:ℕX:(Fin n).toSubtype → Seth:∀ (i : (Fin n).toSubtype), X i ≠ ∅⊢ iProd X ≠ ∅ inst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅⊢ ∀ (x : Object), x ∉ Fin 0 All goals completed! 🐙 have empty (i:Fin 0) : X i := False.elim (inst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:@Chapter3.SetTheory.Set.Fin _fvar.276266 0 = @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := Eq.mpr (id (congrArg (fun _a => _a) (propext Chapter3.SetTheory.Set.eq_empty_iff_forall_notMem))) Chapter3.SetTheory.Set.finite_choice._proof_1i:(Fin 0).toSubtype⊢ False inst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:@Chapter3.SetTheory.Set.Fin _fvar.276266 0 = @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := Eq.mpr (id (congrArg (fun _a => _a) (propext Chapter3.SetTheory.Set.eq_empty_iff_forall_notMem))) Chapter3.SetTheory.Set.finite_choice._proof_1i:∅.toSubtype⊢ False; All goals completed! 🐙) inst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:Chapter3.SetTheory.Set.Fin 0 = ∅ := ?_mvar.276706empty:(i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 0).toSubtype) → Chapter3.SetTheory.Set.toSubtype (@_fvar.276559 i) := fun i => False.elim (@?_mvar.277183 i)⊢ tuple empty ∈ iProd X; inst✝:SetTheoryX:(Fin 0).toSubtype → Seth:∀ (i : (Fin 0).toSubtype), X i ≠ ∅this:Chapter3.SetTheory.Set.Fin 0 = ∅ := ?_mvar.276706empty:(i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 0).toSubtype) → Chapter3.SetTheory.Set.toSubtype (@_fvar.276559 i) := fun i => False.elim (@?_mvar.277183 i)⊢ ∃ x, tuple empty = tuple x; All goals completed! 🐙 set X' : Fin n → Set := fun i ↦ X (Fin_embed n (n+1) (inst✝: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 All goals completed! 🐙) i) inst✝: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':(Chapter3.SetTheory.Set.Fin _fvar.276566).toSubtype → Chapter3.Set := fun i => @_fvar.276573 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)hX':∀ (i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype), @_fvar.279391 i ≠ @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := fun i => @_fvar.276574 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)⊢ iProd X ≠ ∅ inst✝: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':(Chapter3.SetTheory.Set.Fin _fvar.276566).toSubtype → Chapter3.Set := fun i => @_fvar.276573 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)hX':∀ (i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype), @_fvar.279391 i ≠ @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := fun i => @_fvar.276574 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)x'_obj:Objecthx':x'_obj ∈ iProd X'⊢ iProd X ≠ ∅ inst✝: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':(Chapter3.SetTheory.Set.Fin _fvar.276566).toSubtype → Chapter3.Set := fun i => @_fvar.276573 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)hX':∀ (i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype), @_fvar.279391 i ≠ @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := fun i => @_fvar.276574 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)x'_obj:Objecthx':∃ x, x'_obj = tuple x⊢ iProd X ≠ ∅; inst✝: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':(Chapter3.SetTheory.Set.Fin _fvar.276566).toSubtype → Chapter3.Set := fun i => @_fvar.276573 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)hX':∀ (i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype), @_fvar.279391 i ≠ @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := fun i => @_fvar.276574 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)x':(i : (Fin n).toSubtype) → (X' i).toSubtype⊢ iProd X ≠ ∅ set last : Fin (n+1) := Fin_mk (n+1) n (inst✝: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':(@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype → Chapter3.Set := fun i => @_fvar.276573 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)hX':∀ (i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype), @_fvar.279391 i ≠ @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := fun i => @_fvar.276574 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)x':(i : (Fin n).toSubtype) → (X' i).toSubtype⊢ n < n + 1 All goals completed! 🐙) inst✝: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':(Chapter3.SetTheory.Set.Fin _fvar.276566).toSubtype → Chapter3.Set := fun i => @_fvar.276573 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)hX':∀ (i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype), @_fvar.279391 i ≠ @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := fun i => @_fvar.276574 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(Chapter3.SetTheory.Set.Fin (_fvar.276566 + 1)).toSubtype := Chapter3.SetTheory.Set.Fin_mk (_fvar.276566 + 1) _fvar.276566 ⋯a:Objectha:a ∈ X last⊢ iProd X ≠ ∅ have x : ∀ i, X i := fun i => if h : i = n then have : i = last := inst✝: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':(@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype → Chapter3.Set := fun i => @_fvar.276573 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)hX':∀ (i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype), @_fvar.279391 i ≠ @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := fun i => @_fvar.276574 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(@Chapter3.SetTheory.Set.Fin _fvar.276266 (_fvar.276566 + 1)).toSubtype := Chapter3.SetTheory.Set.Fin_mk (_fvar.276566 + 1) _fvar.276566 ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeh:↑i = n⊢ i = last inst✝: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':(@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype → Chapter3.Set := fun i => @_fvar.276573 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)hX':∀ (i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype), @_fvar.279391 i ≠ @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := fun i => @_fvar.276574 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(@Chapter3.SetTheory.Set.Fin _fvar.276266 (_fvar.276566 + 1)).toSubtype := Chapter3.SetTheory.Set.Fin_mk (_fvar.276566 + 1) _fvar.276566 ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeh:↑i = n⊢ ↑i = ↑last; All goals completed! 🐙 ⟨a, inst✝: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':(@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype → Chapter3.Set := fun i => @_fvar.276573 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)hX':∀ (i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype), @_fvar.279391 i ≠ @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := fun i => @_fvar.276574 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(@Chapter3.SetTheory.Set.Fin _fvar.276266 (_fvar.276566 + 1)).toSubtype := Chapter3.SetTheory.Set.Fin_mk (_fvar.276566 + 1) _fvar.276566 ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeh:↑i = nthis:_fvar.281668 = _fvar.281526 := Subtype.ext (Eq.mpr (id (Eq.trans (congrArg (fun x => x = ↑_fvar.276566) (Chapter3.SetTheory.Set.finite_choice._simp_1 _fvar.281668)) (Chapter3.SetTheory.Object.natCast_inj._simp_1 (↑_fvar.281668) _fvar.276566))) _fvar.286474)⊢ a ∈ X i All 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' := inst✝: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':(@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype → Chapter3.Set := fun i => @_fvar.276573 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)hX':∀ (i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype), @_fvar.279391 i ≠ @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := fun i => @_fvar.276574 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(@Chapter3.SetTheory.Set.Fin _fvar.276266 (_fvar.276566 + 1)).toSubtype := Chapter3.SetTheory.Set.Fin_mk (_fvar.276566 + 1) _fvar.276566 ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeh:¬↑i = nthis:↑_fvar.281668 < _fvar.276566 := lt_of_le_of_ne (Nat.lt_succ_iff.mp (Chapter3.SetTheory.Set.Fin.toNat_lt _fvar.281668)) _fvar.286502i':(@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype := Chapter3.SetTheory.Set.Fin_mk _fvar.276566 (↑_fvar.281668) _fvar.291025⊢ X i = X' i' All goals completed! 🐙 ⟨x' i', inst✝: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':(@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype → Chapter3.Set := fun i => @_fvar.276573 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)hX':∀ (i : (@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype), @_fvar.279391 i ≠ @EmptyCollection.emptyCollection Chapter3.Set Chapter3.SetTheory.Set.instEmpty := fun i => @_fvar.276574 (Chapter3.SetTheory.Set.Fin_embed _fvar.276566 (_fvar.276566 + 1) ⋯ i)x':(i : (Fin n).toSubtype) → (X' i).toSubtypelast:(@Chapter3.SetTheory.Set.Fin _fvar.276266 (_fvar.276566 + 1)).toSubtype := Chapter3.SetTheory.Set.Fin_mk (_fvar.276566 + 1) _fvar.276566 ⋯a:Objectha:a ∈ X lasti:(Fin (n + 1)).toSubtypeh:¬↑i = nthis✝:↑_fvar.281668 < _fvar.276566 := lt_of_le_of_ne (Nat.lt_succ_iff.mp (Chapter3.SetTheory.Set.Fin.toNat_lt _fvar.281668)) _fvar.286502i':(@Chapter3.SetTheory.Set.Fin _fvar.276266 _fvar.276566).toSubtype := Chapter3.SetTheory.Set.Fin_mk _fvar.276566 (↑_fvar.281668) _fvar.291025this:@_fvar.276573 _fvar.281668 = @_fvar.279391 _fvar.291032 := of_eq_true (Eq.trans (congrArg (fun x => @_fvar.276573 _fvar.281668 = @_fvar.276573 x) (Eq.trans ((fun {α} {p} val val_1 e_val => Eq.rec (motive := fun val_2 e_val => ∀ (property : p val), ⟨val, property⟩ = ⟨val_2, e_val ▸ property⟩) (fun property => Eq.refl ⟨val, property⟩) e_val) (↑(Chapter3.SetTheory.Set.Fin_mk _fvar.276566 (↑_fvar.281668) _fvar.291025)) (↑_fvar.281668) (Chapter3.SetTheory.Set.Fin.coe_toNat _fvar.281668) (@Chapter3.SetTheory.Set.Fin_embed._proof_2 _fvar.276266 _fvar.276566 (_fvar.276566 + 1) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.276566) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.276566 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.276566 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.atom_pf ↑_fvar.276566) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.276566) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑_fvar.276566) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)) (Eq.refl false))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 (_fvar.276566 + 1) _fvar.276566) (congrArg (fun x => x < ↑_fvar.276566) (Eq.trans (Nat.cast_add _fvar.276566 1) (congrArg (HAdd.hAdd ↑_fvar.276566) Nat.cast_one)))) a))))))) (Chapter3.SetTheory.Set.Fin_mk _fvar.276566 (↑_fvar.281668) _fvar.291025))) (Subtype.coe_eta _fvar.281668 (@Eq.ndrec Chapter3.Object (↑(Chapter3.SetTheory.Set.Fin_mk _fvar.276566 (↑_fvar.281668) _fvar.291025)) (fun val => (fun x => x ∈ @Chapter3.SetTheory.Set.Fin _fvar.276266 (_fvar.276566 + 1)) val) (@Chapter3.SetTheory.Set.Fin_embed._proof_2 _fvar.276266 _fvar.276566 (_fvar.276566 + 1) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑_fvar.276566) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.276566 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_zero (↑_fvar.276566 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.atom_pf ↑_fvar.276566) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (↑_fvar.276566) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑_fvar.276566) (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)) (Eq.refl false))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (id (Eq.mp (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 (_fvar.276566 + 1) _fvar.276566) (congrArg (fun x => x < ↑_fvar.276566) (Eq.trans (Nat.cast_add _fvar.276566 1) (congrArg (HAdd.hAdd ↑_fvar.276566) Nat.cast_one)))) a))))))) (Chapter3.SetTheory.Set.Fin_mk _fvar.276566 (↑_fvar.281668) _fvar.291025)) (↑_fvar.281668) (Chapter3.SetTheory.Set.Fin.coe_toNat _fvar.281668))))) (eq_self (@_fvar.276573 _fvar.281668)))⊢ ↑(x' i') ∈ X i All goals completed! 🐙⟩ 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' := inst✝:SetTheory⊢ Function.Injective fun p => SetTheory.set_to_object {p.fst, SetTheory.set_to_object {p.fst, p.snd}} All 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 on the structure would generate a lemma requiring proof of Unknown identifier `t.x`sorry = sorry : Propt.x = Unknown identifier `t'.x`t'.x, but these functions have different types when Unknown identifier `t.X`sorry ≠ sorry : Propt.X ≠ Unknown identifier `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' := inst✝: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' inst✝: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'; 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✝ }; inst✝: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✝ }; inst✝: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✝; inst✝: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✝); All 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) := inst✝:SetTheoryn:ℕt:Tuple nt':Tuple n⊢ t = t' ↔ ∀ (n_1 : (Fin n).toSubtype), ↑(t.x n_1) = ↑(t'.x n_1) All goals completed! 🐙
noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'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 Chapter3.OrderedPair.eq.{u_1, u_2} [SetTheory] (x y x' y' : Object) : { fst := x, snd := y } = { fst := x', snd := y' } ↔ x = x' ∧ y = y'OrderedPair.eq or Chapter3.SetTheory.Set.tuple_inj.{u_1, u_2} [SetTheory] {I : Set} {X : I.toSubtype → Set} (x y : (i : I.toSubtype) → (X i).toSubtype) : tuple x = tuple y ↔ x = ySetTheory.Set.tuple_inj

theorem declaration uses 'sorry'OrderedPair.refl (p: OrderedPair) : p = p := inst✝:SetTheoryp:OrderedPair⊢ p = p All goals completed! 🐙
theorem declaration uses 'sorry'OrderedPair.symm (p q: OrderedPair) : p = q ↔ q = p := inst✝:SetTheoryp:OrderedPairq:OrderedPair⊢ p = q ↔ q = p All goals completed! 🐙theorem declaration uses 'sorry'OrderedPair.trans {p q r: OrderedPair} (hpq: p=q) (hqr: q=r) : p=r := inst✝:SetTheoryp:OrderedPairq:OrderedPairr:OrderedPairhpq:p = qhqr:q = r⊢ p = r All goals completed! 🐙theorem declaration uses 'sorry'SetTheory.Set.tuple_refl {I:Set} {X: I → Set} (a: ∀ i, X i) : tuple a = tuple a := inst✝:SetTheoryI:SetX:I.toSubtype → Seta:(i : I.toSubtype) → (X i).toSubtype⊢ tuple a = tuple a All 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 := inst✝: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 All 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 := inst✝: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 All 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) := inst✝:SetTheoryA:SetB:SetC:Set⊢ A ×ˢ (B ∪ C) = A ×ˢ B ∪ A ×ˢ C All 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) := inst✝:SetTheoryA:SetB:SetC:Set⊢ A ×ˢ (B ∩ C) = A ×ˢ B ∩ A ×ˢ C All 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) := inst✝:SetTheoryA:SetB:SetC:Set⊢ A ×ˢ (B \ C) = A ×ˢ B \ A ×ˢ C All 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) := inst✝:SetTheoryA:SetB:SetC:Set⊢ (A ∪ B) ×ˢ C = A ×ˢ C ∪ B ×ˢ C All 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) := inst✝:SetTheoryA:SetB:SetC:Set⊢ (A ∩ B) ×ˢ C = A ×ˢ C ∩ B ×ˢ C All 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) := inst✝:SetTheoryA:SetB:SetC:Set⊢ (A \ B) ×ˢ C = A ×ˢ C \ B ×ˢ C All 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) := inst✝:SetTheoryA:SetB:SetC:SetD:Set⊢ A ×ˢ B ∩ C ×ˢ D = (A ∩ C) ×ˢ (B ∩ D) All 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)) := inst✝: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`. All 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)) := inst✝: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`. All 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 := inst✝:SetTheoryA:SetB:SetC:SetD:SethA:A ≠ ∅hB:B ≠ ∅hC:C ≠ ∅hD:D ≠ ∅⊢ A ×ˢ B ⊆ C ×ˢ D ↔ A ⊆ C ∧ B ⊆ D All 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) := inst✝: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`. All 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 := inst✝:SetTheoryX:SetY:SetZ:Setf:Z.toSubtype → X.toSubtypeg:Z.toSubtype → Y.toSubtype⊢ ∃! h, fst ∘ h = f ∧ snd ∘ h = g All 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 = ∅ := inst✝:SetTheoryn:ℕX:(Fin n).toSubtype → Set⊢ iProd X = ∅ ↔ ∃ i, X i = ∅ All 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))) := inst✝: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) All 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' := inst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypef':X.toSubtype → Y.toSubtype⊢ graph f = graph f' ↔ f = f' All 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 := inst✝:SetTheoryX:SetY:SetG:SethG:G ⊆ X ×ˢ Yhvert:∀ (x : X.toSubtype), ∃! y, OrderedPair.toObject { fst := ↑x, snd := ↑y } ∈ G⊢ ∃! f, G = graph f All goals completed! 🐙

Exercise 3.5.11. This trivially follows from Chapter3.SetTheory.Set.powerset_axiom.{u_1, u_2} [SetTheory] {X Y : Set} (F : Object) : F ∈ X ^ Y ↔ ∃ f, ↑f = FSetTheory.Set.powerset_axiom, but the exercise is to derive it from Chapter3.SetTheory.Set.exists_powerset.{u_1, u_2} [SetTheory] (X : Set) : ∃ Z, ∀ (x : Object), x ∈ Z ↔ ∃ Y, x = SetTheory.set_to_object Y ∧ Y ⊆ XSetTheory.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) := inst✝:SetTheoryX:Setf:nat.toSubtype → X.toSubtype → X.toSubtypec:X.toSubtype⊢ ∃! a, a 0 = c ∧ ∀ (n : ℕ), a ↑(n + 1) = f (↑n) (a ↑n) All 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' := inst✝: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 := inst✝: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' All goals completed! 🐙 inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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' inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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' inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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'inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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₂ inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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' inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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' inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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 finst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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' inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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 inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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 finst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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 inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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 inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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 inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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 = x2inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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 inst✝: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 : (@Chapter3.nat _fvar.324429).toSubtype} {n : ℕ}, Chapter3.SetTheory.Set.nat_equiv.symm m = n → m = ↑n := fun {m} {n} => @?_mvar.325256 m nnat_coe_eq_zero:∀ {m : (@Chapter3.nat _fvar.324429).toSubtype}, Chapter3.SetTheory.Set.nat_equiv.symm m = 0 → m = 0 := fun {m} => @_fvar.325257 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 All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙
end Chapter3