awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set α
t : Set β
hs : s.Finite
hle : s.encard ≤ t.encard
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have inl : ∀ (hs : Set.Finite.{u_1} (α := α) ∅) (hle : encard.{u_1} (α := α) ∅ ≤ t.encard), ∃ (f : α → β), ∅ ⊆ f ⁻¹' t ∧ InjOn f ∅
Tactic: classical
  obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
  · simp
  · exact (encard_ne_top_iff.mpr hs h).elim
  obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
  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]
  obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'
  simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s
  use Function.update f₀ a b
  rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
  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]
  refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
  · rintro x hx; split_ifs with h
    · assumption
    · exact (hf₀s x hx h).1
  exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])
Cleared hypotheses: s, hs, hle
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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 ∅
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have inr : ∀ (h : s.encard = ⊤), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
Tactic: classical
  obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
  · simp
  · exact (encard_ne_top_iff.mpr hs h).elim
  obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
  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]
  obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'
  simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s
  use Function.update f₀ a b
  rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
  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]
  refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
  · rintro x hx; split_ifs with h
    · assumption
    · exact (hf₀s x hx h).1
  exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have inr₁ : ∀ (a : α) (has : a ∈ s), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
Tactic: classical
  obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
  · simp
  · exact (encard_ne_top_iff.mpr hs h).elim
  obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
  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]
  obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'
  simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s
  use Function.update f₀ a b
  rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
  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]
  refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
  · rintro x hx; split_ifs with h
    · assumption
    · exact (hf₀s x hx h).1
  exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
inr₂ : ∀ (h : s.encard = ⊤), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₃ inr₄ : ∀ (a : α) (has : a ∈ s), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have inr₅ : ∀ (a : α) (has : a ∈ s) (b : β) (hbt : b ∈ t), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
Tactic: classical
  obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
  · simp
  · exact (encard_ne_top_iff.mpr hs h).elim
  obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
  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]
  obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'
  simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s
  use Function.update f₀ a b
  rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
  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]
  refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
  · rintro x hx; split_ifs with h
    · assumption
    · exact (hf₀s x hx h).1
  exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
inr₂ : ∀ (h : s.encard = ⊤), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₃ inr₄ : ∀ (a : α) (has : a ∈ s), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₅ : ∀ (a : α) (has : a ∈ s) (b : β) (hbt : b ∈ t), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have inr₆ : ∀ (a : α) (has : a ∈ s) (b : β) (hbt : b ∈ t) (hle' : (s \ {a}).encard ≤ (t \ {b}).encard),
  ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
Tactic: classical
  obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
  · simp
  · exact (encard_ne_top_iff.mpr hs h).elim
  obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
  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]
  obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'
  simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s
  use Function.update f₀ a b
  rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
  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]
  refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
  · rintro x hx; split_ifs with h
    · assumption
    · exact (hf₀s x hx h).1
  exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
inr₂ : ∀ (h : s.encard = ⊤), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₃ inr₄ : ∀ (a : α) (has : a ∈ s), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₅ : ∀ (a : α) (has : a ∈ s) (b : β) (hbt : b ∈ t), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₆ :
  ∀ (a : α) (has : a ∈ s) (b : β) (hbt : b ∈ t) (hle' : (s \ {a}).encard ≤ (t \ {b}).encard),
    ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have inr₇ : ∀ (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})), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
Tactic: classical
  obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
  · simp
  · exact (encard_ne_top_iff.mpr hs h).elim
  obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
  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]
  obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'
  simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s
  use Function.update f₀ a b
  rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
  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]
  refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
  · rintro x hx; split_ifs with h
    · assumption
    · exact (hf₀s x hx h).1
  exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
inr₂ : ∀ (h : s.encard = ⊤), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₃ inr₄ : ∀ (a : α) (has : a ∈ s), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₅ : ∀ (a : α) (has : a ∈ s) (b : β) (hbt : b ∈ t), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₆ :
  ∀ (a : α) (has : a ∈ s) (b : β) (hbt : b ∈ t) (hle' : (s \ {a}).encard ≤ (t \ {b}).encard),
    ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₇ :
  ∀ (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})), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have inr₈ : ∀ (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), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
