feat(order/minimal): Image of maximals under a rel_embedding

[erdOne]

---

[tb65536]

You can take advantage of existing variables, and it might even make sense to move some more of these to the variables line at the top of the file.

[tb65536]

I feel like this hypothesis ought to be h, and the hypothesis in the proof ought to be h' or h₁ or hf.

Suggested change

	(t : set α) (h₁ : ∀ x y ∈ t, r x y ↔ s (f x) (f y)) :
	(t : set α) (h : ∀ x y ∈ t, r x y ↔ s (f x) (f y)) :

[tb65536]

Here's a minor golf, up to you.

Suggested change

	rintros _ ⟨y, hy, rfl⟩ e,
	exact (h₁ _ hy _ hx.1).mp (hx.2 hy ((h₁ _ hx.1 _ hy).mpr e)) },
	rintros _ ⟨y, hy, rfl⟩,
	exact (h₁ _ hy _ hx.1).mp ∘ hx.2 hy ∘ (h₁ _ hx.1 _ hy).mpr },

[tb65536]

Here's a golf.

Suggested change

	refine ⟨x, ⟨hx, _⟩, rfl⟩,
	rintros y hy e,
	exact (h₁ _ hy _ hx).mpr (h ⟨y, hy, rfl⟩ ((h₁ _ hx _ hy).mp e)) }
	exact ⟨x, ⟨hx, λ y hy, (h₁ y hy x hx).mpr ∘ h ⟨y, hy, rfl⟩ ∘ (h₁ x hx y hy).mp⟩, rfl⟩ }