ι : Type ?u.16131
α : Type u
β : Type v
γ : Type w
δ : Type ?u.16140
π : ι → Type ?u.16145
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
⊢ x = y
ι : Type ?u.16131
α : Type u
β : Type v
γ : Type w
δ : Type ?u.16140
π : ι → Type ?u.16145
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
⊢ Injective f
intro x y hf
case inl
ι : Type ?u.16131
α : Type u
β : Type v
γ : Type w
δ : Type ?u.16140
π : ι → Type ?u.16145
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : x < y
⊢ x = y

case inr.inl
ι : Type ?u.16131
α : Type u
β : Type v
γ : Type w
δ : Type ?u.16140
π : ι → Type ?u.16145
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x : α
hf : f x = f x
⊢ x = x

case inr.inr
ι : Type ?u.16131
α : Type u
β : Type v
γ : Type w
δ : Type ?u.16140
π : ι → Type ?u.16145
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : y < x
⊢ x = y
ι : Type ?u.16131
α : Type u
β : Type v
γ : Type w
δ : Type ?u.16140
π : ι → Type ?u.16145
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
⊢ x = y
rcases lt_trichotomy x y with (hxy | rfl | hxy)
no goals
case inl
ι : Type ?u.16131
α : Type u
β : Type v
γ : Type w
δ : Type ?u.16140
π : ι → Type ?u.16145
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : x < y
⊢ x = y
exact absurd hf <| h _ _ hxy
no goals
case inr.inl
ι : Type ?u.16131
α : Type u
β : Type v
γ : Type w
δ : Type ?u.16140
π : ι → Type ?u.16145
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x : α
hf : f x = f x
⊢ x = x
rfl
no goals
case inr.inr
ι : Type ?u.16131
α : Type u
β : Type v
γ : Type w
δ : Type ?u.16140
π : ι → Type ?u.16145
r : α → α → Prop
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
x y : α
hf : f x = f y
hxy : y < x
⊢ x = y
exact absurd hf.symm <| h _ _ hxy