Tactic: classical
  obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
  · simp
  · exact (encard_ne_top_iff.mpr hs h).elim
  obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
  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]
  obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'
  simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s
  use Function.update f₀ a b
  rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
  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]
  refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
  · rintro x hx; split_ifs with h
    · assumption
    · exact (hf₀s x hx h).1
  exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
inr₂ : ∀ (h : s.encard = ⊤), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₃ inr₄ : ∀ (a : α) (has : a ∈ s), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₅ : ∀ (a : α) (has : a ∈ s) (b : β) (hbt : b ∈ t), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₆ :
  ∀ (a : α) (has : a ∈ s) (b : β) (hbt : b ∈ t) (hle' : (s \ {a}).encard ≤ (t \ {b}).encard),
    ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₇ :
  ∀ (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})), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
inr₈ :
  ∀ (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), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have h : ∀ (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),
  s ⊆ Function.update (β := fun (a : α) ↦ β) f₀ a b ⁻¹' t ∧ InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) s
Tactic: classical
  obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
  · simp
  · exact (encard_ne_top_iff.mpr hs h).elim
  obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le hle)
  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]
  obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'
  simp only [preimage_diff, subset_def, mem_diff, mem_singleton_iff, mem_preimage, and_imp] at hf₀s
  use Function.update f₀ a b
  rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
  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]
  refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
  · rintro x hx; split_ifs with h
    · assumption
    · exact (hf₀s x hx h).1
  exact InjOn.congr hinj (fun x ⟨_, hxa⟩ ↦ by rwa [Function.update_of_ne])
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Nonempty β
hs : s.Finite
h : s.encard = t.encard
⊢ ∃ (f : α → β), BijOn f s t
have obtain : ∀ (f : α → β) (hf : s ⊆ f ⁻¹' t) (hinj : InjOn f s), ∃ (f : α → β), BijOn f s t
Tactic: obtain ⟨f, hf, hinj⟩ := hs.exists_injOn_of_encard_le h.le
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (f : α → β), BijOn f s t
have h₁ : BijOn f s t
Tactic: use f
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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 t
have h₁ : t = f '' s
Tactic: convert! hinj.bijOn_image
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ t = f '' s
have h₁ : t = t
Tactic: rw [(hs.image f).eq_of_subset_of_encard_le (image_subset_iff.mpr hf)
    (h.symm.trans hinj.encard_image.symm).le]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hc : t.encard < s.encard
hf : MapsTo f s t
⊢ ∃ a₁ ∈ s, ∃ a₂ ∈ s, a₁ ≠ a₂ ∧ f a₁ = f a₂
have contrapose! : ∀ (hc : ∀ (a₁ : α) (_ : a₁ ∈ s) (a₂ : α) (_ : a₂ ∈ s) (_ : a₁ ≠ a₂), f a₁ ≠ f a₂), s.encard ≤ t.encard
Tactic: contrapose! hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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₂
⊢ s.encard ≤ t.encard
have suffices : Function.Injective (MapsTo.restrict f s t hf)
Tactic: suffices Function.Injective (hf.restrict f) by
    let f' : s ↪ t := ⟨hf.restrict, this⟩
    exact f'.encard_le
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ (↑s.ncard : ℕ∞) = s.encard
have rwa : (↑s.encard.toNat : ℕ∞) = s.encard
Tactic: rwa [ncard, ENat.coe_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rwa : (↑s.encard.toNat : ℕ∞) = s.encard
⊢ (↑s.ncard : ℕ∞) = s.encard
have rwa₁ : s.encard ≠ ⊤
Tactic: rwa [ncard, ENat.coe_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rwa : (↑s.encard.toNat : ℕ∞) = s.encard
rwa₁ : s.encard ≠ ⊤
⊢ (↑s.ncard : ℕ∞) = s.encard
have rwa₂ : ¬s.encard = ⊤
Tactic: rwa [ncard, ENat.coe_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rwa : (↑s.encard.toNat : ℕ∞) = s.encard
rwa₁ : s.encard ≠ ⊤
rwa₂ : ¬s.encard = ⊤
⊢ (↑s.ncard : ℕ∞) = s.encard
have rwa₃ : ¬s.Infinite
Tactic: rwa [ncard, ENat.coe_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rwa : (↑s.encard.toNat : ℕ∞) = s.encard
rwa₁ : s.encard ≠ ⊤
rwa₂ : ¬s.encard = ⊤
rwa₃ : ¬s.Infinite
⊢ (↑s.ncard : ℕ∞) = s.encard
have rwa₄ : ¬¬s.Finite
Tactic: rwa [ncard, ENat.coe_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard = hs.toFinset (s := s).card
have rw : Nat.card.{u_1} (↑s : Type u_1) = 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]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : Nat.card.{u_1} (↑s : Type u_1) = hs.toFinset (s := s).card
⊢ s.ncard = hs.toFinset (s := s).card
have rw₁ : Fintype.card.{u_1} (↑s : Type u_1) = 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]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ s.ncard = hs.toFinset (s := s).card
have rw₂ : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑s : Type u_1)
Tactic: rw [← _root_.Nat.card_coe_set_eq, @Nat.card_eq_fintype_card _ hs.fintype,
    @Finite.card_toFinset _ _ hs.fintype hs]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
⊢ Fintype.card.{u_1} (↑s : Type u_1) = s.ncard
have rw : Fintype.card.{u_1} (↑s : Type u_1) = s.toFinset.card
Tactic: rw [ncard_eq_toFinset_card', toFinset_card]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
rw : Fintype.card.{u_1} (↑s : Type u_1) = s.toFinset.card
⊢ Fintype.card.{u_1} (↑s : Type u_1) = s.ncard
have rw₁ : Fintype.card.{u_1} (↑s : Type u_1) = Fintype.card.{u_1} (↑s : Type u_1)
Tactic: rw [ncard_eq_toFinset_card', toFinset_card]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ
⊢ s.encard ≤ (↑k : ℕ∞) ↔ s.Finite ∧ s.ncard ≤ k
have rw : s.Finite → ((∃ (n₀ : ℕ), s.encard = (↑n₀ : ℕ∞) ∧ n₀ ≤ k) ↔ s.ncard ≤ k)
Tactic: rw [encard_le_coe_iff, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ s.ncard ≤ k
have rwa : s.encard.toNat ≤ k
Tactic: rwa [ncard_def, hn₀, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ s.ncard ≤ k
have rwa₁ : ENat.toNat (↑n₀ : ℕ∞) ≤ k
Tactic: rwa [ncard_def, hn₀, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ
hfin : s.Finite
h : s.ncard ≤ k
⊢ s.encard = (↑s.ncard : ℕ∞)
have rw : s.encard = s.encard
Tactic: rw [hfin.cast_ncard_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
⊢ s.ncard = 0
have rw : Nat.card.{u_1} (↑s : Type u_1) = 0
Tactic: rw [← _root_.Nat.card_coe_set_eq, @Nat.card_eq_zero_of_infinite _ hs.to_subtype]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
rw : Nat.card.{u_1} (↑s : Type u_1) = 0
⊢ s.ncard = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [← _root_.Nat.card_coe_set_eq, @Nat.card_eq_zero_of_infinite _ hs.to_subtype]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ s.ncard ≤ t.ncard
have rw : s.encard ≤ t.encard
Tactic: rw [← Nat.cast_le (α := ℕ∞), ht.cast_ncard_eq, (ht.subset hst).cast_ncard_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
⊢ s.ncard = 0 ↔ s = ∅
have rw : Eq (α := ℕ∞) (↑s.ncard : ℕ∞) (↑0 : ℕ∞) ↔ s = ∅
Tactic: rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, Nat.cast_zero, encard_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
rw : Eq (α := ℕ∞) (↑s.ncard : ℕ∞) (↑0 : ℕ∞) ↔ s = ∅
⊢ s.ncard = 0 ↔ s = ∅
have rw₁ : s.encard = (↑0 : ℕ∞) ↔ s = ∅
Tactic: rw [← Nat.cast_inj (R := ℕ∞), hs.cast_ncard_eq, Nat.cast_zero, encard_eq_zero]