ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.SimplicialCategory C<VAR>K K' K'' : C<VAR>f : K ⟶ K'<VAR>f' : K' ⟶ K''<VAR>L : C<GOAL>CategoryTheory.SimplicialCategory.sHomWhiskerRight (f ≫ f') L = CategoryTheory.SimplicialCategory.sHomWhiskerRight f' L ≫ CategoryTheory.SimplicialCategory.sHomWhiskerRight f L
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.SimplicialCategory C<VAR>K L : C<GOAL>CategoryTheory.SimplicialCategory.sHomWhiskerLeft K (𝟙 L) = 𝟙 (CategoryTheory.SimplicialCategory.sHom K L)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.SimplicialCategory C<VAR>K : C<VAR>L L' L'' : C<VAR>g : L ⟶ L'<VAR>g' : L' ⟶ L''<GOAL>CategoryTheory.SimplicialCategory.sHomWhiskerLeft K (g ≫ g') = CategoryTheory.SimplicialCategory.sHomWhiskerLeft K g ≫ CategoryTheory.SimplicialCategory.sHomWhiskerLeft K g'
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.SimplicialCategory C<VAR>K K' L L' : C<VAR>f : K ⟶ K'<VAR>g : L ⟶ L'<GOAL>CategoryTheory.SimplicialCategory.sHomWhiskerLeft K' g ≫ CategoryTheory.SimplicialCategory.sHomWhiskerRight f L' = CategoryTheory.SimplicialCategory.sHomWhiskerRight f L ≫ CategoryTheory.SimplicialCategory.sHomWhiskerLeft K g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.SimplicialCategory C<GOAL>∀ {X Y : Cᵒᵖ} (φ : X ⟶ Y) (L : C), ((CategoryTheory.SimplicialCategory.sHomFunctor C).map φ).app L = CategoryTheory.SimplicialCategory.sHomWhiskerRight φ.unop L
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.SimplicialCategory C<VAR>K : Cᵒᵖ<GOAL>∀ {X Y : C} (φ : X ⟶ Y), ((CategoryTheory.SimplicialCategory.sHomFunctor C).obj K).map φ = CategoryTheory.SimplicialCategory.sHomWhiskerLeft (Opposite.unop K) φ
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.SimplicialCategory C<VAR>K : Cᵒᵖ<VAR>L : C<GOAL>((CategoryTheory.SimplicialCategory.sHomFunctor C).obj K).obj L = CategoryTheory.SimplicialCategory.sHom (Opposite.unop K) L
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : SimplicialObject.Splitting.IndexSet Δ<GOAL>(s.cofan Δ).inj A ≫ s.πSummand A = 𝟙 (SimplicialObject.Splitting.summand s.N Δ A)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A B : SimplicialObject.Splitting.IndexSet Δ<VAR>h : B ≠ A<GOAL>(s.cofan Δ).inj A ≫ s.πSummand B = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Preadditive C<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>𝟙 (X.obj Δ) = ∑ A : SimplicialObject.Splitting.IndexSet Δ, s.πSummand A ≫ (s.cofan Δ).inj A
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Preadditive C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.σ i ≫ s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n + 1])) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>n : ℕ<VAR>A : SimplicialObject.Splitting.IndexSet (Opposite.op [n])<VAR>hA : ¬A.EqId<GOAL>(s.cofan (Opposite.op [n])).inj A ≫ AlgebraicTopology.DoldKan.PInfty.f n = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Preadditive C<VAR>Z : C<VAR>n : ℕ<VAR>f : Z ⟶ X _[n]<GOAL>f ≫ AlgebraicTopology.DoldKan.PInfty.f n = 0 ↔ f ≫ s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n])) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Preadditive C<VAR>n : ℕ<GOAL>AlgebraicTopology.DoldKan.PInfty.f n ≫ s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n])) = s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n]))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Preadditive C<VAR>n : ℕ<GOAL>s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n])) ≫ (s.cofan (Opposite.op [n])).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n])) ≫ AlgebraicTopology.DoldKan.PInfty.f n = AlgebraicTopology.DoldKan.PInfty.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Preadditive C<VAR>j k : ℕ<VAR>A : SimplicialObject.Splitting.IndexSet (Opposite.op [j])<VAR>hA : ¬A.EqId<GOAL>(s.cofan (Opposite.op [j])).inj A ≫ K[X].d j k ≫ s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op [k])) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Preadditive C<VAR>i j : ℕ<GOAL>s.nondegComplex.d i j = s.d i j
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Preadditive C<GOAL>∀ (a : ℕ), s.nondegComplex.X a = s.N a
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Preadditive C<VAR>n : ℕ<GOAL>s.toKaroubiNondegComplexIsoN₁.inv.f.f n = s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n]))
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>X : CategoryTheory.SimplicialObject C<VAR>s : SimplicialObject.Splitting X<VAR>CategoryTheory.Preadditive C<VAR>n : ℕ<GOAL>s.toKaroubiNondegComplexIsoN₁.hom.f.f n = (s.cofan (Opposite.op [n])).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n])) ≫ AlgebraicTopology.DoldKan.PInfty.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S : SimplicialObject.Split C<GOAL>SimplicialObject.Split.nondegComplexFunctor.obj S = S.s.nondegComplex
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>S₁ S₂ : SimplicialObject.Split C<VAR>Φ : S₁ ⟶ S₂<VAR>n : ℕ<GOAL>(SimplicialObject.Split.nondegComplexFunctor.map Φ).f n = Φ.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : SimplicialObject.Split C<VAR>n : ℕ<GOAL>(SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁.hom.app X).f.f n = (X.s.cofan (Opposite.op [n])).inj (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n])) ≫ AlgebraicTopology.DoldKan.PInfty.f n
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : SimplicialObject.Split C<VAR>n : ℕ<GOAL>(SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁.inv.app X).f.f n = X.s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op [n]))
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>g : β → α<VAR>hf : Function.Injective f<VAR>hg : Function.Injective g<GOAL>∃ h, Function.Bijective h
<VAR>α : Type u<VAR>β : Type v<GOAL>(α ↪ β) → (β ↪ α) → Nonempty (α ≃ β)
<VAR>ι : Type u<VAR>β : ι → Type v<VAR>I : Nonempty ι<GOAL>∃ i, Nonempty ((j : ι) → β i ↪ β j)
<VAR>α : Type u<VAR>β : Type v<GOAL>Nonempty (α ↪ β) ∨ Nonempty (β ↪ α)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>n : ℕ<VAR>Δ' : SimplexCategory<VAR>i : Δ' ⟶ [n]<VAR>hi : CategoryTheory.Mono i<VAR>h₁ : Δ'.len ≠ n<VAR>h₂ : ¬AlgebraicTopology.DoldKan.Isδ₀ i<GOAL>AlgebraicTopology.DoldKan.PInfty.f n ≫ X.map i.op = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>Δ Δ' : SimplexCategory<VAR>i : Δ ⟶ Δ'<VAR>CategoryTheory.Mono i<GOAL>AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K[X] i ≫ AlgebraicTopology.DoldKan.PInfty.f Δ.len = AlgebraicTopology.DoldKan.PInfty.f Δ'.len ≫ X.map i.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : CategoryTheory.SimplicialObject C<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>(AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X).f.app Δ = (AlgebraicTopology.DoldKan.Γ₀.splitting K[X]).desc Δ fun A => AlgebraicTopology.DoldKan.PInfty.f (Opposite.unop A.fst).len ≫ X.map A.e.op
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.hom.app X = AlgebraicTopology.DoldKan.Γ₂.map (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.hom.app X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.inv.app X = AlgebraicTopology.DoldKan.Γ₂.map (AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁.inv.app X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)<GOAL>AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app P = (AlgebraicTopology.DoldKan.N₂ ⋙ AlgebraicTopology.DoldKan.Γ₂).map P.decompId_i ≫ (AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.hom ≫ AlgebraicTopology.DoldKan.Γ₂N₁.natTrans).app P.X ≫ P.decompId_p
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>X : CategoryTheory.SimplicialObject C<GOAL>AlgebraicTopology.DoldKan.Γ₂N₁.natTrans.app X = (AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso.app X).inv ≫ AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app ((CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)).obj X)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<VAR>P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)<GOAL>AlgebraicTopology.DoldKan.N₂Γ₂.inv.app (AlgebraicTopology.DoldKan.N₂.obj P) ≫ AlgebraicTopology.DoldKan.N₂.map (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans.app P) = 𝟙 (AlgebraicTopology.DoldKan.N₂.obj P)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>(𝟙 AlgebraicTopology.DoldKan.N₂ ◫ AlgebraicTopology.DoldKan.N₂Γ₂.inv) ≫ (AlgebraicTopology.DoldKan.N₂.associator AlgebraicTopology.DoldKan.Γ₂ AlgebraicTopology.DoldKan.N₂).inv ≫ AlgebraicTopology.DoldKan.Γ₂N₂.natTrans ◫ 𝟙 AlgebraicTopology.DoldKan.N₂ = 𝟙 AlgebraicTopology.DoldKan.N₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>AlgebraicTopology.DoldKan.Γ₂N₂.inv = AlgebraicTopology.DoldKan.Γ₂N₂.natTrans
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Limits.HasFiniteCoproducts C<GOAL>AlgebraicTopology.DoldKan.Γ₂N₁.inv = AlgebraicTopology.DoldKan.Γ₂N₁.natTrans
<VAR>α : Type u_1<VAR>Fintype α<GOAL>Nat.card α = Fintype.card α
<VAR>α : Type u_1<GOAL>∀ {x : Fintype α}, Fintype.card α = Nat.card α
<VAR>α : Type u_1<VAR>s : Finset α<GOAL>Nat.card { x // x ∈ s } = s.card
<VAR>α : Type u_1<VAR>s : Set α<VAR>Fintype ↑s<GOAL>Nat.card ↑s = s.toFinset.card
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Finite<GOAL>Nat.card ↑s = hs.toFinset.card
<VAR>α : Type u_1<VAR>IsEmpty α<GOAL>Nat.card α = 0
<VAR>α : Type u_1<VAR>Infinite α<GOAL>Nat.card α = 0
<VAR>α : Type u_1<VAR>s : Set α<VAR>hs : s.Infinite<GOAL>Nat.card ↑s = 0
<VAR>α : Type u_1<GOAL>Nat.card α = 0 ↔ IsEmpty α ∨ Infinite α
<VAR>α : Type u_1<GOAL>Nat.card α ≠ 0 ↔ Nonempty α ∧ Finite α
<VAR>α : Type u_1<GOAL>0 < Nat.card α ↔ Nonempty α ∧ Finite α
<VAR>α : Type u_1<VAR>Nonempty α<VAR>Finite α<GOAL>0 < Nat.card α
<VAR>α : Type u_1<VAR>h : Nat.card α ≠ 0<GOAL>Finite α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ≃ β<GOAL>Nat.card α = Nat.card β
<VAR>α : Type u<VAR>β : Type v<VAR>Finite β<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Nat.card α ≤ Nat.card β
<VAR>α : Type u<VAR>β : Type v<VAR>Finite α<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Nat.card β ≤ Nat.card α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Bijective f<GOAL>Nat.card α = Nat.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite β<VAR>f : α → β<GOAL>Function.Bijective f ↔ Function.Injective f ∧ Nat.card α = Nat.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite α<VAR>f : α → β<GOAL>Function.Bijective f ↔ Function.Surjective f ∧ Nat.card α = Nat.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite β<VAR>f : α → β<VAR>inj : Function.Injective f<VAR>hc : Nat.card β ≤ Nat.card α<GOAL>Function.Bijective f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite α<VAR>f : α → β<VAR>surj : Function.Surjective f<VAR>hc : Nat.card α ≤ Nat.card β<GOAL>Function.Bijective f
<VAR>α : Type u_3<VAR>n : ℕ<VAR>f : α ≃ Fin n<GOAL>Nat.card α = n
<VAR>α : Type u_1<VAR>s t : Set α<VAR>ht : t.Finite<VAR>h : s ⊆ t<GOAL>Nat.card ↑s ≤ Nat.card ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>hs : s.Finite<GOAL>Nat.card ↑(f '' s) ≤ Nat.card ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>f : α → β<VAR>hf : Set.InjOn f s<GOAL>Nat.card ↑(f '' s) = Nat.card ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>s : Set α<GOAL>Nat.card ↑(f '' s) = Nat.card ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Set α<VAR>e : α ≃ β<GOAL>Nat.card ↑(⇑e '' s) = Nat.card ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<VAR>hf : Set.InjOn f (f ⁻¹' s)<VAR>hsf : s ⊆ Set.range f<GOAL>Nat.card ↑(f ⁻¹' s) = Nat.card ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set β<VAR>hf : Function.Injective f<VAR>hsf : s ⊆ Set.range f<GOAL>Nat.card ↑(f ⁻¹' s) = Nat.card ↑s
<VAR>α : Type u_1<VAR>a : α<VAR>Subsingleton α<GOAL>Nat.card α = 1
<VAR>α : Type u_1<VAR>Unique α<GOAL>Nat.card α = 1
<VAR>α : Type u_1<GOAL>Nat.card α = 1 ↔ Subsingleton α ∧ Nonempty α
<VAR>α : Type u_1<GOAL>Nat.card α = 1 ↔ ∃ x, ∀ (y : α), y = x
<VAR>α : Type u_1<GOAL>Nat.card α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = Set.univ
<VAR>α : Type u_1<VAR>x : α<GOAL>Nat.card α = 2 ↔ ∃! y, y ≠ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite α<VAR>Finite β<GOAL>Nat.card (α ⊕ β) = Nat.card α + Nat.card β
<VAR>α : Type u_3<VAR>β : Type u_4<GOAL>Nat.card (α × β) = Nat.card α * Nat.card β
<VAR>α : Type u_3<GOAL>Nat.card (ULift.{u_4, u_3} α) = Nat.card α
<VAR>α : Type u_3<GOAL>Nat.card (PLift α) = Nat.card α
<VAR>α : Type u_1<VAR>β : α → Type u_3<VAR>Fintype α<GOAL>Nat.card ((a : α) → β a) = ∏ a : α, Nat.card (β a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Finite α<GOAL>Nat.card (α → β) = Nat.card β ^ Nat.card α
<VAR>n : ℕ<GOAL>Nat.card (ZMod n) = n
<VAR>α : Type u_1<VAR>Fintype α<GOAL>PartENat.card α = ↑(Fintype.card α)
<VAR>α : Type u_1<VAR>Infinite α<GOAL>PartENat.card α = ⊤
<VAR>α : Type u_3<VAR>β : Type u_4<GOAL>PartENat.card (α ⊕ β) = PartENat.card α + PartENat.card β
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α ≃ β<GOAL>PartENat.card α = PartENat.card β
<VAR>α : Type u_3<GOAL>PartENat.card (ULift.{u_4, u_3} α) = PartENat.card α
<VAR>α : Type u_3<GOAL>PartENat.card (PLift α) = PartENat.card α
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>h : Set.InjOn f s<GOAL>PartENat.card ↑(f '' s) = PartENat.card ↑s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>h : Function.Injective f<GOAL>PartENat.card ↑(f '' s) = PartENat.card ↑s
<VAR>n : ℕ<VAR>c : Cardinal.{u_3}<GOAL>↑n ≤ Cardinal.toPartENat c ↔ ↑n ≤ c
<VAR>c : Cardinal.{u_3}<VAR>n : ℕ<GOAL>Cardinal.toPartENat c ≤ ↑n ↔ c ≤ ↑n
<VAR>n : ℕ<VAR>c : Cardinal.{u_3}<GOAL>↑n = Cardinal.toPartENat c ↔ ↑n = c
<VAR>c : Cardinal.{u_3}<VAR>n : ℕ<GOAL>Cardinal.toPartENat c = ↑n ↔ c = ↑n
<VAR>n : ℕ<VAR>c : Cardinal.{u_3}<GOAL>↑n < Cardinal.toPartENat c ↔ ↑n < c
<VAR>n : ℕ<VAR>c : Cardinal.{u_3}<GOAL>Cardinal.toPartENat c < ↑n ↔ c < ↑n
<VAR>α : Type u_3<GOAL>PartENat.card α = 0 ↔ IsEmpty α
<VAR>α : Type u_3<GOAL>PartENat.card α ≤ 1 ↔ Subsingleton α
<VAR>α : Type u_3<GOAL>1 < PartENat.card α ↔ Nontrivial α
<VAR>a : Cardinal.{u_1}<GOAL>(Cardinal.toENat a).toNat = Cardinal.toNat a
<VAR>n : ℕ∞<GOAL>Cardinal.toNat ↑n = n.toNat
<VAR>n : ℕ<GOAL>Cardinal.toNat ↑n = n
<VAR>c : Cardinal.{u}<GOAL>Cardinal.toNat c = 0 ↔ c = 0 ∨ Cardinal.aleph0 ≤ c
<VAR>c : Cardinal.{u}<GOAL>Cardinal.toNat c ≠ 0 ↔ c ≠ 0 ∧ c < Cardinal.aleph0
<VAR>c : Cardinal.{u}<GOAL>0 < Cardinal.toNat c ↔ c ≠ 0 ∧ c < Cardinal.aleph0
<VAR>c : Cardinal.{u_1}<VAR>h : c < Cardinal.aleph0<GOAL>↑(Cardinal.toNat c) = c
<VAR>c : Cardinal.{u}<VAR>h : c < Cardinal.aleph0<GOAL>Cardinal.toNat c = Classical.choose ⋯
<VAR>c : Cardinal.{u_1}<VAR>h : Cardinal.aleph0 ≤ c<GOAL>Cardinal.toNat c = 0
<VAR>c : Cardinal.{u_1}<VAR>h : Cardinal.aleph0 ≤ c<GOAL>↑(Cardinal.toNat c) = 0
<GOAL>StrictMonoOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
<GOAL>MonotoneOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
<GOAL>Set.InjOn (⇑Cardinal.toNat) (Set.Iio Cardinal.aleph0)
<VAR>c d : Cardinal.{u}<VAR>hc : c < Cardinal.aleph0<VAR>hd : d < Cardinal.aleph0<GOAL>Cardinal.toNat c = Cardinal.toNat d ↔ c = d
<VAR>c d : Cardinal.{u}<VAR>hc : c < Cardinal.aleph0<VAR>hd : d < Cardinal.aleph0<GOAL>Cardinal.toNat c ≤ Cardinal.toNat d ↔ c ≤ d
<VAR>c d : Cardinal.{u}<VAR>hc : c < Cardinal.aleph0<VAR>hd : d < Cardinal.aleph0<GOAL>Cardinal.toNat c < Cardinal.toNat d ↔ c < d
<VAR>c d : Cardinal.{u}<VAR>hcd : c ≤ d<VAR>hd : d < Cardinal.aleph0<GOAL>Cardinal.toNat c ≤ Cardinal.toNat d
<VAR>c d : Cardinal.{u}<VAR>hd : d < Cardinal.aleph0<VAR>hcd : c ≤ d<GOAL>Cardinal.toNat c ≤ Cardinal.toNat d
<VAR>c d : Cardinal.{u}<VAR>hcd : c < d<VAR>hd : d < Cardinal.aleph0<GOAL>Cardinal.toNat c < Cardinal.toNat d
<VAR>c d : Cardinal.{u}<VAR>hd : d < Cardinal.aleph0<VAR>hcd : c < d<GOAL>Cardinal.toNat c < Cardinal.toNat d
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.toNat (OfNat.ofNat n) = OfNat.ofNat n
<GOAL>Function.RightInverse Nat.cast ⇑Cardinal.toNat
<VAR>α : Type u<VAR>h : Infinite α<GOAL>Cardinal.toNat (Cardinal.mk α) = 0
<VAR>α : Type u<VAR>Fintype α<GOAL>Cardinal.toNat (Cardinal.mk α) = Fintype.card α
<VAR>c : Cardinal.{u}<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Cardinal.toNat c = n ↔ c = ↑n
<VAR>c : Cardinal.{u}<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>Cardinal.toNat c = OfNat.ofNat n ↔ c = OfNat.ofNat n
<VAR>c : Cardinal.{u}<GOAL>Cardinal.toNat c = 1 ↔ c = 1
<VAR>α : Type u<GOAL>Cardinal.toNat (Cardinal.mk α) = 1 ↔ Subsingleton α ∧ Nonempty α
<VAR>c : Cardinal.{v}<GOAL>Cardinal.toNat (Cardinal.lift.{u, v} c) = Cardinal.toNat c
<VAR>α : Type u<VAR>β : Type v<VAR>e : α ≃ β<GOAL>Cardinal.toNat (Cardinal.mk α) = Cardinal.toNat (Cardinal.mk β)
<VAR>x y : Cardinal.{u_1}<GOAL>Cardinal.toNat (x * y) = Cardinal.toNat x * Cardinal.toNat y
<VAR>α : Type u<VAR>s : Finset α<VAR>f : α → Cardinal.{u_1}<GOAL>Cardinal.toNat (∏ i ∈ s, f i) = ∏ i ∈ s, Cardinal.toNat (f i)
<VAR>c d : Cardinal.{u}<VAR>hc : c < Cardinal.aleph0<VAR>hd : d < Cardinal.aleph0<GOAL>Cardinal.toNat (c + d) = Cardinal.toNat c + Cardinal.toNat d
<VAR>a : Cardinal.{u}<VAR>b : Cardinal.{v}<VAR>ha : a < Cardinal.aleph0<VAR>hb : b < Cardinal.aleph0<GOAL>Cardinal.toNat (Cardinal.lift.{v, u} a + Cardinal.lift.{u, v} b) = Cardinal.toNat a + Cardinal.toNat b
<VAR>x : ↑I × ↑I<GOAL>Path.Homotopy.reflTransSymmAux x ∈ I
<GOAL>Continuous Path.Homotopy.transReflReparamAux
<VAR>t : ↑I<GOAL>Path.Homotopy.transReflReparamAux t ∈ I
<GOAL>Path.Homotopy.transReflReparamAux 0 = 0
<GOAL>Path.Homotopy.transReflReparamAux 1 = 1
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ : X<VAR>p : Path x₀ x₁<GOAL>p.trans (Path.refl x₁) = p.reparam (fun t => ⟨Path.Homotopy.transReflReparamAux t, ⋯⟩) ⋯ ⋯ ⋯
<GOAL>Continuous Path.Homotopy.transAssocReparamAux
<VAR>t : ↑I<GOAL>Path.Homotopy.transAssocReparamAux t ∈ I
<GOAL>Path.Homotopy.transAssocReparamAux 0 = 0
<GOAL>Path.Homotopy.transAssocReparamAux 1 = 1
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x₀ x₁ x₂ x₃ : X<VAR>p : Path x₀ x₁<VAR>q : Path x₁ x₂<VAR>r : Path x₂ x₃<GOAL>(p.trans q).trans r = (p.trans (q.trans r)).reparam (fun t => ⟨Path.Homotopy.transAssocReparamAux t, ⋯⟩) ⋯ ⋯ ⋯
<VAR>X : Type u_1<VAR>x : FundamentalGroupoid X<GOAL>(FundamentalGroupoid.equiv X) x = x.as
<VAR>X : Type u_1<VAR>x : X<GOAL>((FundamentalGroupoid.equiv X).symm x).as = x
<VAR>X : Type u_1<GOAL>IsEmpty (FundamentalGroupoid X) ↔ IsEmpty X
<VAR>X : Type u_1<GOAL>Nonempty (FundamentalGroupoid X) ↔ Nonempty X
<VAR>X : Type u_1<GOAL>Subsingleton (FundamentalGroupoid X) ↔ Subsingleton X
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x y z : FundamentalGroupoid X<VAR>p : x ⟶ y<VAR>q : y ⟶ z<GOAL>p ≫ q = Path.Homotopic.Quotient.comp p q
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>x : FundamentalGroupoid X<GOAL>𝟙 x = ⟦Path.refl x.as⟧
<VAR>X Y : TopCat<VAR>x₀ x₁ : ↑X<VAR>f : C(↑X, ↑Y)<VAR>p : Path.Homotopic.Quotient x₀ x₁<GOAL>(FundamentalGroupoid.fundamentalGroupoidFunctor.map f).map p = p.mapFn f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : AlgebraicTopology.DoldKan.HigherFacesVanish q φ<VAR>j : Fin (n + 2)<VAR>hj₁ : j ≠ 0<VAR>hj₂ : n + 2 ≤ ↑j + q<GOAL>φ ≫ X.δ j = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : AlgebraicTopology.DoldKan.HigherFacesVanish (q + 1) φ<GOAL>AlgebraicTopology.DoldKan.HigherFacesVanish q φ
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>Y Z : C<VAR>q n : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : AlgebraicTopology.DoldKan.HigherFacesVanish q φ<VAR>f : Z ⟶ Y<GOAL>AlgebraicTopology.DoldKan.HigherFacesVanish q (f ≫ φ)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : AlgebraicTopology.DoldKan.HigherFacesVanish q φ<VAR>hnaq : n = a + q<GOAL>φ ≫ (AlgebraicTopology.DoldKan.Hσ q).f (n + 1) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : AlgebraicTopology.DoldKan.HigherFacesVanish q φ<VAR>hqn : n < q<GOAL>φ ≫ (AlgebraicTopology.DoldKan.Hσ q).f (n + 1) = 0
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>CategoryTheory.Preadditive C<VAR>X : CategoryTheory.SimplicialObject C<VAR>Y : C<VAR>n q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : AlgebraicTopology.DoldKan.HigherFacesVanish q φ<GOAL>AlgebraicTopology.DoldKan.HigherFacesVanish (q + 1) (φ ≫ (𝟙 (AlgebraicTopology.AlternatingFaceMapComplex.obj X) + AlgebraicTopology.DoldKan.Hσ q).f (n + 1))
<GOAL>∀ (a : ℤ × ℤ), SetTheory.PGame.Domineering.shiftUp a = Prod.map id (fun x => x + 1) a
<GOAL>∀ (a : ℤ × ℤ), SetTheory.PGame.Domineering.shiftUp.symm a = Prod.map id (fun x => x + -1) a
<GOAL>∀ (a : ℤ × ℤ), SetTheory.PGame.Domineering.shiftRight.symm a = Prod.map (fun x => x + -1) id a
<GOAL>∀ (a : ℤ × ℤ), SetTheory.PGame.Domineering.shiftRight a = Prod.map (fun x => x + 1) id a
<VAR>b : SetTheory.PGame.Domineering.Board<VAR>x : ℤ × ℤ<GOAL>x ∈ SetTheory.PGame.Domineering.left b ↔ x ∈ b ∧ (x.1, x.2 - 1) ∈ b
<VAR>b : SetTheory.PGame.Domineering.Board<VAR>x : ℤ × ℤ<GOAL>x ∈ SetTheory.PGame.Domineering.right b ↔ x ∈ b ∧ (x.1 - 1, x.2) ∈ b
<VAR>b : SetTheory.PGame.Domineering.Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ SetTheory.PGame.Domineering.right b<GOAL>(m.1 - 1, m.2) ∈ Finset.erase b m
<VAR>b : SetTheory.PGame.Domineering.Board<VAR>m : ℤ × ℤ<VAR>h : m ∈ SetTheory.PGame.Domineering.left b<GOAL>(m.1, m.2 - 1) ∈ Finset.erase b m