no goals
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
⊢ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y ∧ f x = f y
classical
  by_contra' hz
  refine' hc.not_le (card_le_card_of_inj_on f hf _)
  intro x hx y hy
  contrapose
  exact hz x hx y hy
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
⊢ False
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
⊢ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y ∧ f x = f y
by_contra' hz
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
⊢ ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
⊢ False
refine' hc.not_le (card_le_card_of_inj_on f hf _)
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ f x = f y → x = y
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
⊢ ∀ (a₁ : α), a₁ ∈ s → ∀ (a₂ : α), a₂ ∈ s → f a₁ = f a₂ → a₁ = a₂
intro x hx y hy
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ¬x = y → ¬f x = f y
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ f x = f y → x = y
contrapose
no goals
α : Type u_2
β : Type u_1
s t✝ : Finset α
f✝ : α → β
n : ℕ
t : Finset β
hc : card t < card s
f : α → β
hf : ∀ (a : α), a ∈ s → f a ∈ t
hz : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → f x ≠ f y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ¬x = y → ¬f x = f y
exact hz x hx y hy