case intro.intro
α : Type u_2
β : Type ?u.36838
γ : Type ?u.36841
ι : Type u_1
ι' : Type ?u.36847
r p q : α → α → Prop
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s t : Set ι
f g✝ : ι → α
g : ↑s → ι
hg : ∀ (i : ↑s), f (g i) ≤ f ↑i
ht : PairwiseDisjoint s f
x y : ↑s
hxy : g x ≠ g y
⊢ (Disjoint on f) (g x) (g y)
α : Type u_2
β : Type ?u.36838
γ : Type ?u.36841
ι : Type u_1
ι' : Type ?u.36847
r p q : α → α → Prop
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s t : Set ι
f g✝ : ι → α
g : ↑s → ι
hg : ∀ (i : ↑s), f (g i) ≤ f ↑i
ht : PairwiseDisjoint s f
⊢ PairwiseDisjoint (Set.range g) f
rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ hxy
no goals
case intro.intro
α : Type u_2
β : Type ?u.36838
γ : Type ?u.36841
ι : Type u_1
ι' : Type ?u.36847
r p q : α → α → Prop
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s t : Set ι
f g✝ : ι → α
g : ↑s → ι
hg : ∀ (i : ↑s), f (g i) ≤ f ↑i
ht : PairwiseDisjoint s f
x y : ↑s
hxy : g x ≠ g y
⊢ (Disjoint on f) (g x) (g y)
exact ((ht x.2 y.2) fun h => hxy <| congr_arg g <| Subtype.ext h).mono (hg x) (hg y)