awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hsurj : Set.SurjOn f (↑s : Set α) (↑t : Set β)
hst : #s ≤ #t
this_1 : image f s = t
this_2 : #(image f s) = #t
this : #(image f s) ≤ #s
⊢ #(image f s) = #s

Tactic:
lia
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f (↑s : Set α) (↑t : Set β)
hsurj : Set.SurjOn f (↑s : Set α) (↑t : Set β)
hst : #s ≤ #t
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 α)
have₅ : ∀ (this : image f s = t) (this : #(image f s) = #t) (this : #(image f s) ≤ #s), #(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

Premises used: Finset.card_image_iff
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
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 : α) ⋯
x : β
hx : x ∈ (↑t : Set β)
⊢ x ∈ f' '' (↑s.attach : Set ↥s)

Tactic:
simpa [f'] using hsurj x hx
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
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 : α) ⋯
⊢ 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
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
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 β)
⊢ #s.attach ≤ #t

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
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 β)
⊢ Set.InjOn f' (↑s.attach : Set ↥s)

Tactic:
have hinj' := injOn_of_surjOn_of_card_le f' (fun x hx ↦ hf _ _) hsurj' (by simpa)
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
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 β)
hinj' : Set.InjOn f' (↑s.attach : Set ↥s)
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₁ ha₁ ∈ (↑s.attach : Set ↥s)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
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 β)
hinj' : Set.InjOn f' (↑s.attach : Set ↥s)
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) a₂ ha₂ ∈ (↑s.attach : Set ↥s)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
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 β)
hinj' : Set.InjOn f' (↑s.attach : Set ↥s)
⊢ a₁ = a₂

