Examples depending on precisely one of propext/choice/sound?

Stream: new members

[Louis Cabarion]

For educational purposes, I am looking for three simple and pedagogically effective theorems, each relying only on precisely one of the following axioms respectively: [propext], [Classical.choice] and [Quot.sound].

What would be suitable candidates that are accessible to an undergraduate audience? The simpler, the better.

Something like this:

theorem only_propext […] : […] := by […]
#print axioms only_propext
-- 'only_propext' depends on axioms: [propext]

theorem only_choice […] : […] := by […]
#print axioms only_choice
-- 'only_choice' depends on axioms: [Classical.choice]

theorem only_quot_sound […] : […] := by […]
#print axioms only_quot_sound
-- 'only_quot_sound' depends on axioms: [Quot.sound]

[Aaron Liu]

Here's what I came up with, what do you think?

import Mathlib

recall Quotient.exact {α : Sort u} {s : Setoid α} {a b : α} : ⟦a⟧ = ⟦b⟧ → a ≈ b
#print axioms Quotient.exact
-- 'Quotient.exact' depends on axioms: [propext]

recall Function.surjInv {α : Sort u} {β : Sort v} {f : α → β} (h : Function.Surjective f) (b : β) : α
#print axioms Function.surjInv
-- 'Function.surjInv' depends on axioms: [Classical.choice]

recall funext {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : ∀ (x : α), f x = g x) : f = g
#print axioms funext
-- 'funext' depends on axioms: [Quot.sound]

[Louis Cabarion]

Thanks @Aaron Liu those are three spot-on examples. Great finds, as always!

TIL about recall — perfect for examples like these.