ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b
have h := LinearOrder.compare_eq_compareOfLessAndEq (f a) (f b)
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b
simp only [h, compareOfLessAndEq]
case inr.inl.inr.inr
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

case inr.inr.inr.inl
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
split_ifs <;> try (first | rfl | contradiction)
no goals
case inr.inr.inr.inr
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt
(first | rfl | contradiction)
no goals
case inr.inr.inr.inr
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt
first | rfl | contradiction
no goals
case inr.inr.inr.inr
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ Ordering.gt = Ordering.gt
rfl
case inr.inr.inr.inl
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
case inr.inr.inr.inl
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
contradiction
case inr.inl.inr.inr
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
this : ¬f a = f b
⊢ False
case inr.inl.inr.inr
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
have : ¬ f a = f b := by rename_i h; exact inj.ne h
no goals
case inr.inl.inr.inr
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
this : ¬f a = f b
⊢ False
contradiction
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h✝³ : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : ¬a < b
h : ¬a = b
⊢ ¬f a = f b
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ ¬f a = f b
rename_i h
no goals
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h✝³ : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : ¬a < b
h : ¬a = b
⊢ ¬f a = f b
exact inj.ne h
case inr.inr.inr.inl
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
this : f a = f b
⊢ False
case inr.inr.inr.inl
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
have : f a = f b := by rename_i h; exact congrArg f h
no goals
case inr.inr.inr.inl
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
this : f a = f b
⊢ False
contradiction
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h✝³ : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : ¬a < b
h : a = b
⊢ f a = f b
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : ¬f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ f a = f b
rename_i h
no goals
ι : Type ?u.93186
α : Type u
β : Type v
γ : Type w
π : ι → Type ?u.93197
r : α → α → Prop
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h✝³ : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : ¬a < b
h : a = b
⊢ f a = f b
exact congrArg f h