Tactic:
exact congrArg Subtype.val (@hinj' ⟨a₁, ha₁⟩ (by simp) ⟨a₂, ha₂⟩ (by simp) ha₁a₂)

Premises used: congrArg, Subtype.val
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
t : Finset β
inst : DecidableEq β
h : #s ≤ #t
⊢ image f s = t ↔ Set.BijOn f (↑s : Set α) (↑t : Set β)

Tactic:
grind [injOn_of_surjOn_of_card_le, Set.BijOn, image_eq_iff_surjOn_mapsTo]

Premises used: Finset.injOn_of_surjOn_of_card_le, Finset.image_eq_iff_surjOn_mapsTo, Set.BijOn
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
h : Disjoint s t
⊢ #(s.disjUnion t h) = #s + #t

Tactic:
Multiset.card_add _ _

Premises used: Multiset.card_add, Finset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #(s ∪ ∅) + #(s ∩ ∅) = #s + card.{u_1} (α := α) ∅

Tactic:
simp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ ∀ (a : α) (s_1 : Finset α),
    a ∉ s_1 → #(s ∪ s_1) + #(s ∩ s_1) = #s + #s_1 → #(s ∪ insert a s_1) + #(s ∩ insert a s_1) = #s + #(insert a s_1)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) + #(s ∪ t) = #s + #t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #(s ∪ t) = #s + #t - #(s ∩ t)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) = #s + #t - #(s ∪ t)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #(s ∪ t) ≤ #s + #t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
rw : #(s ∪ t) = #(s ∪ t) + #(s ∩ t) ↔ Disjoint s t
⊢ #(s ∪ t) = #s + #t ↔ Disjoint s t

Tactic:
rw [← card_union_add_card_inter]

Premises used: Finset.card_union_add_card_inter
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ #(s ∪ t) = #(s ∪ t) + #(s ∩ t) ↔ Disjoint s t

Tactic:
simp [disjoint_iff_inter_eq_empty]

Premises used: Finset.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : s ⊆ t
this : #(t \ s) = #(t \ s ∪ s) - #s
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : #(t \ s) = #t - #s), #(t \ s) = #t - #s
⊢ #(t \ s) = #t - #s

Tactic:
rwa [sdiff_union_of_subset h] at this

Premises used: Finset.sdiff_union_of_subset
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : s ⊆ t
suffices : #(t \ s) = #(t \ s ∪ s) - #s
⊢ #(t \ s) = #t - #s

Tactic:
suffices #(t \ s) = #(t \ s ∪ s) - #s by rwa [sdiff_union_of_subset h] at this
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : s ⊆ t
rw : #(t \ s) = #(t \ s) + #s - #s
rw₁ rw₂ : #(t \ s) = #(t \ s)
⊢ #(t \ s) = #(t \ s ∪ s) - #s

Tactic:
rw [card_union_of_disjoint sdiff_disjoint, Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right, Finset.card_union_of_disjoint, Finset.sdiff_disjoint
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
rw : #(t \ s) = #(t \ (s ∩ t))
rw₁ : s ∩ t ⊆ t
⊢ #(t \ s) = #t - #(s ∩ t)

Tactic:
rw [← card_sdiff_of_subset]

Premises used: Finset.card_sdiff_of_subset
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ #(t \ s) = #(t \ (s ∩ t))

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ s ∩ t ⊆ t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : s ⊆ t
⊢ #(t \ s) + #s = #t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #t - #s = #t - #(s ∩ t) - #(s \ t)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #t - #(s ∩ t) - #(s \ t) = #(t \ (s ∩ t)) - #(s \ t)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #(t \ (s ∩ t)) - #(s \ t) = #(t \ s) - #(s \ t)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #t - #s ≤ #(t \ s)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ #s ≤ #(s \ t) + #t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : #(s \ t ∪ t) = #(s ∪ t)
rw₁ rw₂ : #(s ∪ t) = #(s ∪ t)
⊢ #(s \ t) + #t = #(s ∪ t)

Tactic:
rw [← card_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]

Premises used: Finset.sdiff_union_self_eq_union, Finset.card_union_of_disjoint, Finset.sdiff_disjoint
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
h : #s < #t
⊢ (t \ s).Nonempty

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
h : #s < #t
⊢ ∃ e ∈ t, e ∉ s

Tactic:
simpa [Finset.Nonempty] using sdiff_nonempty_of_card_lt_card h

Premises used: Finset.sdiff_nonempty_of_card_lt_card, Finset.Nonempty
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
h : #s < #t
⊢ ∃ e ∈ t, e ∉ s

Tactic:
classical simpa [Finset.Nonempty] using sdiff_nonempty_of_card_lt_card h

Premises used: Finset.Nonempty
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : #(s \ t ∪ s ∩ t) = #s
rw₁ rw₂ : #s = #s
⊢ #(s \ t) + #(s ∩ t) = #s

Tactic:
rw [← card_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]

Premises used: Finset.disjoint_sdiff_inter, Finset.card_union_of_disjoint, Finset.sdiff_union_inter
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #(s ∩ t) + #(s \ t) = #s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ #(s \ t) ≤ #(t \ s) ↔ #s ≤ #t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ #(s \ t) < #(t \ s) ↔ #s < #t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ #(s \ t) = #(t \ s) ↔ #s = #t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : #s < #t + #u
contrapose! : ∀ (hstu : t ∩ u = ∅), #t + #u ≤ #s
⊢ (t ∩ u).Nonempty

Tactic:
contrapose! hstu
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
⊢ #t + #u = #(t ∪ u)

Tactic:
simp [← card_union_add_card_inter, hstu]

Premises used: Finset.card_union_add_card_inter
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
a : t ∪ u ⊆ s
⊢ #(t ∪ u) ≤ #s

Tactic:
gcongr
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
⊢ t ∪ u ⊆ s

Tactic:
union_subset hts hus

Premises used: Finset.union_subset
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
⊢ t ∪ u ⊆ s

Tactic:
exact union_subset hts hus

Premises used: Finset.union_subset
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
_ : #t + #u = #(t ∪ u)
_₁ : #(t ∪ u) ≤ #s
⊢ #t + #u ≤ #s

Tactic:
calc
    _ = #(t ∪ u) := by simp [← card_union_add_card_inter, hstu]
    _ ≤ #s := by gcongr; exact union_subset hts hus

Premises used: Union.union
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
p : α → Prop
inst : DecidablePred p
inst_1 : (x : α) → Decidable ¬p x
rw : #(filter p s ∪ {a ∈ s | ¬p a}) = #s
rw₁ rw₂ : #s = #s
⊢ #(filter p s) + #({a ∈ s | ¬p a}) = #s

Tactic:
rw [← card_union_of_disjoint (disjoint_filter_filter_not _ _ _), filter_union_filter_not_eq]

Premises used: Finset.disjoint_filter_filter_not, Finset.filter_union_filter_not_eq, Finset.card_union_of_disjoint
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
p : α → Prop
inst : DecidablePred p
inst_1 : (x : α) → Decidable ¬p x
rw : #(filter p s ∪ {a ∈ s | ¬p a}) = #s
rw₁ rw₂ : #s = #s
⊢ #(filter p s) + #({a ∈ s | ¬p a}) = #s

Tactic:
classical
  rw [← card_union_of_disjoint (disjoint_filter_filter_not _ _ _), filter_union_filter_not_eq]

Premises used: Finset.disjoint_filter_filter_not, Finset.filter_union_filter_not_eq, Finset.card_union_of_disjoint
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ s ⊆ t ∧ t ⊆ t ∧ #t = #t

Tactic:
simp [hst]
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
refine : ∀ k < #t, n ≤ k → (∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
⊢ ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = n

Tactic:
refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
_ : k < #t → n ≤ k → (∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
⊢ k < #t → n ≤ k → (∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
_
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
h : k < #t
hnk : n ≤ k
this : ∀ (u : Finset α) (hu₁ : s ⊆ u) (hu₂ : u ⊆ t) (hu₃ : #u = k + 1), ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
⊢ (∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
⟨u, hu₁, hu₂, hu₃⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
h : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ (u \ s).Nonempty

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
h : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
obtain : ∀ (a : α) (ha : a ∈ u \ s), ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
⊢ ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
obtain ⟨a, ha⟩ : (u \ s).Nonempty := by grind

Premises used: SDiff.sdiff, Finset.Nonempty
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
h : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u \ s
⊢ s ⊆ u.erase a ∧ u.erase a ⊆ t ∧ #(u.erase a) = k

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
h : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
a : α
ha : a ∈ u \ s
⊢ ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
exact ⟨u.erase a, by grind⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
refine : ∀ k < #t, n ≤ k → (∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
refine₁ :
  ∀ k < #t,
    ∀ (hnk : n ≤ k) (u : Finset α) (hu₁ : s ⊆ u) (hu₂ : u ⊆ t) (hu₃ : #u = k + 1),
      ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
refine₂ :
  ∀ k < #t,
    ∀ (hnk : n ≤ k) (u : Finset α) (hu₁ : s ⊆ u) (hu₂ : u ⊆ t) (hu₃ : #u = k + 1) (a : α) (ha : a ∈ u \ s),
      ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
⊢ ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = n

Tactic:
classical
  refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩
  intro k _ hnk ⟨u, hu₁, hu₂, hu₃⟩
  obtain ⟨a, ha⟩ : (u \ s).Nonempty := by grind
  exact ⟨u.erase a, by grind⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
hns : n ≤ #s
⊢ card.{u_1} (α := α) ∅ ≤ n

Tactic:
simp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
hns : n ≤ #s
⊢ ∃ t ⊆ s, #t = n

Tactic:
simpa using exists_subsuperset_card_eq s.empty_subset (by simp) hns

Premises used: Finset.empty_subset, Finset.exists_subsuperset_card_eq
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
⊢ n ≤ #s ↔ ∃ t ⊆ s, #t = n

Tactic:
⟨fun h => ?_, fun ⟨t, hst, ht⟩ => ht ▸ card_le_card hst⟩

Premises used: Finset.card_le_card, _private.0.Finset.le_card_iff_exists_subset_card.match_1, Eq.rec, LE.le, Iff.intro, Finset.card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
refine : ∀ (h : n ≤ #s), ∃ t ⊆ s, #t = n
⊢ n ≤ #s ↔ ∃ t ⊆ s, #t = n

Tactic:
refine ⟨fun h => ?_, fun ⟨t, hst, ht⟩ => ht ▸ card_le_card hst⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
h : n ≤ #s
⊢ ∃ t ⊆ s, #t = n

Tactic:
exists_subset_card_eq h

Premises used: Finset.exists_subset_card_eq
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
n : ℕ
h : n ≤ #s
⊢ ∃ t ⊆ s, #t = n

Tactic:
exact exists_subset_card_eq h

Premises used: Finset.exists_subset_card_eq
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
mk :
  ∀ (val : Multiset α) (nodup : val.Nodup),
    #{ val := val, nodup := nodup : Finset α } = 1 ↔ ∃ (a : α), { val := val, nodup := nodup : Finset α } = {a}
⊢ #s = 1 ↔ ∃ (a : α), s = {a}

Tactic:
cases s
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
val : Multiset α
nodup : val.Nodup
⊢ #{ val := val, nodup := nodup : Finset α } = 1 ↔ ∃ (a : α), { val := val, nodup := nodup : Finset α } = {a}

Tactic:
simp only [Multiset.card_eq_one, Finset.card, ← val_inj, singleton_val]

Premises used: Finset.singleton_val, Finset.card, Multiset.card_eq_one, Finset.val_inj
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
mp : (∃ a ∉ s, insert a s = t) → s ⊆ t ∧ #s + 1 = #t
mpr : s ⊆ t ∧ #s + 1 = #t → ∃ a ∉ s, insert a s = t
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ #s + 1 = #t

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ (∃ a ∉ s, insert a s = t) → s ⊆ t ∧ #s + 1 = #t

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
hst : s ⊆ t
h : #s + 1 = #t
⊢ #(t \ s) = 1

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
hst : s ⊆ t
h : #s + 1 = #t
mpr : ∀ (a : α) (ha : t \ s = {a}), ∃ a ∉ s, insert a s = t
⊢ ∃ a ∉ s, insert a s = t

Tactic:
obtain ⟨a, ha⟩ : ∃ a, t \ s = {a} := card_eq_one.mp (by grind)

Premises used: Finset.card_eq_one, Iff.mp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inl :
  card.{u_1} (α := α) ∅ ≤ 1 ↔
    ∀ (a : α), Membership.mem (γ := Finset α) ∅ a → ∀ (b : α), Membership.mem (γ := Finset α) ∅ b → a = b
inr : ∀ (x : α) (hx : x ∈ s), #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
⊢ card.{u_1} (α := α) ∅ ≤ 1 ↔
    ∀ (a : α), Membership.mem (γ := Finset α) ∅ a → ∀ (b : α), Membership.mem (γ := Finset α) ∅ b → a = b

Tactic:
simp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
(Nat.succ_le_of_lt (card_pos.2 ⟨x, hx⟩)).ge_iff_eq'.trans (card_eq_one.trans ⟨?_, ?_⟩)

Premises used: Iff.mpr, Finset.card_eq_one, Nat.succ_le_of_lt, LE.le.ge_iff_eq', Iff.intro, Exists.intro, Iff.trans, Finset.card_pos
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
inr : (∃ (a : α), s = {a}) → ∀ a ∈ s, ∀ b ∈ s, a = b
inr₁ : (∀ a ∈ s, ∀ b ∈ s, a = b) → ∃ (a : α), s = {a}
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
refine (Nat.succ_le_of_lt (card_pos.2 ⟨x, hx⟩)).ge_iff_eq'.trans (card_eq_one.trans ⟨?_, ?_⟩)

Premises used: Iff.mpr, Finset.card_eq_one, Nat.succ_le_of_lt, LE.le.ge_iff_eq', Iff.intro, Exists.intro, Iff.trans, Finset.card_pos
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ (∃ (a : α), s = {a}) → ∀ a ∈ s, ∀ b ∈ s, a = b

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
h : ∀ a ∈ s, ∀ b ∈ s, a = b
⊢ s = {x}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) → ∃ (a : α), s = {a}

Tactic:
exact fun h => ⟨x, by grind⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b

Tactic:
grind [card_le_one]

Premises used: Finset.card_le_one
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ Subsingleton.{u_1 + 1} ↥s

Tactic:
card_le_one.trans (s : Set α).subsingleton_coe.symm

Premises used: Finset.card_le_one, SetLike.coe, Iff.trans, Set.subsingleton_coe, Iff.symm
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
rw : Subsingleton.{u_1 + 1} ↥s ↔ (↑s : Set α).Subsingleton
rw₁ : Subsingleton.{u_1 + 1} ↥s ↔ Subsingleton.{u_1 + 1} (↑(↑s : Set α) : Type u_1)
rw₂ rw₃ : Subsingleton.{u_1 + 1} ↥s ↔ Subsingleton.{u_1 + 1} ↥s
⊢ #s ≤ 1 ↔ (↑s : Set α).Subsingleton

Tactic:
rw [card_le_one_iff_subsingleton_coe, ← Set.subsingleton_coe, SetLike.coe_sort_coe]

Premises used: SetLike.coe_sort_coe, Finset.card_le_one_iff_subsingleton_coe, Set.subsingleton_coe
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
⊢ #s ≤ 1 ↔ ∃ (x : α), s ⊆ {x}

Tactic:
⟨fun H => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
refine_1 : ∀ (H : #s ≤ 1), ∃ (x : α), s ⊆ {x}
refine_2 : (∃ (x : α), s ⊆ {x}) → #s ≤ 1
⊢ #s ≤ 1 ↔ ∃ (x : α), s ⊆ {x}

Tactic:
refine ⟨fun H => ?_, ?_⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
H : #s ≤ 1
refine_1 : ∀ (H : card.{u_1} (α := α) ∅ ≤ 1), ∃ (x : α), Subset (α := Finset α) ∅ {x}
refine_1₁ : ∀ (x : α) (hx : x ∈ s), ∃ (x : α), s ⊆ {x}
⊢ ∃ (x : α), s ⊆ {x}

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : Nonempty α
H : card.{u_1} (α := α) ∅ ≤ 1
⊢ ∃ (x : α), Subset (α := Finset α) ∅ {x}

Tactic:
⟨Classical.arbitrary α, empty_subset _⟩

Premises used: Exists.intro, Classical.arbitrary, Finset.empty_subset
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
inst : Nonempty α
H : card.{u_1} (α := α) ∅ ≤ 1
⊢ ∃ (x : α), Subset (α := Finset α) ∅ {x}

Tactic:
exact ⟨Classical.arbitrary α, empty_subset _⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
rw : Membership.mem (γ := Finset α) {x} x
rw₁ rw₂ : x = x
⊢ Membership.mem (γ := Finset α) {x} y

Tactic:
rw [card_le_one.1 H y hy x hx, mem_singleton]

Premises used: Finset.mem_singleton, Finset.card_le_one, Iff.mp
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
⊢ ∃ (x : α), s ⊆ {x}

Tactic:
exact ⟨x, fun y hy => by rw [card_le_one.1 H y hy x hx, mem_singleton]⟩
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ card (α := α) {x}

Tactic:
card_le_card hx

Premises used: Finset.card_le_card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
x : α
hx : s ⊆ {x}
⊢ #s ≤ card (α := α) {x}

Tactic:
exact card_le_card hx

Premises used: Finset.card_le_card
-- Module: Mathlib.Data.Finset.Card
Goal:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
⊢ Nonempty α

Tactic:
have : Nonempty α := ⟨a⟩