α : Type u
lt : α → α → Prop
inst✝¹ : IsTrichotomous α lt
inst✝ : IsIrrefl α lt
a b : α
hab : a = b
⊢ ¬lt b b ∧ ¬lt b b
α : Type u
lt : α → α → Prop
inst✝¹ : IsTrichotomous α lt
inst✝ : IsIrrefl α lt
a b : α
hab : a = b
⊢ ¬lt a b ∧ ¬lt b a
rw [hab]
no goals
α : Type u
lt : α → α → Prop
inst✝¹ : IsTrichotomous α lt
inst✝ : IsIrrefl α lt
a b : α
hab : a = b
⊢ ¬lt b b ∧ ¬lt b b
exact ⟨irrefl_of lt b, irrefl_of lt b⟩