awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
a1 : α
h1 : a1 ∈ s
a2 : α
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
rw : j (i a1 h1) ⋯ = j (i a2 h2) ⋯
⊢ a1 = a2

Tactic:
rw [← left_inv a1 h1, ← left_inv a2 h2]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
j : (a : β) → a ∈ t → α
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a
a1 : α
h1 : a1 ∈ s
a2 : α
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ j (i a1 h1) ⋯ = j (i a2 h2) ⋯

Tactic:
simp only [eq]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : α → β
hi : Set.MapsTo i (↑s : Set α) (↑t : Set β)
i_inj : Set.InjOn i (↑s : Set α)
i_surj : Set.SurjOn i (↑s : Set α) (↑t : Set β)
⊢ ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), (fun (a : α) (x : a ∈ s) ↦ i a) a ha = b

Tactic:
simpa using i_surj
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : α → β
j : β → α
hi : Set.MapsTo i (↑s : Set α) (↑t : Set β)
hj : Set.MapsTo j (↑t : Set β) (↑s : Set α)
left_inv : Set.LeftInvOn j i (↑s : Set α)
right_inv : Set.RightInvOn j i (↑t : Set β)
⊢ #s = #t

Tactic:
card_bij' (fun a _ ↦ i a) (fun b _ ↦ j b) hi hj left_inv right_inv

Premises used: Finset.card_bij'
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ Membership.mem (α := β) t ((e : (a : α) → β) i : β)
⊢ #s = #t

Tactic:
card_nbij' e e.symm ?_ ?_ ?_ ?_

Premises used: Finset.card_nbij', Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ Membership.mem (α := β) t ((e : (a : α) → β) i : β)
refine_1 : Set.MapsTo (⇑e : (a : α) → β) (↑s : Set α) (↑t : Set β)
refine_2 : Set.MapsTo (⇑e.symm : (a : β) → α) (↑t : Set β) (↑s : Set α)
refine_3 : Set.LeftInvOn.{u_1, u_2} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β) (↑s : Set α)
refine_4 : Set.RightInvOn.{u_1, u_2} (α := α) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β) (↑t : Set β)
⊢ #s = #t

Tactic:
refine card_nbij' e e.symm ?_ ?_ ?_ ?_

Premises used: Finset.card_nbij', Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ Membership.mem (α := β) t ((e : (a : α) → β) i : β)
⊢ Set.MapsTo (⇑e : (a : α) → β) (↑s : Set α) (↑t : Set β)

Tactic:
simp [hst, Set.MapsTo, Set.LeftInvOn, Set.RightInvOn]

Premises used: Set.LeftInvOn, Set.RightInvOn, Set.MapsTo
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ Membership.mem (α := β) t ((e : (a : α) → β) i : β)
⊢ Set.MapsTo (⇑e.symm : (a : β) → α) (↑t : Set β) (↑s : Set α)

Tactic:
simp [hst, Set.MapsTo, Set.LeftInvOn, Set.RightInvOn]

Premises used: Set.LeftInvOn, Set.RightInvOn, Set.MapsTo
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ Membership.mem (α := β) t ((e : (a : α) → β) i : β)
⊢ Set.LeftInvOn.{u_1, u_2} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β) (↑s : Set α)

Tactic:
simp [hst, Set.MapsTo, Set.LeftInvOn, Set.RightInvOn]

Premises used: Set.LeftInvOn, Set.RightInvOn, Set.MapsTo
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ Membership.mem (α := β) t ((e : (a : α) → β) i : β)
⊢ Set.RightInvOn.{u_1, u_2} (α := α) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β) (↑t : Set β)

Tactic:
simp [hst, Set.MapsTo, Set.LeftInvOn, Set.RightInvOn]

Premises used: Set.LeftInvOn, Set.RightInvOn, Set.MapsTo
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α → β
he : Bijective e
hst : ∀ (i : α), i ∈ s ↔ e i ∈ t
⊢ #s = #t

Tactic:
card_equiv (.ofBijective e he) hst

Premises used: Finset.card_equiv, Equiv.ofBijective
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α → β
he : Set.BijOn e (↑s : Set α) (↑t : Set β)
⊢ #s = #t

