awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
hne : Nonempty α
h : (Function.invFunOn f s '' f '' s).encard = s.encard
⊢ Function.invFunOn f s '' f '' s = s

Tactic:
exact hs.eq_of_subset_of_encard_le' (f.invFunOn_image_image_subset s) h.symm.le

Premises used: Eq.le, Set.Finite.eq_of_subset_of_encard_le', Function.invFunOn_image_image_subset, Eq.symm
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Function.Injective f
ht : t ⊆ range f
rw : (f '' f ⁻¹' t).encard = t.encard
rw₁ : (t ∩ range f).encard = t.encard
rw₂ rw₃ : t.encard = t.encard
⊢ (f ⁻¹' t).encard = t.encard

Tactic:
rw [← hf.encard_image, image_preimage_eq_inter_range, inter_eq_self_of_subset_left ht]

Premises used: Set.image_preimage_eq_inter_range, Function.Injective.encard_image, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Bijective f
t : Set β
⊢ t ⊆ range f

Tactic:
simp [hf.surjective.range_eq]

Premises used: Function.Surjective.range_eq, Function.Bijective.surjective
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
f_inj : InjOn f s
grw : (f '' s).encard ≤ t.encard
grw₁ grw₂ : t.encard ≤ t.encard
⊢ s.encard ≤ t.encard

Tactic:
grw [← f_inj.encard_image, hf.image_subset]

Premises used: Set.InjOn.encard_image, Set.MapsTo.image_subset
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
P Q : Set α
⊢ encard (α := (↑P : Type u_1)) (P ↓∩ Q) ≤ P.encard

Tactic:
(Function.Embedding.subtype _).encard_le

Premises used: Function.Embedding.encard_le, Function.Embedding.subtype
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
P Q : Set α
x x_1 : (↑(P ↓∩ Q) : Type u_1)
h :
  Eq.{u_1 + 1} (α := (↑Q : Type u_1))
    ((fun (x : (↑(P ↓∩ Q) : Type u_1)) ↦
        (match (motive := (↑(P ↓∩ Q) : Type u_1) → (↑Q : Type u_1)) x with
          | ⟨⟨x, property⟩, hx⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ Q) x hx :
          (↑Q : Type u_1)))
      x)
    ((fun (x : (↑(P ↓∩ Q) : Type u_1)) ↦
        (match (motive := (↑(P ↓∩ Q) : Type u_1) → (↑Q : Type u_1)) x with
          | ⟨⟨x, property⟩, hx⟩ => Subtype.mk (p := fun (x : α) ↦ x ∈ Q) x hx :
          (↑Q : Type u_1)))
      x_1)
⊢ x = x_1

Tactic:
simpa [Subtype.coe_inj] using h

Premises used: Subtype.coe_inj
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
inl :
  ∀ (hs : Set.Finite.{u_1} (α := α) ∅) (hle : encard.{u_1} (α := α) ∅ ≤ t.encard),
    ∃ (f : α → β), ∅ ⊆ f ⁻¹' t ∧ InjOn f ∅
inr : ∀ (h : s.encard = ⊤), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₁ : ∀ (a : α) (has : a ∈ s), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt

Premises used: Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
t : Set β
hs : Set.Finite.{u_1} (α := α) ∅
hle : encard.{u_1} (α := α) ∅ ≤ t.encard
⊢ ∃ (f : α → β), ∅ ⊆ f ⁻¹' t ∧ InjOn f ∅

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
h : s.encard = ⊤
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
(encard_ne_top_iff.mpr hs h).elim

Premises used: Iff.mpr, False.elim, Set.encard_ne_top_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
h : s.encard = ⊤
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
exact (encard_ne_top_iff.mpr hs h).elim

Premises used: Iff.mpr, False.elim, Set.encard_ne_top_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
inr : ∀ (b : β) (hbt : b ∈ t), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)

Premises used: Iff.mpr, LT.lt.trans_le, Exists.intro, Iff.mp, Set.encard_pos
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
rwa : (s \ {a}).encard + 1 ≤ (t \ {b}).encard + 1
rwa₁ : s.encard ≤ (t \ {b}).encard + 1
rwa₂ rwa₃ rwa₄ rwa₅ : s.encard ≤ t.encard
⊢ (s \ {a}).encard ≤ (t \ {b}).encard

Tactic:
rwa [← WithTop.add_le_add_iff_right WithTop.one_ne_top,
    encard_diff_singleton_add_one has, encard_diff_singleton_add_one hbt]

