awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = (↑n : ℕ∞)
hk : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
rw : t₀.encard + 1 = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
⊢ (insert x t₀).encard = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have rw₁ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
Tactic: rw [encard_insert_of_notMem hx.2, ht₀]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
h : ∀ (n : ℕ) (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
hk : ⊤ ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = ⊤
have hk₁ : s.encard = ⊤
Tactic: rw [top_le_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
hk : k ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = k
have zero : ∀ (hk : 0 ≤ s.encard), ∃ t ⊆ s, t.encard = 0
Tactic: induction k using ENat.nat_induction with
  | zero => exact ⟨∅, empty_subset _, by simp⟩
  | succ n IH =>
    obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hk)
    simp only [Nat.cast_succ] at *
    have hne : t₀ ≠ s := by
      rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk; simp at hk
    obtain ⟨x, hx⟩ := exists_of_ssubset (ht₀s.ssubset_of_ne hne)
    exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_notMem hx.2, ht₀]⟩
  | top => rw [top_le_iff] at hk; exact ⟨s, Subset.rfl, hk⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
hk : k ≤ s.encard
zero : ∀ (hk : 0 ≤ s.encard), ∃ t ⊆ s, t.encard = 0
⊢ ∃ t ⊆ s, t.encard = k
have succ : ∀ (n : ℕ) (IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)) (hk : (↑n.succ : ℕ∞) ≤ s.encard),
  ∃ t ⊆ s, t.encard = (↑n.succ : ℕ∞)
Tactic: induction k using ENat.nat_induction with
  | zero => exact ⟨∅, empty_subset _, by simp⟩
  | succ n IH =>
    obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hk)
    simp only [Nat.cast_succ] at *
    have hne : t₀ ≠ s := by
      rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk; simp at hk
    obtain ⟨x, hx⟩ := exists_of_ssubset (ht₀s.ssubset_of_ne hne)
    exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_notMem hx.2, ht₀]⟩
  | top => rw [top_le_iff] at hk; exact ⟨s, Subset.rfl, hk⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
k : ℕ∞
hk : k ≤ s.encard
zero : ∀ (hk : 0 ≤ s.encard), ∃ t ⊆ s, t.encard = 0
succ :
  ∀ (n : ℕ) (IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)) (hk : (↑n.succ : ℕ∞) ≤ s.encard),
    ∃ t ⊆ s, t.encard = (↑n.succ : ℕ∞)
⊢ ∃ t ⊆ s, t.encard = k
have top : (∀ (n : ℕ) (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)) → ∀ (hk : ⊤ ≤ s.encard), ∃ t ⊆ s, t.encard = ⊤
Tactic: induction k using ENat.nat_induction with
  | zero => exact ⟨∅, empty_subset _, by simp⟩
  | succ n IH =>
    obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hk)
    simp only [Nat.cast_succ] at *
    have hne : t₀ ≠ s := by
      rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk; simp at hk
    obtain ⟨x, hx⟩ := exists_of_ssubset (ht₀s.ssubset_of_ne hne)
    exact ⟨insert x t₀, insert_subset hx.1 ht₀s, by rw [encard_insert_of_notMem hx.2, ht₀]⟩
  | top => rw [top_le_iff] at hk; exact ⟨s, Subset.rfl, hk⟩
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k
have inl : ∀ (hs : s.encard = ⊤), ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k
Tactic: obtain (hs | hs) := eq_or_ne s.encard ⊤
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
inl : ∀ (hs : s.encard = ⊤), ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k
have inr : ∀ (hs : s.encard ≠ ⊤), ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k
Tactic: obtain (hs | hs) := eq_or_ne s.encard ⊤
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k
have hsk₁ : k = ⊤
Tactic: rw [hs, top_le_iff] at hsk
Cleared hypotheses: hsk, hkt, hs
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : k = ⊤
hkt : k ≤ t.encard
hs : s.encard = ⊤
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k
have inl : ∀ (hkt : ⊤ ≤ t.encard), ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = ⊤
Tactic: subst hsk
Cleared hypotheses: k, hsk, hkt
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
k : ℕ∞
hst : s ⊆ t
hsk : s.encard ≤ k
hkt : k ≤ t.encard
hs : s.encard ≠ ⊤
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = k
have inr : ∀ (k : ℕ∞) (hsk : s.encard ≤ s.encard + k) (hkt : s.encard + k ≤ t.encard),
  ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k
