Session 11: Ascending to categories of richer structures🔗

1. A category of richer structures: Endomaps of sets🔗

Exercise 1 (p. 153)

How many maps can you find? (There are fewer than seven.)

Solution: Exercise 1

Label the elements in the three-element set A as a_1, a_2, a_3 (clockwise starting with any element); label the elements in the set X as x_1 for the element forming the one-element loop and x_2, x_3, x_4 (anticlockwise starting with any element) for the elements forming the three-element cycle, ignoring all other elements.

inductive A
  | a₁ | a₂ | a₃

inductive X
  | x₁ | x₂ | x₃ | x₄

def A' : SetWithEndomap := {
  carrier := A
  toEnd := fun
    | A.a₁ => A.a₂
    | A.a₂ => A.a₃
    | A.a₃ => A.a₁
}

def X' : SetWithEndomap := {
  carrier := X
  toEnd := fun -- a restriction of α to the subset {x₁, x₂, x₃, x₄}
    | X.x₁ => X.x₁
    | X.x₂ => X.x₃
    | X.x₃ => X.x₄
    | X.x₄ => X.x₂
}

Then there are four structure-preserving maps from A to X, which we call f_1, f_2, f_3, f_4 below.

def f₁ : A ⟶ X
  | A.a₁ => X.x₁
  | A.a₂ => X.x₁
  | A.a₃ => X.x₁

-- f₁ is structure-preserving
example : A' ⟶ X' := ⟨
  f₁,
  by⊢ f₁ ⊚ A'.toEnd = X'.toEnd ⊚ f₁
    funext aha:A'.carrier⊢ (f₁ ⊚ A'.toEnd) a = (X'.toEnd ⊚ f₁) a
    cases ah.a₁⊢ (f₁ ⊚ A'.toEnd) A.a₁ = (X'.toEnd ⊚ f₁) A.a₁h.a₂⊢ (f₁ ⊚ A'.toEnd) A.a₂ = (X'.toEnd ⊚ f₁) A.a₂h.a₃⊢ (f₁ ⊚ A'.toEnd) A.a₃ = (X'.toEnd ⊚ f₁) A.a₃ <;>h.a₁⊢ (f₁ ⊚ A'.toEnd) A.a₁ = (X'.toEnd ⊚ f₁) A.a₁h.a₂⊢ (f₁ ⊚ A'.toEnd) A.a₂ = (X'.toEnd ⊚ f₁) A.a₂h.a₃⊢ (f₁ ⊚ A'.toEnd) A.a₃ = (X'.toEnd ⊚ f₁) A.a₃ rflAll goals completed! 🐙
⟩

def f₂ : A ⟶ X
  | A.a₁ => X.x₂
  | A.a₂ => X.x₃
  | A.a₃ => X.x₄

-- f₂ is structure-preserving
example : A' ⟶ X' := ⟨
  f₂,
  by⊢ f₂ ⊚ A'.toEnd = X'.toEnd ⊚ f₂
    funext aha:A'.carrier⊢ (f₂ ⊚ A'.toEnd) a = (X'.toEnd ⊚ f₂) a
    cases ah.a₁⊢ (f₂ ⊚ A'.toEnd) A.a₁ = (X'.toEnd ⊚ f₂) A.a₁h.a₂⊢ (f₂ ⊚ A'.toEnd) A.a₂ = (X'.toEnd ⊚ f₂) A.a₂h.a₃⊢ (f₂ ⊚ A'.toEnd) A.a₃ = (X'.toEnd ⊚ f₂) A.a₃ <;>h.a₁⊢ (f₂ ⊚ A'.toEnd) A.a₁ = (X'.toEnd ⊚ f₂) A.a₁h.a₂⊢ (f₂ ⊚ A'.toEnd) A.a₂ = (X'.toEnd ⊚ f₂) A.a₂h.a₃⊢ (f₂ ⊚ A'.toEnd) A.a₃ = (X'.toEnd ⊚ f₂) A.a₃ rflAll goals completed! 🐙
⟩

def f₃ : A ⟶ X
  | A.a₁ => X.x₃
  | A.a₂ => X.x₄
  | A.a₃ => X.x₂

-- f₃ is structure-preserving
example : A' ⟶ X' := ⟨
  f₃,
  by⊢ f₃ ⊚ A'.toEnd = X'.toEnd ⊚ f₃
    funext aha:A'.carrier⊢ (f₃ ⊚ A'.toEnd) a = (X'.toEnd ⊚ f₃) a
    cases ah.a₁⊢ (f₃ ⊚ A'.toEnd) A.a₁ = (X'.toEnd ⊚ f₃) A.a₁h.a₂⊢ (f₃ ⊚ A'.toEnd) A.a₂ = (X'.toEnd ⊚ f₃) A.a₂h.a₃⊢ (f₃ ⊚ A'.toEnd) A.a₃ = (X'.toEnd ⊚ f₃) A.a₃ <;>h.a₁⊢ (f₃ ⊚ A'.toEnd) A.a₁ = (X'.toEnd ⊚ f₃) A.a₁h.a₂⊢ (f₃ ⊚ A'.toEnd) A.a₂ = (X'.toEnd ⊚ f₃) A.a₂h.a₃⊢ (f₃ ⊚ A'.toEnd) A.a₃ = (X'.toEnd ⊚ f₃) A.a₃ rflAll goals completed! 🐙
⟩

def f₄ : A ⟶ X
  | A.a₁ => X.x₄
  | A.a₂ => X.x₂
  | A.a₃ => X.x₃

-- f₄ is structure-preserving
example : A' ⟶ X' := ⟨
  f₄,
  by⊢ f₄ ⊚ A'.toEnd = X'.toEnd ⊚ f₄
    funext aha:A'.carrier⊢ (f₄ ⊚ A'.toEnd) a = (X'.toEnd ⊚ f₄) a
    cases ah.a₁⊢ (f₄ ⊚ A'.toEnd) A.a₁ = (X'.toEnd ⊚ f₄) A.a₁h.a₂⊢ (f₄ ⊚ A'.toEnd) A.a₂ = (X'.toEnd ⊚ f₄) A.a₂h.a₃⊢ (f₄ ⊚ A'.toEnd) A.a₃ = (X'.toEnd ⊚ f₄) A.a₃ <;>h.a₁⊢ (f₄ ⊚ A'.toEnd) A.a₁ = (X'.toEnd ⊚ f₄) A.a₁h.a₂⊢ (f₄ ⊚ A'.toEnd) A.a₂ = (X'.toEnd ⊚ f₄) A.a₂h.a₃⊢ (f₄ ⊚ A'.toEnd) A.a₃ = (X'.toEnd ⊚ f₄) A.a₃ rflAll goals completed! 🐙
⟩

3. The category of graphs🔗

Exercise 2 (p. 158)

inductive X
  | a | b | c

def α : X ⟶ X
  | X.a => X.c
  | X.b => X.a
  | X.c => X.b

def Xα : SetWithEndomap := {
  carrier := X
  toEnd := α
}

inductive Y
  | p | q | r

def β : Y ⟶ Y
  | Y.p => Y.q
  | Y.q => Y.r
  | Y.r => Y.p

def Yβ : SetWithEndomap := {
  carrier := Y
  toEnd := β
}

Find an isomorphism from X^{↻\alpha} to Y^{↻\beta}. How many such isomorphisms are there?

Hint: You need to find {X \xrightarrow{f} Y} such that {f \alpha = \beta f}, and check that f has an inverse {Y \xrightarrow{f^{-1}} X} (meaning {f^{-1}f = 1_X} and {ff^{-1} = 1_Y}). Then you'll still need to check that f^{-1} is a map in 𝑺↻ (meaning {f^{-1} \beta = \alpha f^{-1}}), but see Exercise 4, below.

Solution: Exercise 2

There are three such isomorphisms, which we call f_1, f_2, f_3 below.

def f₁ : X ⟶ Y
  | X.a => Y.r
  | X.b => Y.q
  | X.c => Y.p

--f₁ is an isomorphism
example : ∃ f : Xα ⟶ Yβ, IsIso f := by⊢ ∃ f, IsIso f
  let f : Xα ⟶ Yβ := ⟨
    f₁,
    by⊢ f₁ ⊚ Xα.toEnd = Yβ.toEnd ⊚ f₁
      -- fα = βf
      funext xhx:Xα.carrier⊢ (f₁ ⊚ Xα.toEnd) x = (Yβ.toEnd ⊚ f₁) x
      cases xh.a⊢ (f₁ ⊚ Xα.toEnd) X.a = (Yβ.toEnd ⊚ f₁) X.ah.b⊢ (f₁ ⊚ Xα.toEnd) X.b = (Yβ.toEnd ⊚ f₁) X.bh.c⊢ (f₁ ⊚ Xα.toEnd) X.c = (Yβ.toEnd ⊚ f₁) X.c <;>h.a⊢ (f₁ ⊚ Xα.toEnd) X.a = (Yβ.toEnd ⊚ f₁) X.ah.b⊢ (f₁ ⊚ Xα.toEnd) X.b = (Yβ.toEnd ⊚ f₁) X.bh.c⊢ (f₁ ⊚ Xα.toEnd) X.c = (Yβ.toEnd ⊚ f₁) X.c rflAll goals completed! 🐙
  ⟩
  let finv : Yβ ⟶ Xα := ⟨
    fun
      | Y.p => X.c
      | Y.q => X.b
      | Y.r => X.a,
    byf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩⊢ (fun x ↦
      match x with
      | Y.p => X.c
      | Y.q => X.b
      | Y.r => X.a) ⊚
    Yβ.toEnd =
  Xα.toEnd ⊚ fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a
      -- f⁻¹β = αf⁻¹
      funext yhf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩y:Yβ.carrier⊢ ((fun x ↦
        match x with
        | Y.p => X.c
        | Y.q => X.b
        | Y.r => X.a) ⊚
      Yβ.toEnd)
    y =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.c
      | Y.q => X.b
      | Y.r => X.a)
    y
      cases yh.pf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.c
        | Y.q => X.b
        | Y.r => X.a) ⊚
      Yβ.toEnd)
    Y.p =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.c
      | Y.q => X.b
      | Y.r => X.a)
    Y.ph.qf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.c
        | Y.q => X.b
        | Y.r => X.a) ⊚
      Yβ.toEnd)
    Y.q =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.c
      | Y.q => X.b
      | Y.r => X.a)
    Y.qh.rf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.c
        | Y.q => X.b
        | Y.r => X.a) ⊚
      Yβ.toEnd)
    Y.r =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.c
      | Y.q => X.b
      | Y.r => X.a)
    Y.r <;>h.pf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.c
        | Y.q => X.b
        | Y.r => X.a) ⊚
      Yβ.toEnd)
    Y.p =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.c
      | Y.q => X.b
      | Y.r => X.a)
    Y.ph.qf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.c
        | Y.q => X.b
        | Y.r => X.a) ⊚
      Yβ.toEnd)
    Y.q =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.c
      | Y.q => X.b
      | Y.r => X.a)
    Y.qh.rf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.c
        | Y.q => X.b
        | Y.r => X.a) ⊚
      Yβ.toEnd)
    Y.r =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.c
      | Y.q => X.b
      | Y.r => X.a)
    Y.r rflAll goals completed! 🐙
  ⟩
  use fhf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ IsIso f
  use finvhf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ finv ⊚ f = 𝟙 Xα ∧ f ⊚ finv = 𝟙 Yβ
  constructorh.leftf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ finv ⊚ f = 𝟙 Xαh.rightf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ f ⊚ finv = 𝟙 Yβ
  ·h.leftf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ finv ⊚ f = 𝟙 Xα -- f⁻¹f = 𝟙 X
    have h : finv.val ⊚ f.val = 𝟙 X := by⊢ ∃ f, IsIso f
      funext xhf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩x:Xα.carrier⊢ (↑finv ⊚ ↑f) x = 𝟙 X x
      cases xh.af:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.a = 𝟙 X X.ah.bf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.b = 𝟙 X X.bh.cf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.c = 𝟙 X X.c <;>h.af:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.a = 𝟙 X X.ah.bf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.b = 𝟙 X X.bh.cf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.c = 𝟙 X X.c rflAll goals completed! 🐙
    exact Subtype.ext hAll goals completed! 🐙
  ·h.rightf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ f ⊚ finv = 𝟙 Yβ -- ff⁻¹ = 𝟙 Y
    have h : f.val ⊚ finv.val = 𝟙 Y := by⊢ ∃ f, IsIso f
      funext yhf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩y:Yβ.carrier⊢ (↑f ⊚ ↑finv) y = 𝟙 Y y
      cases yh.pf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.p = 𝟙 Y Y.ph.qf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.q = 𝟙 Y Y.qh.rf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.r = 𝟙 Y Y.r <;>h.pf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.p = 𝟙 Y Y.ph.qf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.q = 𝟙 Y Y.qh.rf:Xα ⟶ Yβ := ⟨f₁, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.c
    | Y.q => X.b
    | Y.r => X.a,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.r = 𝟙 Y Y.r rflAll goals completed! 🐙
    exact Subtype.ext hAll goals completed! 🐙

