awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ #s = #t
have refine : ∀ (a1 : α) (h1 : a1 ∈ s) (a2 : α) (h2 : a2 ∈ s) (eq : i a1 h1 = i a2 h2), a1 = a2
Tactic: refine card_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩)
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ a1 = a2
have rw : j (i a1 h1) sorry = j (i a2 h2) sorry
Tactic: rw [← left_inv a1 h1, ← left_inv a2 h2]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
e : α ≃ β
hst : ∀ (i : α), i ∈ s ↔ Membership.mem (α := β) t ((e : (a : α) → β) i : β)
⊢ #s = #t
have refine_1 : Set.MapsTo (⇑e : (a : α) → β) (↑s : Set α) (↑t : Set β)
Tactic: refine card_nbij' e e.symm ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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 β)
⊢ #s = #t
have refine_2 : Set.MapsTo (⇑e.symm : (a : β) → α) (↑t : Set β) (↑s : Set α)
Tactic: refine card_nbij' e e.symm ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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 α)
⊢ #s = #t
have refine_3 : Set.LeftInvOn.{u_1, u_2} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β) (↑s : Set α)
Tactic: refine card_nbij' e e.symm ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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 α)
⊢ #s = #t
have refine_4 : Set.RightInvOn.{u_1, u_2} (α := α) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β) (↑t : Set β)
Tactic: refine card_nbij' e e.symm ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : ↥s → ↥t
hf : Injective f
⊢ #s ≤ #t
have inl : ∀ {f : ↥∅ → ↥t} (hf : Injective f), card.{u_1} (α := α) ∅ ≤ #t
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀⟩
Cleared hypotheses: s, f, hf
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ #s ≤ #t
have inr : ∀ (a₀ : α) (ha₀ : a₀ ∈ s), #s ≤ #t
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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₀)) :
      β)
⊢ #s ≤ #t
have inr : Set.MapsTo f' (↑s : Set α) (↑t : Set β)
Tactic: apply card_le_card_of_injOn f'
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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 β)
⊢ #s ≤ #t
have inr₁ : Set.InjOn f' (↑s : Set α)
Tactic: apply card_le_card_of_injOn f'
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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₂
⊢ a₁ = a₂
have inr : ∀ (ha₁ : a₁ ∈ s) ⦃a₂ : α⦄ (ha₂ : a₂ ∈ s) (haa : f' a₁ = f' a₂), a₁ = a₂
Tactic: rw [mem_coe] at ha₁ ha₂
Cleared hypotheses: ha₁, a₂, ha₂, haa
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
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₂
⊢ a₁ = a₂
have haa₁ : f (if h : True then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₁ sorry else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀) =
  f (if h : True then Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₂ sorry else Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₀ ha₀)
