α : Type ?u.492925
β : Type ?u.492928
γ : Type ?u.492931
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')
α : Type ?u.492925
β : Type ?u.492928
γ : Type ?u.492931
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ (_root_.Disjoint on fun a => filter (fun c => f c = a) s) x' y'
simp_rw [disjoint_left, mem_filter]
case intro.intro
α : Type ?u.492925
β : Type ?u.492928
γ : Type ?u.492931
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
i : α
left✝¹ : i ∈ s
hx : f i ∈ ↑t
left✝ : i ∈ s
hy : f i ∈ ↑t
hne : f i ≠ f i
⊢ False
α : Type ?u.492925
β : Type ?u.492928
γ : Type ?u.492931
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')
rintro i ⟨_, rfl⟩ ⟨_, rfl⟩
no goals
case intro.intro
α : Type ?u.492925
β : Type ?u.492928
γ : Type ?u.492931
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
i : α
left✝¹ : i ∈ s
hx : f i ∈ ↑t
left✝ : i ∈ s
hy : f i ∈ ↑t
hne : f i ≠ f i
⊢ False
exact hne rfl
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.492931
s✝ s₁ s₂ : Finset α
t✝ t₁ t₂ : α → Finset β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
h : ∀ (x : α), x ∈ s → f x ∈ t
b : α
⊢ b ∈
      disjiUnion t (fun a => filter (fun c => f c = a) s)
        (_ :
          ∀ (x' : β),
            x' ∈ ↑t → ∀ (y' : β), y' ∈ ↑t → x' ≠ y' → (_root_.Disjoint on fun a => filter (fun c => f c = a) s) x' y') ↔
    b ∈ s
simpa using h b