case intro.intro
α : Type ?u.39435
β : Type ?u.39438
γ : Type ?u.39441
ι : Type u_1
ι' : Type ?u.39447
r p q : α → α → Prop
a b : ι
h : {a} ≠ {b}
⊢ (Disjoint on id) {a} {b}
α : Type ?u.39435
β : Type ?u.39438
γ : Type ?u.39441
ι : Type u_1
ι' : Type ?u.39447
r p q : α → α → Prop
⊢ PairwiseDisjoint (range singleton) id
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h
no goals
case intro.intro
α : Type ?u.39435
β : Type ?u.39438
γ : Type ?u.39441
ι : Type u_1
ι' : Type ?u.39447
r p q : α → α → Prop
a b : ι
h : {a} ≠ {b}
⊢ (Disjoint on id) {a} {b}
exact disjoint_singleton.2 (ne_of_apply_ne _ h)