-- Mathlib/SetTheory/Cardinal/SchroederBernstein.lean
theorem min_injective [I : Nonempty ι] : ∃ i, Nonempty (∀ j, β i ↪ β j) :=
  let ⟨s, hs⟩ := show ∃ s, Maximal (· ∈ sets β) s by
    refine zorn_subset _ fun c hc hcc ↦
      ⟨⋃₀ c, fun i x ⟨p, hpc, hxp⟩ y ⟨q, hqc, hyq⟩ hi ↦ ?_, fun _ ↦ subset_sUnion_of_mem⟩
    exact (hcc.total hpc hqc).elim (fun h ↦ hc hqc i (h hxp) hyq hi)
      fun h ↦ hc hpc i hxp (h hyq) hi
  let ⟨i, e⟩ :=
    show ∃ i, Surjective fun x : s => x.val i from
      Classical.by_contradiction fun h =>
        have h : ∀ i, ∃ y, ∀ x ∈ s, (x : ∀ i, β i) i ≠ y

Proof state:
ι : Type u
β : ι → Type v
I : Nonempty ι
c : Set (Set ((i : ι) → β i))
hc : c ⊆ Function.Embedding.sets β
hcc : IsChain (fun x1 x2 => x1 ⊆ x2) c
i : ι
x : (i : ι) → β i
x✝¹ : x ∈ ⋃₀ c
y : (i : ι) → β i
x✝ : y ∈ ⋃₀ c
hi : (fun x => x i) x = (fun x => x i) y
p : Set ((i : ι) → β i)
hpc : p ∈ c
hxp : x ∈ p
q : Set ((i : ι) → β i)
hqc : q ∈ c
hyq : y ∈ q
⊢ x = y

Tactic:
exact (hcc.total hpc hqc).elim (fun h ↦ hc hqc i (h hxp) hyq hi)
  fun h ↦ hc hpc i hxp (h hyq) hi

Result:
no goals

Proof state:
case inl.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y = f
⊢ (fun x => x i) x = (fun x => x i) y → x = y

Tactic:
simp [hx, hy]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h : ¬∃ i, Surjective fun x => ↑x i
⊢ ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y

Tactic:
simpa [Surjective] using h

Result:
no goals

Proof state:
case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ (fun x => x i) x = (fun x => x i) y → x = y

Tactic:
subst x

Result:
case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
y : (i : ι) → β i
hy : y ∈ s
⊢ (fun x => x i) f = (fun x => x i) y → f = y

Proof state:
ι : Type u
β : ι → Type v
I : Nonempty ι
⊢ ∃ s, Maximal (fun x => x ∈ Function.Embedding.sets β) s

Tactic:
refine zorn_subset _ fun c hc hcc ↦
  ⟨⋃₀ c, fun i x ⟨p, hpc, hxp⟩ y ⟨q, hqc, hyq⟩ hi ↦ ?_, fun _ ↦ subset_sUnion_of_mem⟩

Result:
ι : Type u
β : ι → Type v
I : Nonempty ι
c : Set (Set ((i : ι) → β i))
hc : c ⊆ Function.Embedding.sets β
hcc : IsChain (fun x1 x2 => x1 ⊆ x2) c
i : ι
x : (i : ι) → β i
x✝¹ : x ∈ ⋃₀ c
y : (i : ι) → β i
x✝ : y ∈ ⋃₀ c
hi : (fun x => x i) x = (fun x => x i) y
p : Set ((i : ι) → β i)
hpc : p ∈ c
hxp : x ∈ p
q : Set ((i : ι) → β i)
hqc : q ∈ c
hyq : y ∈ q
⊢ x = y

Proof state:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x : (i : ι) → β i
hx : x ∈ insert f s
y : (i : ι) → β i
hy : y ∈ insert f s
⊢ (fun x => x i) x = (fun x => x i) y → x = y

Tactic:
rcases hx with hx | hx <;> rcases hy with hy | hy

Result:
case inl.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y = f
⊢ (fun x => x i) x = (fun x => x i) y → x = y

case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ (fun x => x i) x = (fun x => x i) y → x = y

case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ (fun x => x i) x = (fun x => x i) y → x = y

case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ (fun x => x i) x = (fun x => x i) y → x = y

Proof state:
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ (fun x => x i) x = (fun x => x i) y → x = y

Tactic:
subst y

Result:
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x : (i : ι) → β i
hx : x ∈ s
⊢ (fun x => x i) x = (fun x => x i) f → x = f

Proof state:
case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ (fun x => x i) x = (fun x => x i) y → x = y

Tactic:
exact hs.prop i hx hy

Result:
no goals

Proof state:
case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
y : (i : ι) → β i
hy : y ∈ s
⊢ (fun x => x i) f = (fun x => x i) y → f = y

Tactic:
exact fun e => (hf i y hy e.symm).elim

Result:
no goals

Proof state:
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x => x ∈ Function.Embedding.sets β) s
h✝ : ¬∃ i, Surjective fun x => ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x : (i : ι) → β i
hx : x ∈ s
⊢ (fun x => x i) x = (fun x => x i) f → x = f

Tactic:
exact fun e => (hf i x hx e).elim

Result:
no goals