def f₂ : X ⟶ Y
  | X.a => Y.q
  | X.b => Y.p
  | X.c => Y.r

--f₂ is an isomorphism
example : ∃ f : Xα ⟶ Yβ, IsIso f := by⊢ ∃ f, IsIso f
  let f : Xα ⟶ Yβ := ⟨
    f₂,
    by⊢ f₂ ⊚ Xα.toEnd = Yβ.toEnd ⊚ f₂
      -- fα = βf
      funext xhx:Xα.carrier⊢ (f₂ ⊚ Xα.toEnd) x = (Yβ.toEnd ⊚ f₂) x
      cases xh.a⊢ (f₂ ⊚ Xα.toEnd) X.a = (Yβ.toEnd ⊚ f₂) X.ah.b⊢ (f₂ ⊚ Xα.toEnd) X.b = (Yβ.toEnd ⊚ f₂) X.bh.c⊢ (f₂ ⊚ Xα.toEnd) X.c = (Yβ.toEnd ⊚ f₂) X.c <;>h.a⊢ (f₂ ⊚ Xα.toEnd) X.a = (Yβ.toEnd ⊚ f₂) X.ah.b⊢ (f₂ ⊚ Xα.toEnd) X.b = (Yβ.toEnd ⊚ f₂) X.bh.c⊢ (f₂ ⊚ Xα.toEnd) X.c = (Yβ.toEnd ⊚ f₂) X.c rflAll goals completed! 🐙
  ⟩
  let finv : Yβ ⟶ Xα := ⟨
    fun
      | Y.p => X.b
      | Y.q => X.a
      | Y.r => X.c,
    byf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩⊢ (fun x ↦
      match x with
      | Y.p => X.b
      | Y.q => X.a
      | Y.r => X.c) ⊚
    Yβ.toEnd =
  Xα.toEnd ⊚ fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c
      -- f⁻¹β = αf⁻¹
      funext yhf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩y:Yβ.carrier⊢ ((fun x ↦
        match x with
        | Y.p => X.b
        | Y.q => X.a
        | Y.r => X.c) ⊚
      Yβ.toEnd)
    y =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.b
      | Y.q => X.a
      | Y.r => X.c)
    y
      cases yh.pf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.b
        | Y.q => X.a
        | Y.r => X.c) ⊚
      Yβ.toEnd)
    Y.p =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.b
      | Y.q => X.a
      | Y.r => X.c)
    Y.ph.qf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.b
        | Y.q => X.a
        | Y.r => X.c) ⊚
      Yβ.toEnd)
    Y.q =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.b
      | Y.q => X.a
      | Y.r => X.c)
    Y.qh.rf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.b
        | Y.q => X.a
        | Y.r => X.c) ⊚
      Yβ.toEnd)
    Y.r =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.b
      | Y.q => X.a
      | Y.r => X.c)
    Y.r <;>h.pf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.b
        | Y.q => X.a
        | Y.r => X.c) ⊚
      Yβ.toEnd)
    Y.p =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.b
      | Y.q => X.a
      | Y.r => X.c)
    Y.ph.qf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.b
        | Y.q => X.a
        | Y.r => X.c) ⊚
      Yβ.toEnd)
    Y.q =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.b
      | Y.q => X.a
      | Y.r => X.c)
    Y.qh.rf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.b
        | Y.q => X.a
        | Y.r => X.c) ⊚
      Yβ.toEnd)
    Y.r =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.b
      | Y.q => X.a
      | Y.r => X.c)
    Y.r rflAll goals completed! 🐙
  ⟩
  use fhf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ IsIso f
  use finvhf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ finv ⊚ f = 𝟙 Xα ∧ f ⊚ finv = 𝟙 Yβ
  constructorh.leftf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ finv ⊚ f = 𝟙 Xαh.rightf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ f ⊚ finv = 𝟙 Yβ
  ·h.leftf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ finv ⊚ f = 𝟙 Xα -- f⁻¹f = 𝟙 X
    have h : finv.val ⊚ f.val = 𝟙 X := by⊢ ∃ f, IsIso f
      funext xhf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩x:Xα.carrier⊢ (↑finv ⊚ ↑f) x = 𝟙 X x
      cases xh.af:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.a = 𝟙 X X.ah.bf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.b = 𝟙 X X.bh.cf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.c = 𝟙 X X.c <;>h.af:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.a = 𝟙 X X.ah.bf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.b = 𝟙 X X.bh.cf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.c = 𝟙 X X.c rflAll goals completed! 🐙
    exact Subtype.ext hAll goals completed! 🐙
  ·h.rightf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ f ⊚ finv = 𝟙 Yβ -- ff⁻¹ = 𝟙 Y
    have h : f.val ⊚ finv.val = 𝟙 Y := by⊢ ∃ f, IsIso f
      funext yhf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩y:Yβ.carrier⊢ (↑f ⊚ ↑finv) y = 𝟙 Y y
      cases yh.pf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.p = 𝟙 Y Y.ph.qf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.q = 𝟙 Y Y.qh.rf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.r = 𝟙 Y Y.r <;>h.pf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.p = 𝟙 Y Y.ph.qf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.q = 𝟙 Y Y.qh.rf:Xα ⟶ Yβ := ⟨f₂, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.b
    | Y.q => X.a
    | Y.r => X.c,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.r = 𝟙 Y Y.r rflAll goals completed! 🐙
    exact Subtype.ext hAll goals completed! 🐙

def f₃ : X ⟶ Y
  | X.a => Y.p
  | X.b => Y.r
  | X.c => Y.q

--f₃ is an isomorphism
example : ∃ f : Xα ⟶ Yβ, IsIso f := by⊢ ∃ f, IsIso f
  let f : Xα ⟶ Yβ := ⟨
    f₃,
    by⊢ f₃ ⊚ Xα.toEnd = Yβ.toEnd ⊚ f₃
      -- fα = βf
      funext xhx:Xα.carrier⊢ (f₃ ⊚ Xα.toEnd) x = (Yβ.toEnd ⊚ f₃) x
      cases xh.a⊢ (f₃ ⊚ Xα.toEnd) X.a = (Yβ.toEnd ⊚ f₃) X.ah.b⊢ (f₃ ⊚ Xα.toEnd) X.b = (Yβ.toEnd ⊚ f₃) X.bh.c⊢ (f₃ ⊚ Xα.toEnd) X.c = (Yβ.toEnd ⊚ f₃) X.c <;>h.a⊢ (f₃ ⊚ Xα.toEnd) X.a = (Yβ.toEnd ⊚ f₃) X.ah.b⊢ (f₃ ⊚ Xα.toEnd) X.b = (Yβ.toEnd ⊚ f₃) X.bh.c⊢ (f₃ ⊚ Xα.toEnd) X.c = (Yβ.toEnd ⊚ f₃) X.c rflAll goals completed! 🐙
  ⟩
  let finv : Yβ ⟶ Xα := ⟨
    fun
      | Y.p => X.a
      | Y.q => X.c
      | Y.r => X.b,
    byf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩⊢ (fun x ↦
      match x with
      | Y.p => X.a
      | Y.q => X.c
      | Y.r => X.b) ⊚
    Yβ.toEnd =
  Xα.toEnd ⊚ fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b
      -- f⁻¹β = αf⁻¹
      funext yhf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩y:Yβ.carrier⊢ ((fun x ↦
        match x with
        | Y.p => X.a
        | Y.q => X.c
        | Y.r => X.b) ⊚
      Yβ.toEnd)
    y =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.a
      | Y.q => X.c
      | Y.r => X.b)
    y
      cases yh.pf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.a
        | Y.q => X.c
        | Y.r => X.b) ⊚
      Yβ.toEnd)
    Y.p =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.a
      | Y.q => X.c
      | Y.r => X.b)
    Y.ph.qf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.a
        | Y.q => X.c
        | Y.r => X.b) ⊚
      Yβ.toEnd)
    Y.q =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.a
      | Y.q => X.c
      | Y.r => X.b)
    Y.qh.rf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.a
        | Y.q => X.c
        | Y.r => X.b) ⊚
      Yβ.toEnd)
    Y.r =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.a
      | Y.q => X.c
      | Y.r => X.b)
    Y.r <;>h.pf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.a
        | Y.q => X.c
        | Y.r => X.b) ⊚
      Yβ.toEnd)
    Y.p =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.a
      | Y.q => X.c
      | Y.r => X.b)
    Y.ph.qf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.a
        | Y.q => X.c
        | Y.r => X.b) ⊚
      Yβ.toEnd)
    Y.q =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.a
      | Y.q => X.c
      | Y.r => X.b)
    Y.qh.rf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩⊢ ((fun x ↦
        match x with
        | Y.p => X.a
        | Y.q => X.c
        | Y.r => X.b) ⊚
      Yβ.toEnd)
    Y.r =
  (Xα.toEnd ⊚ fun x ↦
      match x with
      | Y.p => X.a
      | Y.q => X.c
      | Y.r => X.b)
    Y.r rflAll goals completed! 🐙
  ⟩
  use fhf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ IsIso f
  use finvhf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ finv ⊚ f = 𝟙 Xα ∧ f ⊚ finv = 𝟙 Yβ
  constructorh.leftf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ finv ⊚ f = 𝟙 Xαh.rightf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ f ⊚ finv = 𝟙 Yβ
  ·h.leftf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ finv ⊚ f = 𝟙 Xα -- f⁻¹f = 𝟙 X
    have h : finv.val ⊚ f.val = 𝟙 X := by⊢ ∃ f, IsIso f
      funext xhf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩x:Xα.carrier⊢ (↑finv ⊚ ↑f) x = 𝟙 X x
      cases xh.af:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.a = 𝟙 X X.ah.bf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.b = 𝟙 X X.bh.cf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.c = 𝟙 X X.c <;>h.af:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.a = 𝟙 X X.ah.bf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.b = 𝟙 X X.bh.cf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑finv ⊚ ↑f) X.c = 𝟙 X X.c rflAll goals completed! 🐙
    exact Subtype.ext hAll goals completed! 🐙
  ·h.rightf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ f ⊚ finv = 𝟙 Yβ -- ff⁻¹ = 𝟙 Y
    have h : f.val ⊚ finv.val = 𝟙 Y := by⊢ ∃ f, IsIso f
      funext yhf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩y:Yβ.carrier⊢ (↑f ⊚ ↑finv) y = 𝟙 Y y
      cases yh.pf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.p = 𝟙 Y Y.ph.qf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.q = 𝟙 Y Y.qh.rf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.r = 𝟙 Y Y.r <;>h.pf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.p = 𝟙 Y Y.ph.qf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.q = 𝟙 Y Y.qh.rf:Xα ⟶ Yβ := ⟨f₃, ⋯⟩finv:Yβ ⟶ Xα := 
  ⟨fun x ↦
    match x with
    | Y.p => X.a
    | Y.q => X.c
    | Y.r => X.b,
    ⋯⟩⊢ (↑f ⊚ ↑finv) Y.r = 𝟙 Y Y.r rflAll goals completed! 🐙
    exact Subtype.ext hAll goals completed! 🐙

