ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat<GOAL>(AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).val.base x = (PrimeSpectrum.comap (HomogeneousLocalization.mapId 𝒜 ⋯)) (LocalRing.closedPoint (HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat<GOAL>(AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).val.base x = (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>CategoryTheory.IsIso (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).val.base
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat<VAR>z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>HomogeneousLocalization.mk z ∈ ((AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).val.base x).asIdeal ↔ ↑z.num ∈ (↑x).asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>t : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)<GOAL>(TopologicalSpace.Opens.map (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).val.base).obj (PrimeSpectrum.basicOpen (HomogeneousLocalization.mk t)) = (TopologicalSpace.Opens.comap { toFun := Subtype.val, continuous_toFun := ⋯ }) (ProjectiveSpectrum.basicOpen 𝒜 ↑t.num)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>U : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace)ᵒᵖ<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toOpen (HomogeneousLocalization.Away 𝒜 f) (Opposite.unop U)) ((AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).val.c.app U) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ 𝒜 f) (((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).presheaf.map (CategoryTheory.homOfLE ⋯).op)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (↑(CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))) ((AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).val.base x)) (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f) x) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ 𝒜 f) (((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).presheaf.Γgerm x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(ProjectiveSpectrum.basicOpen 𝒜 f)<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>IsLocalization ((AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).val.base x).asIdeal.primeCompl (HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(ProjectiveSpectrum.basicOpen 𝒜 f)<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk (HomogeneousLocalization.Away 𝒜 f) ((AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).val.base x)) (AlgebraicGeometry.ProjectiveSpectrum.Proj.specStalkEquiv 𝒜 f x f_deg hm).hom = HomogeneousLocalization.mapId 𝒜 ⋯
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>x : ↥(ProjectiveSpectrum.basicOpen 𝒜 f)<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f) x = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.specStalkEquiv 𝒜 f x f_deg hm).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.stalkIso' 𝒜 ↑x).toCommRingCatIso.inv ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrictStalkIso ⋯ x).inv)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<GOAL>CategoryTheory.IsIso (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f)
<VAR>α : Type u_2<VAR>Fintype α<VAR>s : Finset α<GOAL>s.dens = ↑s.card / ↑(Fintype.card α)
<VAR>α : Type u_2<VAR>Fintype α<GOAL>∅.dens = 0
<VAR>α : Type u_2<VAR>Fintype α<VAR>a : α<GOAL>{a}.dens = (↑(Fintype.card α))⁻¹
<VAR>α : Type u_2<VAR>Fintype α<VAR>s : Finset α<VAR>a : α<VAR>h : a ∉ s<GOAL>(Finset.cons a s h).dens = s.dens + (↑(Fintype.card α))⁻¹
<VAR>α : Type u_2<VAR>Fintype α<VAR>s t : Finset α<VAR>h : Disjoint s t<GOAL>(s.disjUnion t h).dens = s.dens + t.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>s : Finset α<GOAL>s.dens = 0 ↔ s = ∅
<VAR>α : Type u_2<VAR>Fintype α<VAR>s : Finset α<GOAL>s.dens ≠ 0 ↔ s.Nonempty
<VAR>α : Type u_2<VAR>Fintype α<VAR>s : Finset α<GOAL>0 < s.dens ↔ s.Nonempty
<VAR>α : Type u_2<VAR>Fintype α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>s.dens ≤ t.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>s t : Finset α<VAR>h : s ⊂ t<GOAL>s.dens < t.dens
<VAR>α : Type u_2<VAR>Fintype α<GOAL>Monotone Finset.dens
<VAR>α : Type u_2<VAR>Fintype α<GOAL>StrictMono Finset.dens
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Fintype α<VAR>s : Finset α<VAR>Fintype β<VAR>f : α ↪ β<GOAL>(Finset.map f s).dens ≤ s.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>Nonempty α<GOAL>Finset.univ.dens = 1
<VAR>α : Type u_2<VAR>Fintype α<VAR>s : Finset α<VAR>Nonempty α<GOAL>s.dens = 1 ↔ s = Finset.univ
<VAR>α : Type u_2<VAR>Fintype α<VAR>s : Finset α<VAR>Nonempty α<GOAL>s.dens ≠ 1 ↔ s ≠ Finset.univ
<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).dens + (s ∪ t).dens = s.dens + t.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>s t : Finset α<VAR>DecidableEq α<VAR>h : Disjoint s t<GOAL>(s ∪ t).dens = s.dens + t.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>s t : Finset α<VAR>DecidableEq α<VAR>h : s ⊆ t<GOAL>(t \ s).dens + s.dens = t.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s \ t).dens + t.dens = (s ∪ t).dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>s t : Finset α<VAR>DecidableEq α<VAR>h : s.card = t.card<GOAL>(s \ t).dens = (t \ s).dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s \ t).dens + (s ∩ t).dens = s.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∩ t).dens + (s \ t).dens = s.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>s : Finset α<VAR>DecidableEq α<VAR>p : α → Prop<VAR>DecidablePred p<VAR>(x : α) → Decidable ¬p x<GOAL>(Finset.filter p s).dens + (Finset.filter (fun a => ¬p a) s).dens = s.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(s ∪ t).dens ≤ s.dens + t.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>s t : Finset α<VAR>DecidableEq α<GOAL>s.dens ≤ (s \ t).dens + t.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>s t : Finset α<VAR>DecidableEq α<VAR>h : s ⊆ t<GOAL>(t \ s).dens = t.dens - s.dens
<VAR>α : Type u_2<VAR>Fintype α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>t.dens - s.dens ≤ (t \ s).dens
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>s : Finset α<GOAL>List.Sorted r (Finset.sort r s)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>s : Finset α<GOAL>↑(Finset.sort r s) = s.val
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>s : Finset α<GOAL>(Finset.sort r s).Nodup
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>DecidableEq α<VAR>s : Finset α<GOAL>(Finset.sort r s).toFinset = s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ Finset.sort r s ↔ a ∈ s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>s : Finset α<GOAL>(Finset.sort r s).length = s.card
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<GOAL>Finset.sort r ∅ = []
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>a : α<GOAL>Finset.sort r {a} = [a]
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>IsTrans α r<VAR>IsAntisymm α r<VAR>IsTotal α r<VAR>s : Finset α<GOAL>(Finset.sort r s).Perm s.toList
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<GOAL>List.Sorted (fun x x_1 => x < x_1) (Finset.sort (fun x x_1 => x ≤ x_1) s)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<GOAL>List.Sorted (fun x x_1 => x > x_1) (Finset.sort (fun x x_1 => x ≥ x_1) s)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>h : 0 < (Finset.sort (fun x x_1 => x ≤ x_1) s).length<VAR>H : s.Nonempty<GOAL>(Finset.sort (fun x x_1 => x ≤ x_1) s).get ⟨0, h⟩ = s.min' H
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>h : 0 < (Finset.sort (fun x x_1 => x ≤ x_1) s).length<GOAL>(Finset.sort (fun x x_1 => x ≤ x_1) s).get ⟨0, h⟩ = s.min' ⋯
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>s.min' h = (Finset.sort (fun x x_1 => x ≤ x_1) s).get ⟨0, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>h : (Finset.sort (fun x x_1 => x ≤ x_1) s).length - 1 < (Finset.sort (fun x x_1 => x ≤ x_1) s).length<VAR>H : s.Nonempty<GOAL>(Finset.sort (fun x x_1 => x ≤ x_1) s).get ⟨(Finset.sort (fun x x_1 => x ≤ x_1) s).length - 1, h⟩ = s.max' H
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>h : (Finset.sort (fun x x_1 => x ≤ x_1) s).length - 1 < (Finset.sort (fun x x_1 => x ≤ x_1) s).length<GOAL>(Finset.sort (fun x x_1 => x ≤ x_1) s).get ⟨(Finset.sort (fun x x_1 => x ≤ x_1) s).length - 1, h⟩ = s.max' ⋯
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>s.max' h = (Finset.sort (fun x x_1 => x ≤ x_1) s).get ⟨(Finset.sort (fun x x_1 => x ≤ x_1) s).length - 1, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>i : Fin k<GOAL>↑((s.orderIsoOfFin h) i) = (s.orderEmbOfFin h) i
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>x : { x // x ∈ s }<GOAL>↑((s.orderIsoOfFin h).symm x) = List.indexOf (↑x) (Finset.sort (fun x x_1 => x ≤ x_1) s)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>i : Fin k<GOAL>(s.orderEmbOfFin h) i = (Finset.sort (fun x x_1 => x ≤ x_1) s).get ⟨↑i, ⋯⟩
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>i : Fin k<GOAL>(s.orderEmbOfFin h) i ∈ s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<GOAL>Set.range ⇑(s.orderEmbOfFin h) = ↑s
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>hz : 0 < k<GOAL>(s.orderEmbOfFin h) ⟨0, hz⟩ = s.min' ⋯
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>hz : 0 < k<GOAL>(s.orderEmbOfFin h) ⟨k - 1, ⋯⟩ = s.max' ⋯
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>i : Fin 1<GOAL>({a}.orderEmbOfFin ⋯) i = a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>f : Fin k → α<VAR>hfs : ∀ (x : Fin k), f x ∈ s<VAR>hmono : StrictMono f<GOAL>f = ⇑(s.orderEmbOfFin h)
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>f : Fin k ↪o α<VAR>hfs : ∀ (x : Fin k), f x ∈ s<GOAL>f = s.orderEmbOfFin h
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>k l : ℕ<VAR>s : Finset α<VAR>i : Fin k<VAR>j : Fin l<VAR>h : s.card = k<VAR>h' : s.card = l<GOAL>(s.orderEmbOfFin h) i = (s.orderEmbOfFin h') j ↔ ↑i = ↑j
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : k ≤ s.card<VAR>a : Fin k<GOAL>(s.orderEmbOfCardLe h) a ∈ s
<VAR>n : ℕ<GOAL>Finset.sort (fun x y => x ≤ y) Finset.univ = List.finRange n
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s ∈ t.powerset ↔ s ⊆ t
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>↑s.powerset = Finset.toSet ⁻¹' 𝒫↑s
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>∅ ∈ s.powerset
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s ∈ s.powerset
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.powerset.Nonempty
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s.powerset ⊆ t.powerset ↔ s ⊆ t
<VAR>α : Type u_1<GOAL>Function.Injective Finset.powerset
<VAR>α : Type u_1<VAR>s t : Finset α<GOAL>s.powerset = t.powerset ↔ s = t
<VAR>α : Type u_1<GOAL>∅.powerset = {∅}
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.powerset = {∅} ↔ s = ∅
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.powerset.card = 2 ^ s.card
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>a : α<VAR>ht : t ∈ s.powerset<VAR>h : a ∉ s<GOAL>a ∉ t
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>(insert a s).powerset = s.powerset ∪ Finset.image (insert a) s.powerset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>t ∈ s.ssubsets ↔ t ⊂ s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>∅ ∈ s.ssubsets
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s t : Finset α<GOAL>s ∈ Finset.powersetCard n t ↔ s ⊆ t ∧ s.card = n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>Finset.powersetCard n s ⊆ Finset.powersetCard n t
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Finset α<GOAL>(Finset.powersetCard n s).card = s.card.choose n
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Finset.powersetCard 0 s = {∅}
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>(↑(Finset.powersetCard n ∅)).Subsingleton
<VAR>α : Type u_1<VAR>s : Finset α<VAR>i : ℕ<GOAL>Multiset.map Finset.val (Finset.powersetCard i s).val = Multiset.powersetCard i s.val
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Finset.powersetCard 1 s = Finset.map { toFun := singleton, inj' := ⋯ } s
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Finset α<GOAL>Finset.powersetCard n s = ∅ ↔ s.card < n
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Finset α<VAR>hn : 0 < n<GOAL>Finset.powersetCard (s.card + n) s = ∅
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Finset α<GOAL>Finset.powersetCard n s = Finset.filter (fun x => x.card = n) s.powerset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>x : α<VAR>s : Finset α<VAR>h : x ∉ s<VAR>n : ℕ<GOAL>Finset.powersetCard n.succ (insert x s) = Finset.powersetCard n.succ s ∪ Finset.image (insert x) (Finset.powersetCard n s)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>s : Finset α<GOAL>(Finset.powersetCard n s).Nonempty ↔ n ≤ s.card
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Finset.powersetCard s.card s = {s}
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Pairwise fun i j => Disjoint (Finset.powersetCard i s) (Finset.powersetCard j s)
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>s.powerset = (Finset.range (s.card + 1)).disjiUnion (fun i => Finset.powersetCard i s) ⋯
<VAR>α : Type u_1<VAR>DecidableEq (Finset α)<VAR>s : Finset α<GOAL>s.powerset = (Finset.range (s.card + 1)).biUnion fun i => Finset.powersetCard i s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>u : Finset α<VAR>n : ℕ<VAR>hn : n < u.card<GOAL>(Finset.powersetCard n.succ u).sup id = u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ↪ β<VAR>n : ℕ<VAR>s : Finset α<GOAL>Finset.powersetCard n (Finset.map f s) = Finset.map (Finset.mapEmbedding f).toEmbedding (Finset.powersetCard n s)
<VAR>n : ℕ<GOAL>Finset.antidiagonal n = Finset.map { toFun := fun i => (i, n - i), inj' := ⋯ } (Finset.range (n + 1))
<VAR>n : ℕ<GOAL>Finset.antidiagonal n = Finset.map { toFun := fun i => (n - i, i), inj' := ⋯ } (Finset.range (n + 1))
<VAR>n : ℕ<GOAL>Finset.antidiagonal n = Finset.image (fun i => (i, n - i)) (Finset.range (n + 1))
<VAR>n : ℕ<GOAL>Finset.antidiagonal n = Finset.image (fun i => (n - i, i)) (Finset.range (n + 1))
<VAR>n : ℕ<GOAL>(Finset.antidiagonal n).card = n + 1
<GOAL>Finset.antidiagonal 0 = {(0, 0)}
<VAR>n : ℕ<GOAL>Finset.antidiagonal (n + 1) = Finset.cons (0, n + 1) (Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap (Function.Embedding.refl ℕ)) (Finset.antidiagonal n)) ⋯
<VAR>n : ℕ<GOAL>Finset.antidiagonal (n + 1) = Finset.cons (n + 1, 0) (Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.antidiagonal n)) ⋯
<VAR>n : ℕ<GOAL>Finset.antidiagonal (n + 2) = Finset.cons (0, n + 2) (Finset.cons (n + 2, 0) (Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective }.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective }) (Finset.antidiagonal n)) ⋯) ⋯
<VAR>n : ℕ<VAR>kl : ℕ × ℕ<VAR>hlk : kl ∈ Finset.antidiagonal n<GOAL>kl.1 < n + 1
<VAR>n : ℕ<VAR>kl : ℕ × ℕ<VAR>hlk : kl ∈ Finset.antidiagonal n<GOAL>kl.2 < n + 1
<VAR>n k : ℕ<VAR>h : k ≤ n<GOAL>Finset.filter (fun a => a.2 ≤ k) (Finset.antidiagonal n) = Finset.map ({ toFun := fun x => x + (n - k), inj' := ⋯ }.prodMap (Function.Embedding.refl ℕ)) (Finset.antidiagonal k)
<VAR>n k : ℕ<VAR>h : k ≤ n<GOAL>Finset.filter (fun a => a.1 ≤ k) (Finset.antidiagonal n) = Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := fun x => x + (n - k), inj' := ⋯ }) (Finset.antidiagonal k)
<VAR>n k : ℕ<VAR>h : k ≤ n<GOAL>Finset.filter (fun a => k ≤ a.1) (Finset.antidiagonal n) = Finset.map ({ toFun := fun x => x + k, inj' := ⋯ }.prodMap (Function.Embedding.refl ℕ)) (Finset.antidiagonal (n - k))
<VAR>n k : ℕ<VAR>h : k ≤ n<GOAL>Finset.filter (fun a => k ≤ a.2) (Finset.antidiagonal n) = Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := fun x => x + k, inj' := ⋯ }) (Finset.antidiagonal (n - k))
<VAR>n : ℕ<GOAL>∀ (x : { x // x ∈ Finset.antidiagonal n }), ↑((Finset.Nat.antidiagonalEquivFin n) x) = x.1.1
<VAR>n : ℕ<GOAL>∀ (x : Fin (n + 1)), ↑((Finset.Nat.antidiagonalEquivFin n).symm x) = (↑x, n - ↑x)
<VAR>α β : Type u<VAR>(P : Prop) → Decidable P<VAR>s : Finset α<VAR>f : α → β<GOAL>f <$> s = Finset.image f s
<VAR>α β : Type u<VAR>(P : Prop) → Decidable P<VAR>s : Finset α<VAR>t : Finset (α → β)<GOAL>(Seq.seq t fun x => s) = t.sup fun f => Finset.image f s
<VAR>α β : Type u<VAR>(P : Prop) → Decidable P<VAR>s : Finset α<VAR>t : Finset β<GOAL>(SeqLeft.seqLeft s fun x => t) = if t = ∅ then ∅ else s
<VAR>α β : Type u<VAR>(P : Prop) → Decidable P<VAR>s : Finset α<VAR>t : Finset β<GOAL>(SeqRight.seqRight s fun x => t) = if s = ∅ then ∅ else t
<VAR>(P : Prop) → Decidable P<VAR>α β γ : Type u<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.image₂ f s t = Seq.seq (f <$> s) fun x => t
<VAR>(P : Prop) → Decidable P<VAR>α β : Type u_1<GOAL>(fun x x_1 => x >>= x_1) = Finset.sup
<VAR>α : Type u<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.traverse pure s = s
<VAR>α β : Type u<VAR>h : α → β<GOAL>Functor.map h ∘ Multiset.toFinset = Multiset.toFinset ∘ Functor.map h
<VAR>α β γ : Type u<VAR>G : Type u → Type u<VAR>Applicative G<VAR>CommApplicative G<VAR>g : α → G β<VAR>h : β → γ<VAR>s : Finset α<GOAL>Functor.map h <$> Finset.traverse g s = Finset.traverse (Functor.map h ∘ g) s
<VAR>α : Type u_1<GOAL>none.toFinset = ∅
<VAR>α : Type u_1<VAR>a : α<GOAL>(some a).toFinset = {a}
<VAR>α : Type u_1<VAR>a : α<VAR>o : Option α<GOAL>a ∈ o.toFinset ↔ a ∈ o
<VAR>α : Type u_1<VAR>o : Option α<GOAL>o.toFinset.card = o.elim 0 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>o : Option α<GOAL>o ∈ Finset.insertNone s ↔ ∀ a ∈ o, a ∈ s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>p : Option α → Prop<GOAL>(∀ a ∈ Finset.insertNone s, p a) ↔ p none ∧ ∀ a ∈ s, p (some a)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>a : α<GOAL>some a ∈ Finset.insertNone s ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>none ∈ Finset.insertNone s
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>(Finset.insertNone s).Nonempty
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>(Finset.insertNone s).card = s.card + 1
<VAR>α : Type u_1<VAR>s : Finset (Option α)<VAR>x : α<GOAL>x ∈ Finset.eraseNone s ↔ some x ∈ s
<VAR>α : Type u_1<VAR>s : Finset (Option α)<VAR>p : Option α → Prop<GOAL>(∀ a ∈ Finset.eraseNone s, p (some a)) ↔ ∀ (a : α), some a ∈ s → p (some a)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset (Option α)<GOAL>Finset.eraseNone s = s.biUnion Option.toFinset
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Finset.eraseNone (Finset.map Function.Embedding.some s) = s
<VAR>α : Type u_1<VAR>DecidableEq (Option α)<VAR>s : Finset α<GOAL>Finset.eraseNone (Finset.image some s) = s
<VAR>α : Type u_1<VAR>s : Finset (Option α)<GOAL>↑(Finset.eraseNone s) = some ⁻¹' ↑s
<VAR>α : Type u_1<VAR>DecidableEq (Option α)<VAR>DecidableEq α<VAR>s t : Finset (Option α)<GOAL>Finset.eraseNone (s ∪ t) = Finset.eraseNone s ∪ Finset.eraseNone t
<VAR>α : Type u_1<VAR>DecidableEq (Option α)<VAR>DecidableEq α<VAR>s t : Finset (Option α)<GOAL>Finset.eraseNone (s ∩ t) = Finset.eraseNone s ∩ Finset.eraseNone t
<VAR>α : Type u_1<GOAL>Finset.eraseNone ∅ = ∅
<VAR>α : Type u_1<GOAL>Finset.eraseNone {none} = ∅
<VAR>α : Type u_1<VAR>DecidableEq (Option α)<VAR>s : Finset (Option α)<GOAL>Finset.image some (Finset.eraseNone s) = s.erase none
<VAR>α : Type u_1<VAR>DecidableEq (Option α)<VAR>s : Finset (Option α)<GOAL>Finset.map Function.Embedding.some (Finset.eraseNone s) = s.erase none
<VAR>α : Type u_1<VAR>DecidableEq (Option α)<VAR>s : Finset (Option α)<GOAL>Finset.insertNone (Finset.eraseNone s) = insert none s
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Finset.eraseNone (Finset.insertNone s) = s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Finset.Icc s t = Finset.filter (fun x => s ⊆ x) t.powerset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Finset.Ico s t = Finset.filter (fun x => s ⊆ x) t.ssubsets
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Finset.Ioc s t = Finset.filter (fun x => s ⊂ x) t.powerset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>Finset.Ioo s t = Finset.filter (fun x => s ⊂ x) t.ssubsets
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.Iic s = s.powerset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>Finset.Iio s = s.ssubsets
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>Finset.Icc s t = Finset.image (fun x => s ∪ x) (t \ s).powerset
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>Finset.Ico s t = Finset.image (fun x => s ∪ x) (t \ s).ssubsets
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>(Finset.Icc s t).card = 2 ^ (t.card - s.card)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>(Finset.Ico s t).card = 2 ^ (t.card - s.card) - 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>(Finset.Ioc s t).card = 2 ^ (t.card - s.card) - 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>(Finset.Ioo s t).card = 2 ^ (t.card - s.card) - 2
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>(Finset.Iic s).card = 2 ^ s.card
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>s : Finset α<GOAL>(Finset.Iio s).card = 2 ^ s.card - 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f : Finset α → β<GOAL>Monotone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s ≤ f (Finset.cons a s ha)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f : Finset α → β<GOAL>Antitone f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f (Finset.cons a s ha) ≤ f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f : Finset α → β<GOAL>StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s < f (Finset.cons a s ha)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>f : Finset α → β<GOAL>StrictAnti f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f (Finset.cons a s ha) < f s