case intro.intro
α : Type u_1
ι : Type ?u.1017
ι' : Type ?u.1020
a b : α
h : {a} ≠ {b}
⊢ (Disjoint on id) {a} {b}
α : Type u_1
ι : Type ?u.1017
ι' : Type ?u.1020
⊢ Set.PairwiseDisjoint (Set.range singleton) id
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h
no goals
case intro.intro
α : Type u_1
ι : Type ?u.1017
ι' : Type ?u.1020
a b : α
h : {a} ≠ {b}
⊢ (Disjoint on id) {a} {b}
exact disjoint_singleton.2 (ne_of_apply_ne _ h)