Premises used: WithTop.one_ne_top, Set.encard_diff_singleton_add_one, WithTop.add_le_add_iff_right
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
⊢ (s \ {a}).encard ≤ (t \ {b}).encard

Tactic:
have hle' : (s \ {a}).encard ≤ (t \ {b}).encard := by
    rwa [← WithTop.add_le_add_iff_right WithTop.one_ne_top,
    encard_diff_singleton_add_one has, encard_diff_singleton_add_one hbt]
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
inr :
  ∀ (f₀ : α → β) (hf₀s : s \ {a} ⊆ f₀ ⁻¹' (t \ {b})) (hinj : InjOn f₀ (s \ {a})), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'

Premises used: Set.Finite.diff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hf₀s : s \ {a} ⊆ f₀ ⁻¹' (t \ {b})
hinj : InjOn f₀ (s \ {a})
⊢ ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b

Tactic:
simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s

Premises used: Set.subset_def, and_imp, Set.mem_singleton_iff, Set.mem_diff, Set.preimage_diff, Set.mem_preimage
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
h : s ⊆ Function.update (β := fun (a : α) ↦ β) f₀ a b ⁻¹' t ∧ InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) s
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s

Tactic:
use Function.update f₀ a b

Premises used: Function.update
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
h :
  insert a (s \ {a}) ⊆ Function.update (β := fun (a : α) ↦ β) f₀ a b ⁻¹' t ∧
    InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) (s \ {a}) ∧
      Function.update (β := fun (a : α) ↦ β) f₀ a b a ∉ Function.update (β := fun (a : α) ↦ β) f₀ a b '' (s \ {a})
⊢ s ⊆ Function.update (β := fun (a : α) ↦ β) f₀ a b ⁻¹' t ∧ InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) s

Tactic:
rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]

Premises used: Set.insert_eq_of_mem, Set.injOn_insert, Set.insert_diff_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
h :
  (∀ a_1 ∈ s, (if a_1 = a then b else f₀ a_1) ∈ t) ∧
    InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) (s \ {a}) ∧ ∀ x ∈ s, ¬x = a → ¬x = a ∧ ¬f₀ x = b
⊢ insert a (s \ {a}) ⊆ Function.update (β := fun (a : α) ↦ β) f₀ a b ⁻¹' t ∧
    InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) (s \ {a}) ∧
      Function.update (β := fun (a : α) ↦ β) f₀ a b a ∉ Function.update (β := fun (a : α) ↦ β) f₀ a b '' (s \ {a})

Tactic:
simp only [mem_diff, mem_singleton_iff, insert_diff_singleton, subset_def,
    mem_insert_iff, mem_preimage, Function.update_apply, forall_eq_or_imp, ite_true, and_imp,
    mem_image, ite_eq_left_iff, not_exists, not_and, not_forall, exists_prop, and_iff_right hbt]

Premises used: Set.subset_def, ite_eq_left_iff, and_imp, Set.mem_image, not_exists, Function.update_apply, forall_eq_or_imp, ite_true, and_iff_right, exists_prop, Set.mem_singleton_iff, Set.mem_diff, Set.insert_diff_singleton, Set.mem_insert_iff, not_and, Classical.not_forall, Set.mem_preimage
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ (∀ a_1 ∈ s, (if a_1 = a then b else f₀ a_1) ∈ t) ∧
    InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) (s \ {a}) ∧ ∀ x ∈ s, ¬x = a → ¬x = a ∧ ¬f₀ x = b

Tactic:
⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩

Premises used: And.right, And.intro
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
h : ∀ a_1 ∈ s, (if a_1 = a then b else f₀ a_1) ∈ t
h₁ : InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) (s \ {a})
⊢ (∀ a_1 ∈ s, (if a_1 = a then b else f₀ a_1) ∈ t) ∧
    InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) (s \ {a}) ∧ ∀ x ∈ s, ¬x = a → ¬x = a ∧ ¬f₀ x = b

Tactic:
refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
pos : ∀ (h : x = a), b ∈ t
neg : ∀ (h : ¬x = a), f₀ x ∈ t
⊢ (if x = a then b else f₀ x) ∈ t

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
h : x = a
⊢ b ∈ t

Tactic:
assumption
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
h : ¬x = a
⊢ f₀ x ∈ t

Tactic:
(hf₀s x hx h).1

Premises used: And.left
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
hx : x ∈ s
h : ¬x = a
⊢ f₀ x ∈ t

Tactic:
exact (hf₀s x hx h).1

