case intro.intro
α : Type ?u.54766
β : Type ?u.54769
γ : Type ?u.54772
f✝ : α ↪ β
s✝ s : Finset α
t : α → Finset β
f : β ↪ γ
h : Set.PairwiseDisjoint (↑s) t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
xa : β
hfa : xa ∈ t a
hxa : ↑f xa ∈ (fun a => map f (t a)) a
hxb : ↑f xa ∈ (fun a => map f (t a)) b
⊢ False
α : Type ?u.54766
β : Type ?u.54769
γ : Type ?u.54772
f✝ : α ↪ β
s✝ s : Finset α
t : α → Finset β
f : β ↪ γ
h : Set.PairwiseDisjoint (↑s) t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
x : γ
hxa : x ∈ (fun a => map f (t a)) a
hxb : x ∈ (fun a => map f (t a)) b
⊢ False
obtain ⟨xa, hfa, rfl⟩ := mem_map.mp hxa
case intro.intro.intro.intro
α : Type ?u.54766
β : Type ?u.54769
γ : Type ?u.54772
f✝ : α ↪ β
s✝ s : Finset α
t : α → Finset β
f : β ↪ γ
h : Set.PairwiseDisjoint (↑s) t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
xa : β
hfa : xa ∈ t a
hxa : ↑f xa ∈ (fun a => map f (t a)) a
hxb : ↑f xa ∈ (fun a => map f (t a)) b
xb : β
hfb : xb ∈ t b
hfab : ↑f xb = ↑f xa
⊢ False
case intro.intro
α : Type ?u.54766
β : Type ?u.54769
γ : Type ?u.54772
f✝ : α ↪ β
s✝ s : Finset α
t : α → Finset β
f : β ↪ γ
h : Set.PairwiseDisjoint (↑s) t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
xa : β
hfa : xa ∈ t a
hxa : ↑f xa ∈ (fun a => map f (t a)) a
hxb : ↑f xa ∈ (fun a => map f (t a)) b
⊢ False
obtain ⟨xb, hfb, hfab⟩ := mem_map.mp hxb
case intro.intro.intro.intro
α : Type ?u.54766
β : Type ?u.54769
γ : Type ?u.54772
f✝ : α ↪ β
s✝ s : Finset α
t : α → Finset β
f : β ↪ γ
h : Set.PairwiseDisjoint (↑s) t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
xb : β
hfb : xb ∈ t b
hfa : xb ∈ t a
hxa : ↑f xb ∈ (fun a => map f (t a)) a
hxb : ↑f xb ∈ (fun a => map f (t a)) b
hfab : ↑f xb = ↑f xb
⊢ False
case intro.intro.intro.intro
α : Type ?u.54766
β : Type ?u.54769
γ : Type ?u.54772
f✝ : α ↪ β
s✝ s : Finset α
t : α → Finset β
f : β ↪ γ
h : Set.PairwiseDisjoint (↑s) t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
xa : β
hfa : xa ∈ t a
hxa : ↑f xa ∈ (fun a => map f (t a)) a
hxb : ↑f xa ∈ (fun a => map f (t a)) b
xb : β
hfb : xb ∈ t b
hfab : ↑f xb = ↑f xa
⊢ False
obtain rfl := f.injective hfab
no goals
case intro.intro.intro.intro
α : Type ?u.54766
β : Type ?u.54769
γ : Type ?u.54772
f✝ : α ↪ β
s✝ s : Finset α
t : α → Finset β
f : β ↪ γ
h : Set.PairwiseDisjoint (↑s) t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
xb : β
hfb : xb ∈ t b
hfa : xb ∈ t a
hxa : ↑f xb ∈ (fun a => map f (t a)) a
hxb : ↑f xb ∈ (fun a => map f (t a)) b
hfab : ↑f xb = ↑f xb
⊢ False
exact disjoint_left.mp (h ha hb hab) hfa hfb