α : Type u_1
β : Type u_2
γ : Type ?u.31419
f✝ : α ↪ β
s✝ s t : Finset α
f : α ↪ β
⊢ (∀ (a : β) (x : α), x ∈ s → ↑f x = a → ∀ (b : β) (x : α), x ∈ t → ↑f x = b → a ≠ b) ↔
    ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b
α : Type u_1
β : Type u_2
γ : Type ?u.31419
f✝ : α ↪ β
s✝ s t : Finset α
f : α ↪ β
⊢ _root_.Disjoint (map f s) (map f t) ↔ _root_.Disjoint s t
simp only [disjoint_iff_ne, mem_map, exists_prop, exists_imp, and_imp]
α : Type u_1
β : Type u_2
γ : Type ?u.31419
f✝ : α ↪ β
s✝ s t : Finset α
f : α ↪ β
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b) →
    ∀ (a : β) (x : α), x ∈ s → ↑f x = a → ∀ (b : β) (x : α), x ∈ t → ↑f x = b → a ≠ b
α : Type u_1
β : Type u_2
γ : Type ?u.31419
f✝ : α ↪ β
s✝ s t : Finset α
f : α ↪ β
⊢ (∀ (a : β) (x : α), x ∈ s → ↑f x = a → ∀ (b : β) (x : α), x ∈ t → ↑f x = b → a ≠ b) ↔
    ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b
refine' ⟨fun h a ha b hb hab => h _ _ ha rfl _ _ hb rfl <| congr_arg _ hab, _⟩
α : Type u_1
β : Type u_2
γ : Type ?u.31419
f✝ : α ↪ β
s✝ s t : Finset α
f : α ↪ β
h : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ↑f a ≠ ↑f b
α : Type u_1
β : Type u_2
γ : Type ?u.31419
f✝ : α ↪ β
s✝ s t : Finset α
f : α ↪ β
⊢ (∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b) →
    ∀ (a : β) (x : α), x ∈ s → ↑f x = a → ∀ (b : β) (x : α), x ∈ t → ↑f x = b → a ≠ b
rintro h _ a ha rfl _ b hb rfl
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.31419
f✝ : α ↪ β
s✝ s t : Finset α
f : α ↪ β
h : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b
a : α
ha : a ∈ s
b : α
hb : b ∈ t
⊢ ↑f a ≠ ↑f b
exact f.injective.ne (h _ ha _ hb)