ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>s : Finset α<VAR>f g : α → β<VAR>comm_ff : (↑s).Pairwise fun x y => Commute (f x) (f y)<VAR>comm_gg : (↑s).Pairwise fun x y => Commute (g x) (g y)<VAR>comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)<GOAL>(↑s).Pairwise fun x y => Commute ((f * g) x) ((f * g) y)
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Monoid β<VAR>s : Finset α<VAR>f g : α → β<VAR>comm_ff : (↑s).Pairwise fun x y => Commute (f x) (f y)<VAR>comm_gg : (↑s).Pairwise fun x y => Commute (g x) (g y)<VAR>comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)<GOAL>s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>AddMonoid β<VAR>s : Finset α<VAR>f g : α → β<VAR>comm_ff : (↑s).Pairwise fun x y => AddCommute (f x) (f y)<VAR>comm_gg : (↑s).Pairwise fun x y => AddCommute (g x) (g y)<VAR>comm_gf : (↑s).Pairwise fun x y => AddCommute (g x) (f y)<GOAL>s.noncommSum (f + g) ⋯ = s.noncommSum f comm_ff + s.noncommSum g comm_gg
<VAR>ι : Type u_2<VAR>M : ι → Type u_6<VAR>(i : ι) → Monoid (M i)<VAR>Fintype ι<VAR>DecidableEq ι<VAR>x : (i : ι) → M i<GOAL>Finset.univ.noncommProd (fun i => Pi.mulSingle i (x i)) ⋯ = x
<VAR>ι : Type u_2<VAR>M : ι → Type u_6<VAR>(i : ι) → AddMonoid (M i)<VAR>Fintype ι<VAR>DecidableEq ι<VAR>x : (i : ι) → M i<GOAL>Finset.univ.noncommSum (fun i => Pi.single i (x i)) ⋯ = x
<VAR>ι : Type u_2<VAR>γ : Type u_5<VAR>Monoid γ<VAR>M : ι → Type u_6<VAR>(i : ι) → Monoid (M i)<VAR>Finite ι<VAR>DecidableEq ι<VAR>f g : ((i : ι) → M i) →* γ<VAR>h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)<GOAL>f = g
<VAR>ι : Type u_2<VAR>γ : Type u_5<VAR>AddMonoid γ<VAR>M : ι → Type u_6<VAR>(i : ι) → AddMonoid (M i)<VAR>Finite ι<VAR>DecidableEq ι<VAR>f g : ((i : ι) → M i) →+ γ<VAR>h : ∀ (i : ι) (x : M i), f (Pi.single i x) = g (Pi.single i x)<GOAL>f = g
<VAR>α : Type u_1<GOAL>(Matroid.emptyOn α).E = ∅
<VAR>α : Type u_1<VAR>B : Set α<GOAL>(Matroid.emptyOn α).Base B ↔ B = ∅
<VAR>α : Type u_1<VAR>I : Set α<GOAL>(Matroid.emptyOn α).Indep I ↔ I = ∅
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.E = ∅ ↔ M = Matroid.emptyOn α
<VAR>α : Type u_1<GOAL>(Matroid.emptyOn α)✶ = Matroid.emptyOn α
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.restrict ∅ = Matroid.emptyOn α
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M = Matroid.emptyOn α ∨ M.Nonempty
<VAR>α : Type u_1<VAR>IsEmpty α<VAR>M : Matroid α<GOAL>M = Matroid.emptyOn α
<VAR>α : Type u_1<VAR>E : Set α<GOAL>(Matroid.loopyOn E).E = E
<VAR>α : Type u_2<GOAL>Matroid.loopyOn ∅ = Matroid.emptyOn α
<VAR>α : Type u_1<VAR>E I : Set α<GOAL>(Matroid.loopyOn E).Indep I ↔ I = ∅
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E : Set α<GOAL>M = Matroid.loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅
<VAR>α : Type u_1<VAR>E B : Set α<GOAL>(Matroid.loopyOn E).Base B ↔ B = ∅
<VAR>α : Type u_1<VAR>E I X : Set α<GOAL>(Matroid.loopyOn E).Basis I X ↔ I = ∅ ∧ X ⊆ E
<VAR>α : Type u_1<VAR>E : Set α<VAR>hE : E.Finite<GOAL>(Matroid.loopyOn E).Finite
<VAR>α : Type u_1<VAR>E R : Set α<GOAL>(Matroid.loopyOn E).restrict R = Matroid.loopyOn R
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.Base ∅ ↔ M = Matroid.loopyOn M.E
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M = Matroid.loopyOn M.E ∨ M.RkPos
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>¬M.RkPos ↔ M = Matroid.loopyOn M.E
<VAR>α : Type u_1<VAR>E : Set α<GOAL>(Matroid.freeOn E).E = E
<VAR>α : Type u_1<VAR>E : Set α<GOAL>(Matroid.freeOn E)✶ = Matroid.loopyOn E
<VAR>α : Type u_1<VAR>E : Set α<GOAL>(Matroid.loopyOn E)✶ = Matroid.freeOn E
<VAR>α : Type u_2<GOAL>Matroid.freeOn ∅ = Matroid.emptyOn α
<VAR>α : Type u_1<VAR>E B : Set α<GOAL>(Matroid.freeOn E).Base B ↔ B = E
<VAR>α : Type u_1<VAR>E I : Set α<GOAL>(Matroid.freeOn E).Indep I ↔ I ⊆ E
<VAR>α : Type u_1<VAR>E I : Set α<VAR>hIE : I ⊆ E<GOAL>(Matroid.freeOn E).Indep I
<VAR>α : Type u_1<VAR>E I X : Set α<GOAL>(Matroid.freeOn E).Basis I X ↔ I = X ∧ X ⊆ E
<VAR>α : Type u_1<VAR>E I X : Set α<GOAL>(Matroid.freeOn E).Basis' I X ↔ I = X ∩ E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E : Set α<GOAL>M = Matroid.freeOn E ↔ M.E = E ∧ M.Indep E
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.Indep M.E ↔ M = Matroid.freeOn M.E
<VAR>α : Type u_1<VAR>E R : Set α<VAR>h : R ⊆ E<GOAL>(Matroid.freeOn E).restrict R = Matroid.freeOn R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<GOAL>M.restrict I = Matroid.freeOn I ↔ M.Indep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>M.restrict I = Matroid.freeOn I
<VAR>α : Type u_1<VAR>E I : Set α<GOAL>(Matroid.uniqueBaseOn I E).E = E
<VAR>α : Type u_1<VAR>E B I : Set α<VAR>hIE : I ⊆ E<GOAL>(Matroid.uniqueBaseOn I E).Base B ↔ B = I
<VAR>α : Type u_1<VAR>I E : Set α<GOAL>Matroid.uniqueBaseOn (I ∩ E) E = Matroid.uniqueBaseOn I E
<VAR>α : Type u_1<VAR>E I J : Set α<GOAL>(Matroid.uniqueBaseOn I E).Indep J ↔ J ⊆ I ∩ E
<VAR>α : Type u_1<VAR>E I J : Set α<VAR>hIE : I ⊆ E<GOAL>(Matroid.uniqueBaseOn I E).Indep J ↔ J ⊆ I
<VAR>α : Type u_1<VAR>E I X J : Set α<VAR>hI : I ⊆ E<VAR>hX : X ⊆ E<GOAL>(Matroid.uniqueBaseOn I E).Basis J X ↔ J = X ∩ I
<VAR>α : Type u_1<VAR>E I X : Set α<VAR>hI : I ⊆ E<VAR>hX : X ⊆ E<GOAL>(Matroid.uniqueBaseOn I E).Basis (X ∩ I) X
<VAR>α : Type u_1<VAR>I E : Set α<GOAL>(Matroid.uniqueBaseOn I E)✶ = Matroid.uniqueBaseOn (E \ I) E
<VAR>α : Type u_1<VAR>I : Set α<GOAL>Matroid.uniqueBaseOn I I = Matroid.freeOn I
<VAR>α : Type u_1<VAR>I : Set α<GOAL>Matroid.uniqueBaseOn ∅ I = Matroid.loopyOn I
<VAR>α : Type u_1<VAR>I E R : Set α<GOAL>(Matroid.uniqueBaseOn I E).restrict R = Matroid.uniqueBaseOn (I ∩ R ∩ E) R
<VAR>α : Type u_1<VAR>E I : Set α<VAR>h : I ⊆ E<VAR>R : Set α<GOAL>(Matroid.uniqueBaseOn I E).restrict R = Matroid.uniqueBaseOn (I ∩ R) R
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.card = Multiset.card s.val
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Multiset.card s.val = s.card
<VAR>α : Type u_1<VAR>m : Multiset α<VAR>nodup : m.Nodup<GOAL>{ val := m, nodup := nodup }.card = Multiset.card m
<VAR>α : Type u_1<GOAL>∅.card = 0
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s ⊆ t → s.card ≤ t.card
<VAR>α : Type u_1<GOAL>Monotone Finset.card
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.card = 0 ↔ s = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.card ≠ 0 ↔ s.Nonempty
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>0 < s.card ↔ s.Nonempty
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>1 ≤ s.card ↔ s.Nonempty
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ s<GOAL>s.card ≠ 0
<VAR>α : Type u_1<VAR>a : α<GOAL>{a}.card = 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<GOAL>({a} ∩ s).card ≤ 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>(Finset.cons a s h).card = s.card + 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>h : a ∉ s<GOAL>(insert a s).card = s.card + 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<VAR>h : a ∈ s<GOAL>(insert a s).card = s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(insert a s).card ≤ s.card + 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>{a, b}.card ≤ 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b c : α<GOAL>{a, b, c}.card ≤ 3
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b c d : α<GOAL>{a, b, c, d}.card ≤ 4
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b c d e : α<GOAL>{a, b, c, d, e}.card ≤ 5
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b c d e f : α<GOAL>{a, b, c, d, e, f}.card ≤ 6
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<GOAL>(insert a s).card = if a ∈ s then s.card else s.card + 1
<VAR>α : Type u_1<VAR>a b : α<VAR>DecidableEq α<GOAL>{a, b}.card = 1 ∨ {a, b}.card = 2
<VAR>α : Type u_1<VAR>a b : α<VAR>DecidableEq α<VAR>h : a ≠ b<GOAL>{a, b}.card = 2
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<GOAL>a ∈ s → (s.erase a).card = s.card - 1
<VAR>α : Type u_1<VAR>a : α<VAR>DecidableEq α<VAR>R : Type u_4<VAR>AddGroupWithOne R<VAR>s : Finset α<VAR>hs : a ∈ s<GOAL>↑(s.erase a).card = ↑s.card - 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<GOAL>a ∈ s → (s.erase a).card + 1 = s.card
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<GOAL>a ∈ s → (s.erase a).card < s.card
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<GOAL>(s.erase a).card ≤ s.card
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<GOAL>s.card - 1 ≤ (s.erase a).card
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>DecidableEq α<GOAL>(s.erase a).card = if a ∈ s then s.card - 1 else s.card
<VAR>n : ℕ<GOAL>(Finset.range n).card = n
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.attach.card = s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>m.toFinset.card = Multiset.card m.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>m.toFinset.card ≤ Multiset.card m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<VAR>h : m.Nodup<GOAL>m.toFinset.card = Multiset.card m
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>Multiset.card m.dedup = Multiset.card m ↔ m.Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>m : Multiset α<GOAL>m.toFinset.card = Multiset.card m ↔ m.Nodup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.toFinset.card = l.dedup.length
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>l.toFinset.card ≤ l.length
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>h : l.Nodup<GOAL>l.toFinset.card = l.length
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.toList.length = s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → β<VAR>DecidableEq β<GOAL>(Finset.image f s).card ≤ s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → β<VAR>DecidableEq β<VAR>H : Set.InjOn f ↑s<GOAL>(Finset.image f s).card = s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → β<VAR>DecidableEq β<VAR>H : (Finset.image f s).card = s.card<GOAL>Set.InjOn f ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → β<VAR>DecidableEq β<GOAL>(Finset.image f s).card = s.card ↔ Set.InjOn f ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>DecidableEq β<VAR>s : Finset α<VAR>H : Function.Injective f<GOAL>(Finset.image f s).card = s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → β<VAR>DecidableEq β<VAR>y : β<GOAL>(Finset.filter (fun x => f x = y) s).card ≠ 0 ↔ y ∈ Finset.image f s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>P : α → Prop<VAR>DecidablePred P<VAR>n : ℕ<GOAL>(Finset.filter P s).card ≤ n ↔ ∀ s' ⊆ s, n < s'.card → ∃ a ∈ s', ¬P a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α ↪ β<GOAL>(Finset.map f s).card = s.card
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : Finset α<GOAL>(Finset.subtype p s).card = (Finset.filter p s).card
<VAR>α : Type u_1<VAR>s : Finset α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>(Finset.filter p s).card ≤ s.card
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>h : s ⊆ t<VAR>h₂ : t.card ≤ s.card<GOAL>s = t
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>hst : s ⊆ t<VAR>hts : t.card ≤ s.card<GOAL>t = s
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>h : t.card ≤ s.card<GOAL>s ⊆ t ↔ s = t
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α ↪ α<VAR>hs : Finset.map f s ⊆ s<GOAL>Finset.map f s = s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>h : (Finset.filter p s).card = s.card<VAR>x : α<VAR>hx : x ∈ s<GOAL>p x
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>h : s ⊂ t<GOAL>s.card < t.card
<VAR>α : Type u_1<GOAL>StrictMono Finset.card
<VAR>α : Type u_1<VAR>s : Finset α<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.card = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>i : (a : α) → a ∈ s → β<VAR>hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t<VAR>i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂<VAR>i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b<GOAL>s.card = t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>i : (a : α) → a ∈ s → β<VAR>j : (a : β) → a ∈ t → α<VAR>hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t<VAR>hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s<VAR>left_inv : ∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a<VAR>right_inv : ∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a<GOAL>s.card = t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>i : α → β<VAR>hi : ∀ a ∈ s, i a ∈ t<VAR>i_inj : Set.InjOn i ↑s<VAR>i_surj : Set.SurjOn i ↑s ↑t<GOAL>s.card = t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>i : α → β<VAR>j : β → α<VAR>hi : ∀ a ∈ s, i a ∈ t<VAR>hj : ∀ a ∈ t, j a ∈ s<VAR>left_inv : ∀ a ∈ s, j (i a) = a<VAR>right_inv : ∀ a ∈ t, i (j a) = a<GOAL>s.card = t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>e : α ≃ β<VAR>hst : ∀ (i : α), i ∈ s ↔ e i ∈ t<GOAL>s.card = t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>e : α → β<VAR>he : Function.Bijective e<VAR>hst : ∀ (i : α), i ∈ s ↔ e i ∈ t<GOAL>s.card = t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<VAR>f_inj : Set.InjOn f ↑s<GOAL>s.card ≤ t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → β<VAR>hf : Set.SurjOn f ↑s ↑t<GOAL>t.card ≤ s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<VAR>hc : t.card < s.card<VAR>f : α → β<VAR>hf : ∀ a ∈ s, f a ∈ t<GOAL>∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ f x = f y
<VAR>α : Type u_1<VAR>s : Finset α<VAR>n : ℕ<VAR>f : ℕ → α<VAR>hf : ∀ i < n, f i ∈ s<VAR>f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j<GOAL>n ≤ s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<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.card ≤ s.card<VAR>b : β<GOAL>b ∈ t → ∃ a, ∃ (ha : a ∈ s), b = f a ha
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Finset α<VAR>t : Finset β<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.card ≤ t.card<VAR>a₁ : α<VAR>ha₁ : a₁ ∈ s<VAR>a₂ : α<VAR>ha₂ : a₂ ∈ s<VAR>ha₁a₂ : f a₁ ha₁ = f a₂ ha₂<GOAL>a₁ = a₂
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>h : Disjoint s t<GOAL>(s.disjUnion t h).card = s.card + t.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t).card + (s ∩ t).card = s.card + t.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).card + (s ∪ t).card = s.card + t.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t).card = s.card + t.card - (s ∩ t).card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).card = s.card + t.card - (s ∪ t).card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t).card ≤ s.card + t.card
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>(s ∪ t).card = s.card + t.card ↔ Disjoint s t
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>s t : Finset α<VAR>DecidableEq α<VAR>AddGroupWithOne R<GOAL>↑(s ∩ t).card = ↑s.card + ↑t.card - ↑(s ∪ t).card
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>s t : Finset α<VAR>DecidableEq α<VAR>AddGroupWithOne R<GOAL>↑(s ∪ t).card = ↑s.card + ↑t.card - ↑(s ∩ t).card
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>DecidableEq α<VAR>h : s ⊆ t<GOAL>(t \ s).card = t.card - s.card
<VAR>α : Type u_1<VAR>R : Type u_3<VAR>s t : Finset α<VAR>DecidableEq α<VAR>AddGroupWithOne R<VAR>h : s ⊆ t<GOAL>↑(t \ s).card = ↑t.card - ↑s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>(t \ s).card + s.card = t.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>t.card - s.card ≤ (t \ s).card
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>s.card ≤ (s \ t).card + t.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s \ t).card + t.card = (s ∪ t).card
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>DecidableEq α<VAR>h : s.card = t.card<GOAL>(s \ t).card = (t \ s).card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s \ t).card + (s ∩ t).card = s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).card + (s \ t).card = s.card
<VAR>α : Type u_1<VAR>s t u : Finset α<VAR>DecidableEq α<VAR>hts : t ⊆ s<VAR>hus : u ⊆ s<VAR>hstu : s.card < t.card + u.card<GOAL>(t ∩ u).Nonempty
<VAR>α : Type u_1<VAR>s : Finset α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>(x : α) → Decidable ¬p x<GOAL>(Finset.filter p s).card + (Finset.filter (fun a => ¬p a) s).card = s.card
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>n : ℕ<VAR>hst : s ⊆ t<VAR>hsn : s.card ≤ n<VAR>hnt : n ≤ t.card<GOAL>∃ u, s ⊆ u ∧ u ⊆ t ∧ u.card = n
<VAR>α : Type u_1<VAR>s : Finset α<VAR>n : ℕ<VAR>hns : n ≤ s.card<GOAL>∃ t ⊆ s, t.card = n
<VAR>α : Type u_1<VAR>A B : Finset α<VAR>i : ℕ<VAR>h₁ : i + B.card ≤ A.card<VAR>h₂ : B ⊆ A<GOAL>∃ C, B ⊆ C ∧ C ⊆ A ∧ C.card = i + B.card
<VAR>α : Type u_1<VAR>A : Finset α<VAR>i : ℕ<VAR>h₁ : i ≤ A.card<GOAL>∃ B ⊆ A, B.card = i
<VAR>α : Type u_1<VAR>s : Finset α<VAR>n : ℕ<GOAL>n ≤ s.card ↔ ∃ t ⊆ s, t.card = n
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>X Y : Finset α<VAR>n : ℕ<VAR>hXY : 2 * n < (X ∪ Y).card<GOAL>∃ C, n < C.card ∧ (C ⊆ X ∨ C ⊆ Y)
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.card = 1 ↔ ∃ a, s = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.toFinset.card = 1 ↔ Multiset.card s ≠ 0 ∧ ∃ a, s = Multiset.card s • {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.card + 1 = t.card
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.card ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.card ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.card ≤ 1 ↔ Subsingleton { x // x ∈ s }
<VAR>α : Type u_1<VAR>s : Finset α<VAR>Nonempty α<GOAL>s.card ≤ 1 ↔ ∃ x, s ⊆ {x}
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : 1 < s.card<VAR>a : α<GOAL>∃ b ∈ s, b ≠ a
<VAR>α : Type u_1<VAR>Subsingleton α<VAR>s : Finset α<GOAL>s.card ≤ 1
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>1 < s.card ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>1 < s.card ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>1 < s.card ↔ s.Nontrivial
<VAR>ι : Type u_4<VAR>α : ι → Type u_5<VAR>(i : ι) → DecidableEq (α i)<VAR>s : Finset ((i : ι) → α i)<VAR>h : 1 < s.card<GOAL>∃ i, 1 < (Finset.image (fun x => x i) s).card ∧ ∀ (ai : α i), Finset.filter (fun x => x i = ai) s ⊂ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>n : ℕ<VAR>DecidableEq α<GOAL>s.card = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ t.card = n
<VAR>α : Type u_1<VAR>s : Finset α<VAR>DecidableEq α<GOAL>s.card = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y}
<VAR>α : Type u_1<VAR>s : Finset α<VAR>DecidableEq α<GOAL>s.card = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>2 < s.card ↔ ∃ a b c, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>2 < s.card ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c
<VAR>α : Type u_1<VAR>p : Finset α → Sort u_4<VAR>H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s<VAR>s : Finset α<GOAL>Finset.strongInduction H s = H s fun t x => Finset.strongInduction H t
<VAR>α : Type u_1<VAR>p : Finset α → Sort u_4<VAR>s : Finset α<VAR>H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s<GOAL>s.strongInductionOn H = H s fun t x => t.strongInductionOn H
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>p : Finset α → Prop<VAR>s : Finset α<VAR>h₀ : p ∅<VAR>h₁ : ∀ (a : α) (s : Finset α), a ∉ s → (∀ t ⊆ s, p t) → p (insert a s)<GOAL>p s
<VAR>α : Type u_1<VAR>p : (s : Finset α) → s.Nonempty → Prop<VAR>h₀ : ∀ (a : α), p {a} ⋯<VAR>h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>p s hs
<VAR>α : Type u_1<VAR>n : ℕ<VAR>p : Finset α → Sort u_4<VAR>H : (t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁<VAR>s : Finset α<GOAL>Finset.strongDownwardInduction H s = H s fun {t} ht x => Finset.strongDownwardInduction H t ht
<VAR>α : Type u_1<VAR>n : ℕ<VAR>p : Finset α → Sort u_4<VAR>s : Finset α<VAR>H : (t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁<GOAL>(fun a => s.strongDownwardInductionOn H a) = H s fun {t} ht x => t.strongDownwardInductionOn H ht
<VAR>α : Type u_4<GOAL>WellFounded LT.lt
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>R : Type u_5<VAR>m : Matrix I J (Matrix K L R)<VAR>ik : I × K<VAR>jl : J × L<GOAL>(Matrix.comp I J K L R) m ik jl = m ik.1 jl.1 ik.2 jl.2
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>R : Type u_5<VAR>n : Matrix (I × K) (J × L) R<VAR>i : I<VAR>j : J<VAR>k : K<VAR>l : L<GOAL>(Matrix.comp I J K L R).symm n i j k l = n (i, k) (j, l)
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>R : Type u_5<VAR>AddCommMonoid R<VAR>m : Matrix I J (Matrix K L R)<VAR>ik : I × K<VAR>jl : J × L<GOAL>(Matrix.compAddEquiv I J K L R) m ik jl = m ik.1 jl.1 ik.2 jl.2
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>R : Type u_5<VAR>AddCommMonoid R<VAR>n : Matrix (I × K) (J × L) R<VAR>i : I<VAR>j : J<VAR>k : K<VAR>l : L<GOAL>(Matrix.compAddEquiv I J K L R).symm n i j k l = n (i, k) (j, l)
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>Fintype I<VAR>Fintype J<VAR>m : Matrix I I (Matrix J J R)<VAR>ik jl : I × J<GOAL>(Matrix.compRingEquiv I J R) m ik jl = m ik.1 jl.1 ik.2 jl.2
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>R : Type u_5<VAR>Semiring R<VAR>Fintype I<VAR>Fintype J<VAR>n : Matrix (I × J) (I × J) R<VAR>i j : I<VAR>k l : J<GOAL>(Matrix.compRingEquiv I J R).symm n i j k l = n (i, k) (j, l)
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>L : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>CommSemiring K<VAR>AddCommMonoid R<VAR>Module K R<GOAL>∀ (a : Matrix (I × K) (J × L) R), (Matrix.compLinearEquiv I J L R K).symm a = (Matrix.compAddEquiv I J K L R).symm a
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>L : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>CommSemiring K<VAR>AddCommMonoid R<VAR>Module K R<GOAL>∀ (a : Matrix I J (Matrix K L R)), (Matrix.compLinearEquiv I J L R K) a = (Matrix.compAddEquiv I J K L R) a
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>R : Type u_5<VAR>K : Type u_6<VAR>CommSemiring K<VAR>Semiring R<VAR>Fintype I<VAR>Fintype J<VAR>Algebra K R<VAR>DecidableEq I<VAR>DecidableEq J<VAR>n : Matrix (I × J) (I × J) R<VAR>i j : I<VAR>k l : J<GOAL>(Matrix.compAlgEquiv I J R K).symm n i j k l = n (i, k) (j, l)
<VAR>I : Type u_1<VAR>J : Type u_2<VAR>R : Type u_5<VAR>K : Type u_6<VAR>CommSemiring K<VAR>Semiring R<VAR>Fintype I<VAR>Fintype J<VAR>Algebra K R<VAR>DecidableEq I<VAR>DecidableEq J<VAR>m : Matrix I I (Matrix J J R)<VAR>ik jl : I × J<GOAL>(Matrix.compAlgEquiv I J R K) m ik jl = m ik.1 jl.1 ik.2 jl.2
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>w : m → α<VAR>i : m<VAR>j : ι<GOAL>Matrix.col ι w i j = w i
<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_6<VAR>v : n → α<VAR>i : ι<VAR>j : n<GOAL>Matrix.row ι v i j = v j
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>Nonempty ι<GOAL>Function.Injective (Matrix.col ι)
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>Nonempty ι<VAR>v w : m → α<GOAL>Matrix.col ι v = Matrix.col ι w ↔ v = w
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>Zero α<GOAL>Matrix.col ι 0 = 0
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>Zero α<VAR>Nonempty ι<VAR>v : m → α<GOAL>Matrix.col ι v = 0 ↔ v = 0
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>Add α<VAR>v w : m → α<GOAL>Matrix.col ι (v + w) = Matrix.col ι v + Matrix.col ι w
<VAR>m : Type u_2<VAR>R : Type u_5<VAR>α : Type v<VAR>ι : Type u_6<VAR>SMul R α<VAR>x : R<VAR>v : m → α<GOAL>Matrix.col ι (x • v) = x • Matrix.col ι v
<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_6<VAR>Nonempty ι<GOAL>Function.Injective (Matrix.row ι)
<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_6<VAR>Nonempty ι<VAR>v w : n → α<GOAL>Matrix.row ι v = Matrix.row ι w ↔ v = w
<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_6<VAR>Zero α<GOAL>Matrix.row ι 0 = 0
<VAR>n : Type u_3<VAR>α : Type v<VAR>ι : Type u_6<VAR>Zero α<VAR>Nonempty ι<VAR>v : n → α<GOAL>Matrix.row ι v = 0 ↔ v = 0
<VAR>m : Type u_2<VAR>α : Type v<VAR>ι : Type u_6<VAR>Add α<VAR>v w : m → α<GOAL>Matrix.row ι (v + w) = Matrix.row ι v + Matrix.row ι w