ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>s : Finset α<GOAL>s.compls = ∅ ↔ s = ∅
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>a : α<GOAL>{a}.compls = {aᶜ}
<VAR>α : Type u_2<VAR>BooleanAlgebra α<VAR>Fintype α<GOAL>Finset.univ.compls = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>BooleanAlgebra α<VAR>s t : Finset α<GOAL>(s ∪ t).compls = s.compls ∪ t.compls
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>BooleanAlgebra α<VAR>s t : Finset α<GOAL>(s ∩ t).compls = s.compls ∩ t.compls
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>BooleanAlgebra α<VAR>s t : Finset α<GOAL>(s ⊼ t).compls = s.compls ⊻ t.compls
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>BooleanAlgebra α<VAR>s t : Finset α<GOAL>(s ⊻ t).compls = s.compls ⊼ t.compls
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>BooleanAlgebra α<VAR>s t : Finset α<GOAL>s ⊼ t.compls = s.diffs t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>BooleanAlgebra α<VAR>s t : Finset α<GOAL>s.compls ⊼ t = t.diffs s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>BooleanAlgebra α<VAR>s t : Finset α<GOAL>s.diffs t.compls = s ⊼ t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>n : ℕ<VAR>h𝒜 : Set.Sized n ↑𝒜<GOAL>Set.Sized (Fintype.card α - n) ↑𝒜.compls
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Fintype α<VAR>𝒜 : Finset (Finset α)<VAR>n : ℕ<VAR>hn : n ≤ Fintype.card α<GOAL>Set.Sized n ↑𝒜.compls ↔ Set.Sized (Fintype.card α - n) ↑𝒜
<VAR>α : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>Mul α<VAR>A B : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>A.hadamard B i j = A i j * B i j
<VAR>α : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>A B : Matrix m n α<VAR>CommSemigroup α<GOAL>A.hadamard B = B.hadamard A
<VAR>α : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>A B C : Matrix m n α<VAR>Semigroup α<GOAL>(A.hadamard B).hadamard C = A.hadamard (B.hadamard C)
<VAR>α : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>A B C : Matrix m n α<VAR>Distrib α<GOAL>A.hadamard (B + C) = A.hadamard B + A.hadamard C
<VAR>α : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>A B C : Matrix m n α<VAR>Distrib α<GOAL>(B + C).hadamard A = B.hadamard A + C.hadamard A
<VAR>α : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_6<VAR>A B : Matrix m n α<VAR>Mul α<VAR>SMul R α<VAR>IsScalarTower R α α<VAR>k : R<GOAL>(k • A).hadamard B = k • A.hadamard B
<VAR>α : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>R : Type u_6<VAR>A B : Matrix m n α<VAR>Mul α<VAR>SMul R α<VAR>SMulCommClass R α α<VAR>k : R<GOAL>A.hadamard (k • B) = k • A.hadamard B
<VAR>α : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>A : Matrix m n α<VAR>MulZeroClass α<GOAL>A.hadamard 0 = 0
<VAR>α : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>A : Matrix m n α<VAR>MulZeroClass α<GOAL>Matrix.hadamard 0 A = 0
<VAR>α : Type u_1<VAR>n : Type u_5<VAR>DecidableEq n<VAR>MulZeroOneClass α<VAR>M : Matrix n n α<GOAL>M.hadamard 1 = Matrix.diagonal fun i => M i i
<VAR>α : Type u_1<VAR>n : Type u_5<VAR>DecidableEq n<VAR>MulZeroOneClass α<VAR>M : Matrix n n α<GOAL>Matrix.hadamard 1 M = Matrix.diagonal fun i => M i i
<VAR>α : Type u_1<VAR>n : Type u_5<VAR>DecidableEq n<VAR>MulZeroClass α<VAR>v w : n → α<GOAL>(Matrix.diagonal v).hadamard (Matrix.diagonal w) = Matrix.diagonal (v * w)
<VAR>α : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>A B : Matrix m n α<VAR>Fintype m<VAR>Fintype n<VAR>Semiring α<GOAL>∑ i : m, ∑ j : n, A.hadamard B i j = (A * B.transpose).trace
<VAR>α : Type u_1<VAR>m : Type u_4<VAR>n : Type u_5<VAR>A B : Matrix m n α<VAR>Fintype m<VAR>Fintype n<VAR>Semiring α<VAR>DecidableEq m<VAR>DecidableEq n<VAR>v : m → α<VAR>w : n → α<GOAL>Matrix.dotProduct (Matrix.vecMul v (A.hadamard B)) w = (Matrix.diagonal v * A * (B * Matrix.diagonal w).transpose).trace
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<GOAL>M.dualIndepMatroid.Indep I = (I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B)
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M.dualIndepMatroid.E = M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<GOAL>M✶.Indep I ↔ I ⊆ M.E ∧ ∃ B, M.Base B ∧ Disjoint I B
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M✶.E = M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : I ⊆ M.E := by aesop_mat<GOAL>M✶.Indep I ↔ ∃ B, M.Base B ∧ Disjoint I B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<GOAL>M✶.Dep I ↔ (∀ (B : Set α), M.Base B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : B ⊆ M.E := by aesop_mat<GOAL>M✶.Base B ↔ M.Base (M.E \ B)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<GOAL>M✶.Base B ↔ M.Base (M.E \ B) ∧ B ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>{B | M✶.Base B} = (fun X => M.E \ X) '' {B | M.Base B}
<VAR>α : Type u_1<VAR>M : Matroid α<GOAL>M✶✶ = M
<VAR>α : Type u_1<GOAL>Function.Involutive Matroid.dual
<VAR>α : Type u_1<GOAL>Function.Injective Matroid.dual
<VAR>α : Type u_1<VAR>M₁ M₂ : Matroid α<GOAL>M₁✶ = M₂✶ ↔ M₁ = M₂
<VAR>α : Type u_1<VAR>M₁ M₂ : Matroid α<GOAL>M₁ = M₂✶ ↔ M₂ = M₁✶
<VAR>α : Type u_1<VAR>M₁ M₂ : Matroid α<GOAL>M₁ = M₂✶ ↔ M₁✶ = M₂
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>h : M✶.Base B<GOAL>M.Base (M.E \ B)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>h : M.Base B<GOAL>M✶.Base (M.E \ B)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B X : Set α<VAR>hB : M.Base B<VAR>hBX : M.Basis (B ∩ X) X<GOAL>M✶.Basis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B X : Set α<VAR>hB : M.Base B<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.Basis (B ∩ X) X ↔ M✶.Basis (M.E \ B ∩ (M.E \ X)) (M.E \ X)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>hB : B ⊆ M.E := by aesop_mat<GOAL>M.Base B ↔ M✶.Base (M.E \ B)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>h : M✶.RkPos<GOAL>¬M.Base M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B : Set α<VAR>h : M✶.RkPos<VAR>hB : M.Base B<GOAL>B ⊂ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>h : M✶.RkPos<VAR>hI : M.Indep I<GOAL>I ⊂ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.Coindep X ↔ M✶.Indep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>hX : M.Coindep X<GOAL>M✶.Indep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<GOAL>M✶.Coindep X ↔ M.Indep X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I : Set α<VAR>hI : M.Indep I<GOAL>M✶.Coindep I
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.Coindep X ↔ (∃ B, M.Base B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>hX : X ⊆ M.E := by aesop_mat<GOAL>M.Coindep X ↔ ∃ B, M.Base B ∧ B ⊆ M.E \ X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<GOAL>M.Coindep X ↔ ∃ B, M.Base B ∧ X ⊆ M.E \ B
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>hX : M.Coindep X<GOAL>X ⊆ M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>h : M.Coindep X<GOAL>∃ B, M.Base B ∧ B ⊆ M.E \ X
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>X : Set α<VAR>h : M.Coindep X<GOAL>∃ B, M.Base B ∧ X ⊆ M.E \ B
<VAR>α : Type u_4<VAR>self : Finset α<GOAL>self.val.Nodup
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s.val = t.val → s = t
<VAR>α : Type u_1<GOAL>Function.Injective Finset.val
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s.val = t.val ↔ s = t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s.val.dedup = s.val
<VAR>α : Type u_1<VAR>a : α<VAR>s : Finset α<GOAL>a ∈ s ↔ a ∈ s.val
<VAR>α : Type u_1<VAR>a : α<VAR>s : Finset α<GOAL>a ∈ s.val ↔ a ∈ s
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<VAR>nd : s.Nodup<GOAL>a ∈ { val := s, nodup := nd } ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>(∀ b ∈ s, ¬a = b) ↔ a ∉ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>(∀ b ∈ s, ¬b = a) ↔ a ∉ s
<VAR>α : Type u_1<VAR>a : α<VAR>s : Finset α<GOAL>a ∈ ↑s ↔ a ∈ s
<VAR>α : Type u_4<VAR>s : Finset α<GOAL>{a | a ∈ s} = ↑s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>x : ↑↑s<GOAL>↑x ∈ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>x : ↑↑s<VAR>h : ↑x ∈ ↑s<GOAL>⟨↑x, h⟩ = x
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<GOAL>s₁ = s₂ ↔ ∀ (a : α), a ∈ s₁ ↔ a ∈ s₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<GOAL>(∀ (a : α), a ∈ s₁ ↔ a ∈ s₂) → s₁ = s₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<GOAL>↑s₁ = ↑s₂ ↔ s₁ = s₂
<VAR>α : Type u_4<GOAL>Function.Injective Finset.toSet
<VAR>α : Type u_4<VAR>s : Finset α<VAR>p : { x // x ∈ s } → Prop<GOAL>(∀ (x : { x // x ∈ s }), p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩
<VAR>α : Type u_4<VAR>s : Finset α<VAR>p : { x // x ∈ s } → Prop<GOAL>(∃ x, p x) ↔ ∃ x, ∃ (h : x ∈ s), p ⟨x, h⟩
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>↑↑s = { x // x ∈ s }
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s ⊆ t ↔ s.val ⊆ t.val
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s ⊂ t ↔ s ⊆ t ∧ ¬t ⊆ s
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s ⊆ s
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>h : s = t<GOAL>s ⊆ t
<VAR>α : Type u_1<VAR>s₁ s₂ s₃ : Finset α<GOAL>s₁ ⊆ s₂ → s₂ ⊆ s₃ → s₁ ⊆ s₃
<VAR>α : Type u_1<VAR>s₁ s₂ s₃ : Finset α<GOAL>s₁ ⊇ s₂ → s₂ ⊇ s₃ → s₁ ⊇ s₃
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<VAR>a : α<GOAL>s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>h : s ⊆ t<VAR>a : α<GOAL>a ∉ t → a ∉ s
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<VAR>H₁ : s₁ ⊆ s₂<VAR>H₂ : s₂ ⊆ s₁<GOAL>s₁ = s₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<GOAL>s₁ ⊆ s₂ ↔ ∀ ⦃x : α⦄, x ∈ s₁ → x ∈ s₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<GOAL>↑s₁ ⊆ ↑s₂ ↔ s₁ ⊆ s₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<GOAL>s₁.val ≤ s₂.val ↔ s₁ ⊆ s₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<GOAL>s₁ = s₂ ↔ s₁ ⊆ s₂ ∧ s₂ ⊆ s₁
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t
<VAR>α : Type u_1<GOAL>(fun x x_1 => x ≤ x_1) = fun x x_1 => x ⊆ x_1
<VAR>α : Type u_1<GOAL>(fun x x_1 => x < x_1) = fun x x_1 => x ⊂ x_1
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<GOAL>s₁ ≤ s₂ ↔ s₁ ⊆ s₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<GOAL>s₁ < s₂ ↔ s₁ ⊂ s₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<GOAL>↑s₁ ⊂ ↑s₂ ↔ s₁ ⊂ s₂
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<GOAL>s₁.val < s₂.val ↔ s₁ ⊂ s₂
<VAR>α : Type u_1<GOAL>StrictMono Finset.val
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s ⊂ t ↔ s ⊆ t ∧ s ≠ t
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<VAR>h : s₁ ⊆ s₂<GOAL>s₁ ⊂ s₂ ↔ ∃ x ∈ s₂, x ∉ s₁
<VAR>α : Type u_1<VAR>s₁ s₂ s₃ : Finset α<VAR>hs₁s₂ : s₁ ⊂ s₂<VAR>hs₂s₃ : s₂ ⊆ s₃<GOAL>s₁ ⊂ s₃
<VAR>α : Type u_1<VAR>s₁ s₂ s₃ : Finset α<VAR>hs₁s₂ : s₁ ⊆ s₂<VAR>hs₂s₃ : s₂ ⊂ s₃<GOAL>s₁ ⊂ s₃
<VAR>α : Type u_1<VAR>s₁ s₂ : Finset α<VAR>h : s₁ ⊂ s₂<GOAL>∃ x ∈ s₂, x ∉ s₁
<VAR>α : Type u_1<GOAL>⇑Finset.coeEmb = Finset.toSet
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>(↑s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Nonempty { x // x ∈ s } ↔ s.Nonempty
<VAR>α : Type u_1<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>∃ x, x ∈ s
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>hst : s ⊆ t<VAR>hs : s.Nonempty<GOAL>t.Nonempty
<VAR>α : Type u_1<VAR>s : Finset α<VAR>h : s.Nonempty<VAR>p : Prop<GOAL>(∀ x ∈ s, p) ↔ p
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.Nonempty → Nonempty { x // x ∈ s }
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.Nonempty → Nonempty α
<VAR>α : Type u_1<GOAL>∅.val = 0
<VAR>α : Type u_1<VAR>a : α<GOAL>a ∉ ∅
<VAR>α : Type u_1<GOAL>¬∅.Nonempty
<VAR>α : Type u_1<GOAL>{ val := 0, nodup := ⋯ } = ∅
<VAR>α : Type u_1<VAR>a : α<VAR>s : Finset α<VAR>h : a ∈ s<GOAL>s ≠ ∅
<VAR>α : Type u_1<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>s ≠ ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>∅ ⊆ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>H : ∀ (x : α), x ∉ s<GOAL>s = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s = ∅ ↔ ∀ (x : α), x ∉ s
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.val = 0 ↔ s = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s ⊆ ∅ ↔ s = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>¬s ⊂ ∅
<VAR>α : Type u_1<VAR>s : Finset α<VAR>h : s ≠ ∅<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.Nonempty ↔ s ≠ ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>¬s.Nonempty ↔ s = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s = ∅ ∨ s.Nonempty
<VAR>α : Type u_1<GOAL>↑∅ = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>↑s = ∅ ↔ s = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>IsEmpty { x // x ∈ s } ↔ s = ∅
<VAR>α : Type u_1<VAR>IsEmpty α<VAR>s : Finset α<GOAL>s = ∅
<VAR>α : Type u_1<GOAL>⊥ = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>∅ ⊂ s ↔ s.Nonempty
<VAR>α : Type u_1<VAR>a : α<GOAL>{a}.val = {a}
<VAR>α : Type u_1<VAR>x y : α<VAR>h : x ∈ {y}<GOAL>x = y
<VAR>α : Type u_1<VAR>a b : α<GOAL>a ∉ {b} ↔ a ≠ b
<VAR>α : Type u_1<VAR>a : α<VAR>s : Finset α<GOAL>s.val = {a} ↔ s = {a}
<VAR>α : Type u_1<VAR>a : α<GOAL>{a}.Nonempty
<VAR>α : Type u_1<VAR>a : α<GOAL>{a} ≠ ∅
<VAR>α : Type u_1<VAR>a : α<GOAL>∅ ⊂ {a}
<VAR>α : Type u_1<VAR>a : α<GOAL>↑{a} = {a}
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>↑s = {a} ↔ s = {a}
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>↑s ⊆ {a} ↔ s ⊆ {a}
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>{a} ⊆ ↑s ↔ {a} ⊆ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>s = {a} ↔ a ∈ s ∧ ∀ x ∈ s, x = a
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>s = {a} ↔ s.Nonempty ∧ ∀ x ∈ s, x = a
<VAR>α : Type u_1<VAR>Unique α<VAR>s : Finset α<GOAL>s.Nonempty ↔ s = {default}
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>(∃ a, s = {a}) ↔ ∃! a, a ∈ s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<GOAL>↑{a} ⊆ s ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>{a} ⊆ s ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>s ⊆ {a} ↔ s = ∅ ∨ s = {a}
<VAR>α : Type u_1<VAR>a b : α<GOAL>{a} ⊆ {b} ↔ a = b
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>h : s.Nonempty<GOAL>s ⊆ {a} ↔ s = {a}
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>s ⊆ {a} ↔ ∀ b ∈ s, b = a
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>s ⊂ {a} ↔ s = ∅
<VAR>α : Type u_1<VAR>s : Finset α<VAR>x : α<VAR>hs : s ⊂ {x}<GOAL>s = ∅
<VAR>α : Type u_1<GOAL>¬∅.Nontrivial
<VAR>α : Type u_1<VAR>a : α<GOAL>¬{a}.Nontrivial
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>hs : s.Nontrivial<GOAL>s ≠ {a}
<VAR>α : Type u_1<VAR>s : Finset α<VAR>hs : s.Nontrivial<VAR>a : α<GOAL>∃ b ∈ s, b ≠ a
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<GOAL>s = {a} ∨ s.Nontrivial
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<GOAL>s.Nontrivial ↔ s ≠ {a}
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.Nonempty → (∃ a, s = {a}) ∨ s.Nontrivial
<VAR>α : Type u_1<VAR>i : α<GOAL>↑default = i
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a b : α<VAR>h : a ∉ s<GOAL>b ∈ Finset.cons a s h ↔ b = a ∨ b ∈ s
<VAR>α : Type u_1<VAR>a b : α<VAR>s : Finset α<VAR>hb : b ∉ s<VAR>ha : a ∈ s<GOAL>a ∈ Finset.cons b s hb
<VAR>α : Type u_1<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>a ∈ Finset.cons a s h
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>(Finset.cons a s h).val = a ::ₘ s.val
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<VAR>p : α → Prop<GOAL>(∀ x ∈ Finset.cons a s h, p x) ↔ p a ∧ ∀ x ∈ s, p x
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>p : α → Prop<VAR>h : a ∉ s<VAR>H : ∀ x ∈ Finset.cons a s h, p x<VAR>x : α<GOAL>x ∈ s → p x
<VAR>α : Type u_1<VAR>a : α<VAR>s : Multiset α<VAR>h : (a ::ₘ s).Nodup<GOAL>{ val := a ::ₘ s, nodup := h } = Finset.cons a { val := s, nodup := ⋯ } ⋯
<VAR>α : Type u_1<VAR>a : α<GOAL>Finset.cons a ∅ ⋯ = {a}
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>(Finset.cons a s h).Nonempty
<VAR>α : Type u_1<VAR>m : Multiset α<VAR>hm : m.Nodup<GOAL>{ val := m, nodup := hm }.Nonempty ↔ m ≠ 0
<VAR>α : Type u_1<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>↑(Finset.cons a s h) = insert a ↑s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>s ⊆ Finset.cons a s h
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>s ⊂ Finset.cons a s h
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>Finset.cons a s h ⊆ t ↔ a ∈ t ∧ s ⊆ t
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>a : α<VAR>hs : a ∉ s<VAR>ht : a ∉ t<GOAL>Finset.cons a s hs ⊆ Finset.cons a t ht ↔ s ⊆ t
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s ⊂ t ↔ ∃ a, ∃ (h : a ∉ s), Finset.cons a s h ⊆ t
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ s → a ∉ t
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>Disjoint s t ↔ ∀ ⦃a : α⦄, a ∈ t → a ∉ s
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>Disjoint s t ↔ ∀ a ∈ s, ∀ b ∈ t, a ≠ b
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s.val.Disjoint t.val ↔ Disjoint s t
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>a b : α<VAR>h : Disjoint s t<VAR>ha : a ∈ s<VAR>hb : b ∈ t<GOAL>a ≠ b
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>¬Disjoint s t ↔ ∃ a ∈ s, a ∈ t
<VAR>α : Type u_1<VAR>s t u : Finset α<VAR>h : s ⊆ u<VAR>d : Disjoint u t<GOAL>Disjoint s t
<VAR>α : Type u_1<VAR>s t u : Finset α<VAR>h : t ⊆ u<VAR>d : Disjoint s u<GOAL>Disjoint s t
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Disjoint ∅ s
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Disjoint s ∅
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>Disjoint {a} s ↔ a ∉ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>Disjoint s {a} ↔ a ∉ s
<VAR>α : Type u_1<VAR>a b : α<GOAL>Disjoint {a} {b} ↔ a ≠ b
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Disjoint s s ↔ s = ∅
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>Disjoint ↑s ↑t ↔ Disjoint s t
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>s : Set ι<VAR>f : ι → Finset α<GOAL>(s.PairwiseDisjoint fun i => ↑(f i)) ↔ s.PairwiseDisjoint f
<VAR>α : Type u_4<VAR>s t : Finset α<VAR>h : Disjoint s t<VAR>a : α<GOAL>a ∈ s.disjUnion t h ↔ a ∈ s ∨ a ∈ t
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>h : Disjoint s t<GOAL>↑(s.disjUnion t h) = ↑s ∪ ↑t
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>h : Disjoint s t<GOAL>s.disjUnion t h = t.disjUnion s ⋯
<VAR>α : Type u_1<VAR>t : Finset α<VAR>h : Disjoint ∅ t := ⋯<GOAL>∅.disjUnion t h = t
<VAR>α : Type u_1<VAR>s : Finset α<VAR>h : Disjoint s ∅ := ⋯<GOAL>s.disjUnion ∅ h = s
<VAR>α : Type u_1<VAR>a : α<VAR>t : Finset α<VAR>h : Disjoint {a} t<GOAL>{a}.disjUnion t h = Finset.cons a t ⋯
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<VAR>h : Disjoint s {a}<GOAL>s.disjUnion {a} h = Finset.cons a s ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>insert a s = { val := Multiset.ndinsert a s.val, nodup := ⋯ }
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(insert a s).val = Multiset.ndinsert a s.val
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(insert a s).val = (a ::ₘ s.val).dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>(insert a s).val = a ::ₘ s.val
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<GOAL>a ∈ insert b s ↔ a = b ∨ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>a ∈ insert a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<VAR>h : a ∈ s<GOAL>a ∈ insert b s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<VAR>h : b ∈ insert a s<GOAL>b ≠ a → b ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<VAR>ha : b ∈ insert a s<VAR>hb : b ∉ s<GOAL>b = a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>insert a ∅ = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>Finset.cons a s h = insert a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>↑(insert a s) = insert a ↑s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>x y : α<GOAL>x ∈ insert y s ↔ x ∈ insert y ↑s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∈ s<GOAL>insert a s = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>insert a s = s ↔ a ∈ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>insert a s ≠ s ↔ a ∉ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>{a, a} = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Finset α<GOAL>insert a (insert b s) = insert b (insert a s)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>↑{a, b} = {a, b}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<GOAL>↑s = {a, b} ↔ s = {a, b}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>{a, b} = {b, a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>insert a (insert a s) = insert a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(insert a s).Nonempty
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>insert a s ≠ ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>s ≠ insert a t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>insert a s ⊆ t ↔ a ∈ t ∧ s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>ha : a ∈ t<VAR>hs : s ⊆ t<GOAL>insert a s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>s ⊆ insert a s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>insert a s ⊆ insert a t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<VAR>ha : a ∉ s<GOAL>insert a s ⊆ insert a t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a b : α<VAR>ha : a ∉ s<GOAL>insert a s = insert b s ↔ a = b
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Set.InjOn (fun a => insert a s) (↑s)ᶜ
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>s ⊂ insert a s
<VAR>α : Type u_4<VAR>p : Finset α → Prop<VAR>empty : p ∅<VAR>cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), p s → p (Finset.cons a s h)<VAR>s : Finset α<GOAL>p s
<VAR>α : Type u_4<VAR>p : Finset α → Prop<VAR>s : Finset α<VAR>h₁ : p ∅<VAR>h₂ : ∀ ⦃a : α⦄ {s : Finset α} (h : a ∉ s), p s → p (Finset.cons a s h)<GOAL>p s
<VAR>α : Type u_4<VAR>p : Finset α → Prop<VAR>DecidableEq α<VAR>empty : p ∅<VAR>insert : ∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → p s → p (insert a s)<VAR>s : Finset α<GOAL>p s
<VAR>α : Type u_4<VAR>p : Finset α → Prop<VAR>DecidableEq α<VAR>s : Finset α<VAR>empty : p ∅<VAR>insert : ∀ ⦃a : α⦄ {s : Finset α}, a ∉ s → p s → p (insert a s)<GOAL>p s
<VAR>α : Type u_4<VAR>p : Finset α → Prop<VAR>DecidableEq α<VAR>S : Finset α<VAR>h₁ : p ∅<VAR>h₂ : ∀ {a : α} {s : Finset α}, a ∈ S → s ⊆ S → a ∉ s → p s → p (insert a s)<GOAL>p S
<VAR>α : Type u_4<VAR>p : (s : Finset α) → s.Nonempty → Prop<VAR>singleton : ∀ (a : α), p {a} ⋯<VAR>cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), p s hs → p (Finset.cons a s h) ⋯<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>p s hs
<VAR>α : Type u_4<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>∃ t a, ∃ (ha : a ∉ t), Finset.cons a t ha = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Sup.sup = Union.union
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>Inf.inf = Inter.inter
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Disjoint s t ↔ s ∩ t = ∅
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t).val = s.val.ndunion t.val
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t).val = s.val ∪ t.val
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : Disjoint s t<GOAL>s.disjUnion t h = s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<VAR>t : Finset α<VAR>h : a ∈ s<GOAL>a ∈ s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>t : Finset α<VAR>a : α<VAR>s : Finset α<VAR>h : a ∈ t<GOAL>a ∈ s ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>p : α → Prop<GOAL>(∀ a ∈ s ∪ t, p a) ↔ (∀ a ∈ s, p a) ∧ ∀ a ∈ t, p a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∉ s ∪ t ↔ a ∉ s ∧ a ∉ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>↑(s₁ ∪ s₂) = ↑s₁ ∪ ↑s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>hs : s ⊆ u<GOAL>t ⊆ u → s ∪ t ⊆ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>s₁ ⊆ s₁ ∪ s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>s₂ ⊆ s₁ ∪ s₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u v : Finset α<VAR>hsu : s ⊆ u<VAR>htv : t ⊆ v<GOAL>s ∪ t ⊆ u ∪ v
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ t : Finset α<VAR>h : s₁ ⊆ s₂<GOAL>s₁ ∪ t ⊆ s₂ ∪ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t₁ t₂ : Finset α<VAR>h : t₁ ⊆ t₂<GOAL>s ∪ t₁ ⊆ s ∪ t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ : Finset α<GOAL>s₁ ∪ s₂ = s₂ ∪ s₁
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s₁ s₂ s₃ : Finset α<GOAL>s₁ ∪ s₂ ∪ s₃ = s₁ ∪ (s₂ ∪ s₃)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s ∪ s = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>h : s ∪ t ⊆ u<GOAL>s ⊆ u
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t u : Finset α<VAR>h : s ∪ t ⊆ u<GOAL>t ⊆ u