Tactic:
card_nbij e he.mapsTo he.injOn he.surjOn

Premises used: Set.BijOn.injOn, Set.BijOn.surjOn, Set.BijOn.mapsTo, Finset.card_nbij
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
f_inj : Set.InjOn f (↑s : Set α)
⊢ #s = #(image f s)

Tactic:
(card_image_of_injOn f_inj).symm

Premises used: Finset.card_image_of_injOn, Eq.symm
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
f_inj : Set.InjOn f (↑s : Set α)
⊢ #(image f s) ≤ #t

Tactic:
card_le_card <| image_subset_iff.2 hf

Premises used: Iff.mpr, Finset.card_le_card, Finset.image_subset_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
f_inj : Set.InjOn f (↑s : Set α)
⊢ #s ≤ #t

Tactic:
calc
    #s = #(s.image f) := (card_image_of_injOn f_inj).symm
    _ ≤ #t := card_le_card <| image_subset_iff.2 hf

Premises used: Iff.mpr, Finset.card_le_card, Finset.image_subset_iff, Finset.card_image_of_injOn, Eq.symm, Finset.image
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
f_inj : Set.InjOn f (↑s : Set α)
⊢ #s ≤ #t

Tactic:
classical
  calc
    #s = #(s.image f) := (card_image_of_injOn f_inj).symm
    _ ≤ #t := card_le_card <| image_subset_iff.2 hf

Premises used: Iff.mpr, Finset.card_le_card, Finset.image_subset_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
inl : ∀ {f : ↥∅ → ↥t} (hf : Injective f), card.{u_1} (α := α) ∅ ≤ #t
inr : ∀ (a₀ : α) (ha₀ : a₀ ∈ s), #s ≤ #t
⊢ #s ≤ #t

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀⟩

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
t : Finset β
f : ↥∅ → ↥t
hf : Injective f
⊢ card.{u_1} (α := α) ∅ ≤ #t

Tactic:
simp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β :=
  fun (a : α) ↦
    (↑(f
          (if ha : a ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
          else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)) :
      β)
inr : Set.MapsTo f' (↑s : Set α) (↑t : Set β)
inr₁ : Set.InjOn f' (↑s : Set α)
⊢ #s ≤ #t

Tactic:
apply card_le_card_of_injOn f'

Premises used: Finset.card_le_card_of_injOn
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β :=
  fun (a : α) ↦
    (↑(f
          (if ha : a ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
          else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)) :
      β)
⊢ Set.MapsTo f' (↑s : Set α) (↑t : Set β)

Tactic:
aesop (add safe unfold Set.MapsTo)

Premises used: Set.MapsTo
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β :=
  fun (a : α) ↦
    (↑(f
          (if ha : a ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
          else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)) :
      β)
a₁ : α
ha₁ : a₁ ∈ (↑s : Set α)
a₂ : α
ha₂ : a₂ ∈ (↑s : Set α)
haa : f' a₁ = f' a₂
inr : ∀ (ha₁ : a₁ ∈ s) ⦃a₂ : α⦄ (ha₂ : a₂ ∈ s) (haa : f' a₁ = f' a₂), a₁ = a₂
⊢ a₁ = a₂

Tactic:
rw [mem_coe] at ha₁ ha₂

Premises used: Finset.mem_coe
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β :=
  fun (a : α) ↦
    (↑(f
          (if ha : a ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
          else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)) :
      β)
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
haa : f' a₁ = f' a₂
⊢ f (if h : True then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₁ ⋯ else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀) =
    f (if h : True then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₂ ⋯ else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)

