ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>α : Type u_12<VAR>DecidableEq o<VAR>Zero α<VAR>(i : o) → DecidableEq (m' i)<VAR>One α<GOAL>Matrix.blockDiagonal' 1 = 1
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>DecidableEq o<VAR>AddZeroClass α<VAR>M N : (i : o) → Matrix (m' i) (n' i) α<GOAL>Matrix.blockDiagonal' (M + N) = Matrix.blockDiagonal' M + Matrix.blockDiagonal' N
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>DecidableEq o<VAR>AddZeroClass α<VAR>M : (i : o) → Matrix (m' i) (n' i) α<GOAL>(Matrix.blockDiagonal'AddMonoidHom m' n' α) M = Matrix.blockDiagonal' M
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>DecidableEq o<VAR>AddGroup α<VAR>M : (i : o) → Matrix (m' i) (n' i) α<GOAL>Matrix.blockDiagonal' (-M) = -Matrix.blockDiagonal' M
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>DecidableEq o<VAR>AddGroup α<VAR>M N : (i : o) → Matrix (m' i) (n' i) α<GOAL>Matrix.blockDiagonal' (M - N) = Matrix.blockDiagonal' M - Matrix.blockDiagonal' N
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>α : Type u_12<VAR>DecidableEq o<VAR>NonUnitalNonAssocSemiring α<VAR>(i : o) → Fintype (n' i)<VAR>Fintype o<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>N : (i : o) → Matrix (n' i) (p' i) α<GOAL>(Matrix.blockDiagonal' fun k => M k * N k) = Matrix.blockDiagonal' M * Matrix.blockDiagonal' N
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>α : Type u_12<VAR>DecidableEq o<VAR>(i : o) → DecidableEq (m' i)<VAR>Fintype o<VAR>(i : o) → Fintype (m' i)<VAR>NonAssocSemiring α<VAR>M : (i : o) → Matrix (m' i) (m' i) α<GOAL>(Matrix.blockDiagonal'RingHom m' α) M = Matrix.blockDiagonal' M
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>α : Type u_12<VAR>DecidableEq o<VAR>(i : o) → DecidableEq (m' i)<VAR>Fintype o<VAR>(i : o) → Fintype (m' i)<VAR>Semiring α<VAR>M : (i : o) → Matrix (m' i) (m' i) α<VAR>n : ℕ<GOAL>Matrix.blockDiagonal' (M ^ n) = Matrix.blockDiagonal' M ^ n
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>DecidableEq o<VAR>R : Type u_14<VAR>Semiring R<VAR>AddCommMonoid α<VAR>Module R α<VAR>x : R<VAR>M : (i : o) → Matrix (m' i) (n' i) α<GOAL>Matrix.blockDiagonal' (x • M) = x • Matrix.blockDiagonal' M
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>M : Matrix ((i : o) × m' i) ((i : o) × n' i) α<VAR>k : o<VAR>i : m' k<VAR>j : n' k<GOAL>M.blockDiag' k i j = M ⟨k, i⟩ ⟨k, j⟩
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>β : Type u_13<VAR>M : Matrix ((i : o) × m' i) ((i : o) × n' i) α<VAR>f : α → β<GOAL>(M.map f).blockDiag' = fun k => (M.blockDiag' k).map f
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>M : Matrix ((i : o) × m' i) ((i : o) × n' i) α<VAR>k : o<GOAL>Mᵀ.blockDiag' k = (M.blockDiag' k)ᵀ
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_14<VAR>AddMonoid α<VAR>StarAddMonoid α<VAR>M : Matrix ((i : o) × m' i) ((i : o) × n' i) α<VAR>k : o<GOAL>Mᴴ.blockDiag' k = (M.blockDiag' k)ᴴ
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>Zero α<GOAL>Matrix.blockDiag' 0 = 0
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>α : Type u_12<VAR>Zero α<VAR>DecidableEq o<VAR>(i : o) → DecidableEq (m' i)<VAR>d : (i : o) × m' i → α<VAR>k : o<GOAL>(Matrix.diagonal d).blockDiag' k = Matrix.diagonal fun i => d ⟨k, i⟩
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>Zero α<VAR>DecidableEq o<VAR>M : (i : o) → Matrix (m' i) (n' i) α<GOAL>(Matrix.blockDiagonal' M).blockDiag' = M
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>Zero α<VAR>DecidableEq o<GOAL>Function.Injective Matrix.blockDiagonal'
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>Zero α<VAR>DecidableEq o<VAR>M N : (i : o) → Matrix (m' i) (n' i) α<GOAL>Matrix.blockDiagonal' M = Matrix.blockDiagonal' N ↔ M = N
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>α : Type u_12<VAR>Zero α<VAR>DecidableEq o<VAR>(i : o) → DecidableEq (m' i)<VAR>One α<GOAL>Matrix.blockDiag' 1 = 1
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>AddZeroClass α<VAR>M N : Matrix ((i : o) × m' i) ((i : o) × n' i) α<GOAL>(M + N).blockDiag' = M.blockDiag' + N.blockDiag'
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>AddZeroClass α<VAR>M : Matrix ((i : o) × m' i) ((i : o) × n' i) α<VAR>k : o<GOAL>(Matrix.blockDiag'AddMonoidHom m' n' α) M k = M.blockDiag' k
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>AddGroup α<VAR>M : Matrix ((i : o) × m' i) ((i : o) × n' i) α<GOAL>(-M).blockDiag' = -M.blockDiag'
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>AddGroup α<VAR>M N : Matrix ((i : o) × m' i) ((i : o) × n' i) α<GOAL>(M - N).blockDiag' = M.blockDiag' - N.blockDiag'
<VAR>o : Type u_4<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>α : Type u_12<VAR>R : Type u_14<VAR>Monoid R<VAR>AddMonoid α<VAR>DistribMulAction R α<VAR>x : R<VAR>M : Matrix ((i : o) × m' i) ((i : o) × n' i) α<GOAL>(x • M).blockDiag' = x • M.blockDiag'
<VAR>R : Type u_10<VAR>CommRing R<VAR>m : Type u_14<VAR>n : Type u_15<VAR>k : Type u_16<VAR>Fintype n<VAR>p : m → Prop<VAR>q : k → Prop<VAR>A : Matrix m n R<VAR>B : Matrix n k R<GOAL>(A * B).toBlock p q = A.toBlock p ⊤ * B.toBlock ⊤ q
<VAR>R : Type u_10<VAR>CommRing R<VAR>m : Type u_14<VAR>n : Type u_15<VAR>k : Type u_16<VAR>Fintype n<VAR>p : m → Prop<VAR>q : n → Prop<VAR>DecidablePred q<VAR>r : k → Prop<VAR>A : Matrix m n R<VAR>B : Matrix n k R<GOAL>(A * B).toBlock p r = A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r
<VAR>α : Type u<VAR>Fintype α<VAR>Fintype (Shrink.{v, u} α)<GOAL>Fintype.card (Shrink.{v, u} α) = Fintype.card α
<VAR>α : Type u_4<VAR>Fintype α<GOAL>Finset.univ = Finset.insertNone Finset.univ
<VAR>α : Type u_4<VAR>Fintype α<GOAL>Fintype.card (Option α) = Fintype.card α + 1
<VAR>P : (α : Type u) → [inst : Fintype α] → Prop<VAR>of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β<VAR>h_empty : P PEmpty.{u + 1}<VAR>h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)<VAR>α : Type u<VAR>h_fintype : Fintype α<GOAL>P α
<VAR>P : Type u → Prop<VAR>of_equiv : ∀ {α β : Type u}, α ≃ β → P α → P β<VAR>h_empty : P PEmpty.{u + 1}<VAR>h_option : ∀ {α : Type u} [inst : Fintype α], P α → P (Option α)<VAR>α : Type u<VAR>Finite α<GOAL>P α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>b : β<VAR>f : α → β<GOAL>Option.elim' b f none = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>f : α → β<GOAL>Option.elim' b f (some a) = f a
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>b : β<VAR>f : α → β<VAR>a : Option α<GOAL>Option.elim' b f a = a.elim b f
<VAR>α : Type u_3<VAR>a b : α<GOAL>a ∈ some b ↔ b = a
<VAR>α : Type u_1<VAR>Inhabited α<VAR>a : α<GOAL>(some a).iget = a
<VAR>α : Type u_1<VAR>a : α<VAR>o : Option α<GOAL>a ∈ o.toList ↔ a ∈ o
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>a : (MvQPF.P F).A<VAR>f' : ((MvQPF.P F).drop.B a).Arrow α<VAR>f : (MvQPF.P F).last.B a → (MvQPF.P F).W α<GOAL>MvQPF.recF g ((MvQPF.P F).wMk a f' f) = g (MvQPF.abs ⟨a, TypeVec.splitFun f' (MvQPF.recF g ∘ f)⟩)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>x : (MvQPF.P F).W α<GOAL>MvQPF.recF g x = g (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.recF g) ((MvQPF.P F).wDest' x)))
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>u : F (α ::: β) → β<VAR>x y : (MvQPF.P F).W α<GOAL>MvQPF.WEquiv x y → MvQPF.recF u x = MvQPF.recF u y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x y : (MvQPF.P F).W α<VAR>h : MvQPF.abs ((MvQPF.P F).wDest' x) = MvQPF.abs ((MvQPF.P F).wDest' y)<GOAL>MvQPF.WEquiv x y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : (MvQPF.P F).W α<GOAL>MvQPF.WEquiv x x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x y : (MvQPF.P F).W α<GOAL>MvQPF.WEquiv x y → MvQPF.WEquiv y x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>a : (MvQPF.P F).A<VAR>f' : ((MvQPF.P F).drop.B a).Arrow α<VAR>f : (MvQPF.P F).last.B a → (MvQPF.P F).W α<GOAL>MvQPF.wrepr ((MvQPF.P F).wMk a f' f) = (MvQPF.P F).wMk' (MvQPF.repr (MvQPF.abs (MvFunctor.map (TypeVec.id ::: MvQPF.wrepr) ⟨a, (MvQPF.P F).appendContents f' f⟩)))
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : (MvQPF.P F).W α<GOAL>MvQPF.WEquiv (MvQPF.wrepr x) x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α β : TypeVec.{u} n<VAR>g : α.Arrow β<VAR>x y : (MvQPF.P F).W α<GOAL>MvQPF.WEquiv x y → MvQPF.WEquiv (MvFunctor.map g x) (MvFunctor.map g y)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>x : F (α ::: MvQPF.Fix F α)<GOAL>MvQPF.Fix.rec g (MvQPF.Fix.mk x) = g (MvFunctor.map (TypeVec.id ::: MvQPF.Fix.rec g) x)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>a : (MvQPF.P F).A<VAR>f' : ((MvQPF.P F).drop.B a).Arrow α<VAR>f : (MvQPF.P F).last.B a → (MvQPF.P F).W α<GOAL>MvQPF.Fix.mk (MvQPF.abs ⟨a, (MvQPF.P F).appendContents f' fun x => ⟦f x⟧⟩) = ⟦(MvQPF.P F).wMk a f' f⟧
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g₁ g₂ : MvQPF.Fix F α → β<VAR>h : ∀ (x : F (α ::: MvQPF.Fix F α)), MvFunctor.map (TypeVec.id ::: g₁) x = MvFunctor.map (TypeVec.id ::: g₂) x → g₁ (MvQPF.Fix.mk x) = g₂ (MvQPF.Fix.mk x)<VAR>x : MvQPF.Fix F α<GOAL>g₁ x = g₂ x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>β : Type u<VAR>g : F (α ::: β) → β<VAR>h : MvQPF.Fix F α → β<VAR>hyp : ∀ (x : F (α ::: MvQPF.Fix F α)), h (MvQPF.Fix.mk x) = g (MvFunctor.map (TypeVec.id ::: h) x)<GOAL>MvQPF.Fix.rec g = h
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : MvQPF.Fix F α<GOAL>MvQPF.Fix.mk x.dest = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : F (α ::: MvQPF.Fix F α)<GOAL>(MvQPF.Fix.mk x).dest = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>p : MvQPF.Fix F α → Prop<VAR>h : ∀ (x : F (α ::: MvQPF.Fix F α)), MvFunctor.LiftP (α.PredLast p) x → p (MvQPF.Fix.mk x)<VAR>x : MvQPF.Fix F α<GOAL>p x
<VAR>α : Type u_4<VAR>self : Fintype α<VAR>x : α<GOAL>x ∈ Fintype.elems
<VAR>α : Type u_1<VAR>Fintype α<VAR>x : α<GOAL>x ∈ Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>x : α<GOAL>x ∈ Finset.univ.val
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<GOAL>s = Finset.univ ↔ ∀ (x : α), x ∈ s
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<GOAL>(∀ (x : α), x ∈ s) → s = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<GOAL>↑Finset.univ = Set.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<GOAL>↑s = Set.univ ↔ s = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<VAR>Subsingleton α<GOAL>s.Nonempty → s = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Finset.univ.Nonempty ↔ Nonempty α
<VAR>α : Type u_1<VAR>Fintype α<VAR>Nonempty α<GOAL>Finset.univ.Nonempty
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Finset.univ = ∅ ↔ IsEmpty α
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Finset.univ.Nontrivial ↔ Nontrivial α
<VAR>α : Type u_1<VAR>Fintype α<VAR>h : Nontrivial α<GOAL>Finset.univ.Nontrivial
<VAR>α : Type u_1<VAR>Fintype α<VAR>IsEmpty α<GOAL>Finset.univ = ∅
<VAR>α : Type u_1<VAR>Fintype α<VAR>Unique α<GOAL>Finset.univ = {default}
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<GOAL>s ⊆ Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<GOAL>⊤ = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<GOAL>s ⊂ Finset.univ ↔ s ≠ Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<GOAL>Finset.univ ⊆ s ↔ s = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s t : Finset α<GOAL>Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ s → a ∈ t
<VAR>α : Type u_1<VAR>Fintype α<VAR>s t : Finset α<GOAL>Codisjoint s t ↔ ∀ ⦃a : α⦄, a ∉ t → a ∈ s
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>s \ t = s ∩ tᶜ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>sᶜ = Finset.univ \ s
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<VAR>DecidableEq α<VAR>a : α<GOAL>a ∈ sᶜ ↔ a ∉ s
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<VAR>DecidableEq α<VAR>a : α<GOAL>a ∉ sᶜ ↔ a ∈ s
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>↑sᶜ = (↑s)ᶜ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>sᶜ ⊆ tᶜ ↔ t ⊆ s
<VAR>α : Type u_1<VAR>Fintype α<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>sᶜ ⊂ tᶜ ↔ t ⊂ s
<VAR>α : Type u_1<VAR>Fintype α<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>s ⊆ tᶜ ↔ t ⊆ sᶜ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<VAR>DecidableEq α<VAR>a : α<GOAL>s ⊆ {a}ᶜ ↔ a ∉ s
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<GOAL>∅ᶜ = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<GOAL>Finset.univᶜ = ∅
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>sᶜ = ∅ ↔ s = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>sᶜ = Finset.univ ↔ s = ∅
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s ∪ sᶜ = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s ∩ sᶜ = ∅
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t)ᶜ = sᶜ ∩ tᶜ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t)ᶜ = sᶜ ∪ tᶜ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<VAR>DecidableEq α<VAR>a : α<GOAL>(s.erase a)ᶜ = insert a sᶜ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<VAR>DecidableEq α<VAR>a : α<GOAL>(insert a s)ᶜ = sᶜ.erase a
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<VAR>DecidableEq α<VAR>a : α<VAR>ha : a ∉ s<GOAL>insert a (insert a s)ᶜ = sᶜ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>x : α<GOAL>insert x {x}ᶜ = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>(x : α) → Decidable ¬p x<GOAL>(Finset.filter p Finset.univ)ᶜ = Finset.filter (fun x => ¬p x) Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>sᶜ ≠ Finset.univ ↔ s.Nonempty
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>a : α<GOAL>{a}ᶜ = Finset.univ.erase a
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Set.InjOn (fun a => insert a s) ↑sᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>Fintype β<VAR>f : β → α<VAR>hf : Function.Surjective f<GOAL>Finset.image f Finset.univ = Finset.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>Fintype β<VAR>f : β ≃ α<GOAL>Finset.image (⇑f) Finset.univ = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.univ ∩ s = s
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>s ∩ Finset.univ = s
<VAR>α : Type u_1<VAR>Fintype α<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>s ∩ t = Finset.univ ↔ s = Finset.univ ∧ t = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>Subsingleton α<VAR>a : α<GOAL>{a} = Finset.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : β ↪ α<VAR>hf : Function.Surjective ⇑f<GOAL>Finset.map f Finset.univ = Finset.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>Fintype β<VAR>f : β ≃ α<GOAL>Finset.map f.toEmbedding Finset.univ = Finset.univ
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>Fintype α<VAR>Fintype β<VAR>e : α ≃ β<GOAL>Finset.map e.toEmbedding Finset.univ = Finset.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>f : α → β<VAR>Fintype β<VAR>DecidablePred fun y => ∃ x, f x = y<VAR>DecidableEq β<GOAL>Finset.filter (fun y => ∃ x, f x = y) Finset.univ = Finset.image f Finset.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>f : α → β<VAR>Fintype β<VAR>DecidablePred fun y => y ∈ Set.range f<VAR>DecidableEq β<GOAL>Finset.filter (fun y => y ∈ Set.range f) Finset.univ = Finset.image f Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<GOAL>↑(Finset.filter p Finset.univ) = {x | p x}
<VAR>α : Type u_1<VAR>s : Finset α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>Fintype { a // p a }<GOAL>Finset.subtype p s = Finset.univ ↔ ∀ ⦃a : α⦄, p a → a ∈ s
<VAR>α : Type u_1<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>Fintype { a // p a }<GOAL>Finset.subtype p Finset.univ = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>Fintype { a // p a }<GOAL>Finset.map (Function.Embedding.subtype p) Finset.univ = Finset.filter p Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>Fintype { a // p a }<GOAL>Multiset.map Subtype.val Finset.univ.val = (Finset.filter p Finset.univ).val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>f : α → β<VAR>p : α → Prop<VAR>DecidablePred p<VAR>Fintype { a // p a }<GOAL>Multiset.map (Subtype.restrict p f) Finset.univ.val = Multiset.map f (Finset.filter p Finset.univ).val
<VAR>α : Type u_1<VAR>Fintype α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.filter (fun x => x ∈ s) Finset.univ = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>b : ↑(Set.range f)<GOAL>f (hf.invOfMemRange b) = ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>a : α<GOAL>hf.invOfMemRange ⟨f a, ⋯⟩ = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>Nonempty α<GOAL>(Set.range f).restrict (Function.invFun f) = hf.invOfMemRange
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.Surjective hf.invOfMemRange
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>b : ↑(Set.range ⇑f)<GOAL>f (f.invOfMemRange b) = ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>a : α<GOAL>f.invOfMemRange ⟨f a, ⋯⟩ = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α ↪ β<VAR>Nonempty α<GOAL>(Set.range ⇑f).restrict (Function.invFun ⇑f) = f.invOfMemRange
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α ↪ β<GOAL>Function.Surjective f.invOfMemRange
<VAR>α : Type u_1<VAR>a : α<VAR>Subsingleton α<GOAL>Finset.univ = {a}
<VAR>α : Type u_1<VAR>IsEmpty α<GOAL>Finset.univ = ∅
<VAR>α : Type u_1<VAR>s t : Set α<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>h : s = t<GOAL>s.toFinset = t.toFinset
<VAR>α : Type u_1<VAR>s : Set α<VAR>Fintype ↑s<VAR>a : α<GOAL>a ∈ s.toFinset ↔ a ∈ s
<VAR>α : Type u_1<VAR>p : Set α<VAR>s : Finset α<VAR>H : ∀ (x : α), x ∈ s ↔ x ∈ p<GOAL>p.toFinset = s
<VAR>α : Type u_1<VAR>s : Set α<VAR>Fintype ↑s<GOAL>↑s.toFinset = s
<VAR>α : Type u_1<VAR>s : Set α<VAR>Fintype ↑s<GOAL>s.toFinset.Nonempty ↔ s.Nonempty
<VAR>α : Type u_1<VAR>s t : Set α<VAR>Fintype ↑s<VAR>Fintype ↑t<GOAL>s.toFinset = t.toFinset ↔ s = t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>Fintype ↑s<VAR>Fintype ↑t<GOAL>s.toFinset ⊆ t.toFinset ↔ s ⊆ t
<VAR>α : Type u_1<VAR>s : Set α<VAR>Fintype ↑s<VAR>t : Finset α<GOAL>s.toFinset ⊂ t ↔ s ⊂ ↑t
<VAR>α : Type u_1<VAR>t : Set α<VAR>s : Finset α<VAR>Fintype ↑t<GOAL>s ⊆ t.toFinset ↔ ↑s ⊆ t
<VAR>α : Type u_1<VAR>t : Set α<VAR>s : Finset α<VAR>Fintype ↑t<GOAL>s ⊂ t.toFinset ↔ ↑s ⊂ t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>Fintype ↑s<VAR>Fintype ↑t<GOAL>s.toFinset ⊂ t.toFinset ↔ s ⊂ t
<VAR>α : Type u_1<VAR>s : Set α<VAR>Fintype ↑s<VAR>t : Finset α<GOAL>s.toFinset ⊆ t ↔ s ⊆ ↑t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>Fintype ↑s<VAR>Fintype ↑t<GOAL>Disjoint s.toFinset t.toFinset ↔ Disjoint s t
<VAR>α : Type u_1<VAR>s t : Set α<VAR>DecidableEq α<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>Fintype ↑(s ∩ t)<GOAL>(s ∩ t).toFinset = s.toFinset ∩ t.toFinset
<VAR>α : Type u_1<VAR>s t : Set α<VAR>DecidableEq α<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>Fintype ↑(s ∪ t)<GOAL>(s ∪ t).toFinset = s.toFinset ∪ t.toFinset
<VAR>α : Type u_1<VAR>s t : Set α<VAR>DecidableEq α<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>Fintype ↑(s \ t)<GOAL>(s \ t).toFinset = s.toFinset \ t.toFinset
<VAR>α : Type u_1<VAR>s t : Set α<VAR>DecidableEq α<VAR>Fintype ↑s<VAR>Fintype ↑t<VAR>Fintype ↑(symmDiff s t)<GOAL>(symmDiff s t).toFinset = symmDiff s.toFinset t.toFinset
<VAR>α : Type u_1<VAR>s : Set α<VAR>DecidableEq α<VAR>Fintype ↑s<VAR>Fintype α<VAR>Fintype ↑sᶜ<GOAL>sᶜ.toFinset = s.toFinsetᶜ
<VAR>α : Type u_1<VAR>Fintype ↑∅<GOAL>∅.toFinset = ∅
<VAR>α : Type u_1<VAR>Fintype α<VAR>Fintype ↑Set.univ<GOAL>Set.univ.toFinset = Finset.univ
<VAR>α : Type u_1<VAR>s : Set α<VAR>Fintype ↑s<GOAL>s.toFinset = ∅ ↔ s = ∅
<VAR>α : Type u_1<VAR>s : Set α<VAR>Fintype α<VAR>Fintype ↑s<GOAL>s.toFinset = Finset.univ ↔ s = Set.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>Fintype ↑{x | p x}<GOAL>{x | p x}.toFinset = Finset.filter p Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Set α<VAR>Fintype ↑s<GOAL>s.toFinset ⊂ Finset.univ ↔ s ⊂ Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Set α<VAR>Fintype ↑s<VAR>Fintype ↑(f '' s)<GOAL>(f '' s).toFinset = Finset.image f s.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>Fintype β<VAR>f : β → α<VAR>Fintype ↑(Set.range f)<GOAL>(Set.range f).toFinset = Finset.image f Finset.univ
<VAR>α : Type u_1<VAR>a : α<VAR>Fintype ↑{a}<GOAL>{a}.toFinset = {a}
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>s : Set α<VAR>Fintype ↑(insert a s)<VAR>Fintype ↑s<GOAL>(insert a s).toFinset = insert a s.toFinset
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Set α<VAR>Fintype ↑s<VAR>DecidablePred fun x => x ∈ s<GOAL>Finset.filter (fun x => x ∈ s) Finset.univ = s.toFinset
<VAR>α : Type u_1<VAR>s : Finset α<VAR>Fintype ↑↑s<GOAL>(↑s).toFinset = s
<VAR>n : ℕ<GOAL>Finset.univ = { val := ↑(List.finRange n), nodup := ⋯ }
<VAR>n : ℕ<GOAL>(List.finRange n).toFinset = Finset.univ
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n → α<GOAL>Multiset.map f Finset.univ.val = ↑(List.ofFn f)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>DecidableEq α<VAR>f : Fin n → α<GOAL>Finset.image f Finset.univ = (List.ofFn f).toFinset
<VAR>α : Type u_1<VAR>n : ℕ<VAR>f : Fin n ↪ α<GOAL>Finset.map f Finset.univ = { val := ↑(List.ofFn ⇑f), nodup := ⋯ }
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>Finset.image i.succAbove Finset.univ = {i}ᶜ
<VAR>n : ℕ<GOAL>Finset.image Fin.succ Finset.univ = {0}ᶜ
<VAR>n : ℕ<GOAL>Finset.image Fin.castSucc Finset.univ = {Fin.last n}ᶜ
<VAR>n : ℕ<GOAL>Finset.univ = Finset.cons 0 (Finset.map { toFun := Fin.succ, inj' := ⋯ } Finset.univ) ⋯
<VAR>n : ℕ<GOAL>Finset.univ = Finset.cons (Fin.last n) (Finset.map Fin.castSuccEmb Finset.univ) ⋯
<VAR>n : ℕ<VAR>p : Fin (n + 1)<GOAL>Finset.univ = Finset.cons p (Finset.map p.succAboveEmb Finset.univ) ⋯
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<GOAL>Finset.image l.get Finset.univ = l.toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>l : List α<VAR>f : α → β<GOAL>Finset.image (fun i => f l[↑i]) Finset.univ = (List.map f l).toFinset
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>l : List α<VAR>f : α → β<GOAL>Finset.image (fun x => f (l.get x)) Finset.univ = (List.map f l).toFinset
<VAR>α : Type u<VAR>s : Finset α<GOAL>Finset.univ = s.attach
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Fintype α<VAR>DecidableEq β<VAR>f : α → β<GOAL>↑(Finset.image f Finset.univ) = Set.range f
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.attach = Finset.univ
<VAR>α : Type u_1<VAR>Fintype α<GOAL>⇑Fintype.finsetEquivSet = Finset.toSet
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Finset α<GOAL>Fintype.finsetEquivSet s = ↑s
<VAR>α : Type u_1<VAR>Fintype α<VAR>s : Set α<VAR>Fintype ↑s<GOAL>Fintype.finsetEquivSet.symm s = s.toFinset
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Fintype.finsetOrderIsoSet.toEquiv = Fintype.finsetEquivSet
<VAR>α : Type u_1<VAR>Fintype α<GOAL>⇑Fintype.finsetOrderIsoSet = Finset.toSet