Premises used: And.left
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
x : α
h_1 : x ∈ s \ {a}
left : x ∈ s
hxa : x ∉ {a}
rwa : f₀ x = f₀ x
h : x ≠ a
rwa₁ : f₀ x = f₀ x
h₁ h₂ h₃ : x ≠ a
⊢ f₀ x = Function.update (β := fun (a : α) ↦ β) f₀ a b x

Tactic:
rwa [Function.update_of_ne]

Premises used: Function.update_of_ne
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
f₀ : α → β
hinj : InjOn f₀ (s \ {a})
hf₀s : ∀ x ∈ s, ¬x = a → f₀ x ∈ t ∧ ¬f₀ x = b
⊢ InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) (s \ {a})

Tactic:
exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])

Premises used: _private.0.Set.Finite.exists_injOn_of_encard_le.match_10, Set.InjOn.congr, Eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Nonempty β
hs : s.Finite
h : s.encard = t.encard
obtain : ∀ (f : α → β) (hf : s ⊆ f ⁻¹' t) (hinj : InjOn f s), ∃ (f : α → β), BijOn f s t
⊢ ∃ (f : α → β), BijOn f s t

Tactic:
obtain ⟨f, hf, hinj⟩ := hs.exists_injOn_of_encard_le h.le

Premises used: Eq.le, Set.Finite.exists_injOn_of_encard_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
h₁ : BijOn f s t
⊢ ∃ (f : α → β), BijOn f s t

Tactic:
use f
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ BijOn f s (f '' s)

Tactic:
hinj.bijOn_image

Premises used: Set.InjOn.bijOn_image
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
h₁ : t = f '' s
⊢ BijOn f s t

Tactic:
convert! hinj.bijOn_image

Premises used: Set.InjOn.bijOn_image
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
h₁ h₂ : t = t
⊢ t = f '' s

Tactic:
rw [(hs.image f).eq_of_subset_of_encard_le (image_subset_iff.mpr hf)
    (h.symm.trans hinj.encard_image.symm).le]

Premises used: Iff.mpr, Eq.le, Set.Finite.image, Set.InjOn.encard_image, Set.image_subset_iff, Eq.symm, Set.Finite.eq_of_subset_of_encard_le, Eq.trans
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hc : t.encard < s.encard
hf : MapsTo f s t
contrapose! : ∀ (hc : ∀ (a₁ : α) (_ : a₁ ∈ s) (a₂ : α) (_ : a₂ ∈ s) (_ : a₁ ≠ a₂), f a₁ ≠ f a₂), s.encard ≤ t.encard
⊢ ∃ a₁ ∈ s, ∃ a₂ ∈ s, a₁ ≠ a₂ ∧ f a₁ = f a₂

Tactic:
contrapose! hc
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hc : ∀ (a₁ : α) (_ : a₁ ∈ s) (a₂ : α) (_ : a₂ ∈ s) (_ : a₁ ≠ a₂), f a₁ ≠ f a₂
this : Function.Injective (MapsTo.restrict f s t hf)
f' : Function.Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) (↑t : Type u_2) :=
  { toFun := MapsTo.restrict f s t hf, inj' := this }
⊢ s.encard ≤ t.encard

Tactic:
f'.encard_le

Premises used: Function.Embedding.encard_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hc : ∀ (a₁ : α) (_ : a₁ ∈ s) (a₂ : α) (_ : a₂ ∈ s) (_ : a₁ ≠ a₂), f a₁ ≠ f a₂
this : Function.Injective (MapsTo.restrict f s t hf)
f' : Function.Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) (↑t : Type u_2) :=
  { toFun := MapsTo.restrict f s t hf, inj' := this }
⊢ s.encard ≤ t.encard

Tactic:
exact f'.encard_le

Premises used: Function.Embedding.encard_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hc : ∀ (a₁ : α) (_ : a₁ ∈ s) (a₂ : α) (_ : a₂ ∈ s) (_ : a₁ ≠ a₂), f a₁ ≠ f a₂
suffices : Function.Injective (MapsTo.restrict f s t hf)
⊢ s.encard ≤ t.encard

Tactic:
suffices Function.Injective (hf.restrict f) by
    let f' : s ↪ t := ⟨hf.restrict, this⟩
    exact f'.encard_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hc : ∀ (a₁ : α) (_ : a₁ ∈ s) (a₂ : α) (_ : a₂ ∈ s) (_ : a₁ ≠ a₂), f a₁ ≠ f a₂
⊢ Function.Injective (MapsTo.restrict f s t hf)

Tactic:
simpa only [hf.restrict_inj, not_imp_not] using hc

Premises used: Set.MapsTo.restrict_inj, not_imp_not
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.ncard = s.encard.toNat

Tactic:
rfl

Premises used: Set.ncard, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rwa : (↑s.encard.toNat : ℕ∞) = s.encard
rwa₁ : s.encard ≠ ⊤
rwa₂ : ¬s.encard = ⊤
rwa₃ : ¬s.Infinite
rwa₄ : ¬¬s.Finite
rwa₅ rwa₆ rwa₇ rwa₈ : s.Finite
⊢ (↑s.ncard : ℕ∞) = s.encard

Tactic:
rwa [ncard, ENat.coe_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]

Premises used: Classical.not_not, Set.encard_eq_top_iff, ne_eq, ENat.coe_toNat_eq_self, Set.ncard, Set.Infinite
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
inst : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ (↑s.ncard : ℕ∞) = s.encard

Tactic:
s.toFinite.cast_ncard_eq

Premises used: Set.toFinite, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ (↑s.ncard : ℕ∞) ≤ s.encard

Tactic:
ENat.coe_toNat_le_self _

Premises used: ENat.coe_toNat_le_self, Set.ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ Nat.card.{u_1} (↑s : Type u_1) = s.ncard

Tactic:
rfl

Premises used: Set.encard, Nat.card, dite, Function.extend, ENat.toNat, WithTop.untopD, Set.ncard, WithTop.recTopCoe, ENat.card, rfl, Cardinal.toENatAux
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : Nat.card.{u_1} (↑s : Type u_1) = hs.toFinset (s := s).card
rw₁ : Fintype.card.{u_1} (↑s : Type u_1) = hs.toFinset (s := s).card
rw₂ rw₃ : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑s : Type u_1)
⊢ s.ncard = hs.toFinset (s := s).card

Tactic:
rw [← _root_.Nat.card_coe_set_eq, @Nat.card_eq_fintype_card _ hs.fintype,
    @Finite.card_toFinset _ _ hs.fintype hs]

Premises used: Nat.card_coe_set_eq, Set.Finite.card_toFinset, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
⊢ s.ncard = s.toFinset.card

Tactic:
simp [← _root_.Nat.card_coe_set_eq, Nat.card_eq_fintype_card]

Premises used: Nat.card_coe_set_eq, Nat.card_eq_fintype_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
rw : Fintype.card.{u_1} (↑s : Type u_1) = s.toFinset.card
rw₁ rw₂ : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑s : Type u_1)
⊢ Fintype.card.{u_1} (↑s : Type u_1) = s.ncard

Tactic:
rw [ncard_eq_toFinset_card', toFinset_card]

Premises used: Set.toFinset_card, Set.ncard_eq_toFinset_card'
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ (↑s.ncard : Cardinal.{u_1}) = Cardinal.mk (↑s : Type u_1)

Tactic:
@Nat.cast_card _ hs

Premises used: Set.encard, Nat.card, dite, Function.extend, Nat.cast_card, ENat.toNat, WithTop.untopD, Set.ncard, WithTop.recTopCoe, ENat.card, Cardinal.toENatAux
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ
rw : s.Finite → ((∃ (n₀ : ℕ), s.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ k) ↔ s.ncard ≤ k)
⊢ s.encard ≤ (↑k : ℕ∞) ↔ s.Finite ∧ s.ncard ≤ k

Tactic:
rw [encard_le_coe_iff, and_congr_right_iff]

Premises used: and_congr_right_iff, Set.encard_le_coe_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
h : ∃ (n₀ : ℕ), s.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ k
n₀ : ℕ
hn₀ : s.encard = (↑n₀ : ℕ∞)
hle : n₀ ≤ k
rwa : s.encard.toNat ≤ k
rwa₁ : ENat.toNat (↑n₀ : ℕ∞) ≤ k
rwa₂ rwa₃ rwa₄ rwa₅ : n₀ ≤ k
⊢ s.ncard ≤ k

Tactic:
rwa [ncard_def, hn₀, ENat.toNat_coe]

Premises used: Set.ncard_def, ENat.toNat_coe
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
h : s.ncard ≤ k
rw rw₁ : s.encard = s.encard
⊢ s.encard = (↑s.ncard : ℕ∞)

Tactic:
rw [hfin.cast_ncard_eq]

Premises used: Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ
⊢ s.Finite → ((∃ (n₀ : ℕ), s.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ k) ↔ s.ncard ≤ k)

Tactic:
exact fun hfin ↦ ⟨fun ⟨n₀, hn₀, hle⟩ ↦ by rwa [ncard_def, hn₀, ENat.toNat_coe],
    fun h ↦ ⟨s.ncard, by rw [hfin.cast_ncard_eq], h⟩⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
rw : Nat.card.{u_1} (↑s : Type u_1) = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ s.ncard = 0

Tactic:
rw [← _root_.Nat.card_coe_set_eq, @Nat.card_eq_zero_of_infinite _ hs.to_subtype]

Premises used: Nat.card_eq_zero_of_infinite, Nat.card_coe_set_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
rw : s.encard ≤ t.encard
⊢ s.ncard ≤ t.ncard

Tactic:
rw [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset hst).cast_ncard_eq]

Premises used: Set.Finite.subset, Nat.cast_le, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ s.encard ≤ t.encard

Tactic:
encard_mono hst

Premises used: Set.encard_mono
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ s.encard ≤ t.encard

Tactic:
exact encard_mono hst

Premises used: Set.encard_mono
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
inst : Finite α
⊢ Monotone.{u_1, 0} (α := Set α) ncard

Tactic:
fun _ _ ↦ ncard_le_ncard

Premises used: Monotone, Set.ncard_le_ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : Eq (α := ℕ∞) (↑s.ncard : ℕ∞) (↑0 : ℕ∞) ↔ s = ∅
rw₁ : s.encard = (↑0 : ℕ∞) ↔ s = ∅
rw₂ : s.encard = 0 ↔ s = ∅
rw₃ rw₄ : s = ∅ ↔ s = ∅
⊢ s.ncard = 0 ↔ s = ∅

Tactic:
rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, Nat.cast_zero, encard_eq_zero]