Exercise 3 (p. 159)

Prove that there is no isomorphism (in 𝑺↻)

from

inductive X
  | x₁ | x₂ | x₃ | x₄

def α : X ⟶ X
  | X.x₁ => X.x₂
  | X.x₂ => X.x₃
  | X.x₃ => X.x₄
  | X.x₄ => X.x₂

def Xα : SetWithEndomap := {
  carrier := X
  toEnd := α
}

inductive Y
  | y₁ | y₂ | y₃ | y₄

def β : Y ⟶ Y
  | Y.y₁ => Y.y₂
  | Y.y₂ => Y.y₃
  | Y.y₃ => Y.y₄
  | Y.y₄ => Y.y₁

def Yβ : SetWithEndomap := {
  carrier := Y
  toEnd := β
}

Hint: In fact, more is true: there is no map (in 𝑺↻) from X^{↻\alpha} to Y^{↻\beta}.

Solution: Exercise 3

We give a proof by contradiction below.

example : ¬(∃ f : Xα ⟶ Yβ, IsIso f) := by⊢ ¬∃ f, IsIso f
  rintro ⟨f, _⟩f:Xα ⟶ Yβh✝:IsIso f⊢ False
  -- X.x₂ is a fixed point of α ⊚ α ⊚ α,
  have h₁ : (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂ := by⊢ ¬∃ f, IsIso f rflAll goals completed! 🐙
  -- but β ⊚ β ⊚ β has no fixed points in Y
  have h₂ : ∀ y : Y, (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) y ≠ y := by⊢ ¬∃ f, IsIso f
    intro yf:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂y:Y⊢ (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) y ≠ y
    cases yy₁f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂⊢ (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) Y.y₁ ≠ Y.y₁y₂f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂⊢ (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) Y.y₂ ≠ Y.y₂y₃f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂⊢ (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) Y.y₃ ≠ Y.y₃y₄f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂⊢ (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) Y.y₄ ≠ Y.y₄ <;>y₁f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂⊢ (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) Y.y₁ ≠ Y.y₁y₂f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂⊢ (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) Y.y₂ ≠ Y.y₂y₃f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂⊢ (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) Y.y₃ ≠ Y.y₃y₄f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂⊢ (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) Y.y₄ ≠ Y.y₄ exact fun h ↦ byf:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂h:(Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) Y.y₄ = Y.y₄⊢ False contradictionAll goals completed! 🐙
  -- Since f ⊚ (α ⊚ α ⊚ α) = (β ⊚ β ⊚ β) ⊚ f, we can derive a
  -- contradiction
  have h_contra : f.val ((Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂) =
      (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) (f.val X.x₂) := by⊢ ¬∃ f, IsIso f
    rw [← types_comp_apply f.val (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd),
        ← Category.assoc, ← Category.assoc, ← f.property]f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂h₂:∀ (y : Y), (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) y ≠ y⊢ ↑f ((Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂) = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ ↑f ⊚ Xα.toEnd) X.x₂
    rw [Category.assoc Xα.toEnd f.val, ← f.property]f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂h₂:∀ (y : Y), (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) y ≠ y⊢ ↑f ((Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂) = (Yβ.toEnd ⊚ (↑f ⊚ Xα.toEnd) ⊚ Xα.toEnd) X.x₂
    rw [Category.assoc Xα.toEnd (f.val ⊚ Xα.toEnd),
        Category.assoc Xα.toEnd f.val, ← f.property]f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂h₂:∀ (y : Y), (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) y ≠ y⊢ ↑f ((Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂) = (((↑f ⊚ Xα.toEnd) ⊚ Xα.toEnd) ⊚ Xα.toEnd) X.x₂
    rw [← Category.assoc, ← Category.assoc,
        types_comp_apply (Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd)]All goals completed! 🐙
  have : (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) (f.val X.x₂) =
      f.val X.x₂ := by⊢ ¬∃ f, IsIso f
    rw [← h_contra, h₁]All goals completed! 🐙
  have : (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) (f.val X.x₂) ≠
      f.val X.x₂ := h₂ (f.val X.x₂)f:Xα ⟶ Yβh✝:IsIso fh₁:(Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂ = X.x₂h₂:∀ (y : Y), (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) y ≠ yh_contra:↑f ((Xα.toEnd ⊚ Xα.toEnd ⊚ Xα.toEnd) X.x₂) = (Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) (↑f X.x₂)this✝:(Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) (↑f X.x₂) = ↑f X.x₂this:(Yβ.toEnd ⊚ Yβ.toEnd ⊚ Yβ.toEnd) (↑f X.x₂) ≠ ↑f X.x₂⊢ False
  contradictionAll goals completed! 🐙

Exercise 4 (p. 159)

Suppose {A^{↻\alpha} \xrightarrow{f} B^{↻\beta}} is a map in 𝑺↻, and that as a map of sets, {A \xrightarrow{f} B} has an inverse {B \xrightarrow{f^{-1}} A}. Show that f^{-1} is automatically a map in 𝑺↻.

Solution: Exercise 4

Let {g = f^{-1}}.

example {Aα Bβ : SetWithEndomap}
    (f : Aα ⟶ Bβ) (g : Bβ.carrier ⟶ Aα.carrier)
    (h : g ⊚ f.val = 𝟙 Aα.carrier ∧ f.val ⊚ g = 𝟙 Bβ.carrier)
    : ∃ finv : Bβ ⟶ Aα, finv.val = g := byAα:SetWithEndomapBβ:SetWithEndomapf:Aα ⟶ Bβg:Bβ.carrier ⟶ Aα.carrierh:g ⊚ ↑f = 𝟙 Aα.carrier ∧ ↑f ⊚ g = 𝟙 Bβ.carrier⊢ ∃ finv, ↑finv = g
  obtain ⟨f, hf_comm⟩ := fAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrier⊢ ∃ finv, ↑finv = g
  use ⟨
    g,
    byAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrier⊢ g ⊚ Bβ.toEnd = Aα.toEnd ⊚ g
      funext bhAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrierb:Bβ.carrier⊢ (g ⊚ Bβ.toEnd) b = (Aα.toEnd ⊚ g) b
      apply_fun fhAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrierb:Bβ.carrier⊢ f ((g ⊚ Bβ.toEnd) b) = f ((Aα.toEnd ⊚ g) b)h.injAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrierb:Bβ.carrier⊢ Function.Injective f
      ·hAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrierb:Bβ.carrier⊢ f ((g ⊚ Bβ.toEnd) b) = f ((Aα.toEnd ⊚ g) b) rw [← types_comp_apply (g ⊚ Bβ.toEnd) f, Category.assoc,
            h.2, Category.comp_id]hAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrierb:Bβ.carrier⊢ Bβ.toEnd b = f ((Aα.toEnd ⊚ g) b)
        rw [← types_comp_apply (Aα.toEnd ⊚ g) f, Category.assoc,
            hf_comm, ← Category.assoc, h.2, Category.id_comp]All goals completed! 🐙
      ·h.injAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrierb:Bβ.carrier⊢ Function.Injective f intro a₁ a₂h.injAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrierb:Bβ.carriera₁:Aα.carriera₂:Aα.carrier⊢ f a₁ = f a₂ → a₁ = a₂ hfh.injAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrierb:Bβ.carriera₁:Aα.carriera₂:Aα.carrierhf:f a₁ = f a₂⊢ a₁ = a₂
        have hgf := congrArg g hfh.injAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrierb:Bβ.carriera₁:Aα.carriera₂:Aα.carrierhf:f a₁ = f a₂hgf:g (f a₁) = g (f a₂)⊢ a₁ = a₂
        repeat rw [← types_comp_apply f g, h.1] at hgfh.injAα:SetWithEndomapBβ:SetWithEndomapg:Bβ.carrier ⟶ Aα.carrierf:Aα.carrier ⟶ Bβ.carrierhf_comm:f ⊚ Aα.toEnd = Bβ.toEnd ⊚ fh:g ⊚ ↑⟨f, hf_comm⟩ = 𝟙 Aα.carrier ∧ ↑⟨f, hf_comm⟩ ⊚ g = 𝟙 Bβ.carrierb:Bβ.carriera₁:Aα.carriera₂:Aα.carrierhf:f a₁ = f a₂hgf:𝟙 Aα.carrier a₁ = 𝟙 Aα.carrier a₂⊢ a₁ = a₂
        exact hgfAll goals completed! 🐙
  ⟩

Exercise 5 (p. 159)

{\mathbb{Z} = \{\ldots, -2, -1, 0, 1, 2, 3, \ldots\}} is the set of integers, and \mathbb{Z}^{↻\alpha} and \mathbb{Z}^{↻\beta} are the maps which add 2 and 3: {\alpha(n) = n + 2}, {\beta(n) = n + 3}. Is \mathbb{Z}^{↻\alpha} isomorphic to \mathbb{Z}^{↻\beta}? (If so, find an isomorphism {\mathbb{Z}^{↻\alpha} \xrightarrow{f} \mathbb{Z}^{↻\beta}}; if not, explain how you know they are not isomorphic.)

Solution: Exercise 5

Define the maps \mathbb{Z}^{↻\alpha} and \mathbb{Z}^{↻\beta} as SetWithEndomap structures.

def α := (· + (2 : ℤ))
def β := (· + (3 : ℤ))

abbrev ℤα : SetWithEndomap := {
  carrier := ℤ
  toEnd := α
}

abbrev ℤβ : SetWithEndomap := {
  carrier := ℤ
  toEnd := β
}

We show that \mathbb{Z}^{↻\alpha} is not isomorphic to \mathbb{Z}^{↻\beta}.

example (f : ℤα ⟶ ℤβ) : ¬(IsIso f) := byf:ℤα ⟶ ℤβ⊢ ¬IsIso f
  -- Assume f is an isomorphism, and derive a contradiction
  by_contra hf_isof:ℤα ⟶ ℤβhf_iso:IsIso f⊢ False
  -- We begin by extracting the structure-preserving property of f
  have hf_comm
      : ∀ x : ℤ, (f.val ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ f.val) x := byf:ℤα ⟶ ℤβ⊢ ¬IsIso f
    intro xf:ℤα ⟶ ℤβhf_iso:IsIso fx:ℤ⊢ (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) x
    exact congrFun f.property xAll goals completed! 🐙
  -- and unfolding the definitions of α and β
  have hf_comm' : ∀ x : ℤ, f.val (x + 2) = f.val x + 3 := hf_commf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3⊢ False
  -- The key observation: f.val(x + 2) and f.val(x) have the same
  -- remainder when divided by 3
  have hf_mod_3_eq : ∀ x : ℤ, f.val (x + 2) ≡ f.val x [ZMOD 3] := byf:ℤα ⟶ ℤβ⊢ ¬IsIso f
    intro xf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3x:ℤ⊢ ↑f (x + 2) ≡ ↑f x [ZMOD 3]
    dsimp [Int.ModEq]f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3x:ℤ⊢ ↑f (x + 2) % 3 = ↑f x % 3
    rw [hf_comm' x]f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3x:ℤ⊢ (↑f x + 3) % 3 = ↑f x % 3
    omegaAll goals completed! 🐙
  -- Hence all even numbers map to values with the same remainder
  -- mod 3 as f.val(0),
  have hf_even_congr :
      ∀ x : ℤ, f.val (2 * x) ≡ f.val 0 [ZMOD 3] := byf:ℤα ⟶ ℤβ⊢ ¬IsIso f
    intro xf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]x:ℤ⊢ ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]
    dsimp [Int.ModEq]f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]x:ℤ⊢ ↑f (2 * x) % 3 = ↑f 0 % 3
    induction x with
    | zero =>zerof:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]⊢ ↑f (2 * 0) % 3 = ↑f 0 % 3 simpAll goals completed! 🐙
    | succ x' ih =>succf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]x':ℕih:↑f (2 * ↑x') % 3 = ↑f 0 % 3⊢ ↑f (2 * (↑x' + 1)) % 3 = ↑f 0 % 3 rw [mul_add, mul_one, hf_mod_3_eq (2 * x'), ih]All goals completed! 🐙
    | pred x' ih =>predf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]x':ℕih:↑f (2 * -↑x') % 3 = ↑f 0 % 3⊢ ↑f (2 * (-↑x' - 1)) % 3 = ↑f 0 % 3 rw [mul_sub, ← hf_mod_3_eq (2 * (-x') - 2 * 1),
        mul_one, sub_add_cancel, ih]All goals completed! 🐙
  -- and all odd numbers map to values with the same remainder mod 3
  -- as f.val(1)
  have hf_odd_congr
      : ∀ x : ℤ, f.val (2 * x + 1) ≡ f.val 1 [ZMOD 3] := byf:ℤα ⟶ ℤβ⊢ ¬IsIso f
    intro xf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]x:ℤ⊢ ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]
    dsimp [Int.ModEq]f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]x:ℤ⊢ ↑f (2 * x + 1) % 3 = ↑f 1 % 3
    induction x with
    | zero =>zerof:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]⊢ ↑f (2 * 0 + 1) % 3 = ↑f 1 % 3 simpAll goals completed! 🐙
    | succ x' ih =>succf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]x':ℕih:↑f (2 * ↑x' + 1) % 3 = ↑f 1 % 3⊢ ↑f (2 * (↑x' + 1) + 1) % 3 = ↑f 1 % 3
        rw [mul_add, mul_one]succf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]x':ℕih:↑f (2 * ↑x' + 1) % 3 = ↑f 1 % 3⊢ ↑f (2 * ↑x' + 2 + 1) % 3 = ↑f 1 % 3
        rw [add_assoc, add_comm 2 1, ← add_assoc]succf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]x':ℕih:↑f (2 * ↑x' + 1) % 3 = ↑f 1 % 3⊢ ↑f (2 * ↑x' + 1 + 2) % 3 = ↑f 1 % 3
        rw [hf_mod_3_eq (2 * x' + 1), ih]All goals completed! 🐙
    | pred x' ih =>predf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]x':ℕih:↑f (2 * -↑x' + 1) % 3 = ↑f 1 % 3⊢ ↑f (2 * (-↑x' - 1) + 1) % 3 = ↑f 1 % 3
        rw [mul_sub, ← hf_mod_3_eq (2 * (-x') - 2 * 1 + 1)]predf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]x':ℕih:↑f (2 * -↑x' + 1) % 3 = ↑f 1 % 3⊢ ↑f (2 * -↑x' - 2 * 1 + 1 + 2) % 3 = ↑f 1 % 3
        have : 2 * (-x' : ℤ) - 2 * 1 + 1 + 2 = 2 * (-x') +1 := byf:ℤα ⟶ ℤβ⊢ ¬IsIso f
          ringAll goals completed! 🐙
        rw [this]predf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]x':ℕih:↑f (2 * -↑x' + 1) % 3 = ↑f 1 % 3this:2 * -↑x' - 2 * 1 + 1 + 2 = 2 * -↑x' + 1⊢ ↑f (2 * -↑x' + 1) % 3 = ↑f 1 % 3
        exact ihAll goals completed! 🐙
  -- So the image of f.val can have at most two distinct remainders
  -- mod 3
  have hf_img_set₁ : Set.range (fun x ↦ f.val x % 3) =
      {f.val 0 % 3, f.val 1 % 3} := byf:ℤα ⟶ ℤβ⊢ ¬IsIso f
    ext bhf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carrier⊢ (b ∈ Set.range fun x ↦ ↑f x % 3) ↔ b ∈ {↑f 0 % 3, ↑f 1 % 3}
    constructorh.mpf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carrier⊢ (b ∈ Set.range fun x ↦ ↑f x % 3) → b ∈ {↑f 0 % 3, ↑f 1 % 3}h.mprf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carrier⊢ b ∈ {↑f 0 % 3, ↑f 1 % 3} → b ∈ Set.range fun x ↦ ↑f x % 3
    ·h.mpf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carrier⊢ (b ∈ Set.range fun x ↦ ↑f x % 3) → b ∈ {↑f 0 % 3, ↑f 1 % 3} rintro ⟨a, hfa⟩h.mpf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carriera:ℤα.carrierhfa:(fun x ↦ ↑f x % 3) a = b⊢ b ∈ {↑f 0 % 3, ↑f 1 % 3}
      dsimp at hfah.mpf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = b⊢ b ∈ {↑f 0 % 3, ↑f 1 % 3}
      rw [Set.mem_insert_iff, Set.mem_singleton_iff]h.mpf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = b⊢ b = ↑f 0 % 3 ∨ b = ↑f 1 % 3
      rcases Int.even_or_odd a with ha_even | ha_oddh.mp.inlf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = bha_even:Even a⊢ b = ↑f 0 % 3 ∨ b = ↑f 1 % 3h.mp.inrf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = bha_odd:Odd a⊢ b = ↑f 0 % 3 ∨ b = ↑f 1 % 3
      ·h.mp.inlf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = bha_even:Even a⊢ b = ↑f 0 % 3 ∨ b = ↑f 1 % 3 lefth.mp.inl.hf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = bha_even:Even a⊢ b = ↑f 0 % 3
        obtain ⟨a', ha_even⟩ := ha_evenh.mp.inl.hf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = ba':ℤha_even:a = a' + a'⊢ b = ↑f 0 % 3
        rw [← hfa, ha_even, ← two_mul, hf_even_congr a']All goals completed! 🐙
      ·h.mp.inrf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = bha_odd:Odd a⊢ b = ↑f 0 % 3 ∨ b = ↑f 1 % 3 righth.mp.inr.hf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = bha_odd:Odd a⊢ b = ↑f 1 % 3
        obtain ⟨a', ha_odd⟩ := ha_oddh.mp.inr.hf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = ba':ℤha_odd:a = 2 * a' + 1⊢ b = ↑f 1 % 3
        rw [← hfa, ha_odd, hf_odd_congr a']All goals completed! 🐙
    ·h.mprf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carrier⊢ b ∈ {↑f 0 % 3, ↑f 1 % 3} → b ∈ Set.range fun x ↦ ↑f x % 3 intro hbh.mprf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carrierhb:b ∈ {↑f 0 % 3, ↑f 1 % 3}⊢ b ∈ Set.range fun x ↦ ↑f x % 3
      rcases hb with hb_mem | hb_memh.mpr.inlf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carrierhb_mem:b = ↑f 0 % 3⊢ b ∈ Set.range fun x ↦ ↑f x % 3h.mpr.inrf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carrierhb_mem:b ∈ {↑f 1 % 3}⊢ b ∈ Set.range fun x ↦ ↑f x % 3 <;>h.mpr.inlf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carrierhb_mem:b = ↑f 0 % 3⊢ b ∈ Set.range fun x ↦ ↑f x % 3h.mpr.inrf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carrierhb_mem:b ∈ {↑f 1 % 3}⊢ b ∈ Set.range fun x ↦ ↑f x % 3 (rw [hb_mem]h.mpr.inrf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]b:ℤβ.carrierhb_mem:b ∈ {↑f 1 % 3}⊢ ↑f 1 % 3 ∈ Set.range fun x ↦ ↑f x % 3; simpAll goals completed! 🐙)
  -- Now, since f is an isomorphism, f.val is bijective
  have hf_bij : Function.Bijective f.val :=
    ConcreteCategory.bijective_of_isIso ff:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑f⊢ False
  -- and hence surjective,
  have hf_surj : Function.Surjective f.val := hf_bij.rightf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑f⊢ False
  -- but a surjective function on ℤ must hit all three remainders
  -- mod 3
  have hf_img_set₂ :
      Set.range (fun x ↦ f.val x % 3) = {0, 1, 2} := byf:ℤα ⟶ ℤβ⊢ ¬IsIso f
    ext bhf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrier⊢ (b ∈ Set.range fun x ↦ ↑f x % 3) ↔ b ∈ {0, 1, 2}
    constructorh.mpf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrier⊢ (b ∈ Set.range fun x ↦ ↑f x % 3) → b ∈ {0, 1, 2}h.mprf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrier⊢ b ∈ {0, 1, 2} → b ∈ Set.range fun x ↦ ↑f x % 3
    ·h.mpf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrier⊢ (b ∈ Set.range fun x ↦ ↑f x % 3) → b ∈ {0, 1, 2} rintro ⟨a, hfa⟩h.mpf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carriera:ℤα.carrierhfa:(fun x ↦ ↑f x % 3) a = b⊢ b ∈ {0, 1, 2}
      dsimp at hfah.mpf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = b⊢ b ∈ {0, 1, 2}
      have hf_lbound : 0 ≤ f.val a % 3 := Int.emod_nonneg
          (f.val a) (byf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = b⊢ 3 ≠ 0 decideAll goals completed! 🐙 : (3 : ℤ) ≠ 0)
      have hf_ubound : f.val a % 3 < 3 := Int.emod_lt_of_pos
          (f.val a) (byf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carriera:ℤα.carrierhfa:↑f a % 3 = bhf_lbound:0 ≤ ↑f a % 3⊢ 0 < 3 decideAll goals completed! 🐙 : (0 < (3 : ℤ)))
      interval_cases k : f.val a % 3 using hf_lbound, hf_uboundh.mp.«0»f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carriera:ℤα.carrierk:↑f a % 3 = 0hfa:0 = bhf_lbound:0 ≤ 0hf_ubound:0 < 3⊢ b ∈ {0, 1, 2}h.mp.«1»f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carriera:ℤα.carrierk:↑f a % 3 = 1hfa:1 = bhf_lbound:0 ≤ 1hf_ubound:1 < 3⊢ b ∈ {0, 1, 2}h.mp.«2»f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carriera:ℤα.carrierk:↑f a % 3 = 2hfa:2 = bhf_lbound:0 ≤ 2hf_ubound:2 < 3⊢ b ∈ {0, 1, 2} <;>h.mp.«0»f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carriera:ℤα.carrierk:↑f a % 3 = 0hfa:0 = bhf_lbound:0 ≤ 0hf_ubound:0 < 3⊢ b ∈ {0, 1, 2}h.mp.«1»f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carriera:ℤα.carrierk:↑f a % 3 = 1hfa:1 = bhf_lbound:0 ≤ 1hf_ubound:1 < 3⊢ b ∈ {0, 1, 2}h.mp.«2»f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carriera:ℤα.carrierk:↑f a % 3 = 2hfa:2 = bhf_lbound:0 ≤ 2hf_ubound:2 < 3⊢ b ∈ {0, 1, 2}
        (rw [← hfa]h.mp.«2»f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carriera:ℤα.carrierk:↑f a % 3 = 2hfa:2 = bhf_lbound:0 ≤ 2hf_ubound:2 < 3⊢ 2 ∈ {0, 1, 2}; boundAll goals completed! 🐙)
    ·h.mprf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrier⊢ b ∈ {0, 1, 2} → b ∈ Set.range fun x ↦ ↑f x % 3 rintro (hb | hb | hb)h.mpr.inlf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrierhb:b = 0⊢ b ∈ Set.range fun x ↦ ↑f x % 3h.mpr.inr.inlf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrierhb:b = 1⊢ b ∈ Set.range fun x ↦ ↑f x % 3h.mpr.inr.inrf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrierhb:b ∈ {2}⊢ b ∈ Set.range fun x ↦ ↑f x % 3
      all_goals
        obtain ⟨a, hfa⟩ := hf_surj bh.mpr.inr.inrf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrierhb:b ∈ {2}a:ℤα.carrierhfa:↑f a = b⊢ b ∈ Set.range fun x ↦ ↑f x % 3
        use ahf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrierhb:b ∈ {2}a:ℤα.carrierhfa:↑f a = b⊢ (fun x ↦ ↑f x % 3) a = b
        dsimphf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrierhb:b ∈ {2}a:ℤα.carrierhfa:↑f a = b⊢ ↑f a % 3 = b
        rw [hfa, hb]hf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fb:ℤβ.carrierhb:b ∈ {2}a:ℤα.carrierhfa:↑f a = b⊢ 2 % 3 = 2
        norm_num1All goals completed! 🐙
  -- Since we have found that the image of f.val can have at most
  -- two distinct elements and must also have exactly three distinct
  -- elements, we have a contradiction
  have h_card₁
      : Set.ncard ({f.val 0 % 3, f.val 1 % 3} : Set ℤ) ≤ 2 := byf:ℤα ⟶ ℤβ⊢ ¬IsIso f
    have h := Set.ncard_insert_le (f.val 0 % 3) {f.val 1 % 3}f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fhf_img_set₂:(Set.range fun x ↦ ↑f x % 3) = {0, 1, 2}h:{↑f 0 % 3, ↑f 1 % 3}.ncard ≤ {↑f 1 % 3}.ncard + 1⊢ {↑f 0 % 3, ↑f 1 % 3}.ncard ≤ 2
    rwa [Set.ncard_singleton]f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fhf_img_set₂:(Set.range fun x ↦ ↑f x % 3) = {0, 1, 2}h:{↑f 0 % 3, ↑f 1 % 3}.ncard ≤ 1 + 1⊢ {↑f 0 % 3, ↑f 1 % 3}.ncard ≤ 2 at h
  have h_card₂ : Set.ncard ({0, 1, 2} : Set ℤ) = 3 := byf:ℤα ⟶ ℤβ⊢ ¬IsIso f
    apply Set.ncard_eq_three.mprf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fhf_img_set₂:(Set.range fun x ↦ ↑f x % 3) = {0, 1, 2}h_card₁:{↑f 0 % 3, ↑f 1 % 3}.ncard ≤ 2⊢ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ {0, 1, 2} = {x, y, z}
    use 0, 1, 2hf:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fhf_img_set₂:(Set.range fun x ↦ ↑f x % 3) = {0, 1, 2}h_card₁:{↑f 0 % 3, ↑f 1 % 3}.ncard ≤ 2⊢ 0 ≠ 1 ∧ 0 ≠ 2 ∧ 1 ≠ 2 ∧ {0, 1, 2} = {0, 1, 2}
    trivialAll goals completed! 🐙
  rw [← hf_img_set₁, hf_img_set₂, h_card₂] at h_card₁f:ℤα ⟶ ℤβhf_iso:IsIso fhf_comm:∀ (x : ℤ), (↑f ∘ ℤα.toEnd) x = (ℤβ.toEnd ∘ ↑f) xhf_comm':∀ (x : ℤ), ↑f (x + 2) = ↑f x + 3hf_mod_3_eq:∀ (x : ℤ), ↑f (x + 2) ≡ ↑f x [ZMOD 3]hf_even_congr:∀ (x : ℤ), ↑f (2 * x) ≡ ↑f 0 [ZMOD 3]hf_odd_congr:∀ (x : ℤ), ↑f (2 * x + 1) ≡ ↑f 1 [ZMOD 3]hf_img_set₁:(Set.range fun x ↦ ↑f x % 3) = {↑f 0 % 3, ↑f 1 % 3}hf_bij:Function.Bijective ↑fhf_surj:Function.Surjective ↑fhf_img_set₂:(Set.range fun x ↦ ↑f x % 3) = {0, 1, 2}h_card₁:3 ≤ 2h_card₂:{0, 1, 2}.ncard = 3⊢ False
  linarithAll goals completed! 🐙

Exercise 6 (p. 159)

Each of the following graphs is isomorphic to exactly one of the others. Which?

Solution: Exercise 6

We label the arrows in each graph from top to bottom.

inductive A
  | a₁ | a₂ | a₃

We label the dots in each graph from left to right.

inductive D
  | d₁ | d₂ | d₃

Then the six graphs (a) to (f) are as follows:

def graph_a : IrreflexiveGraph := {
  carrierA := A
  carrierD := D
  toSrc := fun
    | A.a₁ => D.d₂
    | A.a₂ => D.d₁
    | A.a₃ => D.d₃
  toTgt := fun
    | A.a₁ => D.d₃
    | A.a₂ => D.d₂
    | A.a₃ => D.d₂
}

def graph_b : IrreflexiveGraph := {
  carrierA := A
  carrierD := D
  toSrc := fun
    | A.a₁ => D.d₁
    | A.a₂ => D.d₂
    | A.a₃ => D.d₂,
  toTgt := fun
    | A.a₁ => D.d₂
    | A.a₂ => D.d₃
    | A.a₃ => D.d₁
}

def graph_c : IrreflexiveGraph := {
  carrierA := A
  carrierD := D
  toSrc := fun
    | A.a₁ => D.d₁
    | A.a₂ => D.d₁
    | A.a₃ => D.d₁
  toTgt := fun
    | A.a₁ => D.d₃
    | A.a₂ => D.d₂
    | A.a₃ => D.d₃
}

def graph_d : IrreflexiveGraph := {
  carrierA := A
  carrierD := D
  toSrc := fun
    | A.a₁ => D.d₃
    | A.a₂ => D.d₁
    | A.a₃ => D.d₂
  toTgt := fun
    | A.a₁ => D.d₂
    | A.a₂ => D.d₂
    | A.a₃ => D.d₃
}

def graph_e : IrreflexiveGraph := {
  carrierA := A
  carrierD := D
  toSrc := fun
    | A.a₁ => D.d₁
    | A.a₂ => D.d₁
    | A.a₃ => D.d₃
  toTgt := fun
    | A.a₁ => D.d₃
    | A.a₂ => D.d₂
    | A.a₃ => D.d₁
}

def graph_f : IrreflexiveGraph := {
  carrierA := A
  carrierD := D
  toSrc := fun
    | A.a₁ => D.d₁
    | A.a₂ => D.d₁
    | A.a₃ => D.d₁
  toTgt := fun
    | A.a₁ => D.d₂
    | A.a₂ => D.d₃
    | A.a₃ => D.d₃
}

Graph (a) is isomorphic to graph (d).

def f₁ : graph_a ⟶ graph_d := {
  val := (
    fun -- maps arrows
      | A.a₁ => A.a₃
      | A.a₂ => A.a₂
      | A.a₃ => A.a₁,
    fun -- maps dots
      | D.d₁ => D.d₁
      | D.d₂ => D.d₂
      | D.d₃ => D.d₃
  )
  property := by⊢ (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_a.toSrc =
    graph_d.toSrc ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1 ∧
  (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_a.toTgt =
    graph_d.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1
    constructorleft⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).2 ⊚
    graph_a.toSrc =
  graph_d.toSrc ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).1right⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).2 ⊚
    graph_a.toTgt =
  graph_d.toTgt ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).1
    all_goals
      funext xright.hx:graph_a.carrierA⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_a.toTgt)
    x =
  (graph_d.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    x; cases xright.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_a.toTgt)
    A.a₁ =
  (graph_d.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_a.toTgt)
    A.a₂ =
  (graph_d.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_a.toTgt)
    A.a₃ =
  (graph_d.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₃ <;>right.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_a.toTgt)
    A.a₁ =
  (graph_d.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_a.toTgt)
    A.a₂ =
  (graph_d.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_a.toTgt)
    A.a₃ =
  (graph_d.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₃ rflAll goals completed! 🐙
}

def finv₁ : graph_d ⟶ graph_a := {
  val := (
    fun -- maps arrows
      | A.a₁ => A.a₃
      | A.a₂ => A.a₂
      | A.a₃ => A.a₁,
    fun -- maps dots
      | D.d₁ => D.d₁
      | D.d₂ => D.d₂
      | D.d₃ => D.d₃
  )
  property := by⊢ (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_d.toSrc =
    graph_a.toSrc ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1 ∧
  (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_d.toTgt =
    graph_a.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1
    constructorleft⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).2 ⊚
    graph_d.toSrc =
  graph_a.toSrc ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).1right⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).2 ⊚
    graph_d.toTgt =
  graph_a.toTgt ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).1
    all_goals
      funext xright.hx:graph_d.carrierA⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_d.toTgt)
    x =
  (graph_a.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    x; cases xright.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_d.toTgt)
    A.a₁ =
  (graph_a.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_d.toTgt)
    A.a₂ =
  (graph_a.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_d.toTgt)
    A.a₃ =
  (graph_a.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₃ <;>right.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_d.toTgt)
    A.a₁ =
  (graph_a.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_d.toTgt)
    A.a₂ =
  (graph_a.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_d.toTgt)
    A.a₃ =
  (graph_a.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₃ rflAll goals completed! 🐙
}

example : graph_a ≅ graph_d := {
  hom := f₁,
  inv := finv₁,
  hom_inv_id := by⊢ finv₁ ⊚ f₁ = 𝟙 graph_a
    have h₁ : (finv₁.val.1 ⊚ f₁.val.1 = 𝟙 graph_a.carrierA) ∧
        (finv₁.val.2 ⊚ f₁.val.2 = 𝟙 graph_a.carrierD) := by⊢ finv₁ ⊚ f₁ = 𝟙 graph_a
      constructorleft⊢ (↑finv₁).1 ⊚ (↑f₁).1 = 𝟙 graph_a.carrierAright⊢ (↑finv₁).2 ⊚ (↑f₁).2 = 𝟙 graph_a.carrierD <;>left⊢ (↑finv₁).1 ⊚ (↑f₁).1 = 𝟙 graph_a.carrierAright⊢ (↑finv₁).2 ⊚ (↑f₁).2 = 𝟙 graph_a.carrierD (funext xright.hx:graph_a.carrierD⊢ ((↑finv₁).2 ⊚ (↑f₁).2) x = 𝟙 graph_a.carrierD x; cases xright.h.d₁⊢ ((↑finv₁).2 ⊚ (↑f₁).2) D.d₁ = 𝟙 graph_a.carrierD D.d₁right.h.d₂⊢ ((↑finv₁).2 ⊚ (↑f₁).2) D.d₂ = 𝟙 graph_a.carrierD D.d₂right.h.d₃⊢ ((↑finv₁).2 ⊚ (↑f₁).2) D.d₃ = 𝟙 graph_a.carrierD D.d₃ <;>right.h.d₁⊢ ((↑finv₁).2 ⊚ (↑f₁).2) D.d₁ = 𝟙 graph_a.carrierD D.d₁right.h.d₂⊢ ((↑finv₁).2 ⊚ (↑f₁).2) D.d₂ = 𝟙 graph_a.carrierD D.d₂right.h.d₃⊢ ((↑finv₁).2 ⊚ (↑f₁).2) D.d₃ = 𝟙 graph_a.carrierD D.d₃ rflAll goals completed! 🐙)
    have h₂ : (finv₁.val.1 ⊚ f₁.val.1, finv₁.val.2 ⊚ f₁.val.2) =
        (𝟙 graph_a.carrierA, 𝟙 graph_a.carrierD) := by⊢ finv₁ ⊚ f₁ = 𝟙 graph_a
      rw [h₁.1, h₁.2]All goals completed! 🐙
    exact Subtype.ext h₂All goals completed! 🐙,
  inv_hom_id := by⊢ f₁ ⊚ finv₁ = 𝟙 graph_d
    have h₁ : (f₁.val.1 ⊚ finv₁.val.1 = 𝟙 graph_d.carrierA) ∧
        (f₁.val.2 ⊚ finv₁.val.2 = 𝟙 graph_d.carrierD) := by⊢ f₁ ⊚ finv₁ = 𝟙 graph_d
      constructorleft⊢ (↑f₁).1 ⊚ (↑finv₁).1 = 𝟙 graph_d.carrierAright⊢ (↑f₁).2 ⊚ (↑finv₁).2 = 𝟙 graph_d.carrierD <;>left⊢ (↑f₁).1 ⊚ (↑finv₁).1 = 𝟙 graph_d.carrierAright⊢ (↑f₁).2 ⊚ (↑finv₁).2 = 𝟙 graph_d.carrierD (funext xright.hx:graph_d.carrierD⊢ ((↑f₁).2 ⊚ (↑finv₁).2) x = 𝟙 graph_d.carrierD x; cases xright.h.d₁⊢ ((↑f₁).2 ⊚ (↑finv₁).2) D.d₁ = 𝟙 graph_d.carrierD D.d₁right.h.d₂⊢ ((↑f₁).2 ⊚ (↑finv₁).2) D.d₂ = 𝟙 graph_d.carrierD D.d₂right.h.d₃⊢ ((↑f₁).2 ⊚ (↑finv₁).2) D.d₃ = 𝟙 graph_d.carrierD D.d₃ <;>right.h.d₁⊢ ((↑f₁).2 ⊚ (↑finv₁).2) D.d₁ = 𝟙 graph_d.carrierD D.d₁right.h.d₂⊢ ((↑f₁).2 ⊚ (↑finv₁).2) D.d₂ = 𝟙 graph_d.carrierD D.d₂right.h.d₃⊢ ((↑f₁).2 ⊚ (↑finv₁).2) D.d₃ = 𝟙 graph_d.carrierD D.d₃ rflAll goals completed! 🐙)
    have h₂ : (f₁.val.1 ⊚ finv₁.val.1, f₁.val.2 ⊚ finv₁.val.2) =
        (𝟙 graph_d.carrierA, 𝟙 graph_d.carrierD) := by⊢ f₁ ⊚ finv₁ = 𝟙 graph_d
      rw [h₁.1, h₁.2]All goals completed! 🐙
    exact Subtype.ext h₂All goals completed! 🐙
}

Graph (b) is isomorphic to graph (e).

def f₂ : graph_b ⟶ graph_e := {
  val := (
    fun -- maps arrows
      | A.a₁ => A.a₃
      | A.a₂ => A.a₂
      | A.a₃ => A.a₁,
    fun -- maps dots
      | D.d₁ => D.d₃
      | D.d₂ => D.d₁
      | D.d₃ => D.d₂
  )
  property := by⊢ (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).2 ⊚
      graph_b.toSrc =
    graph_e.toSrc ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).1 ∧
  (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).2 ⊚
      graph_b.toTgt =
    graph_e.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).1
    constructorleft⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₁
        | D.d₃ => D.d₂).2 ⊚
    graph_b.toSrc =
  graph_e.toSrc ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₁
        | D.d₃ => D.d₂).1right⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₁
        | D.d₃ => D.d₂).2 ⊚
    graph_b.toTgt =
  graph_e.toTgt ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₁
        | D.d₃ => D.d₂).1
    all_goals
      funext xright.hx:graph_b.carrierA⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).2 ⊚
      graph_b.toTgt)
    x =
  (graph_e.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).1)
    x; cases xright.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).2 ⊚
      graph_b.toTgt)
    A.a₁ =
  (graph_e.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).2 ⊚
      graph_b.toTgt)
    A.a₂ =
  (graph_e.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).2 ⊚
      graph_b.toTgt)
    A.a₃ =
  (graph_e.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).1)
    A.a₃ <;>right.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).2 ⊚
      graph_b.toTgt)
    A.a₁ =
  (graph_e.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).2 ⊚
      graph_b.toTgt)
    A.a₂ =
  (graph_e.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).2 ⊚
      graph_b.toTgt)
    A.a₃ =
  (graph_e.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₁
          | D.d₃ => D.d₂).1)
    A.a₃ rflAll goals completed! 🐙
}