Tactic: simp only [f', ha₁, ha₂, ← Subtype.ext_iff] at haa
Cleared hypotheses: haa
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ #s ≤ #t
have 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 β)
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)
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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 β)
⊢ #s ≤ #t
have 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 α)
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)
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
have by_contra! : ∀ (hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y), False
Tactic: by_contra! hz
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
have refine : Set.InjOn f (↑s : Set α)
Tactic: refine hc.not_ge (card_le_card_of_injOn f hf ?_)
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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 α)
⊢ f x = f y → x = y
have contrapose : ¬x = y → ¬f x = f y
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
hc : #t < #s
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
have by_contra! : (¬∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y) → False
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
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
have by_contra!₄ : (∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y) → False
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
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
have by_contra!₁₁ : ∀ (hz : ∀ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s) (_ : x ≠ y), f x ≠ f y), Set.InjOn f (↑s : Set α)
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
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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 α)
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
have 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
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
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
have 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
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
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ Set.SurjOn f (↑s : Set α) (↑t : Set β)
have rw : t ⊆ image f s
Tactic: rw [Finset.surjOn_iff_subset_image, this]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ Set.SurjOn f (↑s : Set α) (↑t : Set β)
have rw₁ : t ⊆ t
Tactic: rw [Finset.surjOn_iff_subset_image, this]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ Set.SurjOn f (↑s : Set α) (↑t : Set β)
have suffices : image f s = t
Tactic: suffices s.image f = t by rw [Finset.surjOn_iff_subset_image, this]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
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
have this : image f s ⊆ t
Tactic: have : s.image f ⊆ t := hf.finsetImage_subset
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ Set.SurjOn f (↑s : Set α) (↑t : Set β)
have suffices : image f s = t
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)
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ Set.SurjOn f (↑s : Set α) (↑t : Set β)
have suffices₃ : ∀ (this : image f s ⊆ t), image f s = t
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)
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
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 : α) ⋯
⊢ ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), b = f a ha
have hinj' : 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)
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
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)
⊢ ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), b = f a ha
have hmapsto' : Set.MapsTo f' (↑s.attach : Set ↥s) (↑t : Set β)
Tactic: have hmapsto' : Set.MapsTo f' s.attach t := fun x hx ↦ hf _ _
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ ∃ (a : α) (ha : a ∈ s), b = f a ha
have 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
Tactic: obtain ⟨a, ha, rfl⟩ := surjOn_of_injOn_of_card_le _ hmapsto' hinj' (by rwa [card_attach]) hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
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
⊢ Set.InjOn f (↑s : Set α)
have this : image f s = t
Tactic: have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
have rw : #t = #t
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
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
⊢ Set.InjOn f (↑s : Set α)
have this₁ : #(image f s) = #t
Tactic: have : #(s.image f) = #t := by rw [this]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
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
⊢ Set.InjOn f (↑s : Set α)
have this₁ : #(image f s) ≤ #s
Tactic: have : #(s.image f) ≤ #s := card_image_le
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ Set.InjOn f (↑s : Set α)
have rw : #(image f s) = #s
Tactic: rw [← card_image_iff]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
⊢ Set.InjOn f (↑s : Set α)
have have : ∀ (this : image f s = t), Set.InjOn f (↑s : Set α)
Tactic: classical
  have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]
  have : #(s.image f) = #t := by rw [this]
  have : #(s.image f) ≤ #s := card_image_le
  rw [← card_image_iff]
  lia
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
have have₁ have₂ : ∀ (this : image f s = t), Set.InjOn f (↑s : Set α)
⊢ Set.InjOn f (↑s : Set α)
have have₃ : ∀ (this : image f s = t) (this : #(image f s) = #t), Set.InjOn f (↑s : Set α)
Tactic: classical
  have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]
  have : #(s.image f) = #t := by rw [this]
  have : #(s.image f) ≤ #s := card_image_le
  rw [← card_image_iff]
  lia
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
have have₁ have₂ : ∀ (this : image f s = t), Set.InjOn f (↑s : Set α)
have₃ : ∀ (this : image f s = t) (this : #(image f s) = #t), Set.InjOn f (↑s : Set α)
⊢ Set.InjOn f (↑s : Set α)
have have₄ : ∀ (this : image f s = t) (this : #(image f s) = #t) (this : #(image f s) ≤ #s), Set.InjOn f (↑s : Set α)
Tactic: classical
  have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]
  have : #(s.image f) = #t := by rw [this]
  have : #(s.image f) ≤ #s := card_image_le
  rw [← card_image_iff]
  lia
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
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
have have₁ have₂ : ∀ (this : image f s = t), Set.InjOn f (↑s : Set α)
have₃ : ∀ (this : image f s = t) (this : #(image f s) = #t), Set.InjOn f (↑s : Set α)
have₄ : ∀ (this : image f s = t) (this : #(image f s) = #t) (this : #(image f s) ≤ #s), Set.InjOn f (↑s : Set α)
⊢ Set.InjOn f (↑s : Set α)
have have₅ : ∀ (this : image f s = t) (this : #(image f s) = #t) (this : #(image f s) ≤ #s), #(image f s) = #s
Tactic: classical
  have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]
  have : #(s.image f) = #t := by rw [this]
  have : #(s.image f) ≤ #s := card_image_le
  rw [← card_image_iff]
  lia
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun (a : ↥s) ↦ f (↑a : α) ⋯
⊢ a₁ = a₂
have hsurj' : Set.SurjOn f' (↑s.attach : Set ↥s) (↑t : Set β)
Tactic: have hsurj' : Set.SurjOn f' s.attach t := fun x hx ↦ by simpa [f'] using hsurj x hx
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
f' : ↥s → β := fun (a : ↥s) ↦ f (↑a : α) ⋯
hsurj' : Set.SurjOn f' (↑s.attach : Set ↥s) (↑t : Set β)
⊢ a₁ = a₂
have hinj' : Set.InjOn f' (↑s.attach : Set ↥s)
Tactic: have hinj' := injOn_of_surjOn_of_card_le f' (fun x hx ↦ hf _ _) hsurj' (by simpa)
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ #(s ∪ t) = #s + #t ↔ Disjoint s t
have rw : #(s ∪ t) = #(s ∪ t) + #(s ∩ t) ↔ Disjoint s t
Tactic: rw [← card_union_add_card_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : s ⊆ t
this : #(t \ s) = #(t \ s ∪ s) - #s
⊢ #(t \ s) = #t - #s
have rwa : ∀ (this : #(t \ s) = #t - #s), #(t \ s) = #t - #s
Tactic: rwa [sdiff_union_of_subset h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) = #t - #s
have suffices : #(t \ s) = #(t \ s ∪ s) - #s
Tactic: suffices #(t \ s) = #(t \ s ∪ s) - #s by rwa [sdiff_union_of_subset h] at this
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) = #(t \ s ∪ s) - #s
have rw : #(t \ s) = #(t \ s) + #s - #s
Tactic: rw [card_union_of_disjoint sdiff_disjoint, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : s ⊆ t
rw : #(t \ s) = #(t \ s) + #s - #s
⊢ #(t \ s) = #(t \ s ∪ s) - #s
have rw₁ : #(t \ s) = #(t \ s)
Tactic: rw [card_union_of_disjoint sdiff_disjoint, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ #(t \ s) = #t - #(s ∩ t)
have rw : #(t \ s) = #(t \ (s ∩ t))
Tactic: rw [← card_sdiff_of_subset]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
rw : #(t \ s) = #(t \ (s ∩ t))
⊢ #(t \ s) = #t - #(s ∩ t)
have rw₁ : s ∩ t ⊆ t
Tactic: rw [← card_sdiff_of_subset]