Functions

Analysis I, Section 3.3: Functions

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:

A notion of function Unknown identifier `Function`Function X Y between two sets Unknown identifier `X`X, Unknown identifier `Y`Y in the set theory of Section 3.1
Various relations with the Mathlib notion of a function Unknown identifier `X`sorry → sorry : Sort (imax u_1 u_2)X → Unknown identifier `Y`Y between two types Unknown identifier `X`X, Unknown identifier `Y`Y. (Note from Section 3.1 that every Set.{u} (α : Type u) : Type uSet Unknown identifier `X`X can also be viewed as a subtype { x // x ∈ sorry } : Type u_1{x : Unknown identifier `Object`Object // x ∈ Unknown identifier `X`X } of Unknown identifier `Object`Object.)
Basic function properties and operations, such as composition, one-to-one and onto functions, and inverses.

In the rest of the book we will deprecate the Chapter 3 version of a function, and work with the Mathlib notion of a function instead. Even within this section, we will switch to the Mathlib formalism for some of the examples involving number systems such as ℤ : Typeℤ or ℝ : Typeℝ that have not been implemented in the Chapter 3 framework.

We will work here with the version Nat : TypeNat of the natural numbers internal to the Chapter 3 set theory, though usually we will use coercions to then immediately translate to the Mathlib natural numbers ℕ : Typeℕ.

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)variable [SetTheory]

Definition 3.3.1. Function sorry sorry : Type u_2Function Unknown identifier `X`X Unknown identifier `Y`Y is the structure of functions from Unknown identifier `X`X to Unknown identifier `Y`Y. Analogous to the Mathlib type Unknown identifier `X`sorry → sorry : Sort (imax u_1 u_2)X → Unknown identifier `Y`Y.

@[ext]
structure Function (X Y: Set) where
  P : X → Y → Prop
  unique : ∀ x: X, ∃! y: Y, P x y

Chapter3.Function.mk.{u_1, u_2} [SetTheory] {X Y : Set} (P : X.toSubtype → Y.toSubtype → Prop)
  (unique : ∀ (x : X.toSubtype), ∃! y, P x y) : Function X Y

Converting a Chapter 3 function to a Mathlib function . The Chapter 3 definition of a function was nonconstructive, so we have to use the axiom of choice here.

noncomputable def Function.to_fn {X Y: Set} (f: Function X Y) : X → Y :=
  fun x ↦ (f.unique x).choose

noncomputable instance Function.inst_coefn (X Y: Set) : CoeFun (Function X Y) (fun _ ↦ X → Y) where
  coe := Function.to_fn

theorem Function.to_fn_eval {X Y: Set} (f: Function X Y) (x:X) : f.to_fn x = f x := rfl

Converting a Mathlib function to a Chapter 3 Chapter3.Function.{u_1, u_2} [SetTheory] (X Y : Set) : Type u_2Function

abbrev Function.mk_fn {X Y: Set} (f: X → Y) : Function X Y :=
  Function.mk (fun x y ↦ y = f x) (byinst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtype⊢ ∀ (x : X.toSubtype), ∃! y, (fun x y => y = f x) x y simpAll goals completed! 🐙)

Definition 3.3.1

theorem Function.eval {X Y: Set} (f: Function X Y) (x: X) (y: Y) : y = f x ↔ f.P x y := byinst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypey:Y.toSubtype⊢ y = f.to_fn x ↔ f.P x y
  convert ((f.unique x).choose_iff y).symmAll goals completed! 🐙

@[simp]
theorem Function.eval_of {X Y: Set} (f: X → Y) (x:X) : (Function.mk_fn f) x = f x := byinst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypex:X.toSubtype⊢ (mk_fn f).to_fn x = f x
  symminst✝:SetTheoryX:SetY:Setf:X.toSubtype → Y.toSubtypex:X.toSubtype⊢ f x = (mk_fn f).to_fn x; rw [eval]All goals completed! 🐙

Example 3.3.3.

abbrev P_3_3_3a : Nat → Nat → Prop := fun x y ↦ (y:ℕ) = (x:ℕ)+1

theorem SetTheory.Set.P_3_3_3a_existsUnique (x: Nat) : ∃! y: Nat, P_3_3_3a x y := byinst✝:SetTheoryx:Nat.toSubtype⊢ ∃! y, P_3_3_3a x y
  apply ExistsUnique.intro ((x+1:ℕ):Nat)h₁inst✝:SetTheoryx:Nat.toSubtype⊢ P_3_3_3a x ↑(nat_equiv.symm x + 1)h₂inst✝:SetTheoryx:Nat.toSubtype⊢ ∀ (y : Nat.toSubtype), P_3_3_3a x y → y = ↑(nat_equiv.symm x + 1)
  .h₁inst✝:SetTheoryx:Nat.toSubtype⊢ P_3_3_3a x ↑(nat_equiv.symm x + 1) simp [P_3_3_3a]All goals completed! 🐙
  intro y hh₂inst✝:SetTheoryx:Nat.toSubtypey:Nat.toSubtypeh:P_3_3_3a x y⊢ y = ↑(nat_equiv.symm x + 1)
  simpa [P_3_3_3a, Equiv.symm_apply_eq] using hAll goals completed! 🐙

abbrev SetTheory.Set.f_3_3_3a : Function Nat Nat := Function.mk P_3_3_3a P_3_3_3a_existsUnique

theorem SetTheory.Set.f_3_3_3a_eval (x y: Nat) : y = f_3_3_3a x ↔ (y:ℕ) = (x+1:ℕ) :=
  Function.eval _ _ _

theorem SetTheory.Set.f_3_3_3a_eval' (n: ℕ) : f_3_3_3a (n:Nat) = (n+1:ℕ) := byinst✝:SetTheoryn:ℕ⊢ f_3_3_3a.to_fn ↑n = ↑(n + 1)
  symminst✝:SetTheoryn:ℕ⊢ ↑(n + 1) = f_3_3_3a.to_fn ↑n
  simp only [f_3_3_3a_eval, nat_equiv_coe_of_coe]All goals completed! 🐙

theorem SetTheory.Set.f_3_3_3a_eval'' : f_3_3_3a 4 = 5 := f_3_3_3a_eval' 4

theorem SetTheory.Set.f_3_3_3a_eval''' (n:ℕ) : f_3_3_3a (2*n+3: ℕ) = (2*n+4:ℕ) := byinst✝:SetTheoryn:ℕ⊢ f_3_3_3a.to_fn ↑(2 * n + 3) = ↑(2 * n + 4)
  convert f_3_3_3a_eval' _All goals completed! 🐙

abbrev SetTheory.Set.P_3_3_3b : Nat → Nat → Prop := fun x y ↦ (y+1:ℕ) = (x:ℕ)

theorem SetTheory.Set.not_P_3_3_3b_existsUnique : ¬ ∀ x, ∃! y: Nat, P_3_3_3b x y := byinst✝:SetTheory⊢ ¬∀ (x : Nat.toSubtype), ∃! y, P_3_3_3b x y
  by_contra hinst✝:SetTheoryh:∀ (x : Nat.toSubtype), ∃! y, P_3_3_3b x y⊢ False
  choose n hn _ using h (0:Nat)inst✝:SetTheoryh:∀ (x : Nat.toSubtype), ∃! y, P_3_3_3b x yn:Nat.toSubtypehn:P_3_3_3b 0 na✝:∀ (y : Nat.toSubtype), (fun y => P_3_3_3b 0 y) y → y = n⊢ False
  have : ((0:Nat):ℕ) = 0 := byinst✝:SetTheory⊢ ¬∀ (x : Nat.toSubtype), ∃! y, P_3_3_3b x y simp [OfNat.ofNat]All goals completed! 🐙
  simp [P_3_3_3b, this] at hnAll goals completed! 🐙

abbrev SetTheory.Set.P_3_3_3c : (Nat \ {(0:Object)}: Set) → Nat → Prop :=
  fun x y ↦ ((y+1:ℕ):Object) = x

theorem SetTheory.Set.P_3_3_3c_existsUnique (x: (Nat \ {(0:Object)}: Set)) :
    ∃! y: Nat, P_3_3_3c x y := byinst✝:SetTheoryx:(Nat \ {0}).toSubtype⊢ ∃! y, P_3_3_3c x y
  -- Some technical unpacking here due to the subtle distinctions between the `Object` type,
  -- sets converted to subtypes of `Object`, and subsets of those sets.
  obtain ⟨ x, hx ⟩ := xmkinst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}⊢ ∃! y, P_3_3_3c ⟨x, hx⟩ y; simp at hxmkinst✝:SetTheoryx:Objecthx✝:x ∈ Nat \ {0}hx:x ∈ Nat ∧ ¬x = 0⊢ ∃! y, P_3_3_3c ⟨x, hx✝⟩ y; obtain ⟨ hx1, hx2 ⟩ := hxmk.introinst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Nathx2:¬x = 0⊢ ∃! y, P_3_3_3c ⟨x, hx⟩ y
  set n := ((⟨ x, hx1 ⟩:Nat):ℕ)mk.introinst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Nathx2:¬x = 0n:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩⊢ ∃! y, P_3_3_3c ⟨x, hx⟩ y
  have : x = (n:Nat) := byinst✝:SetTheoryx:(Nat \ {0}).toSubtype⊢ ∃! y, P_3_3_3c x y simp [n]All goals completed! 🐙
  simp [P_3_3_3c, this, Object.ofnat_eq'] at hx2 ⊢mk.introinst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Natn:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩this:_fvar.50161 = ↑↑_fvar.50593 := ?_mvar.51000hx2:¬n = 0⊢ ∃! y, nat_equiv.symm y + 1 = n
  replace hx2 : n = (n-1) + 1 := byinst✝:SetTheoryx:(Nat \ {0}).toSubtype⊢ ∃! y, P_3_3_3c x y omegaAll goals completed! 🐙
  apply ExistsUnique.intro ((n-1:ℕ):Nat)mk.intro.h₁inst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Natn:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩this:_fvar.50161 = ↑↑_fvar.50593 := ?_mvar.51000hx2:_fvar.50593 = _fvar.50593 - 1 + 1 := ?_mvar.59231⊢ nat_equiv.symm ↑(n - 1) + 1 = nmk.intro.h₂inst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Natn:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩this:_fvar.50161 = ↑↑_fvar.50593 := ?_mvar.51000hx2:_fvar.50593 = _fvar.50593 - 1 + 1 := ?_mvar.59231⊢ ∀ (y : Nat.toSubtype), nat_equiv.symm y + 1 = n → y = ↑(n - 1)
  .mk.intro.h₁inst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Natn:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩this:_fvar.50161 = ↑↑_fvar.50593 := ?_mvar.51000hx2:_fvar.50593 = _fvar.50593 - 1 + 1 := ?_mvar.59231⊢ nat_equiv.symm ↑(n - 1) + 1 = n simp [←hx2]All goals completed! 🐙
  intro y hymk.intro.h₂inst✝:SetTheoryx:Objecthx:x ∈ Nat \ {0}hx1:x ∈ Natn:ℕ := Chapter3.SetTheory.Set.nat_equiv.symm ⟨_fvar.50161, _fvar.50449⟩this:_fvar.50161 = ↑↑_fvar.50593 := ?_mvar.51000hx2:_fvar.50593 = _fvar.50593 - 1 + 1 := ?_mvar.59231y:Nat.toSubtypehy:nat_equiv.symm y + 1 = n⊢ y = ↑(n - 1); simp [←hy]All goals completed! 🐙

abbrev SetTheory.Set.f_3_3_3c : Function (Nat \ {(0:Object)}: Set) Nat :=
  Function.mk P_3_3_3c P_3_3_3c_existsUnique

theorem SetTheory.Set.f_3_3_3c_eval (x: (Nat \ {(0:Object)}: Set)) (y: Nat) :
    y = f_3_3_3c x ↔ ((y+1:ℕ):Object) = x := Function.eval _ _ _

Create a version of a non-zero Unknown identifier `n`n inside Nat \ {0} : SetNat \ {0} for any natural number n.

abbrev SetTheory.Set.coe_nonzero (n:ℕ) (h: n ≠ 0): (Nat \ {(0:Object)}: Set) :=
  ⟨((n:ℕ):Object), byinst✝:SetTheoryn:ℕh:n ≠ 0⊢ ↑n ∈ Nat \ {0}
    simp [Object.ofnat_eq',h]inst✝:SetTheoryn:ℕh:n ≠ 0⊢ ↑n ∈ Nat
    rw [←Object.ofnat_eq]inst✝:SetTheoryn:ℕh:n ≠ 0⊢ ↑↑n ∈ Nat
    exact Subtype.property _All goals completed! 🐙
  ⟩

theorem SetTheory.Set.f_3_3_3c_eval' (n: ℕ) : f_3_3_3c (coe_nonzero (n+1) (byinst✝:SetTheoryn:ℕ⊢ n + 1 ≠ 0 positivityAll goals completed! 🐙)) = n := byinst✝:SetTheoryn:ℕ⊢ f_3_3_3c.to_fn (coe_nonzero (n + 1) ⋯) = ↑n
  symminst✝:SetTheoryn:ℕ⊢ ↑n = f_3_3_3c.to_fn (coe_nonzero (n + 1) ⋯); simp [f_3_3_3c_eval]All goals completed! 🐙

theorem SetTheory.Set.f_3_3_3c_eval'' : f_3_3_3c (coe_nonzero 4 (byinst✝:SetTheory⊢ 4 ≠ 0 positivityAll goals completed! 🐙)) = 3 := byinst✝:SetTheory⊢ f_3_3_3c.to_fn (coe_nonzero 4 ⋯) = 3
  convert f_3_3_3c_eval' 3All goals completed! 🐙

theorem SetTheory.Set.f_3_3_3c_eval''' (n:ℕ) :
    f_3_3_3c (coe_nonzero (2*n+3) (byinst✝:SetTheoryn:ℕ⊢ 2 * n + 3 ≠ 0 positivityAll goals completed! 🐙)) = (2*n+2:ℕ) := byinst✝:SetTheoryn:ℕ⊢ f_3_3_3c.to_fn (coe_nonzero (2 * n + 3) ⋯) = ↑(2 * n + 2) convert f_3_3_3c_eval' (2*n+2)All goals completed! 🐙

Example 3.3.4 is a little tricky to replicate with the current formalism as the real numbers have not been constructed yet. Instead, I offer some Mathlib counterparts, using the Mathlib API for NNReal : TypeNNReal and ℝ : Typeℝ.

example : ¬ ∃ f: ℝ → ℝ, ∀ x y, y = f x ↔ y^2 = x := byinst✝:SetTheory⊢ ¬∃ f, ∀ (x y : ℝ), y = f x ↔ y ^ 2 = x
  by_contra hinst✝:SetTheoryh:∃ f, ∀ (x y : ℝ), y = f x ↔ y ^ 2 = x⊢ False
  obtain ⟨f, hf⟩ := hintroinst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = x⊢ False; set y := f (-1)introinst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = xy:ℝ := @_fvar.81408 (-1)⊢ False
  have h1 := (hf _ y).mp (byinst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = xy:ℝ := @_fvar.81408 (-1)⊢ y = f ?m.49 rflAll goals completed! 🐙)
  have h2 := sq_nonneg yintroinst✝:SetTheoryf:ℝ → ℝhf:∀ (x y : ℝ), y = f x ↔ y ^ 2 = xy:ℝ := @_fvar.81408 (-1)h1:?_mvar.81525 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h2:?_mvar.81542 := sq_nonneg _fvar.81471⊢ False
  linarithAll goals completed! 🐙

example : ¬ ∃ f: NNReal → ℝ, ∀ x y, y = f x ↔ y^2 = x := byinst✝:SetTheory⊢ ¬∃ f, ∀ (x : NNReal) (y : ℝ), y = f x ↔ y ^ 2 = ↑x
  by_contra hinst✝:SetTheoryh:∃ f, ∀ (x : NNReal) (y : ℝ), y = f x ↔ y ^ 2 = ↑x⊢ False
  obtain ⟨f, hf⟩ := hintroinst✝:SetTheoryf:NNReal → ℝhf:∀ (x : NNReal) (y : ℝ), y = f x ↔ y ^ 2 = ↑x⊢ False; specialize hf 4introinst✝:SetTheoryf:NNReal → ℝhf:∀ (y : ℝ), y = f 4 ↔ y ^ 2 = ↑4⊢ False; set y := f 4introinst✝:SetTheoryf:NNReal → ℝy:ℝ := @_fvar.82895 4hf:∀ (y_1 : ℝ), y_1 = y ↔ y_1 ^ 2 = ↑4⊢ False
  have hy := (hf y).mp (byinst✝:SetTheoryf:NNReal → ℝy:ℝ := @_fvar.82895 4hf:∀ (y_1 : ℝ), y_1 = y ↔ y_1 ^ 2 = ↑4⊢ y = y rflAll goals completed! 🐙)
  have h1 : 2 = y := (hf 2).mpr (byinst✝:SetTheoryf:NNReal → ℝy:ℝ := @_fvar.82895 4hf:∀ (y_1 : ℝ), y_1 = y ↔ y_1 ^ 2 = ↑4hy:_fvar.83076 ^ 2 = ↑4 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ 2 ^ 2 = ↑4 norm_numAll goals completed! 🐙)
  have h2 : -2 = y := (hf (-2)).mpr (byinst✝:SetTheoryf:NNReal → ℝy:ℝ := @_fvar.82895 4hf:∀ (y_1 : ℝ), y_1 = y ↔ y_1 ^ 2 = ↑4hy:_fvar.83076 ^ 2 = ↑4 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:2 = _fvar.83076 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ (-2) ^ 2 = ↑4 norm_numAll goals completed! 🐙)
  linarithAll goals completed! 🐙

example : ∃ f: NNReal → NNReal, ∀ x y, y = f x ↔ y^2 = x := byinst✝:SetTheory⊢ ∃ f, ∀ (x y : NNReal), y = f x ↔ y ^ 2 = x
  use NNReal.sqrthinst✝:SetTheory⊢ ∀ (x y : NNReal), y = NNReal.sqrt x ↔ y ^ 2 = x; intro x yhinst✝:SetTheoryx:NNRealy:NNReal⊢ y = NNReal.sqrt x ↔ y ^ 2 = x
  constructorh.mpinst✝:SetTheoryx:NNRealy:NNReal⊢ y = NNReal.sqrt x → y ^ 2 = xh.mprinst✝:SetTheoryx:NNRealy:NNReal⊢ y ^ 2 = x → y = NNReal.sqrt x <;>h.mpinst✝:SetTheoryx:NNRealy:NNReal⊢ y = NNReal.sqrt x → y ^ 2 = xh.mprinst✝:SetTheoryx:NNRealy:NNReal⊢ y ^ 2 = x → y = NNReal.sqrt x intro hh.mprinst✝:SetTheoryx:NNRealy:NNRealh:y ^ 2 = x⊢ y = NNReal.sqrt x
  ·h.mpinst✝:SetTheoryx:NNRealy:NNRealh:y = NNReal.sqrt x⊢ y ^ 2 = x rw [h, NNReal.sq_sqrt]All goals completed! 🐙
  ·h.mprinst✝:SetTheoryx:NNRealy:NNRealh:y ^ 2 = x⊢ y = NNReal.sqrt x rw [←h, NNReal.sqrt_sq]All goals completed! 🐙

Example 3.3.5. The unused variable Unknown identifier `_x`_x is underscored to avoid triggering a linter.

abbrev SetTheory.Set.P_3_3_5 : Nat → Nat → Prop := fun _x y ↦ y = 7

theorem SetTheory.Set.P_3_3_5_existsUnique (x: Nat) : ∃! y: Nat, P_3_3_5 x y := byinst✝:SetTheoryx:Nat.toSubtype⊢ ∃! y, P_3_3_5 x y
  apply ExistsUnique.intro 7h₁inst✝:SetTheoryx:Nat.toSubtype⊢ P_3_3_5 x 7h₂inst✝:SetTheoryx:Nat.toSubtype⊢ ∀ (y : Nat.toSubtype), P_3_3_5 x y → y = 7 <;>h₁inst✝:SetTheoryx:Nat.toSubtype⊢ P_3_3_5 x 7h₂inst✝:SetTheoryx:Nat.toSubtype⊢ ∀ (y : Nat.toSubtype), P_3_3_5 x y → y = 7 simp [P_3_3_5]All goals completed! 🐙

abbrev SetTheory.Set.f_3_3_5 : Function Nat Nat := Function.mk P_3_3_5 P_3_3_5_existsUnique

theorem SetTheory.Set.f_3_3_5_eval (x: Nat) : f_3_3_5 x = 7 := byinst✝:SetTheoryx:Nat.toSubtype⊢ f_3_3_5.to_fn x = 7
  symminst✝:SetTheoryx:Nat.toSubtype⊢ 7 = f_3_3_5.to_fn x; rw [Function.eval]All goals completed! 🐙

Definition 3.3.8 (Equality of functions)

theorem Function.eq_iff {X Y: Set} (f g: Function X Y) : f = g ↔ ∀ x: X, f x = g x := byinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g ↔ ∀ (x : X.toSubtype), f.to_fn x = g.to_fn x
  constructormpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g → ∀ (x : X.toSubtype), f.to_fn x = g.to_fn xmprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ (∀ (x : X.toSubtype), f.to_fn x = g.to_fn x) → f = g <;>mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g → ∀ (x : X.toSubtype), f.to_fn x = g.to_fn xmprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ (∀ (x : X.toSubtype), f.to_fn x = g.to_fn x) → f = g intro hmprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn x⊢ f = g
  .mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:f = g⊢ ∀ (x : X.toSubtype), f.to_fn x = g.to_fn x simp [h]All goals completed! 🐙
  ext x ympr.P.h.h.ainst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtype⊢ f.P x y ↔ g.P x y; constructormpr.P.h.h.a.mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtype⊢ f.P x y → g.P x ympr.P.h.h.a.mprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtype⊢ g.P x y → f.P x y <;>mpr.P.h.h.a.mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtype⊢ f.P x y → g.P x ympr.P.h.h.a.mprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtype⊢ g.P x y → f.P x y introsmpr.P.h.h.a.mprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtypea✝:g.P x y⊢ f.P x y
  .mpr.P.h.h.a.mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtypea✝:f.P x y⊢ g.P x y rwa [←Function.eval, ←h x, Function.eval]mpr.P.h.h.a.mpinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtypea✝:f.P x y⊢ f.P x y
  rwa [←Function.eval, h x, Function.eval]mpr.P.h.h.a.mprinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:∀ (x : X.toSubtype), f.to_fn x = g.to_fn xx:X.toSubtypey:Y.toSubtypea✝:g.P x y⊢ g.P x y

Example 3.3.10 (simplified). The second part of the example is tricky to replicate in this formalism, so a Mathlib substitute is offered instead.

abbrev SetTheory.Set.f_3_3_10a : Function Nat Nat := Function.mk_fn (fun x ↦ (x^2 + 2*x + 1:ℕ))

abbrev SetTheory.Set.f_3_3_10b : Function Nat Nat := Function.mk_fn (fun x ↦ ((x+1)^2:ℕ))

theorem SetTheory.Set.f_3_3_10_eq : f_3_3_10a = f_3_3_10b := byinst✝:SetTheory⊢ f_3_3_10a = f_3_3_10b
  simp_rw [Function.eq_iff, Function.eval_of]inst✝:SetTheory⊢ ∀ (x : Nat.toSubtype), ↑(nat_equiv.symm x ^ 2 + 2 * nat_equiv.symm x + 1) = ↑((nat_equiv.symm x + 1) ^ 2)
  introsinst✝:SetTheoryx✝:Nat.toSubtype⊢ ↑(nat_equiv.symm x✝ ^ 2 + 2 * nat_equiv.symm x✝ + 1) = ↑((nat_equiv.symm x✝ + 1) ^ 2); simpinst✝:SetTheoryx✝:Nat.toSubtype⊢ nat_equiv.symm x✝ ^ 2 + 2 * nat_equiv.symm x✝ + 1 = (nat_equiv.symm x✝ + 1) ^ 2; ringAll goals completed! 🐙

example : (fun x:NNReal ↦ (x:ℝ)) = (fun x:NNReal ↦ |(x:ℝ)|) := byinst✝:SetTheory⊢ (fun x => ↑x) = fun x => |↑x|
  simp_rw [NNReal.abs_eq]All goals completed! 🐙

example : (fun x:ℝ ↦ (x:ℝ)) ≠ (fun x:ℝ ↦ |(x:ℝ)|) := byinst✝:SetTheory⊢ (fun x => x) ≠ fun x => |x|
  intro hinst✝:SetTheoryh:(fun x => x) = fun x => |x|⊢ False
  let a := (fun (x:ℝ) ↦ x) (-1)inst✝:SetTheoryh:(fun x => x) = fun x => |x|a:?_mvar.91839 := (fun x => x) (-1)⊢ False
  let b := (fun x:ℝ ↦ |(x:ℝ)|) (-1)inst✝:SetTheoryh:(fun x => x) = fun x => |x|a:?_mvar.91839 := (fun x => x) (-1)b:?_mvar.91906 := (fun x => |x|) (-1)⊢ False
  have hab : a = b := byinst✝:SetTheory⊢ (fun x => x) ≠ fun x => |x| unfold ainst✝:SetTheoryh:(fun x => x) = fun x => |x|a:?_mvar.91839 := (fun x => x) (-1)b:?_mvar.91906 := (fun x => |x|) (-1)⊢ (fun x => x) (-1) = b; rw [h]All goals completed! 🐙
  norm_num [a, b] at habAll goals completed! 🐙

Example 3.3.11

abbrev SetTheory.Set.f_3_3_11 (X:Set) : Function (∅:Set) X :=
  Function.mk (fun _ _ ↦ True) (byinst✝:SetTheoryX:Set⊢ ∀ (x : ∅.toSubtype), ∃! y, (fun x x => True) x y intro ⟨ x,hx ⟩inst✝:SetTheoryX:Setx:Objecthx:x ∈ ∅⊢ ∃! y, (fun x x => True) ⟨x, hx⟩ y; simp at hxAll goals completed! 🐙)

theorem declaration uses 'sorry'SetTheory.Set.empty_function_unique {X: Set} (f g: Function (∅:Set) X) : f = g := byinst✝:SetTheoryX:Setf:Function ∅ Xg:Function ∅ X⊢ f = g sorryAll goals completed! 🐙

Definition 3.3.13 (Composition)

noncomputable abbrev Function.comp {X Y Z: Set} (g: Function Y Z) (f: Function X Y) :
    Function X Z :=
  Function.mk_fn (fun x ↦ g (f x))

-- `∘` is already taken in Mathlib for the composition of Mathlib functions,
-- so we use `○` here instead to avoid ambiguity.
infix:90 "○" => Function.comp

theorem Function.comp_eval {X Y Z: Set} (g: Function Y Z) (f: Function X Y) (x: X) :
    (g ○ f) x = g (f x) := Function.eval_of _ _

Compatibility with Mathlib's composition operation.

theorem Function.comp_eq_comp {X Y Z: Set} (g: Function Y Z) (f: Function X Y) :
    (g ○ f).to_fn = g.to_fn ∘ f.to_fn := byinst✝:SetTheoryX:SetY:SetZ:Setg:Function Y Zf:Function X Y⊢ (g○f).to_fn = g.to_fn ∘ f.to_fn
  exth.ainst✝:SetTheoryX:SetY:SetZ:Setg:Function Y Zf:Function X Yx✝:X.toSubtype⊢ ↑((g○f).to_fn x✝) = ↑((g.to_fn ∘ f.to_fn) x✝); simp only [Function.comp_eval, Function.comp_apply]All goals completed! 🐙

Example 3.3.14

abbrev SetTheory.Set.f_3_3_14 : Function Nat Nat := Function.mk_fn (fun x ↦ (2*x:ℕ))

abbrev SetTheory.Set.g_3_3_14 : Function Nat Nat := Function.mk_fn (fun x ↦ (x+3:ℕ))

theorem SetTheory.Set.g_circ_f_3_3_14 :
    g_3_3_14 ○ f_3_3_14 = Function.mk_fn (fun x ↦ ((2*(x:ℕ)+3:ℕ):Nat)) := byinst✝:SetTheory⊢ g_3_3_14○f_3_3_14 = Function.mk_fn fun x => ↑(2 * nat_equiv.symm x + 3)
  simp [Function.eq_iff, Function.eval_of]All goals completed! 🐙

theorem SetTheory.Set.f_circ_g_3_3_14 :
    f_3_3_14 ○ g_3_3_14 = Function.mk_fn (fun x ↦ ((2*(x:ℕ)+6:ℕ):Nat)) := byinst✝:SetTheory⊢ f_3_3_14○g_3_3_14 = Function.mk_fn fun x => ↑(2 * nat_equiv.symm x + 6)
  simp [Function.eq_iff, Function.eval_of]inst✝:SetTheory⊢ ∀ (a : Object) (b : a ∈ Nat), 2 * (nat_equiv.symm ⟨a, b⟩ + 3) = 2 * nat_equiv.symm ⟨a, b⟩ + 6
  introsinst✝:SetTheorya✝:Objectb✝:a✝ ∈ Nat⊢ 2 * (nat_equiv.symm ⟨a✝, b✝⟩ + 3) = 2 * nat_equiv.symm ⟨a✝, b✝⟩ + 6; ringAll goals completed! 🐙

Lemma 3.3.15 (Composition is associative)

theorem SetTheory.Set.comp_assoc {W X Y Z: Set} (h: Function Y Z) (g: Function X Y)
  (f: Function W X) :
    h ○ (g ○ f) = (h ○ g) ○ f := byinst✝:SetTheoryW:SetX:SetY:SetZ:Seth:Function Y Zg:Function X Yf:Function W X⊢ h○(g○f) = (h○g)○f
  simp [Function.eq_iff]All goals completed! 🐙

abbrev Function.one_to_one {X Y: Set} (f: Function X Y) : Prop := ∀ x x': X, x ≠ x' → f x ≠ f x'

theorem Function.one_to_one_iff {X Y: Set} (f: Function X Y) :
    f.one_to_one ↔ ∀ x x': X, f x = f x' → x = x' := byinst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.one_to_one ↔ ∀ (x x' : X.toSubtype), f.to_fn x = f.to_fn x' → x = x'
  peel with x hxh.hinst✝:SetTheoryX:SetY:Setf:Function X Yx:X.toSubtypehx:X.toSubtype⊢ x ≠ hx → f.to_fn x ≠ f.to_fn hx ↔ f.to_fn x = f.to_fn hx → x = hx; tautoAll goals completed! 🐙