def finv₂ : graph_e ⟶ graph_b := {
  val := (
    fun -- maps arrows
      | A.a₁ => A.a₃
      | A.a₂ => A.a₂
      | A.a₃ => A.a₁,
    fun -- maps dots
      | D.d₁ => D.d₂
      | D.d₂ => D.d₃
      | D.d₃ => D.d₁
  )
  property := by⊢ (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).2 ⊚
      graph_e.toSrc =
    graph_b.toSrc ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).1 ∧
  (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).2 ⊚
      graph_e.toTgt =
    graph_b.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).1
    constructorleft⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₂
        | D.d₂ => D.d₃
        | D.d₃ => D.d₁).2 ⊚
    graph_e.toSrc =
  graph_b.toSrc ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₂
        | D.d₂ => D.d₃
        | D.d₃ => D.d₁).1right⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₂
        | D.d₂ => D.d₃
        | D.d₃ => D.d₁).2 ⊚
    graph_e.toTgt =
  graph_b.toTgt ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₂
        | A.a₃ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₂
        | D.d₂ => D.d₃
        | D.d₃ => D.d₁).1
    all_goals
      funext xright.hx:graph_e.carrierA⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).2 ⊚
      graph_e.toTgt)
    x =
  (graph_b.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).1)
    x; cases xright.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).2 ⊚
      graph_e.toTgt)
    A.a₁ =
  (graph_b.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).2 ⊚
      graph_e.toTgt)
    A.a₂ =
  (graph_b.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).2 ⊚
      graph_e.toTgt)
    A.a₃ =
  (graph_b.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).1)
    A.a₃ <;>right.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).2 ⊚
      graph_e.toTgt)
    A.a₁ =
  (graph_b.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).2 ⊚
      graph_e.toTgt)
    A.a₂ =
  (graph_b.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).2 ⊚
      graph_e.toTgt)
    A.a₃ =
  (graph_b.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₂
          | A.a₃ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₂
          | D.d₂ => D.d₃
          | D.d₃ => D.d₁).1)
    A.a₃ rflAll goals completed! 🐙
}