Tactic: obtain ⟨k, rfl⟩ := exists_add_of_le hsk
Cleared hypotheses: k, hsk, hkt
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k
have inr : ∀ (k' : ℕ∞) (hk' : t.encard = s.encard + k + k'), ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k
Tactic: obtain ⟨k', hk'⟩ := exists_add_of_le hkt
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ k ≤ (t \ s).encard
have rw : ∀ (hkt : k + s.encard ≤ (t \ s).encard + s.encard) (k' : ℕ∞) (hk' : t.encard = s.encard + k + k'), k ≤ (t \ s).encard
Tactic: rw [← encard_diff_add_encard_of_subset hst, add_comm] at hkt
Cleared hypotheses: hkt, k', hk'
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k
have hk : k ≤ (t \ s).encard
Tactic: have hk : k ≤ encard (t \ s) := by
    rw [← encard_diff_add_encard_of_subset hst, add_comm] at hkt
    exact WithTop.le_of_add_le_add_right hs hkt
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k : ℕ∞
hsk : s.encard ≤ s.encard + k
hkt : s.encard + k ≤ t.encard
k' : ℕ∞
hk' : t.encard = s.encard + k + k'
hk : k ≤ (t \ s).encard
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + k
have inr : ∀ (r' : Set α) (hr' : r' ⊆ t \ s) (hsk : s.encard ≤ s.encard + r'.encard) (hkt : s.encard + r'.encard ≤ t.encard)
  (hk' : t.encard = s.encard + r'.encard + k') (hk : r'.encard ≤ (t \ s).encard),
  ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + r'.encard
Tactic: obtain ⟨r', hr', rfl⟩ := exists_subset_encard_eq hk
Cleared hypotheses: k, hsk, hkt, hk', hk
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
⊢ ∃ (r : Set α), s ⊆ r ∧ r ⊆ t ∧ r.encard = s.encard + r'.encard
have inr : (s ∪ r').encard = s.encard + r'.encard
Tactic: refine ⟨s ∪ r', subset_union_left, union_subset hst (hr'.trans diff_subset), ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.encard ≠ ⊤
k' : ℕ∞
r' : Set α
hr' : r' ⊆ t \ s
hsk : s.encard ≤ s.encard + r'.encard
hkt : s.encard + r'.encard ≤ t.encard
hk' : t.encard = s.encard + r'.encard + k'
hk : r'.encard ≤ (t \ s).encard
⊢ (s ∪ r').encard = s.encard + r'.encard
have inr : s.encard + r'.encard = s.encard + r'.encard
Tactic: rw [encard_union_eq (disjoint_of_subset_right hr' disjoint_sdiff_right)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
⊢ (f '' s).encard = s.encard
have rw : ENat.card.{u_2} (↑(f '' s) : Type u_2) = s.encard
Tactic: rw [encard, ENat.card_image_of_injOn h, encard]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
rw : ENat.card.{u_2} (↑(f '' s) : Type u_2) = s.encard
⊢ (f '' s).encard = s.encard
have rw₁ : ENat.card.{u_1} (↑s : Type u_1) = s.encard
Tactic: rw [encard, ENat.card_image_of_injOn h, encard]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
rw : ENat.card.{u_2} (↑(f '' s) : Type u_2) = s.encard
rw₁ : ENat.card.{u_1} (↑s : Type u_1) = s.encard
⊢ (f '' s).encard = s.encard
have rw₂ : ENat.card.{u_1} (↑s : Type u_1) = ENat.card.{u_1} (↑s : Type u_1)
Tactic: rw [encard, ENat.card_image_of_injOn h, encard]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
⊢ ENat.card α ≤ (range f).encard
have rw : ENat.card α ≤ (f '' univ).encard
Tactic: rw [← image_univ, hf.encard_image, encard_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
rw : ENat.card α ≤ (f '' univ).encard
⊢ ENat.card α ≤ (range f).encard
have rw₁ : ENat.card α ≤ encard.{u_1} (α := α) univ
Tactic: rw [← image_univ, hf.encard_image, encard_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Injective f
rw : ENat.card α ≤ (f '' univ).encard
rw₁ : ENat.card α ≤ encard.{u_1} (α := α) univ
⊢ ENat.card α ≤ (range f).encard
have rw₂ : ENat.card α ≤ ENat.card α
Tactic: rw [← image_univ, hf.encard_image, encard_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (f '' s).encard ≤ s.encard
have inl : ∀ (h : IsEmpty α), (f '' s).encard ≤ s.encard
Tactic: obtain (h | h) := isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
inl : ∀ (h : IsEmpty α), (f '' s).encard ≤ s.encard
⊢ (f '' s).encard ≤ s.encard
have inr : ∀ (h : Nonempty α), (f '' s).encard ≤ s.encard
Tactic: obtain (h | h) := isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' s).encard ≤ s.encard
have inl : (f '' ∅).encard ≤ encard.{u_1} (α := α) ∅
Tactic: rw [s.eq_empty_of_isEmpty]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
⊢ (f '' s).encard ≤ s.encard
have inr : (Function.invFunOn f s '' f '' s).encard ≤ s.encard
Tactic: grw [← (f.invFunOn_injOn_image s).encard_image, f.invFunOn_image_image_subset s]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
inr : (Function.invFunOn f s '' f '' s).encard ≤ s.encard
⊢ (f '' s).encard ≤ s.encard
have inr₁ : s.encard ≤ s.encard
Tactic: grw [← (f.invFunOn_injOn_image s).encard_image, f.invFunOn_image_image_subset s]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
⊢ InjOn f s
have inl : ∀ (h' : IsEmpty α), InjOn f s
Tactic: obtain (h' | hne) := isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
inl : ∀ (h' : IsEmpty α), InjOn f s
⊢ InjOn f s
have inr : ∀ (hne : Nonempty α), InjOn f s
Tactic: obtain (h' | hne) := isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Finite
h : (f '' s).encard = s.encard
hne : Nonempty α
⊢ InjOn f s
have h₁ : (Function.invFunOn f s '' f '' s).encard = s.encard
Tactic: rw [← (f.invFunOn_injOn_image s).encard_image] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ InjOn f s
have inr : Function.invFunOn f s '' f '' s = s
Tactic: rw [injOn_iff_invFunOn_image_image_eq_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Function.Injective f
ht : t ⊆ range f
⊢ (f ⁻¹' t).encard = t.encard
have rw : (f '' f ⁻¹' t).encard = t.encard
Tactic: rw [← hf.encard_image, image_preimage_eq_inter_range, inter_eq_self_of_subset_left ht]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ (f ⁻¹' t).encard = t.encard
have rw₁ : (t ∩ range f).encard = t.encard
Tactic: rw [← hf.encard_image, image_preimage_eq_inter_range, inter_eq_self_of_subset_left ht]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ (f ⁻¹' t).encard = t.encard
have rw₂ : t.encard = t.encard
Tactic: rw [← hf.encard_image, image_preimage_eq_inter_range, inter_eq_self_of_subset_left ht]
-- 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
f_inj : InjOn f s
⊢ s.encard ≤ t.encard
have grw : (f '' s).encard ≤ t.encard
Tactic: grw [← f_inj.encard_image, hf.image_subset]
-- 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
f_inj : InjOn f s
grw : (f '' s).encard ≤ t.encard
⊢ s.encard ≤ t.encard
have grw₁ : t.encard ≤ t.encard
Tactic: grw [← f_inj.encard_image, hf.image_subset]
-- 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: obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
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: obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
-- 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: obtain (rfl | h | ⟨a, has, -⟩) := s.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt
-- 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
a : α
has : a ∈ s
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have inr : ∀ (b : β) (hbt : b ∈ t), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
Tactic: obtain ⟨b, hbt⟩ := encard_pos.1 ((encard_pos.2 ⟨_, has⟩).trans_le 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
a : α
has : a ∈ s
b : β
hbt : b ∈ t
⊢ (s \ {a}).encard ≤ (t \ {b}).encard
have rwa : (s \ {a}).encard + 1 ≤ (t \ {b}).encard + 1
Tactic: rwa [← WithTop.add_le_add_iff_right WithTop.one_ne_top,
    encard_diff_singleton_add_one has, encard_diff_singleton_add_one hbt]
-- 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
a : α
has : a ∈ s
b : β
hbt : b ∈ t
rwa : (s \ {a}).encard + 1 ≤ (t \ {b}).encard + 1
⊢ (s \ {a}).encard ≤ (t \ {b}).encard
have rwa₁ : s.encard ≤ (t \ {b}).encard + 1
Tactic: rwa [← WithTop.add_le_add_iff_right WithTop.one_ne_top,
    encard_diff_singleton_add_one has, encard_diff_singleton_add_one hbt]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
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
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have hle' : (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]
-- 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
a : α
has : a ∈ s
b : β
hbt : b ∈ t
hle' : (s \ {a}).encard ≤ (t \ {b}).encard
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have inr : ∀ (f₀ : α → β) (hf₀s : s \ {a} ⊆ f₀ ⁻¹' (t \ {b})) (hinj : InjOn f₀ (s \ {a})), ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
Tactic: obtain ⟨f₀, hf₀s, hinj⟩ := exists_injOn_of_encard_le hs.diff hle'
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
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})
⊢ ∃ (f : α → β), s ⊆ f ⁻¹' t ∧ InjOn f s
have hf₀s₁ : ∀ 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
Cleared hypotheses: hf₀s
-- 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
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
have h : s ⊆ Function.update (β := fun (a : α) ↦ β) f₀ a b ⁻¹' t ∧ InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) s
Tactic: use Function.update f₀ a b
-- 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
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
have 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})
Tactic: rw [← insert_eq_of_mem has, ← insert_diff_singleton, injOn_insert (fun h ↦ h.2 rfl)]
-- 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
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
⊢ 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})
have 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
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]
-- 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
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
have h : ∀ a_1 ∈ s, (if a_1 = a then b else f₀ a_1) ∈ t
Tactic: refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
-- 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
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
⊢ (∀ 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
have h₁ : InjOn (Function.update (β := fun (a : α) ↦ β) f₀ a b) (s \ {a})
Tactic: refine ⟨?_, ?_, fun x hxs hxa ↦ ⟨hxa, (hf₀s x hxs hxa).2⟩⟩
-- 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
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
⊢ (if x = a then b else f₀ x) ∈ t
have pos : ∀ (h : x = a), b ∈ t
Tactic: split_ifs with h
-- 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
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
⊢ (if x = a then b else f₀ x) ∈ t
have neg : ∀ (h : ¬x = a), f₀ x ∈ t
Tactic: split_ifs with h
-- 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
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 : x ∈ s \ {a}
left : x ∈ s
hxa : x ∉ {a}
⊢ f₀ x = Function.update (β := fun (a : α) ↦ β) f₀ a b x
have rwa : f₀ x = f₀ x
Tactic: 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
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 : x ∈ s \ {a}
left : x ∈ s
hxa : x ∉ {a}
rwa : f₀ x = f₀ x
⊢ f₀ x = Function.update (β := fun (a : α) ↦ β) f₀ a b x
have h : x ≠ a
Tactic: rwa [Function.update_of_ne]