Compatibility with Mathlib's Function.Injective.{u₁, u₂} {α : Sort u₁} {β : Sort u₂} (f : α → β) : PropFunction.Injective. You may wish to use the Unknown identifier `unfold`unfold tactic to understand Mathlib concepts such as Function.Injective.{u₁, u₂} {α : Sort u₁} {β : Sort u₂} (f : α → β) : PropFunction.Injective.

theorem Function.one_to_one_iff' {X Y: Set} (f: Function X Y) :
    f.one_to_one ↔ Function.Injective f.to_fn := byinst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.one_to_one ↔ Function.Injective f.to_fn
  rw [one_to_one_iff, Function.Injective]All goals completed! 🐙

Example 3.3.18. One half of the example requires the integers, and so is expressed using Mathlib functions instead of Chapter 3 functions.

theorem SetTheory.Set.f_3_3_18_one_to_one :
    (Function.mk_fn (fun (n:Nat) ↦ ((n^2:ℕ):Nat))).one_to_one := byinst✝:SetTheory⊢ (Function.mk_fn fun n => ↑(nat_equiv.symm n ^ 2)).one_to_one
  rw [Function.one_to_one_iff]inst✝:SetTheory⊢ ∀ (x x' : Nat.toSubtype),
  (Function.mk_fn fun n => ↑(nat_equiv.symm n ^ 2)).to_fn x =
      (Function.mk_fn fun n => ↑(nat_equiv.symm n ^ 2)).to_fn x' →
    x = x'
  intro _ _ hinst✝:SetTheoryx✝:Nat.toSubtypex'✝:Nat.toSubtypeh:(Function.mk_fn fun n => ↑(nat_equiv.symm n ^ 2)).to_fn x✝ = (Function.mk_fn fun n => ↑(nat_equiv.symm n ^ 2)).to_fn x'✝⊢ x✝ = x'✝
  simpa [Function.eval, Function.eval_of] using hAll goals completed! 🐙

example : ¬ Function.Injective (fun (n:ℤ) ↦ n^2) := byinst✝:SetTheory⊢ ¬Function.Injective fun n => n ^ 2
  intro hinst✝:SetTheoryh:Function.Injective fun n => n ^ 2⊢ False
  have h1 : (fun n ↦ n ^ 2) 1 = (1:ℤ) := byinst✝:SetTheory⊢ ¬Function.Injective fun n => n ^ 2 norm_numAll goals completed! 🐙
  have h2 : (fun n ↦ n ^ 2) (-1) = (1:ℤ) := byinst✝:SetTheory⊢ ¬Function.Injective fun n => n ^ 2 norm_numAll goals completed! 🐙
  nth_rewrite 2 [←h1] at h2inst✝:SetTheoryh:Function.Injective fun n => n ^ 2h1:(fun n => n ^ 2) 1 = 1 := ?_mvar.127345h2:(fun n => n ^ 2) (-1) = (fun n => n ^ 2) 1⊢ False
  specialize h h2inst✝:SetTheoryh1:(fun n => n ^ 2) 1 = 1 := ?_mvar.127345h2:(fun n => n ^ 2) (-1) = (fun n => n ^ 2) 1h:-1 = 1⊢ False
  contradictionAll goals completed! 🐙

example : Function.Injective (fun (n:ℕ) ↦ n^2) := byinst✝:SetTheory⊢ Function.Injective fun n => n ^ 2
  intro _ _ _inst✝:SetTheorya₁✝:ℕa₂✝:ℕa✝:(fun n => n ^ 2) a₁✝ = (fun n => n ^ 2) a₂✝⊢ a₁✝ = a₂✝; rwa [← pow_left_inj₀ (byinst✝:SetTheorya₁✝:ℕa₂✝:ℕa✝:(fun n => n ^ 2) a₁✝ = (fun n => n ^ 2) a₂✝⊢ 0 ≤ a₁✝ norm_numAll goals completed! 🐙) (byinst✝:SetTheorya₁✝:ℕa₂✝:ℕa✝:(fun n => n ^ 2) a₁✝ = (fun n => n ^ 2) a₂✝⊢ 0 ≤ a₂✝ norm_numAll goals completed! 🐙) (show 2 ≠ 0 byinst✝:SetTheory⊢ Function.Injective fun n => n ^ 2 norm_numAll goals completed! 🐙)]inst✝:SetTheorya₁✝:ℕa₂✝:ℕa✝:(fun n => n ^ 2) a₁✝ = (fun n => n ^ 2) a₂✝⊢ a₁✝ ^ 2 = a₂✝ ^ 2

Remark 3.3.19

theorem SetTheory.Set.two_to_one {X Y: Set} {f: Function X Y} (h: ¬ f.one_to_one) :
    ∃ x x': X, x ≠ x' ∧ f x = f x' := byinst✝:SetTheoryX:SetY:Setf:Function X Yh:¬f.one_to_one⊢ ∃ x x', x ≠ x' ∧ f.to_fn x = f.to_fn x'
  rw [Function.one_to_one] at hinst✝:SetTheoryX:SetY:Setf:Function X Yh:¬∀ (x x' : X.toSubtype), x ≠ x' → f.to_fn x ≠ f.to_fn x'⊢ ∃ x x', x ≠ x' ∧ f.to_fn x = f.to_fn x'; aesopAll goals completed! 🐙

Definition 3.3.20 (Onto functions)

abbrev Function.onto {X Y: Set} (f: Function X Y) : Prop := ∀ y: Y, ∃ x: X, f x = y

Compatibility with Mathlib's Function.Surjective

theorem Function.onto_iff {X Y: Set} (f: Function X Y) : f.onto ↔ Function.Surjective f.to_fn := byinst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.onto ↔ Function.Surjective f.to_fn rflAll goals completed! 🐙

Example 3.3.21 (using Mathlib)

example : ¬ Function.Surjective (fun (n:ℤ) ↦ n^2) := byinst✝:SetTheory⊢ ¬Function.Surjective fun n => n ^ 2
  unfold Function.Surjectiveinst✝:SetTheory⊢ ¬∀ (b : ℤ), ∃ a, (fun n => n ^ 2) a = b; push_neginst✝:SetTheory⊢ ∃ b, ∀ (a : ℤ), a ^ 2 ≠ b
  use (-1)hinst✝:SetTheory⊢ ∀ (a : ℤ), a ^ 2 ≠ -1; intro ahinst✝:SetTheorya:ℤ⊢ a ^ 2 ≠ -1
  linarith [sq_nonneg a]All goals completed! 🐙

abbrev A_3_3_21 := { m:ℤ // ∃ n:ℤ, m = n^2 }

example : Function.Surjective (fun (n:ℤ) ↦ ⟨ n^2, byinst✝:SetTheoryn:ℤ⊢ ∃ n_1, n ^ 2 = n_1 ^ 2 use nAll goals completed! 🐙 ⟩ : ℤ → A_3_3_21) := byinst✝:SetTheory⊢ Function.Surjective fun n => ⟨n ^ 2, ⋯⟩
  rintro ⟨b, ⟨a, ha⟩⟩mk.introinst✝:SetTheoryb:ℤa:ℤha:b = a ^ 2⊢ ∃ a_1, (fun n => ⟨n ^ 2, ⋯⟩) a_1 = ⟨b, ⋯⟩; use ahinst✝:SetTheoryb:ℤa:ℤha:b = a ^ 2⊢ (fun n => ⟨n ^ 2, ⋯⟩) a = ⟨b, ⋯⟩
  simp only [ha]All goals completed! 🐙

Definition 3.3.23 (Bijective functions)

abbrev Function.bijective {X Y: Set} (f: Function X Y) : Prop := f.one_to_one ∧ f.onto

Compatibility with Mathlib's Function.Bijective

theorem Function.bijective_iff {X Y: Set} (f: Function X Y) :
    f.bijective ↔ Function.Bijective f.to_fn := byinst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f.bijective ↔ Function.Bijective f.to_fn
  rw [Function.bijective, Function.Bijective, one_to_one_iff', onto_iff]All goals completed! 🐙

Example 3.3.24 (using Mathlib)

abbrev f_3_3_24 : Fin 3 → ({3,4}:_root_.Set ℕ) := fun x ↦ match x with
| 0 => ⟨ 3, byinst✝:SetTheoryx:Fin 3⊢ 3 ∈ {3, 4} norm_numAll goals completed! 🐙 ⟩
| 1 => ⟨ 3, byinst✝:SetTheoryx:Fin 3⊢ 3 ∈ {3, 4} norm_numAll goals completed! 🐙 ⟩
| 2 => ⟨ 4, byinst✝:SetTheoryx:Fin 3⊢ 4 ∈ {3, 4} norm_numAll goals completed! 🐙 ⟩

example : ¬ Function.Injective f_3_3_24 := byinst✝:SetTheory⊢ ¬Function.Injective f_3_3_24 decideAll goals completed! 🐙

example : ¬ Function.Bijective f_3_3_24 := byinst✝:SetTheory⊢ ¬Function.Bijective f_3_3_24 decideAll goals completed! 🐙

abbrev g_3_3_24 : Fin 2 → ({2,3,4}:_root_.Set ℕ) := fun x ↦ match x with
| 0 => ⟨ 2, byinst✝:SetTheoryx:Fin 2⊢ 2 ∈ {2, 3, 4} norm_numAll goals completed! 🐙 ⟩
| 1 => ⟨ 3, byinst✝:SetTheoryx:Fin 2⊢ 3 ∈ {2, 3, 4} norm_numAll goals completed! 🐙 ⟩

example : ¬ Function.Surjective g_3_3_24 := byinst✝:SetTheory⊢ ¬Function.Surjective g_3_3_24 decideAll goals completed! 🐙

example : ¬ Function.Bijective g_3_3_24 := byinst✝:SetTheory⊢ ¬Function.Bijective g_3_3_24 decideAll goals completed! 🐙

abbrev h_3_3_24 : Fin 3 → ({3,4,5}:_root_.Set ℕ) := fun x ↦ match x with
| 0 => ⟨ 3, byinst✝:SetTheoryx:Fin 3⊢ 3 ∈ {3, 4, 5} norm_numAll goals completed! 🐙 ⟩
| 1 => ⟨ 4, byinst✝:SetTheoryx:Fin 3⊢ 4 ∈ {3, 4, 5} norm_numAll goals completed! 🐙 ⟩
| 2 => ⟨ 5, byinst✝:SetTheoryx:Fin 3⊢ 5 ∈ {3, 4, 5} norm_numAll goals completed! 🐙 ⟩

example : Function.Bijective h_3_3_24 := byinst✝:SetTheory⊢ Function.Bijective h_3_3_24 decideAll goals completed! 🐙

Example 3.3.25 is formulated using Mathlib rather than the set theory framework here to avoid some tedious technical issues (cf. Exercise 3.3.2)

example : Function.Bijective (fun n ↦ ⟨ n+1, byinst✝:SetTheoryn:ℕ⊢ n + 1 ≠ 0 omegaAll goals completed! 🐙⟩ : ℕ → { n:ℕ // n ≠ 0 }) := byinst✝:SetTheory⊢ Function.Bijective fun n => ⟨n + 1, ⋯⟩
  constructorleftinst✝:SetTheory⊢ Function.Injective fun n => ⟨n + 1, ⋯⟩rightinst✝:SetTheory⊢ Function.Surjective fun n => ⟨n + 1, ⋯⟩
  ·leftinst✝:SetTheory⊢ Function.Injective fun n => ⟨n + 1, ⋯⟩ intro _ _leftinst✝:SetTheorya₁✝:ℕa₂✝:ℕ⊢ (fun n => ⟨n + 1, ⋯⟩) a₁✝ = (fun n => ⟨n + 1, ⋯⟩) a₂✝ → a₁✝ = a₂✝
    simp only [Subtype.mk.injEq]leftinst✝:SetTheorya₁✝:ℕa₂✝:ℕ⊢ a₁✝ + 1 = a₂✝ + 1 → a₁✝ = a₂✝; omegaAll goals completed! 🐙
  intro ⟨x, hx⟩rightinst✝:SetTheoryx:ℕhx:x ≠ 0⊢ ∃ a, (fun n => ⟨n + 1, ⋯⟩) a = ⟨x, hx⟩; use x-1hinst✝:SetTheoryx:ℕhx:x ≠ 0⊢ (fun n => ⟨n + 1, ⋯⟩) (x - 1) = ⟨x, hx⟩
  simp only [Subtype.mk.injEq]hinst✝:SetTheoryx:ℕhx:x ≠ 0⊢ x - 1 + 1 = x; omegaAll goals completed! 🐙

example : ¬ Function.Bijective (fun n ↦ n+1) := byinst✝:SetTheory⊢ ¬Function.Bijective fun n => n + 1
  suffices h : ¬ Function.Surjective (fun n ↦ n+1) byinst✝:SetTheoryh:¬Function.Surjective fun n => n + 1 := ?_mvar.230004⊢ ¬Function.Bijective fun n => n + 1 unfold Function.Bijectiveinst✝:SetTheoryh:¬Function.Surjective fun n => n + 1 := ?_mvar.230004⊢ ¬((Function.Injective fun n => n + 1) ∧ Function.Surjective fun n => n + 1); tautoAll goals completed! 🐙
  unfold Function.Surjectiveinst✝:SetTheory⊢ ¬∀ (b : ℕ), ∃ a, (fun n => n + 1) a = b; push_neginst✝:SetTheory⊢ ∃ b, ∀ (a : ℕ), a + 1 ≠ b
  use 0hinst✝:SetTheory⊢ ∀ (a : ℕ), a + 1 ≠ 0; introshinst✝:SetTheorya✝:ℕ⊢ a✝ + 1 ≠ 0
  symmhinst✝:SetTheorya✝:ℕ⊢ 0 ≠ a✝ + 1; apply Nat.zero_ne_add_oneAll goals completed! 🐙

Remark 3.3.27

theorem Function.bijective_incorrect_def :
    ∃ X Y: Set, ∃ f: Function X Y, (∀ x: X, ∃! y: Y, y = f x) ∧ ¬ f.bijective := byinst✝:SetTheory⊢ ∃ X Y f, (∀ (x : X.toSubtype), ∃! y, y = f.to_fn x) ∧ ¬f.bijective
  use Nat, Nathinst✝:SetTheory⊢ ∃ f, (∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn x) ∧ ¬f.bijective
  set f := mk_fn fun x ↦ (0: Nat)hinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ∃ f, (∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn x) ∧ ¬f.bijective; use fhinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ (∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn x) ∧ ¬f.bijective
  constructorh.leftinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn xh.rightinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ¬f.bijective
  ·h.leftinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ∀ (x : Nat.toSubtype), ∃! y, y = f.to_fn x introsh.leftinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtype⊢ ∃! y, y = f.to_fn x✝
    apply existsUnique_of_exists_of_uniqueh.left.hexinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtype⊢ ∃ x, x = f.to_fn x✝h.left.huniqueinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtype⊢ ∀ (y₁ y₂ : Nat.toSubtype), y₁ = f.to_fn x✝ → y₂ = f.to_fn x✝ → y₁ = y₂
    ·h.left.hexinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtype⊢ ∃ x, x = f.to_fn x✝ use 0hinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtype⊢ 0 = f.to_fn x✝; rw [Function.eval]All goals completed! 🐙
    introsh.left.huniqueinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtypey₁✝:Nat.toSubtypey₂✝:Nat.toSubtypea✝¹:y₁✝ = f.to_fn x✝a✝:y₂✝ = f.to_fn x✝⊢ y₁✝ = y₂✝; rw [Function.eval] at *h.left.huniqueinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0x✝:Nat.toSubtypey₁✝:Nat.toSubtypey₂✝:Nat.toSubtypea✝¹:f.P x✝ y₁✝a✝:f.P x✝ y₂✝⊢ y₁✝ = y₂✝; aesopAll goals completed! 🐙
  rw [Function.bijective]h.rightinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ¬(f.one_to_one ∧ f.onto)
  suffices h : ¬ f.one_to_one byinst✝:SetTheoryf:Chapter3.Function (@Chapter3.Nat _fvar.230652) (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0h:¬Chapter3.Function.one_to_one _fvar.230889 := ?_mvar.231550⊢ ¬(f.one_to_one ∧ f.onto) tautoAll goals completed! 🐙
  rw [Function.one_to_one_iff]h.rightinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ¬∀ (x x' : Nat.toSubtype), f.to_fn x = f.to_fn x' → x = x'
  push_negh.rightinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ ∃ x x', f.to_fn x = f.to_fn x' ∧ x ≠ x'; use 0, 1hinst✝:SetTheoryf:Chapter3.Function ?_mvar.230839 (@Chapter3.Nat _fvar.230652) := Chapter3.Function.mk_fn fun x => 0⊢ f.to_fn 0 = f.to_fn 1 ∧ 0 ≠ 1; simp [f]All goals completed! 🐙

We cannot use the notation Unknown identifier `f`sorry⁻¹ : ?m.1f⁻¹ for the inverse because in Mathlib's Inv.{u} (α : Type u) : Type uInv class, the inverse of Unknown identifier `f`f must be exactly of the same type of Unknown identifier `f`f, and Function sorry sorry : Type u_2Function Unknown identifier `Y`Y Unknown identifier `X`X is a different type from Function sorry sorry : Type u_2Function Unknown identifier `X`X Unknown identifier `Y`Y.

abbrev Function.inverse {X Y: Set} (f: Function X Y) (h: f.bijective) :
    Function Y X :=
  Function.mk (fun y x ↦ f x = y) (byinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijective⊢ ∀ (x : Y.toSubtype), ∃! y, (fun y x => f.to_fn x = y) x y
    introsinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtype⊢ ∃! y, (fun y x => f.to_fn x = y) x✝ y
    apply existsUnique_of_exists_of_uniquehexinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtype⊢ ∃ x, (fun y x => f.to_fn x = y) x✝ xhuniqueinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtype⊢ ∀ (y₁ y₂ : X.toSubtype), (fun y x => f.to_fn x = y) x✝ y₁ → (fun y x => f.to_fn x = y) x✝ y₂ → y₁ = y₂
    .hexinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtype⊢ ∃ x, (fun y x => f.to_fn x = y) x✝ x aesopAll goals completed! 🐙
    intro _ _ hx hx'huniqueinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtypey₁✝:X.toSubtypey₂✝:X.toSubtypehx:(fun y x => f.to_fn x = y) x✝ y₁✝hx':(fun y x => f.to_fn x = y) x✝ y₂✝⊢ y₁✝ = y₂✝; simp at hx hx'huniqueinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtypey₁✝:X.toSubtypey₂✝:X.toSubtypehx:f.to_fn y₁✝ = x✝hx':f.to_fn y₂✝ = x✝⊢ y₁✝ = y₂✝
    rw [←hx'] at hxhuniqueinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtypey₁✝:X.toSubtypey₂✝:X.toSubtypehx:f.to_fn y₁✝ = f.to_fn y₂✝hx':f.to_fn y₂✝ = x✝⊢ y₁✝ = y₂✝
    apply f.one_to_one_iff.mp h.1hunique.ainst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex✝:Y.toSubtypey₁✝:X.toSubtypey₂✝:X.toSubtypehx:f.to_fn y₁✝ = f.to_fn y₂✝hx':f.to_fn y₂✝ = x✝⊢ f.to_fn y₁✝ = f.to_fn y₂✝
    simp [hx]All goals completed! 🐙
  )

theorem Function.inverse_eval {X Y: Set} {f: Function X Y} (h: f.bijective) (y: Y) (x: X) :
    x = (f.inverse h) y ↔ f x = y := Function.eval _ _ _

Compatibility with Mathlib's notion of inverse

theorem Function.inverse_eq {X Y: Set} [Nonempty X] {f: Function X Y} (h: f.bijective) :
    (f.inverse h).to_fn = Function.invFun f.to_fn := byinst✝¹:SetTheoryX:SetY:Setinst✝:Nonempty X.toSubtypef:Function X Yh:f.bijective⊢ (f.inverse h).to_fn = Function.invFun f.to_fn
  ext yh.ainst✝¹:SetTheoryX:SetY:Setinst✝:Nonempty X.toSubtypef:Function X Yh:f.bijectivey:Y.toSubtype⊢ ↑((f.inverse h).to_fn y) = ↑(Function.invFun f.to_fn y); congrh.a.e_selfinst✝¹:SetTheoryX:SetY:Setinst✝:Nonempty X.toSubtypef:Function X Yh:f.bijectivey:Y.toSubtype⊢ (f.inverse h).to_fn y = Function.invFun f.to_fn y; symmh.a.e_selfinst✝¹:SetTheoryX:SetY:Setinst✝:Nonempty X.toSubtypef:Function X Yh:f.bijectivey:Y.toSubtype⊢ Function.invFun f.to_fn y = (f.inverse h).to_fn y
  rw [inverse_eval]h.a.e_selfinst✝¹:SetTheoryX:SetY:Setinst✝:Nonempty X.toSubtypef:Function X Yh:f.bijectivey:Y.toSubtype⊢ f.to_fn (Function.invFun f.to_fn y) = y
  apply Function.rightInverse_invFun (f.bijective_iff.mp h).2All goals completed! 🐙

Exercise 3.3.1. Although a proof operating directly on functions would be shorter, the spirit of the exercise is to show these using the Chapter3.Function.eq_iff.{u_1, u_2} [SetTheory] {X Y : Set} (f g : Function X Y) : f = g ↔ ∀ (x : X.toSubtype), f.to_fn x = g.to_fn xFunction.eq_iff definition.

theorem declaration uses 'sorry'Function.refl {X Y:Set} (f: Function X Y) : f = f := byinst✝:SetTheoryX:SetY:Setf:Function X Y⊢ f = f sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.symm {X Y:Set} (f g: Function X Y) : f = g ↔ g = f := byinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Y⊢ f = g ↔ g = f sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.trans {X Y:Set} {f g h: Function X Y} (hfg: f = g) (hgh: g = h) : f = h := byinst✝:SetTheoryX:SetY:Setf:Function X Yg:Function X Yh:Function X Yhfg:f = ghgh:g = h⊢ f = h sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.comp_congr {X Y Z:Set} {f f': Function X Y} (hff': f = f') {g g': Function Y Z}
  (hgg': g = g') : g ○ f = g' ○ f' := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yf':Function X Yhff':f = f'g:Function Y Zg':Function Y Zhgg':g = g'⊢ g○f = g'○f' sorryAll goals completed! 🐙

Exercise 3.3.2

theorem declaration uses 'sorry'Function.comp_of_inj {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hf: f.one_to_one)
  (hg: g.one_to_one) : (g ○ f).one_to_one := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.one_to_onehg:g.one_to_one⊢ (g○f).one_to_one sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.comp_of_surj {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hf: f.onto)
  (hg: g.onto) : (g ○ f).onto := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.ontohg:g.onto⊢ (g○f).onto sorryAll goals completed! 🐙

Exercise 3.3.3 - fill in the sorrys in the statements in a reasonable fashion.

theorem declaration uses 'sorry'empty_function_one_to_one_iff (X: Set) (f: Function ∅ X) : f.one_to_one ↔ sorry := byinst✝:SetTheoryX:Setf:Function ∅ X⊢ f.one_to_one ↔ sorry sorryAll goals completed! 🐙

theorem declaration uses 'sorry'empty_function_onto_iff (X: Set) (f: Function ∅ X) : f.onto ↔ sorry := byinst✝:SetTheoryX:Setf:Function ∅ X⊢ f.onto ↔ sorry sorryAll goals completed! 🐙

theorem declaration uses 'sorry'empty_function_bijective_iff (X: Set) (f: Function ∅ X) : f.bijective ↔ sorry:= byinst✝:SetTheoryX:Setf:Function ∅ X⊢ f.bijective ↔ sorry sorryAll goals completed! 🐙

Exercise 3.3.4.

theorem declaration uses 'sorry'Function.comp_cancel_left {X Y Z:Set} {f f': Function X Y} {g : Function Y Z}
  (heq : g ○ f = g ○ f') (hg: g.one_to_one) : f = f' := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yf':Function X Yg:Function Y Zheq:g○f = g○f'hg:g.one_to_one⊢ f = f' sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.comp_cancel_right {X Y Z:Set} {f: Function X Y} {g g': Function Y Z}
  (heq : g ○ f = g' ○ f) (hf: f.onto) : g = g' := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zg':Function Y Zheq:g○f = g'○fhf:f.onto⊢ g = g' sorryAll goals completed! 🐙

def declaration uses 'sorry'Function.comp_cancel_left_without_hg : Decidable (∀ (X Y Z:Set) (f f': Function X Y) (g : Function Y Z) (heq : g ○ f = g ○ f'), f = f') := byinst✝:SetTheory⊢ Decidable (∀ (X Y Z : Set) (f f' : Function X Y) (g : Function Y Z), g○f = g○f' → f = f')
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

def declaration uses 'sorry'Function.comp_cancel_right_without_hg : Decidable (∀ (X Y Z:Set) (f: Function X Y) (g g': Function Y Z) (heq : g ○ f = g' ○ f), g = g') := byinst✝:SetTheory⊢ Decidable (∀ (X Y Z : Set) (f : Function X Y) (g g' : Function Y Z), g○f = g'○f → g = g')
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

Exercise 3.3.5.

theorem declaration uses 'sorry'Function.comp_injective {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hinj :
    (g ○ f).one_to_one) : f.one_to_one := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhinj:(g○f).one_to_one⊢ f.one_to_one sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.comp_surjective {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hsurj :
    (g ○ f).onto) : g.onto := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhsurj:(g○f).onto⊢ g.onto sorryAll goals completed! 🐙

def declaration uses 'sorry'Function.comp_injective' : Decidable (∀ (X Y Z:Set) (f: Function X Y) (g : Function Y Z) (hinj :
    (g ○ f).one_to_one), g.one_to_one) := byinst✝:SetTheory⊢ Decidable (∀ (X Y Z : Set) (f : Function X Y) (g : Function Y Z), (g○f).one_to_one → g.one_to_one)
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

def declaration uses 'sorry'Function.comp_surjective' : Decidable (∀ (X Y Z:Set) (f: Function X Y) (g : Function Y Z) (hsurj :
    (g ○ f).onto), f.onto) := byinst✝:SetTheory⊢ Decidable (∀ (X Y Z : Set) (f : Function X Y) (g : Function Y Z), (g○f).onto → f.onto)
  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙

Exercise 3.3.6

theorem declaration uses 'sorry'Function.inverse_comp_self {X Y: Set} {f: Function X Y} (h: f.bijective) (x: X) :
    (f.inverse h) (f x) = x := byinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivex:X.toSubtype⊢ (f.inverse h).to_fn (f.to_fn x) = x sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.self_comp_inverse {X Y: Set} {f: Function X Y} (h: f.bijective) (y: Y) :
    f ((f.inverse h) y) = y := byinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijectivey:Y.toSubtype⊢ f.to_fn ((f.inverse h).to_fn y) = y sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.inverse_bijective {X Y: Set} {f: Function X Y} (h: f.bijective) :
    (f.inverse h).bijective := byinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijective⊢ (f.inverse h).bijective sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.inverse_inverse {X Y: Set} {f: Function X Y} (h: f.bijective) :
    (f.inverse h).inverse (f.inverse_bijective h) = f := byinst✝:SetTheoryX:SetY:Setf:Function X Yh:f.bijective⊢ (f.inverse h).inverse ⋯ = f sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.comp_bijective {X Y Z:Set} {f: Function X Y} {g : Function Y Z} (hf: f.bijective)
  (hg: g.bijective) : (g ○ f).bijective := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.bijectivehg:g.bijective⊢ (g○f).bijective sorryAll goals completed! 🐙

Exercise 3.3.7

theorem declaration uses 'sorry'Function.inv_of_comp {X Y Z:Set} {f: Function X Y} {g : Function Y Z}
  (hf: f.bijective) (hg: g.bijective) :
    (g ○ f).inverse (Function.comp_bijective hf hg) = (f.inverse hf) ○ (g.inverse hg) := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Yg:Function Y Zhf:f.bijectivehg:g.bijective⊢ (g○f).inverse ⋯ = f.inverse hf○g.inverse hg sorryAll goals completed! 🐙

Exercise 3.3.8

abbrev Function.inclusion {X Y:Set} (h: X ⊆ Y) :
    Function X Y := Function.mk_fn (fun x ↦ ⟨ x.val, h x.val x.property ⟩ )

abbrev Function.id (X:Set) : Function X X := Function.mk_fn (fun x ↦ x)

theorem declaration uses 'sorry'Function.inclusion_id (X:Set) :
    Function.inclusion (SetTheory.Set.subset_self X) = Function.id X := byinst✝:SetTheoryX:Set⊢ inclusion ⋯ = id X sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.inclusion_comp (X Y Z:Set) (hXY: X ⊆ Y) (hYZ: Y ⊆ Z) :
    Function.inclusion hYZ ○ Function.inclusion hXY = Function.inclusion (SetTheory.Set.subset_trans hXY hYZ) := byinst✝:SetTheoryX:SetY:SetZ:SethXY:X ⊆ YhYZ:Y ⊆ Z⊢ inclusion hYZ○inclusion hXY = inclusion ⋯ sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.comp_id {A B:Set} (f: Function A B) : f ○ Function.id A = f := byinst✝:SetTheoryA:SetB:Setf:Function A B⊢ f○id A = f sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.id_comp {A B:Set} (f: Function A B) : Function.id B ○ f = f := byinst✝:SetTheoryA:SetB:Setf:Function A B⊢ id B○f = f sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.comp_inv {A B:Set} (f: Function A B) (hf: f.bijective) :
    f ○ f.inverse hf = Function.id B := byinst✝:SetTheoryA:SetB:Setf:Function A Bhf:f.bijective⊢ f○f.inverse hf = id B sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Function.inv_comp {A B:Set} (f: Function A B) (hf: f.bijective) :
    f.inverse hf ○ f = Function.id A := byinst✝:SetTheoryA:SetB:Setf:Function A Bhf:f.bijective⊢ f.inverse hf○f = id A sorryAll goals completed! 🐙

open Classical in
theorem declaration uses 'sorry'Function.glue {X Y Z:Set} (hXY: Disjoint X Y) (f: Function X Z) (g: Function Y Z) :
    ∃! h: Function (X ∪ Y) Z, (h ○ Function.inclusion (SetTheory.Set.subset_union_left X Y) = f)
    ∧ (h ○ Function.inclusion (SetTheory.Set.subset_union_right X Y) = g) := byinst✝:SetTheoryX:SetY:SetZ:SethXY:Disjoint X Yf:Function X Zg:Function Y Z⊢ ∃! h, h○inclusion ⋯ = f ∧ h○inclusion ⋯ = g sorryAll goals completed! 🐙

open Classical in
theorem declaration uses 'sorry'Function.glue' {X Y Z:Set} (f: Function X Z) (g: Function Y Z)
    (hfg : ∀ x : ((X ∩ Y): Set), f ⟨x.val, byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Zg:Function Y Zx:(X ∩ Y).toSubtype⊢ ↑x ∈ X aesopAll goals completed! 🐙⟩ = g ⟨x.val, byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Zg:Function Y Zx:(X ∩ Y).toSubtype⊢ ↑x ∈ Y aesopAll goals completed! 🐙⟩)  :
    ∃! h: Function (X ∪ Y) Z, (h ○ Function.inclusion (SetTheory.Set.subset_union_left X Y) = f)
    ∧ (h ○ Function.inclusion (SetTheory.Set.subset_union_right X Y) = g) := byinst✝:SetTheoryX:SetY:SetZ:Setf:Function X Zg:Function Y Zhfg:∀ (x : (X ∩ Y).toSubtype), f.to_fn ⟨↑x, ⋯⟩ = g.to_fn ⟨↑x, ⋯⟩⊢ ∃! h, h○inclusion ⋯ = f ∧ h○inclusion ⋯ = g sorryAll goals completed! 🐙

end Chapter3