example : graph_b ≅ graph_e := {
  hom := f₂,
  inv := finv₂,
  hom_inv_id := by⊢ finv₂ ⊚ f₂ = 𝟙 graph_b
    have h₁ : (finv₂.val.1 ⊚ f₂.val.1 = 𝟙 graph_b.carrierA) ∧
        (finv₂.val.2 ⊚ f₂.val.2 = 𝟙 graph_b.carrierD) := by⊢ finv₂ ⊚ f₂ = 𝟙 graph_b
      constructorleft⊢ (↑finv₂).1 ⊚ (↑f₂).1 = 𝟙 graph_b.carrierAright⊢ (↑finv₂).2 ⊚ (↑f₂).2 = 𝟙 graph_b.carrierD <;>left⊢ (↑finv₂).1 ⊚ (↑f₂).1 = 𝟙 graph_b.carrierAright⊢ (↑finv₂).2 ⊚ (↑f₂).2 = 𝟙 graph_b.carrierD (funext xright.hx:graph_b.carrierD⊢ ((↑finv₂).2 ⊚ (↑f₂).2) x = 𝟙 graph_b.carrierD x; cases xright.h.d₁⊢ ((↑finv₂).2 ⊚ (↑f₂).2) D.d₁ = 𝟙 graph_b.carrierD D.d₁right.h.d₂⊢ ((↑finv₂).2 ⊚ (↑f₂).2) D.d₂ = 𝟙 graph_b.carrierD D.d₂right.h.d₃⊢ ((↑finv₂).2 ⊚ (↑f₂).2) D.d₃ = 𝟙 graph_b.carrierD D.d₃ <;>right.h.d₁⊢ ((↑finv₂).2 ⊚ (↑f₂).2) D.d₁ = 𝟙 graph_b.carrierD D.d₁right.h.d₂⊢ ((↑finv₂).2 ⊚ (↑f₂).2) D.d₂ = 𝟙 graph_b.carrierD D.d₂right.h.d₃⊢ ((↑finv₂).2 ⊚ (↑f₂).2) D.d₃ = 𝟙 graph_b.carrierD D.d₃ rflAll goals completed! 🐙)
    have h₂ : (finv₂.val.1 ⊚ f₂.val.1, finv₂.val.2 ⊚ f₂.val.2) =
        (𝟙 graph_b.carrierA, 𝟙 graph_b.carrierD) := by⊢ finv₂ ⊚ f₂ = 𝟙 graph_b
      rw [h₁.1, h₁.2]All goals completed! 🐙
    exact Subtype.ext h₂All goals completed! 🐙,
  inv_hom_id := by⊢ f₂ ⊚ finv₂ = 𝟙 graph_e
    have h₁ : (f₂.val.1 ⊚ finv₂.val.1 = 𝟙 graph_e.carrierA) ∧
        (f₂.val.2 ⊚ finv₂.val.2 = 𝟙 graph_e.carrierD) := by⊢ f₂ ⊚ finv₂ = 𝟙 graph_e
      constructorleft⊢ (↑f₂).1 ⊚ (↑finv₂).1 = 𝟙 graph_e.carrierAright⊢ (↑f₂).2 ⊚ (↑finv₂).2 = 𝟙 graph_e.carrierD <;>left⊢ (↑f₂).1 ⊚ (↑finv₂).1 = 𝟙 graph_e.carrierAright⊢ (↑f₂).2 ⊚ (↑finv₂).2 = 𝟙 graph_e.carrierD (funext xright.hx:graph_e.carrierD⊢ ((↑f₂).2 ⊚ (↑finv₂).2) x = 𝟙 graph_e.carrierD x; cases xright.h.d₁⊢ ((↑f₂).2 ⊚ (↑finv₂).2) D.d₁ = 𝟙 graph_e.carrierD D.d₁right.h.d₂⊢ ((↑f₂).2 ⊚ (↑finv₂).2) D.d₂ = 𝟙 graph_e.carrierD D.d₂right.h.d₃⊢ ((↑f₂).2 ⊚ (↑finv₂).2) D.d₃ = 𝟙 graph_e.carrierD D.d₃ <;>right.h.d₁⊢ ((↑f₂).2 ⊚ (↑finv₂).2) D.d₁ = 𝟙 graph_e.carrierD D.d₁right.h.d₂⊢ ((↑f₂).2 ⊚ (↑finv₂).2) D.d₂ = 𝟙 graph_e.carrierD D.d₂right.h.d₃⊢ ((↑f₂).2 ⊚ (↑finv₂).2) D.d₃ = 𝟙 graph_e.carrierD D.d₃ rflAll goals completed! 🐙)
    have h₂ : (f₂.val.1 ⊚ finv₂.val.1, f₂.val.2 ⊚ finv₂.val.2) =
        (𝟙 graph_e.carrierA, 𝟙 graph_e.carrierD) := by⊢ f₂ ⊚ finv₂ = 𝟙 graph_e
      rw [h₁.1, h₁.2]All goals completed! 🐙
    exact Subtype.ext h₂All goals completed! 🐙
}

