no goals
α : Type u_1
β : Type ?u.133754
γ : Type ?u.133757
δ : Type ?u.133760
σ : Type ?u.133763
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable β
inst✝³ : Primcodable γ
inst✝² : Primcodable δ
inst✝¹ : Primcodable σ
inst✝ : DecidableEq α
a : ℕ × ℕ
⊢ (fun x x_1 => x ≤ x_1) a.fst a.snd ∧ (fun x x_1 => x ≤ x_1) a.snd a.fst ↔ (fun a b => a = b) a.fst a.snd
simp [le_antisymm_iff]