case intro.intro.intro.intro
α : Type u_1
β : Type ?u.36078
γ : Type ?u.36081
ι : Type u_2
ι' : Type ?u.36087
r p q : α → α → Prop
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s t : Set ι
f g✝ : ι → α
hs : PairwiseDisjoint s f
g : ι → ι
hg : f ∘ g ≤ f
a : ι
ha : a ∈ s
b : ι
hb : b ∈ s
h : g a ≠ g b
⊢ (Disjoint on f) (g a) (g b)
α : Type u_1
β : Type ?u.36078
γ : Type ?u.36081
ι : Type u_2
ι' : Type ?u.36087
r p q : α → α → Prop
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s t : Set ι
f g✝ : ι → α
hs : PairwiseDisjoint s f
g : ι → ι
hg : f ∘ g ≤ f
⊢ PairwiseDisjoint (g '' s) f
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ h
no goals
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.36078
γ : Type ?u.36081
ι : Type u_2
ι' : Type ?u.36087
r p q : α → α → Prop
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s t : Set ι
f g✝ : ι → α
hs : PairwiseDisjoint s f
g : ι → ι
hg : f ∘ g ≤ f
a : ι
ha : a ∈ s
b : ι
hb : b ∈ s
h : g a ≠ g b
⊢ (Disjoint on f) (g a) (g b)
exact (hs ha hb <| ne_of_apply_ne _ h).mono (hg a) (hg b)