Graph (c) is isomorphic to graph (f).

def f₃ : graph_c ⟶ graph_f := {
  val := (
    fun -- maps arrows
      | A.a₁ => A.a₂
      | A.a₂ => A.a₁
      | A.a₃ => A.a₃,
    fun -- maps dots
      | D.d₁ => D.d₁
      | D.d₂ => D.d₂
      | D.d₃ => D.d₃
  )
  property := by⊢ (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_c.toSrc =
    graph_f.toSrc ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1 ∧
  (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_c.toTgt =
    graph_f.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1
    constructorleft⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₂
        | A.a₂ => A.a₁
        | A.a₃ => A.a₃,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).2 ⊚
    graph_c.toSrc =
  graph_f.toSrc ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₂
        | A.a₂ => A.a₁
        | A.a₃ => A.a₃,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).1right⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₂
        | A.a₂ => A.a₁
        | A.a₃ => A.a₃,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).2 ⊚
    graph_c.toTgt =
  graph_f.toTgt ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₂
        | A.a₂ => A.a₁
        | A.a₃ => A.a₃,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).1
    all_goals
      funext xright.hx:graph_c.carrierA⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_c.toTgt)
    x =
  (graph_f.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    x; cases xright.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_c.toTgt)
    A.a₁ =
  (graph_f.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_c.toTgt)
    A.a₂ =
  (graph_f.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_c.toTgt)
    A.a₃ =
  (graph_f.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₃ <;>right.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_c.toTgt)
    A.a₁ =
  (graph_f.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_c.toTgt)
    A.a₂ =
  (graph_f.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_c.toTgt)
    A.a₃ =
  (graph_f.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₃ rflAll goals completed! 🐙
}