Premises used: Set.encard_eq_zero, Nat.cast_inj, Nat.cast_zero, Set.Finite.cast_ncard_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Finset α
rw : ⋯.toFinset (s := (↑s : Set α)).card = s.card
rw₁ rw₂ : s.card = s.card
⊢ (↑s : Set α).ncard = s.card

Tactic:
rw [ncard_eq_toFinset_card _, Finset.finite_toSet_toFinset]

Premises used: Finset.finite_toSet_toFinset, Set.ncard_eq_toFinset_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_3
⊢ ncard.{u_3} (α := α) univ = Nat.card α

Tactic:
Nat.card_univ

Premises used: Set.encard, Nat.card, Nat.card_univ, dite, Function.extend, ENat.toNat, WithTop.untopD, Set.ncard, WithTop.recTopCoe, ENat.card, Cardinal.toENatAux
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
inst : Finite α
s : Set α
⊢ s.ncard ≤ Nat.card α

Tactic:
ncard_univ α ▸ ncard_le_ncard s.subset_univ

Premises used: Set.subset_univ, Eq.rec, Set.ncard_univ, Set.ncard_le_ncard
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_3
rw rw₁ : Eq.{u_3 + 1} (α := Set α) ∅ ∅
⊢ ncard.{u_3} (α := α) ∅ = 0