Tactic:
simp only [f', ha₁, ha₂, ← Subtype.ext_iff] at haa

Premises used: Subtype.ext_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β :=
  fun (a : α) ↦
    (↑(f
          (if ha : a ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
          else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)) :
      β)
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
haa :
  f (if h : True then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₁ ⋯ else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀) =
    f (if h : True then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₂ ⋯ else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)
⊢ a₁ = a₂

Tactic:
Subtype.ext_iff.mp (hf haa)

Premises used: Subtype.ext_iff, Iff.mp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
f' : α → β :=
  fun (a : α) ↦
    (↑(f
          (if ha : a ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
          else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)) :
      β)
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
haa :
  f (if h : True then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₁ ⋯ else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀) =
    f (if h : True then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₂ ⋯ else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)
⊢ a₁ = a₂

Tactic:
exact Subtype.ext_iff.mp (hf haa)

Premises used: Subtype.ext_iff, Iff.mp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
a₀ : α
ha₀ : a₀ ∈ s
inr inr₁ inr₂ : #s ≤ #t
inr₃ :
  let f' : α → β := fun (a : α) ↦
    (↑(f
          (if ha : a ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
          else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)) :
      β);
  Set.MapsTo f' (↑s : Set α) (↑t : Set β)
inr₄ inr₅ :
  let f' : α → β := fun (a : α) ↦
    (↑(f
          (if ha : a ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha
          else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)) :
      β);
  Set.InjOn f' (↑s : Set α)
⊢ #s ≤ #t

Tactic:
classical
    let f' : α → β := fun a => f (if ha : a ∈ s then ⟨a, ha⟩ else ⟨a₀, ha₀⟩)
    apply card_le_card_of_injOn f'
    · aesop (add safe unfold Set.MapsTo)
    · intro a₁ ha₁ a₂ ha₂ haa
      rw [mem_coe] at ha₁ ha₂
      simp only [f', ha₁, ha₂, ← Subtype.ext_iff] at haa
      exact Subtype.ext_iff.mp (hf haa)

Premises used: Subtype.ext_iff, Set.MapsTo, Finset.mem_coe
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : (↑t : Set β) ⊆ f '' (↑s : Set α)
⊢ #t ≤ #s

Tactic:
(card_le_card (mod_cast hf)).trans card_image_le

Premises used: Finset.card_le_card, Finset.card_image_le, LE.le.trans
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : (↑t : Set β) ⊆ f '' (↑s : Set α)
⊢ #t ≤ #s

Tactic:
exact (card_le_card (mod_cast hf)).trans card_image_le

Premises used: Finset.card_le_card, Finset.card_image_le, LE.le.trans
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.SurjOn f (↑s : Set α) (↑t : Set β)
classical classical₁ : #t ≤ #s
⊢ #t ≤ #s

Tactic:
classical unfold Set.SurjOn at hf; exact (card_le_card (mod_cast hf)).trans card_image_le

Premises used: Finset.card_le_card, Set.SurjOn, Finset.card_image_le, LE.le.trans
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
by_contra! : ∀ (hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y), False
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
by_contra! hz
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y
⊢ False

Tactic:
hc.not_ge (card_le_card_of_injOn f hf ?_)

Premises used: Finset.card_le_card_of_injOn, LT.lt.not_ge
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y
refine : Set.InjOn f (↑s : Set α)
⊢ False

Tactic:
refine hc.not_ge (card_le_card_of_injOn f hf ?_)

Premises used: Finset.card_le_card_of_injOn, LT.lt.not_ge
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
contrapose : ¬x = y → ¬f x = f y
⊢ f x = f y → x = y

Tactic:
contrapose
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
⊢ ¬x = y → ¬f x = f y

Tactic:
hz x hx y hy
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
⊢ ¬x = y → ¬f x = f y

Tactic:
exact hz x hx y hy
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
by_contra! by_contra!₁ by_contra!₂ by_contra!₃ : (¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y) → False
by_contra!₄ by_contra!₅ by_contra!₆ by_contra!₇ by_contra!₈ by_contra!₉ by_contra!₁₀ :
  ∀ (hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y), False
by_contra!₁₁ : ∀ (hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y), Set.InjOn f (↑s : Set α)
by_contra!₁₂ :
  ∀ (hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y) ⦃x : α⦄ (hx : x ∈ (↑s : Set α)) ⦃y : α⦄
    (hy : y ∈ (↑s : Set α)), f x = f y → x = y
by_contra!₁₃ :
  ∀ (hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y) ⦃x : α⦄ (hx : x ∈ (↑s : Set α)) ⦃y : α⦄
    (hy : y ∈ (↑s : Set α)), ¬x = y → ¬f x = f y
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
classical
  by_contra! hz
  refine hc.not_ge (card_le_card_of_injOn f hf ?_)
  intro x hx y hy
  contrapose
  exact hz x hx y hy

Premises used: Finset.card_le_card_of_injOn, LT.lt.not_ge
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
inst : DecidableEq β
f : α → β
hc : #(image f s) < #s
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y

Tactic:
exists_ne_map_eq_of_card_lt_of_maps_to hc (coe_image (β := β) ▸ Set.mapsTo_image f s)

Premises used: Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Set.mapsTo_image, Eq.rec, Finset.coe_image, SetLike.coe, Eq.symm
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
inst : DecidableEq β
f : α → β
hc : #(image f s) < #s
⊢ ¬Set.InjOn f (↑s : Set α)

Tactic:
mt card_image_of_injOn hc.ne

Premises used: mt, Finset.card_image_of_injOn, LT.lt.ne
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
⊢ Set.MapsTo f (↑(range n) : Set ℕ) (↑s : Set α)

Tactic:
simpa [Set.MapsTo, mem_range] using hf

Premises used: Finset.mem_range, Set.MapsTo
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
⊢ Set.InjOn f (↑(range n) : Set ℕ)

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hinj : Set.InjOn f (↑s : Set α)
hst : #t ≤ #s
this : image f s = t
rw : t ⊆ image f s
rw₁ rw₂ : t ⊆ t
⊢ Set.SurjOn f (↑s : Set α) (↑t : Set β)

Tactic:
rw [Finset.surjOn_iff_subset_image, this]

Premises used: Finset.surjOn_iff_subset_image
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hinj : Set.InjOn f (↑s : Set α)
hst : #t ≤ #s
suffices : image f s = t
⊢ Set.SurjOn f (↑s : Set α) (↑t : Set β)

Tactic:
suffices s.image f = t by rw [Finset.surjOn_iff_subset_image, this]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hinj : Set.InjOn f (↑s : Set α)
hst : #t ≤ #s
⊢ image f s ⊆ t

Tactic:
have : s.image f ⊆ t := hf.finsetImage_subset
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hinj : Set.InjOn f (↑s : Set α)
hst : #t ≤ #s
this : image f s ⊆ t
⊢ image f s = t

Tactic:
eq_of_subset_of_card_le this (hst.trans_eq (card_image_of_injOn hinj).symm)

Premises used: LE.le.trans_eq, Finset.card_image_of_injOn, Finset.eq_of_subset_of_card_le, Eq.symm
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hinj : Set.InjOn f (↑s : Set α)
hst : #t ≤ #s
this : image f s ⊆ t
⊢ image f s = t

Tactic:
exact eq_of_subset_of_card_le this (hst.trans_eq (card_image_of_injOn hinj).symm)

Premises used: LE.le.trans_eq, Finset.card_image_of_injOn, Finset.eq_of_subset_of_card_le, Eq.symm
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hinj : Set.InjOn f (↑s : Set α)
hst : #t ≤ #s
suffices suffices₁ suffices₂ : image f s = t
suffices₃ : ∀ (this : image f s ⊆ t), image f s = t
⊢ Set.SurjOn f (↑s : Set α) (↑t : Set β)

Tactic:
classical
  suffices s.image f = t by rw [Finset.surjOn_iff_subset_image, this]
  have : s.image f ⊆ t := hf.finsetImage_subset
  exact eq_of_subset_of_card_le this (hst.trans_eq (card_image_of_injOn hinj).symm)
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun (a : ↥s) ↦ f (↑a : α) ⋯
⊢ Set.InjOn f' (↑s.attach : Set ↥s)

Tactic:
have hinj' : Set.InjOn f' s.attach := fun x hx y hy hxy ↦ Subtype.ext (hinj _ _ x.2 y.2 hxy)
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun (a : ↥s) ↦ f (↑a : α) ⋯
hinj' : Set.InjOn f' (↑s.attach : Set ↥s)
⊢ Set.MapsTo f' (↑s.attach : Set ↥s) (↑t : Set β)

Tactic:
have hmapsto' : Set.MapsTo f' s.attach t := fun x hx ↦ hf _ _
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun (a : ↥s) ↦ f (↑a : α) ⋯
hinj' : Set.InjOn f' (↑s.attach : Set ↥s)
hmapsto' : Set.MapsTo f' (↑s.attach : Set ↥s) (↑t : Set β)
b : β
hb : b ∈ t
rwa rwa₁ rwa₂ rwa₃ : #t ≤ #s
⊢ #t ≤ #s.attach

Tactic:
rwa [card_attach]

Premises used: Finset.card_attach
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun (a : ↥s) ↦ f (↑a : α) ⋯
hinj' : Set.InjOn f' (↑s.attach : Set ↥s)
hmapsto' : Set.MapsTo f' (↑s.attach : Set ↥s) (↑t : Set β)
b : β
hb : b ∈ t
obtain : ∀ (a : ↥s) (ha : a ∈ (↑s.attach : Set ↥s)) (hb : f' a ∈ t), ∃ (a_1 : α) (ha : a_1 ∈ s), f' a = f a_1 ha
⊢ ∃ (a : α) (ha : a ∈ s), b = f a ha

Tactic:
obtain ⟨a, ha, rfl⟩ := surjOn_of_injOn_of_card_le _ hmapsto' hinj' (by rwa [card_attach]) hb

Premises used: Finset.surjOn_of_injOn_of_card_le, rfl
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun (a : ↥s) ↦ f (↑a : α) ⋯
hinj' : Set.InjOn f' (↑s.attach : Set ↥s)
hmapsto' : Set.MapsTo f' (↑s.attach : Set ↥s) (↑t : Set β)
a : ↥s
ha : a ∈ (↑s.attach : Set ↥s)
hb : f' a ∈ t
⊢ ∃ (a_1 : α) (ha : a_1 ∈ s), f' a = f a_1 ha

Tactic:
⟨a, a.2, rfl⟩

Premises used: Exists.intro, Subtype.val, rfl, Subtype.property
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun (a : ↥s) ↦ f (↑a : α) ⋯
hinj' : Set.InjOn f' (↑s.attach : Set ↥s)
hmapsto' : Set.MapsTo f' (↑s.attach : Set ↥s) (↑t : Set β)
a : ↥s
ha : a ∈ (↑s.attach : Set ↥s)
hb : f' a ∈ t
⊢ ∃ (a_1 : α) (ha : a_1 ∈ s), f' a = f a_1 ha

Tactic:
exact ⟨a, a.2, rfl⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hsurj : Set.SurjOn f (↑s : Set α) (↑t : Set β)
hst : #s ≤ #t
⊢ (↑(image f s) : Set β) = (↑t : Set β)

Tactic:
simp [hsurj.image_eq_of_mapsTo hf]

Premises used: Set.SurjOn.image_eq_of_mapsTo
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hsurj : Set.SurjOn f (↑s : Set α) (↑t : Set β)
hst : #s ≤ #t
⊢ image f s = t

Tactic:
have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hsurj : Set.SurjOn f (↑s : Set α) (↑t : Set β)
hst : #s ≤ #t
this : image f s = t
rw rw₁ : #t = #t
⊢ #(image f s) = #t

Tactic:
rw [this]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hsurj : Set.SurjOn f (↑s : Set α) (↑t : Set β)
hst : #s ≤ #t
this : image f s = t
⊢ #(image f s) = #t

Tactic:
have : #(s.image f) = #t := by rw [this]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hsurj : Set.SurjOn f (↑s : Set α) (↑t : Set β)
hst : #s ≤ #t
this_1 : image f s = t
this : #(image f s) = #t
⊢ #(image f s) ≤ #s

Tactic:
have : #(s.image f) ≤ #s := card_image_le
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hsurj : Set.SurjOn f (↑s : Set α) (↑t : Set β)
hst : #s ≤ #t
this_1 : image f s = t
this_2 : #(image f s) = #t
this : #(image f s) ≤ #s
rw : #(image f s) = #s
⊢ Set.InjOn f (↑s : Set α)

Tactic:
rw [← card_image_iff]

Premises used: Finset.card_image_iff