ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>s t : Set α<VAR>ht : t.Finite<VAR>h : s ⊂ t<GOAL>s.encard < t.encard
<VAR>α : Type u_1<VAR>Finite α<GOAL>StrictMono Set.encard
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>(s \ t).encard + t.encard = (s ∪ t).encard
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>s.encard ≤ (s \ t).encard + t.encard
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>s.encard - t.encard ≤ (s \ t).encard
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.encard + sᶜ.encard = Set.univ.encard
<VAR>α : Type u_1<VAR>s : Set α<VAR>x : α<GOAL>(insert x s).encard ≤ s.encard + 1
<VAR>α : Type u_1<VAR>s : Set α<VAR>x : α<GOAL>({x} ∩ s).encard ≤ 1
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<GOAL>(s \ {a}).encard + 1 = s.encard
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<GOAL>(s \ {a}).encard = s.encard - 1
<VAR>α : Type u_1<VAR>s : Set α<VAR>x : α<GOAL>s.encard - 1 ≤ (s \ {x}).encard
<VAR>α : Type u_1<VAR>s : Set α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∈ s<GOAL>(insert a (s \ {b})).encard = s.encard
<VAR>α : Type u_1<VAR>s : Set α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∈ s<GOAL>(insert a s \ {b}).encard = s.encard
<VAR>α : Type u_1<VAR>s : Set α<VAR>k : ℕ∞<GOAL>s.encard = k + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.encard = k
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard
<VAR>α : Type u_1<VAR>x y : α<VAR>hne : x ≠ y<GOAL>{x, y}.encard = 2
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.encard = 1 ↔ ∃ x, s = {x}
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.encard ≤ 1 ↔ s = ∅ ∨ ∃ x, s = {x}
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.encard ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
<VAR>α : Type u_1<VAR>s : Set α<GOAL>1 < s.encard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
<VAR>α : Type u_1<VAR>s : Set α<VAR>h : 1 < s.encard<VAR>a : α<GOAL>∃ b ∈ s, b ≠ a
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.encard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.encard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
<VAR>k : ℕ<GOAL>{i | i < k}.encard = ↑k
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite<VAR>h : s ⊆ t<VAR>hst : t.encard = s.encard + 1<GOAL>∃ a, t = insert a s
<VAR>α : Type u_1<VAR>s : Set α<VAR>k : ℕ∞<VAR>hk : k ≤ s.encard<GOAL>∃ t ⊆ s, t.encard = k
<VAR>α : Type u_1<VAR>s t : Set α<VAR>k : ℕ∞<VAR>hst : s ⊆ t<VAR>hsk : s.encard ≤ k<VAR>hkt : k ≤ t.encard<GOAL>∃ r, s ⊆ r ∧ r ⊆ t ∧ r.encard = k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>h : Set.InjOn f s<GOAL>(f '' s).encard = s.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>e : ↑s ≃ ↑t<GOAL>s.encard = t.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Set α<GOAL>(f '' s).encard = s.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>e : ↑s ↪ ↑t<GOAL>s.encard ≤ t.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<GOAL>(f '' s).encard ≤ s.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>hs : s.Finite<VAR>h : (f '' s).encard = s.encard<GOAL>Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : Set β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>ht : t ⊆ Set.range f<GOAL>(f ⁻¹' t).encard = t.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : Set.MapsTo f s t<VAR>f_inj : Set.InjOn f s<GOAL>s.encard ≤ t.encard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty β<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Finite<VAR>hle : s.encard ≤ t.encard<GOAL>∃ f, s ⊆ f ⁻¹' t ∧ Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>Nonempty β<VAR>hs : s.Finite<VAR>h : s.encard = t.encard<GOAL>∃ f, Set.BijOn f s t
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.ncard = s.encard.toNat
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite<GOAL>↑s.ncard = s.encard
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Nat.card ↑s = s.ncard
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>s.ncard = (Set.Finite.toFinset hs).card
<VAR>α : Type u_1<VAR>s : Set α<VAR>Fintype ↑s<GOAL>s.ncard = s.toFinset.card
<VAR>α : Type u_1<VAR>s : Set α<VAR>k : ℕ<GOAL>s.encard ≤ ↑k ↔ s.Finite ∧ s.ncard ≤ k
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Infinite<GOAL>s.ncard = 0
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>ht : t.Finite := by toFinite_tac<GOAL>s.ncard ≤ t.ncard
<VAR>α : Type u_1<VAR>Finite α<GOAL>Monotone Set.ncard
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>s.ncard = 0 ↔ s = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>(↑s).ncard = s.card
<VAR>α : Type u_3<GOAL>Set.univ.ncard = Nat.card α
<VAR>α : Type u_3<GOAL>∅.ncard = 0
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>0 < s.ncard ↔ s.Nonempty
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>hs : s.Finite := by toFinite_tac<GOAL>s.ncard ≠ 0
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.ncard ≠ 0<GOAL>s.Finite
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : 0 < s.ncard<GOAL>s.Finite
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.ncard ≠ 0<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>a : α<GOAL>{a}.ncard = 1
<VAR>α : Type u_1<VAR>a : α<VAR>s : Set α<GOAL>({a} ∩ s).ncard ≤ 1
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>h : a ∉ s<VAR>hs : s.Finite := by toFinite_tac<GOAL>(insert a s).ncard = s.ncard + 1
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<GOAL>(insert a s).ncard = s.ncard
<VAR>α : Type u_1<VAR>a : α<VAR>s : Set α<GOAL>(insert a s).ncard ≤ s.ncard + 1
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>Decidable (a ∈ s)<VAR>hs : s.Finite := by toFinite_tac<GOAL>(insert a s).ncard = if a ∈ s then s.ncard else s.ncard + 1
<VAR>α : Type u_1<VAR>a : α<VAR>s : Set α<GOAL>s.ncard ≤ (insert a s).ncard
<VAR>α : Type u_1<VAR>a b : α<VAR>h : a ≠ b<GOAL>{a, b}.ncard = 2
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>hs : s.Finite := by toFinite_tac<GOAL>(s \ {a}).ncard + 1 = s.ncard
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>hs : s.Finite := by toFinite_tac<GOAL>(s \ {a}).ncard = s.ncard - 1
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>hs : s.Finite := by toFinite_tac<GOAL>(s \ {a}).ncard < s.ncard
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<GOAL>(s \ {a}).ncard ≤ s.ncard
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<GOAL>s.ncard - 1 ≤ (s \ {a}).ncard
<VAR>α : Type u_1<VAR>s : Set α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∈ s<GOAL>(insert a (s \ {b})).ncard = s.ncard
<VAR>α : Type u_1<VAR>s : Set α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hb : b ∈ s<GOAL>(insert a s \ {b}).ncard = s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>hs : s.Finite := by toFinite_tac<GOAL>(f '' s).ncard ≤ s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>H : Set.InjOn f s<GOAL>(f '' s).ncard = s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>h : (f '' s).ncard = s.ncard<VAR>hs : s.Finite := by toFinite_tac<GOAL>Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>hs : s.Finite := by toFinite_tac<GOAL>(f '' s).ncard = s.ncard ↔ Set.InjOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>H : Function.Injective f<GOAL>(f '' s).ncard = s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<VAR>H : Function.Injective f<VAR>hs : s ⊆ Set.range f<GOAL>(f ⁻¹' s).ncard = s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>y : β<VAR>hs : s.Finite := by toFinite_tac<GOAL>{x | x ∈ s ∧ f x = y}.ncard ≠ 0 ↔ y ∈ f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α ↪ β<GOAL>(⇑f '' s).ncard = s.ncard
<VAR>α : Type u_1<VAR>P : α → Prop<VAR>s : Set α<GOAL>{x | ↑x ∈ s}.ncard = (s ∩ setOf P).ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>(s ∩ t).ncard ≤ s.ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>ht : t.Finite := by toFinite_tac<GOAL>(s ∩ t).ncard ≤ t.ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>h' : t.ncard ≤ s.ncard<VAR>ht : t.Finite := by toFinite_tac<GOAL>s = t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : t.ncard ≤ s.ncard<VAR>ht : t.Finite := by toFinite_tac<GOAL>s ⊆ t ↔ s = t
<VAR>α : Type u_1<VAR>s : Set α<VAR>f : α ↪ α<VAR>h : ⇑f '' s ⊆ s<VAR>hs : s.Finite := by toFinite_tac<GOAL>⇑f '' s = s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<VAR>P : α → Prop<VAR>h : {x | x ∈ s ∧ P x}.ncard = s.ncard<VAR>ha : a ∈ s<VAR>hs : s.Finite := by toFinite_tac<GOAL>P a
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊂ t<VAR>ht : t.Finite := by toFinite_tac<GOAL>s.ncard < t.ncard
<VAR>α : Type u_1<VAR>Finite α<GOAL>StrictMono Set.ncard
<VAR>α : Type u_1<VAR>s : Set α<VAR>n : ℕ<VAR>f : (i : ℕ) → i < n → α<VAR>hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a<VAR>hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s<VAR>f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j<GOAL>s.ncard = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>h₁ : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>h₂ : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s), f a ha = f b hb → a = b<VAR>h₃ : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b<GOAL>s.ncard = t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>f_inj : Set.InjOn f s<VAR>ht : t.Finite := by toFinite_tac<GOAL>s.ncard ≤ t.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>hc : t.ncard < s.ncard<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>ht : t.Finite := by toFinite_tac<GOAL>∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
<VAR>α : Type u_1<VAR>s : Set α<VAR>n : ℕ<VAR>f : ℕ → α<VAR>hf : ∀ i < n, f i ∈ s<VAR>f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j<VAR>hs : s.Finite := by toFinite_tac<GOAL>n ≤ s.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂<VAR>hst : t.ncard ≤ s.ncard<VAR>ht : t.Finite := by toFinite_tac<VAR>b : β<GOAL>b ∈ t → ∃ a, ∃ (ha : a ∈ s), b = f a ha
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>t : Set β<VAR>f : (a : α) → a ∈ s → β<VAR>hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t<VAR>hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b<VAR>hst : s.ncard ≤ t.ncard<VAR>a₁ : α<VAR>ha₁ : a₁ ∈ s<VAR>a₂ : α<VAR>ha₂ : a₂ ∈ s<VAR>ha₁a₂ : f a₁ ha₁ = f a₂ ha₂<VAR>hs : s.Finite := by toFinite_tac<GOAL>a₁ = a₂
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite := by toFinite_tac<VAR>ht : t.Finite := by toFinite_tac<GOAL>(s ∪ t).ncard + (s ∩ t).ncard = s.ncard + t.ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite := by toFinite_tac<VAR>ht : t.Finite := by toFinite_tac<GOAL>(s ∩ t).ncard + (s ∪ t).ncard = s.ncard + t.ncard
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>(s ∪ t).ncard ≤ s.ncard + t.ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : Disjoint s t<VAR>hs : s.Finite := by toFinite_tac<VAR>ht : t.Finite := by toFinite_tac<GOAL>(s ∪ t).ncard = s.ncard + t.ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>ht : t.Finite := by toFinite_tac<GOAL>(t \ s).ncard + s.ncard = t.ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>ht : t.Finite := by toFinite_tac<GOAL>(t \ s).ncard = t.ncard - s.ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>ht : t.Finite := by toFinite_tac<GOAL>s.ncard ≤ (s \ t).ncard + t.ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>t.ncard - s.ncard ≤ (t \ s).ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite := by toFinite_tac<VAR>ht : t.Finite := by toFinite_tac<GOAL>(s \ t).ncard + t.ncard = (s ∪ t).ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s.ncard < t.ncard<VAR>hs : s.Finite := by toFinite_tac<GOAL>(t \ s).Nonempty
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s.ncard < t.ncard<VAR>hs : s.Finite := by toFinite_tac<GOAL>∃ e ∈ t, e ∉ s
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>(s ∩ t).ncard + (s \ t).ncard = s.ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite := by toFinite_tac<VAR>ht : t.Finite := by toFinite_tac<GOAL>s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite := by toFinite_tac<VAR>ht : t.Finite := by toFinite_tac<GOAL>s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite := by toFinite_tac<VAR>ht : t.Finite := by toFinite_tac<GOAL>s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite := by toFinite_tac<VAR>hsc : sᶜ.Finite := by toFinite_tac<GOAL>s.ncard + sᶜ.ncard = Nat.card α
<VAR>α : Type u_1<VAR>s t : Set α<VAR>n : ℕ<VAR>hst : s ⊆ t<VAR>hsn : s.ncard ≤ n<VAR>hnt : n ≤ t.ncard<GOAL>∃ u, s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
<VAR>α : Type u_1<VAR>s : Set α<VAR>n : ℕ<VAR>hns : n ≤ s.ncard<GOAL>∃ t ⊆ s, t.ncard = n
<VAR>α : Type u_1<VAR>s t : Set α<VAR>i : ℕ<VAR>h₁ : i + s.ncard ≤ t.ncard<VAR>h₂ : s ⊆ t<GOAL>∃ r, s ⊆ r ∧ r ⊆ t ∧ r.ncard = i + s.ncard
<VAR>α : Type u_1<VAR>s t : Set α<VAR>m : ℕ<VAR>hs : s.ncard ≤ m<VAR>ht : m ≤ t.ncard<VAR>h : s ⊆ t<GOAL>∃ r, s ⊆ r ∧ r ⊆ t ∧ r.ncard = m
<VAR>α : Type u_1<VAR>s : Set α<VAR>i : ℕ<VAR>h₁ : i ≤ s.ncard<GOAL>∃ t ⊆ s, t.ncard = i
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Infinite<VAR>k : ℕ<GOAL>∃ t ⊆ s, t.Finite ∧ t.ncard = k
<VAR>α : Type u_1<VAR>s t : Set α<VAR>ht : t.Infinite<VAR>hst : s ⊆ t<VAR>hs : s.Finite<VAR>k : ℕ<VAR>hsk : s.ncard ≤ k<GOAL>∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k
<VAR>α : Type u_1<VAR>s t : Set α<VAR>n : ℕ<VAR>hst : 2 * n < (s ∪ t).ncard<GOAL>∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.ncard = 1 ↔ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>s t : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>(∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>s.ncard ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>s.ncard ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>s.ncard ≤ 1 ↔ s = ∅ ∨ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>s : Set α<VAR>Nonempty α<VAR>hs : s.Finite := by toFinite_tac<GOAL>s.ncard ≤ 1 ↔ ∃ x, s ⊆ {x}
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>s : Set α<GOAL>s.ncard ≤ 1
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>1 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>1 < s.ncard ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>2 < s.ncard ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite := by toFinite_tac<GOAL>2 < s.ncard ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : 1 < s.ncard<VAR>a : α<GOAL>∃ b ∈ s, b ≠ a
<VAR>α : Type u_1<VAR>s : Set α<VAR>n : ℕ<VAR>h : s.ncard = n + 1<GOAL>∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n
<VAR>α : Type u_1<VAR>s : Set α<VAR>n : ℕ<VAR>hs : s.Finite := by toFinite_tac<GOAL>s.ncard = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.ncard = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.ncard = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
<VAR>α : Type u_1<VAR>A B : Set (Finset α)<VAR>r : ℕ<VAR>h : A ⊆ B<VAR>hB : Set.Sized r B<GOAL>Set.Sized r A
<VAR>α : Type u_1<VAR>r : ℕ<GOAL>Set.Sized r ∅
<VAR>α : Type u_1<VAR>s : Finset α<VAR>r : ℕ<GOAL>Set.Sized r {s} ↔ s.card = r
<VAR>α : Type u_1<VAR>A B : Set (Finset α)<VAR>r : ℕ<GOAL>Set.Sized r (A ∪ B) ↔ Set.Sized r A ∧ Set.Sized r B
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>r : ℕ<VAR>f : ι → Set (Finset α)<GOAL>Set.Sized r (⋃ i, f i) ↔ ∀ (i : ι), Set.Sized r (f i)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>r : ℕ<VAR>f : (i : ι) → κ i → Set (Finset α)<GOAL>Set.Sized r (⋃ i, ⋃ j, f i j) ↔ ∀ (i : ι) (j : κ i), Set.Sized r (f i j)
<VAR>α : Type u_1<VAR>A : Set (Finset α)<VAR>r : ℕ<VAR>hA : Set.Sized r A<GOAL>IsAntichain (fun x x_1 => x ⊆ x_1) A
<VAR>α : Type u_1<VAR>A : Set (Finset α)<VAR>hA : Set.Sized 0 A<GOAL>A.Subsingleton
<VAR>α : Type u_1<VAR>A : Set (Finset α)<VAR>Fintype α<VAR>hA : Set.Sized (Fintype.card α) A<GOAL>A.Subsingleton
<VAR>α : Type u_1<VAR>A : Set (Finset α)<VAR>r : ℕ<VAR>hA : Set.Sized r A<GOAL>∅ ∈ A ↔ A = {∅}
<VAR>α : Type u_1<VAR>A : Set (Finset α)<VAR>r : ℕ<VAR>Fintype α<VAR>hA : Set.Sized r A<GOAL>Finset.univ ∈ A ↔ A = {Finset.univ}
<VAR>α : Type u_1<VAR>s : Finset α<VAR>r : ℕ<GOAL>Set.Sized r ↑(Finset.powersetCard r s)
<VAR>α : Type u_1<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<GOAL>𝒜 ⊆ Finset.powersetCard r Finset.univ ↔ Set.Sized r ↑𝒜
<VAR>α : Type u_1<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<VAR>h𝒜 : Set.Sized r ↑𝒜<GOAL>𝒜.card ≤ (Fintype.card α).choose r
<VAR>α : Type u_1<VAR>𝒜 : Finset (Finset α)<VAR>A : Finset α<VAR>r : ℕ<GOAL>A ∈ 𝒜 # r ↔ A ∈ 𝒜 ∧ A.card = r
<VAR>α : Type u_1<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<GOAL>𝒜 # r ⊆ 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Finset (Finset α)<VAR>r : ℕ<GOAL>Set.Sized r ↑(𝒜 # r)
<VAR>α : Type u_1<VAR>𝒜 : Finset (Finset α)<VAR>A : Finset α<VAR>r₁ r₂ : ℕ<VAR>h₁ : A ∈ 𝒜 # r₁<VAR>h₂ : A ∈ 𝒜 # r₂<GOAL>r₁ = r₂
<VAR>α : Type u_1<VAR>𝒜 : Finset (Finset α)<VAR>A₁ A₂ : Finset α<VAR>r₁ r₂ : ℕ<VAR>h₁ : A₁ ∈ 𝒜 # r₁<VAR>h₂ : A₂ ∈ 𝒜 # r₂<GOAL>r₁ ≠ r₂ → A₁ ≠ A₂
<VAR>α : Type u_1<VAR>𝒜 : Finset (Finset α)<GOAL>Set.univ.PairwiseDisjoint 𝒜.slice
<VAR>α : Type u_1<VAR>𝒜 : Finset (Finset α)<VAR>Fintype α<VAR>DecidableEq α<GOAL>(Finset.Iic (Fintype.card α)).biUnion 𝒜.slice = 𝒜
<VAR>α : Type u_1<VAR>𝒜 : Finset (Finset α)<VAR>Fintype α<GOAL>∑ r ∈ Finset.Iic (Fintype.card α), (𝒜 # r).card = 𝒜.card
<VAR>m n : ℕ<GOAL>(m * n).divisors = m.divisors * n.divisors
<VAR>n : ℕ<GOAL>Nat.divisorsHom n = n.divisors
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>(p ^ 2).divisors = {p ^ 2, p, 1}
<VAR>l : List ℕ<GOAL>l.prod.divisors = (List.map Nat.divisors l).prod
<VAR>s : Multiset ℕ<GOAL>s.prod.divisors = (Multiset.map Nat.divisors s).prod
<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>f : ι → ℕ<GOAL>(∏ i ∈ s, f i).divisors = ∏ i ∈ s, (f i).divisors
<VAR>α : Type u<VAR>r : α → α → Prop<VAR>IsTrans α r<VAR>ι : Type u_1<VAR>hι : Nonempty ι<VAR>f : ι → α<VAR>D : Directed r f<VAR>s : Finset ι<GOAL>∃ z, ∀ i ∈ s, r (f i) (f z)
<VAR>α : Type u<VAR>Nonempty α<VAR>Preorder α<VAR>IsDirected α fun x x_1 => x ≤ x_1<VAR>s : Finset α<GOAL>∃ M, ∀ i ∈ s, i ≤ M
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset ι<VAR>f : ι →₀ α<VAR>t : ι → Finset α<GOAL>f ∈ s.finsupp t ↔ f.support ⊆ s ∧ ∀ i ∈ s, f i ∈ t i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset ι<VAR>f : ι →₀ α<VAR>t : ι →₀ Finset α<VAR>ht : t.support ⊆ s<GOAL>f ∈ s.finsupp ⇑t ↔ ∀ (i : ι), f i ∈ t i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset ι<VAR>t : ι → Finset α<GOAL>(s.finsupp t).card = ∏ i ∈ s, (t i).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>f : ι →₀ Finset α<VAR>g : ι →₀ α<GOAL>g ∈ f.pi ↔ ∀ (i : ι), g i ∈ f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>Zero α<VAR>f : ι →₀ Finset α<GOAL>f.pi.card = f.prod fun i => ↑(f i).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<GOAL>Finset.fold op b f ∅ = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>Finset.fold op b f (Finset.cons a s h) = op (f a) (Finset.fold op b f s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>h : a ∉ s<GOAL>Finset.fold op b f (insert a s) = op (f a) (Finset.fold op b f s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>a : α<GOAL>Finset.fold op b f {a} = op (f a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>g : γ ↪ α<VAR>s : Finset γ<GOAL>Finset.fold op b f (Finset.map g s) = Finset.fold op b (f ∘ ⇑g) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>DecidableEq α<VAR>g : γ → α<VAR>s : Finset γ<VAR>H : ∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y<GOAL>Finset.fold op b f (Finset.image g s) = Finset.fold op b (f ∘ g) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>g : α → β<VAR>H : ∀ x ∈ s, f x = g x<GOAL>Finset.fold op b f s = Finset.fold op b g s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>s : Finset α<VAR>f g : α → β<VAR>b₁ b₂ : β<GOAL>Finset.fold op (op b₁ b₂) (fun x => op (f x) (g x)) s = op (Finset.fold op b₁ f s) (Finset.fold op b₂ g s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>b : β<VAR>s : Finset α<VAR>hd : Decidable (s = ∅)<VAR>c : β<VAR>h : op c (op b c) = op b c<GOAL>Finset.fold op b (fun x => c) s = if s = ∅ then b else op b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>op' : γ → γ → γ<VAR>Std.Commutative op'<VAR>Std.Associative op'<VAR>m : β → γ<VAR>hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)<GOAL>Finset.fold op' (m b) (fun x => m (f x)) s = m (Finset.fold op b f s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>s₁ s₂ : Finset α<VAR>b₁ b₂ : β<VAR>h : Disjoint s₁ s₂<GOAL>Finset.fold op (op b₁ b₂) f (s₁.disjUnion s₂ h) = op (Finset.fold op b₁ f s₁) (Finset.fold op b₂ f s₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>t : ι → Finset α<VAR>b : ι → β<VAR>b₀ : β<VAR>h : (↑s).PairwiseDisjoint t<GOAL>Finset.fold op (Finset.fold op b₀ b s) f (s.disjiUnion t h) = Finset.fold op b₀ (fun i => Finset.fold op (b i) f (t i)) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>b₁ b₂ : β<GOAL>op (Finset.fold op b₁ f (s₁ ∪ s₂)) (Finset.fold op b₂ f (s₁ ∩ s₂)) = op (Finset.fold op b₂ f s₁) (Finset.fold op b₁ f s₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>hi : Std.IdempotentOp op<GOAL>Finset.fold op b f (insert a s) = op (f a) (Finset.fold op b f s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>DecidableEq α<VAR>g : γ → α<VAR>s : Finset γ<VAR>hi : Std.IdempotentOp op<GOAL>Finset.fold op b f (Finset.image g s) = Finset.fold op b (f ∘ g) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>g : α → β<VAR>hb : op b b = b<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Finset.fold op b (fun i => if p i then f i else g i) s = op (Finset.fold op b f (Finset.filter p s)) (Finset.fold op b g (Finset.filter (fun i => ¬p i) s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>Std.IdempotentOp op<VAR>g : α → β<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>Finset.fold op b (fun i => if p i then f i else g i) s = op (Finset.fold op b f (Finset.filter p s)) (Finset.fold op b g (Finset.filter (fun i => ¬p i) s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>r : β → β → Prop<VAR>hr : ∀ {x y z : β}, r x (op y z) ↔ r x y ∧ r x z<VAR>c : β<GOAL>r c (Finset.fold op b f s) ↔ r c b ∧ ∀ x ∈ s, r c (f x)