def finv₃ : graph_f ⟶ graph_c := {
  val := (
    fun -- maps arrows
      | A.a₁ => A.a₂
      | A.a₂ => A.a₁
      | A.a₃ => A.a₃,
    fun -- maps dots
      | D.d₁ => D.d₁
      | D.d₂ => D.d₂
      | D.d₃ => D.d₃
  )
  property := by⊢ (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_f.toSrc =
    graph_c.toSrc ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1 ∧
  (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_f.toTgt =
    graph_c.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1
    constructorleft⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₂
        | A.a₂ => A.a₁
        | A.a₃ => A.a₃,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).2 ⊚
    graph_f.toSrc =
  graph_c.toSrc ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₂
        | A.a₂ => A.a₁
        | A.a₃ => A.a₃,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).1right⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₂
        | A.a₂ => A.a₁
        | A.a₃ => A.a₃,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).2 ⊚
    graph_f.toTgt =
  graph_c.toTgt ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₂
        | A.a₂ => A.a₁
        | A.a₃ => A.a₃,
        fun x ↦
        match x with
        | D.d₁ => D.d₁
        | D.d₂ => D.d₂
        | D.d₃ => D.d₃).1
    all_goals
      funext xright.hx:graph_f.carrierA⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_f.toTgt)
    x =
  (graph_c.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    x; cases xright.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_f.toTgt)
    A.a₁ =
  (graph_c.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_f.toTgt)
    A.a₂ =
  (graph_c.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_f.toTgt)
    A.a₃ =
  (graph_c.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₃ <;>right.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_f.toTgt)
    A.a₁ =
  (graph_c.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_f.toTgt)
    A.a₂ =
  (graph_c.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).2 ⊚
      graph_f.toTgt)
    A.a₃ =
  (graph_c.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₂
          | A.a₂ => A.a₁
          | A.a₃ => A.a₃,
          fun x ↦
          match x with
          | D.d₁ => D.d₁
          | D.d₂ => D.d₂
          | D.d₃ => D.d₃).1)
    A.a₃ rflAll goals completed! 🐙
}

example : graph_c ≅ graph_f := {
  hom := f₃,
  inv := finv₃,
  hom_inv_id := by⊢ finv₃ ⊚ f₃ = 𝟙 graph_c
    have h₁ : (finv₃.val.1 ⊚ f₃.val.1 = 𝟙 graph_c.carrierA) ∧
        (finv₃.val.2 ⊚ f₃.val.2 = 𝟙 graph_c.carrierD) := by⊢ finv₃ ⊚ f₃ = 𝟙 graph_c
      constructorleft⊢ (↑finv₃).1 ⊚ (↑f₃).1 = 𝟙 graph_c.carrierAright⊢ (↑finv₃).2 ⊚ (↑f₃).2 = 𝟙 graph_c.carrierD <;>left⊢ (↑finv₃).1 ⊚ (↑f₃).1 = 𝟙 graph_c.carrierAright⊢ (↑finv₃).2 ⊚ (↑f₃).2 = 𝟙 graph_c.carrierD (funext xright.hx:graph_c.carrierD⊢ ((↑finv₃).2 ⊚ (↑f₃).2) x = 𝟙 graph_c.carrierD x; cases xright.h.d₁⊢ ((↑finv₃).2 ⊚ (↑f₃).2) D.d₁ = 𝟙 graph_c.carrierD D.d₁right.h.d₂⊢ ((↑finv₃).2 ⊚ (↑f₃).2) D.d₂ = 𝟙 graph_c.carrierD D.d₂right.h.d₃⊢ ((↑finv₃).2 ⊚ (↑f₃).2) D.d₃ = 𝟙 graph_c.carrierD D.d₃ <;>right.h.d₁⊢ ((↑finv₃).2 ⊚ (↑f₃).2) D.d₁ = 𝟙 graph_c.carrierD D.d₁right.h.d₂⊢ ((↑finv₃).2 ⊚ (↑f₃).2) D.d₂ = 𝟙 graph_c.carrierD D.d₂right.h.d₃⊢ ((↑finv₃).2 ⊚ (↑f₃).2) D.d₃ = 𝟙 graph_c.carrierD D.d₃ rflAll goals completed! 🐙)
    have h₂ : (finv₃.val.1 ⊚ f₃.val.1, finv₃.val.2 ⊚ f₃.val.2) =
        (𝟙 graph_c.carrierA, 𝟙 graph_c.carrierD) := by⊢ finv₃ ⊚ f₃ = 𝟙 graph_c
      rw [h₁.1, h₁.2]All goals completed! 🐙
    exact Subtype.ext h₂All goals completed! 🐙,
  inv_hom_id := by⊢ f₃ ⊚ finv₃ = 𝟙 graph_f
    have h₁ : (f₃.val.1 ⊚ finv₃.val.1 = 𝟙 graph_f.carrierA) ∧
        (f₃.val.2 ⊚ finv₃.val.2 = 𝟙 graph_f.carrierD) := by⊢ f₃ ⊚ finv₃ = 𝟙 graph_f
      constructorleft⊢ (↑f₃).1 ⊚ (↑finv₃).1 = 𝟙 graph_f.carrierAright⊢ (↑f₃).2 ⊚ (↑finv₃).2 = 𝟙 graph_f.carrierD <;>left⊢ (↑f₃).1 ⊚ (↑finv₃).1 = 𝟙 graph_f.carrierAright⊢ (↑f₃).2 ⊚ (↑finv₃).2 = 𝟙 graph_f.carrierD (funext xright.hx:graph_f.carrierD⊢ ((↑f₃).2 ⊚ (↑finv₃).2) x = 𝟙 graph_f.carrierD x; cases xright.h.d₁⊢ ((↑f₃).2 ⊚ (↑finv₃).2) D.d₁ = 𝟙 graph_f.carrierD D.d₁right.h.d₂⊢ ((↑f₃).2 ⊚ (↑finv₃).2) D.d₂ = 𝟙 graph_f.carrierD D.d₂right.h.d₃⊢ ((↑f₃).2 ⊚ (↑finv₃).2) D.d₃ = 𝟙 graph_f.carrierD D.d₃ <;>right.h.d₁⊢ ((↑f₃).2 ⊚ (↑finv₃).2) D.d₁ = 𝟙 graph_f.carrierD D.d₁right.h.d₂⊢ ((↑f₃).2 ⊚ (↑finv₃).2) D.d₂ = 𝟙 graph_f.carrierD D.d₂right.h.d₃⊢ ((↑f₃).2 ⊚ (↑finv₃).2) D.d₃ = 𝟙 graph_f.carrierD D.d₃ rflAll goals completed! 🐙)
    have h₂ : (f₃.val.1 ⊚ finv₃.val.1, f₃.val.2 ⊚ finv₃.val.2) =
        (𝟙 graph_f.carrierA, 𝟙 graph_f.carrierD) := by⊢ f₃ ⊚ finv₃ = 𝟙 graph_f
      rw [h₁.1, h₁.2]All goals completed! 🐙
    exact Subtype.ext h₂All goals completed! 🐙
}

Exercise 7 (p. 160)

If these two graphs are isomorphic, find an isomorphism between them; if they are not isomorphic, explain how you know they are not.

Solution: Exercise 7

We label the arrows in each graph starting with the arrow at the bottom left and moving clockwise through the four outer arrows (a_1 to a_4) and then vertically upwards through the two inner arrows (a_5 and a_6).

inductive A
  | a₁ | a₂ | a₃ | a₄ | a₅ | a₆

We label the dots in each graph starting with the bottom dot and moving clockwise through the four outer dots (d_1 to d_4) and then finishing with the centre dot (d_5).

inductive D
  | d₁ | d₂ | d₃ | d₄ | d₅

Then the two graphs are as follows:

def graph_L : IrreflexiveGraph := {
  carrierA := A
  carrierD := D
  toSrc := fun
    | A.a₁ => D.d₁
    | A.a₂ => D.d₂
    | A.a₃ => D.d₃
    | A.a₄ => D.d₄
    | A.a₅ => D.d₁
    | A.a₆ => D.d₅
  toTgt := fun
    | A.a₁ => D.d₂
    | A.a₂ => D.d₃
    | A.a₃ => D.d₄
    | A.a₄ => D.d₁
    | A.a₅ => D.d₅
    | A.a₆ => D.d₃
}

def graph_R : IrreflexiveGraph := {
  carrierA := A
  carrierD := D
  toSrc := fun
    | A.a₁ => D.d₂
    | A.a₂ => D.d₃
    | A.a₃ => D.d₃
    | A.a₄ => D.d₄
    | A.a₅ => D.d₁
    | A.a₆ => D.d₅
  toTgt := fun
    | A.a₁ => D.d₁
    | A.a₂ => D.d₂
    | A.a₃ => D.d₄
    | A.a₄ => D.d₁
    | A.a₅ => D.d₅
    | A.a₆ => D.d₃
}

The two graphs are isomorphic, with an isomorphism between them given by f below.

def f : graph_L ⟶ graph_R := {
  val := (
    fun -- maps arrows
      | A.a₁ => A.a₃
      | A.a₂ => A.a₄
      | A.a₃ => A.a₅
      | A.a₄ => A.a₆
      | A.a₅ => A.a₂
      | A.a₆ => A.a₁
      ,
    fun -- maps dots
      | D.d₁ => D.d₃
      | D.d₂ => D.d₄
      | D.d₃ => D.d₁
      | D.d₄ => D.d₅
      | D.d₅ => D.d₂
  )
  property := by⊢ (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toSrc =
    graph_R.toSrc ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1 ∧
  (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt =
    graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1
    constructorleft⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₄
        | A.a₃ => A.a₅
        | A.a₄ => A.a₆
        | A.a₅ => A.a₂
        | A.a₆ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₄
        | D.d₃ => D.d₁
        | D.d₄ => D.d₅
        | D.d₅ => D.d₂).2 ⊚
    graph_L.toSrc =
  graph_R.toSrc ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₄
        | A.a₃ => A.a₅
        | A.a₄ => A.a₆
        | A.a₅ => A.a₂
        | A.a₆ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₄
        | D.d₃ => D.d₁
        | D.d₄ => D.d₅
        | D.d₅ => D.d₂).1right⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₄
        | A.a₃ => A.a₅
        | A.a₄ => A.a₆
        | A.a₅ => A.a₂
        | A.a₆ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₄
        | D.d₃ => D.d₁
        | D.d₄ => D.d₅
        | D.d₅ => D.d₂).2 ⊚
    graph_L.toTgt =
  graph_R.toTgt ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₃
        | A.a₂ => A.a₄
        | A.a₃ => A.a₅
        | A.a₄ => A.a₆
        | A.a₅ => A.a₂
        | A.a₆ => A.a₁,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₄
        | D.d₃ => D.d₁
        | D.d₄ => D.d₅
        | D.d₅ => D.d₂).1
    all_goals
      funext xright.hx:graph_L.carrierA⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    x =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    x; cases xright.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₁ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₂ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₃ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₃right.h.a₄⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₄ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₄right.h.a₅⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₅ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₅right.h.a₆⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₆ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₆ <;>right.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₁ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₂ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₃ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₃right.h.a₄⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₄ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₄right.h.a₅⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₅ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₅right.h.a₆⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).2 ⊚
      graph_L.toTgt)
    A.a₆ =
  (graph_R.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₃
          | A.a₂ => A.a₄
          | A.a₃ => A.a₅
          | A.a₄ => A.a₆
          | A.a₅ => A.a₂
          | A.a₆ => A.a₁,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₄
          | D.d₃ => D.d₁
          | D.d₄ => D.d₅
          | D.d₅ => D.d₂).1)
    A.a₆ rflAll goals completed! 🐙
}

def finv : graph_R ⟶ graph_L := {
  val := (
    fun -- maps arrows
      | A.a₁ => A.a₆
      | A.a₂ => A.a₅
      | A.a₃ => A.a₁
      | A.a₄ => A.a₂
      | A.a₅ => A.a₃
      | A.a₆ => A.a₄,
    fun -- maps dots
      | D.d₁ => D.d₃
      | D.d₂ => D.d₅
      | D.d₃ => D.d₁
      | D.d₄ => D.d₂
      | D.d₅ => D.d₄
  )
  property := by⊢ (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toSrc =
    graph_L.toSrc ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1 ∧
  (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt =
    graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1
    constructorleft⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₆
        | A.a₂ => A.a₅
        | A.a₃ => A.a₁
        | A.a₄ => A.a₂
        | A.a₅ => A.a₃
        | A.a₆ => A.a₄,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₅
        | D.d₃ => D.d₁
        | D.d₄ => D.d₂
        | D.d₅ => D.d₄).2 ⊚
    graph_R.toSrc =
  graph_L.toSrc ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₆
        | A.a₂ => A.a₅
        | A.a₃ => A.a₁
        | A.a₄ => A.a₂
        | A.a₅ => A.a₃
        | A.a₆ => A.a₄,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₅
        | D.d₃ => D.d₁
        | D.d₄ => D.d₂
        | D.d₅ => D.d₄).1right⊢ (fun x ↦
        match x with
        | A.a₁ => A.a₆
        | A.a₂ => A.a₅
        | A.a₃ => A.a₁
        | A.a₄ => A.a₂
        | A.a₅ => A.a₃
        | A.a₆ => A.a₄,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₅
        | D.d₃ => D.d₁
        | D.d₄ => D.d₂
        | D.d₅ => D.d₄).2 ⊚
    graph_R.toTgt =
  graph_L.toTgt ⊚
    (fun x ↦
        match x with
        | A.a₁ => A.a₆
        | A.a₂ => A.a₅
        | A.a₃ => A.a₁
        | A.a₄ => A.a₂
        | A.a₅ => A.a₃
        | A.a₆ => A.a₄,
        fun x ↦
        match x with
        | D.d₁ => D.d₃
        | D.d₂ => D.d₅
        | D.d₃ => D.d₁
        | D.d₄ => D.d₂
        | D.d₅ => D.d₄).1
    all_goals
      funext xright.hx:graph_R.carrierA⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    x =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    x; cases xright.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₁ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₂ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₃ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₃right.h.a₄⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₄ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₄right.h.a₅⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₅ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₅right.h.a₆⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₆ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₆ <;>right.h.a₁⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₁ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₁right.h.a₂⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₂ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₂right.h.a₃⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₃ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₃right.h.a₄⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₄ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₄right.h.a₅⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₅ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₅right.h.a₆⊢ ((fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).2 ⊚
      graph_R.toTgt)
    A.a₆ =
  (graph_L.toTgt ⊚
      (fun x ↦
          match x with
          | A.a₁ => A.a₆
          | A.a₂ => A.a₅
          | A.a₃ => A.a₁
          | A.a₄ => A.a₂
          | A.a₅ => A.a₃
          | A.a₆ => A.a₄,
          fun x ↦
          match x with
          | D.d₁ => D.d₃
          | D.d₂ => D.d₅
          | D.d₃ => D.d₁
          | D.d₄ => D.d₂
          | D.d₅ => D.d₄).1)
    A.a₆ rflAll goals completed! 🐙
}

example : graph_L ≅ graph_R := {
  hom := f,
  inv := finv,
  hom_inv_id := by⊢ finv ⊚ f = 𝟙 graph_L
    have h₁ : (finv.val.1 ⊚ f.val.1 = 𝟙 graph_L.carrierA) ∧
        (finv.val.2 ⊚ f.val.2 = 𝟙 graph_L.carrierD) := by⊢ finv ⊚ f = 𝟙 graph_L
      constructorleft⊢ (↑finv).1 ⊚ (↑f).1 = 𝟙 graph_L.carrierAright⊢ (↑finv).2 ⊚ (↑f).2 = 𝟙 graph_L.carrierD <;>left⊢ (↑finv).1 ⊚ (↑f).1 = 𝟙 graph_L.carrierAright⊢ (↑finv).2 ⊚ (↑f).2 = 𝟙 graph_L.carrierD (funext xright.hx:graph_L.carrierD⊢ ((↑finv).2 ⊚ (↑f).2) x = 𝟙 graph_L.carrierD x; cases xright.h.d₁⊢ ((↑finv).2 ⊚ (↑f).2) D.d₁ = 𝟙 graph_L.carrierD D.d₁right.h.d₂⊢ ((↑finv).2 ⊚ (↑f).2) D.d₂ = 𝟙 graph_L.carrierD D.d₂right.h.d₃⊢ ((↑finv).2 ⊚ (↑f).2) D.d₃ = 𝟙 graph_L.carrierD D.d₃right.h.d₄⊢ ((↑finv).2 ⊚ (↑f).2) D.d₄ = 𝟙 graph_L.carrierD D.d₄right.h.d₅⊢ ((↑finv).2 ⊚ (↑f).2) D.d₅ = 𝟙 graph_L.carrierD D.d₅ <;>right.h.d₁⊢ ((↑finv).2 ⊚ (↑f).2) D.d₁ = 𝟙 graph_L.carrierD D.d₁right.h.d₂⊢ ((↑finv).2 ⊚ (↑f).2) D.d₂ = 𝟙 graph_L.carrierD D.d₂right.h.d₃⊢ ((↑finv).2 ⊚ (↑f).2) D.d₃ = 𝟙 graph_L.carrierD D.d₃right.h.d₄⊢ ((↑finv).2 ⊚ (↑f).2) D.d₄ = 𝟙 graph_L.carrierD D.d₄right.h.d₅⊢ ((↑finv).2 ⊚ (↑f).2) D.d₅ = 𝟙 graph_L.carrierD D.d₅ rflAll goals completed! 🐙)
    have h₂ : (finv.val.1 ⊚ f.val.1, finv.val.2 ⊚ f.val.2) =
        (𝟙 graph_L.carrierA, 𝟙 graph_L.carrierD) := by⊢ finv ⊚ f = 𝟙 graph_L
      rw [h₁.1, h₁.2]All goals completed! 🐙
    exact Subtype.ext h₂All goals completed! 🐙,
  inv_hom_id := by⊢ f ⊚ finv = 𝟙 graph_R
    have h₁ : (f.val.1 ⊚ finv.val.1 = 𝟙 graph_R.carrierA) ∧
        (f.val.2 ⊚ finv.val.2 = 𝟙 graph_R.carrierD) := by⊢ f ⊚ finv = 𝟙 graph_R
      constructorleft⊢ (↑f).1 ⊚ (↑finv).1 = 𝟙 graph_R.carrierAright⊢ (↑f).2 ⊚ (↑finv).2 = 𝟙 graph_R.carrierD <;>left⊢ (↑f).1 ⊚ (↑finv).1 = 𝟙 graph_R.carrierAright⊢ (↑f).2 ⊚ (↑finv).2 = 𝟙 graph_R.carrierD (funext xright.hx:graph_R.carrierD⊢ ((↑f).2 ⊚ (↑finv).2) x = 𝟙 graph_R.carrierD x; cases xright.h.d₁⊢ ((↑f).2 ⊚ (↑finv).2) D.d₁ = 𝟙 graph_R.carrierD D.d₁right.h.d₂⊢ ((↑f).2 ⊚ (↑finv).2) D.d₂ = 𝟙 graph_R.carrierD D.d₂right.h.d₃⊢ ((↑f).2 ⊚ (↑finv).2) D.d₃ = 𝟙 graph_R.carrierD D.d₃right.h.d₄⊢ ((↑f).2 ⊚ (↑finv).2) D.d₄ = 𝟙 graph_R.carrierD D.d₄right.h.d₅⊢ ((↑f).2 ⊚ (↑finv).2) D.d₅ = 𝟙 graph_R.carrierD D.d₅ <;>right.h.d₁⊢ ((↑f).2 ⊚ (↑finv).2) D.d₁ = 𝟙 graph_R.carrierD D.d₁right.h.d₂⊢ ((↑f).2 ⊚ (↑finv).2) D.d₂ = 𝟙 graph_R.carrierD D.d₂right.h.d₃⊢ ((↑f).2 ⊚ (↑finv).2) D.d₃ = 𝟙 graph_R.carrierD D.d₃right.h.d₄⊢ ((↑f).2 ⊚ (↑finv).2) D.d₄ = 𝟙 graph_R.carrierD D.d₄right.h.d₅⊢ ((↑f).2 ⊚ (↑finv).2) D.d₅ = 𝟙 graph_R.carrierD D.d₅ rflAll goals completed! 🐙)
    have h₂ : (f.val.1 ⊚ finv.val.1, f.val.2 ⊚ finv.val.2) =
        (𝟙 graph_R.carrierA, 𝟙 graph_R.carrierD) := by⊢ f ⊚ finv = 𝟙 graph_R
      rw [h₁.1, h₁.2]All goals completed! 🐙
    exact Subtype.ext h₂All goals completed! 🐙
}

Exercise 8 (p. 160)

(Impossible journeys) J is the graph

inductive A
  | a₁ | a₂ | a₃

abbrev D := Fin 2

def J : IrreflexiveGraph := {
  carrierA := A
  carrierD := D
  toSrc := fun
    | A.a₁ => 0
    | A.a₂ => 1
    | A.a₃ => 1
  toTgt := fun
    | A.a₁ => 0
    | A.a₂ => 0
    | A.a₃ => 1
}

G is any graph, and b and e are dots of G.

variable (G : IrreflexiveGraph) (b e : G.carrierD)

(a) Suppose that {G \xrightarrow{f} J} is a map of graphs with {fb = 0} and {fe = 1}. Show that there is no path in G that begins at b and ends at e.

(b) Conversely, suppose that there is no path in G that begins at b and ends at e. Show that there is a map {G \xrightarrow{f} J} with {fb = 0} and {fe = 1}.

Solution: Exercise 8

TODO Exercise 11.8