Tactic:
rw [ncard_eq_zero]

Premises used: Set.ncard_eq_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : s.ncard ≠ 0 ↔ s.Nonempty
rw₁ : ¬s.ncard = 0 ↔ s.Nonempty
rw₂ : ¬s = ∅ ↔ s.Nonempty
rw₃ rw₄ : ¬s = ∅ ↔ s ≠ ∅
⊢ 0 < s.ncard ↔ s.Nonempty

Tactic:
rw [pos_iff_ne_zero, Ne, ncard_eq_zero hs, nonempty_iff_ne_empty]

Premises used: Ne, Set.ncard_eq_zero, Set.nonempty_iff_ne_empty, pos_iff_ne_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ s.ncard ≠ 0

Tactic:
((ncard_pos hs).mpr ⟨a, h⟩).ne.symm

Premises used: Iff.mpr, Ne.symm, Exists.intro, Set.ncard_pos, LT.lt.ne
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.ncard ≠ 0
⊢ s.Finite

Tactic:
s.finite_or_infinite.elim id fun h ↦ (hs h.ncard).elim

Premises used: Set.Infinite.ncard, Set.finite_or_infinite, False.elim, id, Or.elim
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : 0 < s.ncard
⊢ s.Finite

Tactic:
finite_of_ncard_ne_zero hs.ne.symm

Premises used: Ne.symm, Set.finite_of_ncard_ne_zero, LT.lt.ne
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
hs : s.ncard ≠ 0
rw : s ≠ ∅
⊢ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty