ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>∀ (a : B), CategoryTheory.IsIso (F.mapId a)<VAR>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)<GOAL>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), ((CategoryTheory.Pseudofunctor.mkOfLax' F).mapComp f g).hom = CategoryTheory.inv (F.mapComp f g)
<VAR>B : Type u₁<VAR>CategoryTheory.Bicategory B<VAR>C : Type u₂<VAR>CategoryTheory.Bicategory C<VAR>F : CategoryTheory.LaxFunctor B C<VAR>∀ (a : B), CategoryTheory.IsIso (F.mapId a)<VAR>∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)<VAR>a : B<GOAL>((CategoryTheory.Pseudofunctor.mkOfLax' F).mapId a).hom = CategoryTheory.inv (F.mapId a)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F<GOAL>(L.lanAdjunction H).unit = L.lanUnit
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F<VAR>G : CategoryTheory.Functor D H<GOAL>(L.lanAdjunction H).counit.app G = (L.lan.obj (L.comp G)).descOfIsLeftKanExtension (L.lanUnit.app (L.comp G)) G (CategoryTheory.CategoryStruct.id (L.comp G))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F<VAR>G : CategoryTheory.Functor D H<GOAL>CategoryTheory.CategoryStruct.comp (L.lanUnit.app (L.comp G)) (CategoryTheory.whiskerLeft L ((L.lanAdjunction H).counit.app G)) = CategoryTheory.CategoryStruct.id (L.comp G)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F<VAR>G : CategoryTheory.Functor D H<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((L.lanUnit.app (L.comp G)).app X) (((L.lanAdjunction H).counit.app G).app (L.obj X)) = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (CategoryTheory.Functor C H)).obj (L.comp G)).obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F<VAR>G : CategoryTheory.Functor D H<GOAL>CategoryTheory.IsIso ((L.lanAdjunction H).counit.app G) ↔ G.IsLeftKanExtension (CategoryTheory.CategoryStruct.id (L.comp G))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_6, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F<GOAL>(L.ranAdjunction H).counit = L.ranCounit
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F<VAR>G : CategoryTheory.Functor D H<GOAL>(L.ranAdjunction H).unit.app G = (L.ran.obj (L.comp G)).liftOfIsRightKanExtension (L.ranCounit.app (L.comp G)) G (CategoryTheory.CategoryStruct.id (L.comp G))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F<VAR>G : CategoryTheory.Functor D H<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft L ((L.ranAdjunction H).unit.app G)) (L.ranCounit.app (L.comp G)) = CategoryTheory.CategoryStruct.id (L.comp G)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F<VAR>G : CategoryTheory.Functor D H<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (((L.ranAdjunction H).unit.app G).app (L.obj X)) ((L.ranCounit.app (L.comp G)).app X) = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (CategoryTheory.Functor D H)).obj G).obj (L.obj X))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_6, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>L : CategoryTheory.Functor C D<VAR>H : Type u_3<VAR>CategoryTheory.Category.{u_5, u_3} H<VAR>∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F<VAR>G : CategoryTheory.Functor D H<GOAL>CategoryTheory.IsIso ((L.ranAdjunction H).unit.app G) ↔ G.IsRightKanExtension (CategoryTheory.CategoryStruct.id (L.comp G))
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>self : CategoryTheory.IsPreconnected J<VAR>α : Type u₁<VAR>F : CategoryTheory.Functor J (CategoryTheory.Discrete α)<VAR>j : J<GOAL>Nonempty (F ≅ (CategoryTheory.Functor.const J).obj (F.obj j))
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>self : CategoryTheory.IsConnected J<GOAL>Nonempty J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.IsPreconnected J<VAR>α : Type u₂<VAR>F : CategoryTheory.Functor J (CategoryTheory.Discrete α)<VAR>j j' : J<GOAL>F.obj j = F.obj j'
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>h : ∀ {α : Type u₁} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j j' : J), F.obj j = F.obj j'<GOAL>CategoryTheory.IsPreconnected J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>Nonempty J<VAR>h : ∀ {α : Type u₁} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j j' : J), F.obj j = F.obj j'<GOAL>CategoryTheory.IsConnected J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.IsPreconnected J<VAR>α : Type u₂<VAR>F : J → α<VAR>h : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂<VAR>j j' : J<GOAL>F j = F j'
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'<GOAL>CategoryTheory.IsPreconnected J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>Nonempty J<VAR>h : ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'<GOAL>CategoryTheory.IsConnected J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.IsPreconnected J<VAR>p : Set J<VAR>j₀ : J<VAR>h0 : j₀ ∈ p<VAR>h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)<VAR>j : J<GOAL>j ∈ p
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₀ : J<VAR>h : ∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p<GOAL>CategoryTheory.IsConnected J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.IsPreconnected J<VAR>Z : J → Sort u_1<VAR>h₁ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂<VAR>h₂ : {j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁<VAR>j₀ : J<VAR>x : Z j₀<VAR>j : J<GOAL>Nonempty (Z j)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>CategoryTheory.IsPreconnected J<VAR>e : J ≌ K<GOAL>CategoryTheory.IsPreconnected K
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>e : J ≌ K<GOAL>CategoryTheory.IsPreconnected J ↔ CategoryTheory.IsPreconnected K
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>e : J ≌ K<VAR>CategoryTheory.IsConnected J<GOAL>CategoryTheory.IsConnected K
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>e : J ≌ K<GOAL>CategoryTheory.IsConnected J ↔ CategoryTheory.IsConnected K
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.IsPreconnected Jᵒᵖ<GOAL>CategoryTheory.IsPreconnected J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.IsConnected Jᵒᵖ<GOAL>CategoryTheory.IsConnected J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>X : J<GOAL>CategoryTheory.Zag X X
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<GOAL>Symmetric CategoryTheory.Zag
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ : J<VAR>h : CategoryTheory.Zag j₁ j₂<GOAL>CategoryTheory.Zag j₂ j₁
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ : J<VAR>f : j₁ ⟶ j₂<GOAL>CategoryTheory.Zag j₁ j₂
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ : J<VAR>f : j₂ ⟶ j₁<GOAL>CategoryTheory.Zag j₁ j₂
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<GOAL>Symmetric CategoryTheory.Zigzag
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<GOAL>Equivalence CategoryTheory.Zigzag
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>X : J<GOAL>CategoryTheory.Zigzag X X
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ : J<VAR>h : CategoryTheory.Zigzag j₁ j₂<GOAL>CategoryTheory.Zigzag j₂ j₁
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ j₃ : J<VAR>h₁ : CategoryTheory.Zigzag j₁ j₂<VAR>h₂ : CategoryTheory.Zigzag j₂ j₃<GOAL>CategoryTheory.Zigzag j₁ j₃
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ : J<VAR>h : CategoryTheory.Zag j₁ j₂<GOAL>CategoryTheory.Zigzag j₁ j₂
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ : J<VAR>f : j₁ ⟶ j₂<GOAL>CategoryTheory.Zigzag j₁ j₂
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ : J<VAR>f : j₂ ⟶ j₁<GOAL>CategoryTheory.Zigzag j₁ j₂
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ j₃ : J<VAR>h₁ : CategoryTheory.Zag j₁ j₂<VAR>h₂ : CategoryTheory.Zag j₂ j₃<GOAL>CategoryTheory.Zigzag j₁ j₃
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ j₃ : J<VAR>f₁₂ : j₁ ⟶ j₂<VAR>f₂₃ : j₂ ⟶ j₃<GOAL>CategoryTheory.Zigzag j₁ j₃
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ j₃ : J<VAR>f₁₂ : j₁ ⟶ j₂<VAR>f₃₂ : j₃ ⟶ j₂<GOAL>CategoryTheory.Zigzag j₁ j₃
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ j₃ : J<VAR>f₂₁ : j₂ ⟶ j₁<VAR>f₂₃ : j₂ ⟶ j₃<GOAL>CategoryTheory.Zigzag j₁ j₃
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>j₁ j₂ j₃ : J<VAR>f₂₁ : j₂ ⟶ j₁<VAR>f₃₂ : j₃ ⟶ j₂<GOAL>CategoryTheory.Zigzag j₁ j₃
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>F : CategoryTheory.Functor J K<VAR>j₁ j₂ : J<VAR>h : CategoryTheory.Zigzag j₁ j₂<GOAL>CategoryTheory.Zigzag (F.obj j₁) (F.obj j₂)
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>CategoryTheory.Category.{v₂, u₂} K<VAR>F : CategoryTheory.Functor J K<VAR>F.Full<VAR>j₁ j₂ : J<VAR>h : CategoryTheory.Zag (F.obj j₁) (F.obj j₂)<GOAL>CategoryTheory.Zag j₁ j₂
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.IsPreconnected J<VAR>r : J → J → Prop<VAR>hr : Equivalence r<VAR>h : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂<VAR>j₁ j₂ : J<GOAL>r j₁ j₂
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.IsPreconnected J<VAR>j₁ j₂ : J<GOAL>CategoryTheory.Zigzag j₁ j₂
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>h : ∀ (j₁ j₂ : J), CategoryTheory.Zigzag j₁ j₂<GOAL>CategoryTheory.IsPreconnected J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>Nonempty J<VAR>h : ∀ (j₁ j₂ : J), CategoryTheory.Zigzag j₁ j₂<GOAL>CategoryTheory.IsConnected J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>CategoryTheory.IsConnected J<VAR>j₁ j₂ : J<GOAL>∃ l, List.Chain CategoryTheory.Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>h : ∀ (j₁ j₂ : J), ∃ l, List.Chain CategoryTheory.Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂<GOAL>CategoryTheory.IsPreconnected J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>Nonempty J<VAR>h : ∀ (j₁ j₂ : J), ∃ l, List.Chain CategoryTheory.Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂<GOAL>CategoryTheory.IsConnected J
<VAR>J : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} J<VAR>C : Type u₂<VAR>CategoryTheory.Category.{u₁, u₂} C<VAR>CategoryTheory.IsPreconnected J<VAR>X Y : C<VAR>α : (CategoryTheory.Functor.const J).obj X ⟶ (CategoryTheory.Functor.const J).obj Y<VAR>j j' : J<GOAL>α.app j = α.app j'
<VAR>G : Type u_1<VAR>CategoryTheory.Groupoid G<VAR>CategoryTheory.IsPreconnected G<VAR>x y : G<GOAL>Nonempty (x ⟶ y)
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>f : a ⟶ b<GOAL>[CategoryTheory.Bicategory.IsLeftAdjoint f, CategoryTheory.Bicategory.HasAbsLeftKanExtension f (CategoryTheory.CategoryStruct.id a), ∃ (x : CategoryTheory.Bicategory.HasLeftKanExtension f (CategoryTheory.CategoryStruct.id a)), CategoryTheory.Bicategory.Lan.CommuteWith f (CategoryTheory.CategoryStruct.id a) f].TFAE
<VAR>B : Type u<VAR>CategoryTheory.Bicategory B<VAR>a b : B<VAR>u : b ⟶ a<GOAL>[CategoryTheory.Bicategory.IsRightAdjoint u, CategoryTheory.Bicategory.HasAbsLeftKanLift u (CategoryTheory.CategoryStruct.id a), ∃ (x : CategoryTheory.Bicategory.HasLeftKanLift u (CategoryTheory.CategoryStruct.id a)), CategoryTheory.Bicategory.LanLift.CommuteWith u (CategoryTheory.CategoryStruct.id a) u].TFAE
<VAR>R : Type u<VAR>CommRing R<VAR>f : Polynomial R<VAR>x y : R<GOAL>Polynomial.eval (x + y) f = f.sum fun e a => a * (x ^ e + ↑e * x ^ (e - 1) * y + ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2)
<VAR>R : Type u<VAR>CommRing R<VAR>f : Polynomial R<VAR>x y : R<GOAL>Polynomial.eval (x + y) f = ((f.sum fun e a => a * x ^ e) + f.sum fun e a => a * ↑e * x ^ (e - 1) * y) + f.sum fun e a => a * ↑(Polynomial.polyBinomAux1 x y e a) * y ^ 2
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<GOAL>AddAction.stabilizer G ∅ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<GOAL>MulAction.stabilizer G ∅ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<GOAL>MulAction.stabilizer G Set.univ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<GOAL>AddAction.stabilizer G Set.univ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>b : α<GOAL>AddAction.stabilizer G {b} = AddAction.stabilizer G b
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>b : α<GOAL>MulAction.stabilizer G {b} = MulAction.stabilizer G b
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>s : Set α<GOAL>a ∈ AddAction.stabilizer G s ↔ ∀ (b : α), a +ᵥ b ∈ s ↔ b ∈ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>s : Set α<GOAL>a ∈ MulAction.stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>AddGroup G<VAR>AddGroup H<VAR>f : G →+ H<VAR>s : Set G<GOAL>AddSubgroup.map f (AddAction.stabilizer G s) ≤ AddAction.stabilizer H (⇑f '' s)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>Group G<VAR>Group H<VAR>f : G →* H<VAR>s : Set G<GOAL>Subgroup.map f (MulAction.stabilizer G s) ≤ MulAction.stabilizer H (⇑f '' s)
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : Set G<GOAL>↑(AddAction.stabilizer G s) + s = s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Set G<GOAL>↑(MulAction.stabilizer G s) * s = s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Subgroup G<GOAL>MulAction.stabilizer G ↑s = s
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : AddSubgroup G<GOAL>AddAction.stabilizer G ↑s = s
<VAR>G : Type u_1<VAR>Group G<VAR>s : Subgroup G<GOAL>MulAction.stabilizer Gᵐᵒᵖ ↑s = s.op
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : AddSubgroup G<GOAL>AddAction.stabilizer Gᵃᵒᵖ ↑s = s.op
<VAR>G : Type u_1<VAR>AddGroup G<VAR>s : AddSubgroup Gᵃᵒᵖ<GOAL>AddAction.stabilizer G ↑s = s.unop
<VAR>G : Type u_1<VAR>Group G<VAR>s : Subgroup Gᵐᵒᵖ<GOAL>MulAction.stabilizer G ↑s = s.unop
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>MulAction.stabilizer G ↑s = MulAction.stabilizer G s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>DecidableEq α<VAR>s : Finset α<GOAL>AddAction.stabilizer G ↑s = AddAction.stabilizer G s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>DecidableEq α<GOAL>AddAction.stabilizer G ∅ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>DecidableEq α<GOAL>MulAction.stabilizer G ∅ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>DecidableEq α<VAR>Fintype α<GOAL>AddAction.stabilizer G Finset.univ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>DecidableEq α<VAR>Fintype α<GOAL>MulAction.stabilizer G Finset.univ = ⊤
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>DecidableEq α<VAR>b : α<GOAL>AddAction.stabilizer G {b} = AddAction.stabilizer G b
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>DecidableEq α<VAR>b : α<GOAL>MulAction.stabilizer G {b} = MulAction.stabilizer G b
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>DecidableEq α<VAR>s : Finset α<GOAL>a ∈ MulAction.stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>DecidableEq α<VAR>s : Finset α<GOAL>a ∈ AddAction.stabilizer G s ↔ ∀ (b : α), a +ᵥ b ∈ s ↔ b ∈ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>DecidableEq α<VAR>s : Finset α<GOAL>a ∈ MulAction.stabilizer G s ↔ s ⊆ a • s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>DecidableEq α<VAR>s : Finset α<GOAL>a ∈ AddAction.stabilizer G s ↔ s ⊆ a +ᵥ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>DecidableEq α<VAR>s : Finset α<GOAL>a ∈ AddAction.stabilizer G s ↔ a +ᵥ s ⊆ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>DecidableEq α<VAR>s : Finset α<GOAL>a ∈ MulAction.stabilizer G s ↔ a • s ⊆ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>DecidableEq α<VAR>s : Finset α<GOAL>a ∈ MulAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>DecidableEq α<VAR>s : Finset α<GOAL>a ∈ AddAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a +ᵥ b ∈ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>s : Set α<VAR>hs : s.Finite<GOAL>a ∈ AddAction.stabilizer G s ↔ s ⊆ a +ᵥ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>s : Set α<VAR>hs : s.Finite<GOAL>a ∈ MulAction.stabilizer G s ↔ s ⊆ a • s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>s : Set α<VAR>hs : s.Finite<GOAL>a ∈ AddAction.stabilizer G s ↔ a +ᵥ s ⊆ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>s : Set α<VAR>hs : s.Finite<GOAL>a ∈ MulAction.stabilizer G s ↔ a • s ⊆ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>AddGroup G<VAR>AddAction G α<VAR>a : G<VAR>s : Set α<VAR>hs : s.Finite<GOAL>a ∈ AddAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a +ᵥ b ∈ s
<VAR>G : Type u_1<VAR>α : Type u_3<VAR>Group G<VAR>MulAction G α<VAR>a : G<VAR>s : Set α<VAR>hs : s.Finite<GOAL>a ∈ MulAction.stabilizer G s ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
<VAR>G : Type u_1<VAR>CommGroup G<VAR>s : Set G<GOAL>s * ↑(MulAction.stabilizer G s) = s
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>s : Set G<GOAL>s + ↑(AddAction.stabilizer G s) = s
<VAR>G : Type u_1<VAR>CommGroup G<VAR>s : Set G<GOAL>MulAction.stabilizer (G ⧸ MulAction.stabilizer G s) (QuotientGroup.mk '' s) = ⊥
<VAR>G : Type u_1<VAR>AddCommGroup G<VAR>s : Set G<GOAL>AddAction.stabilizer (G ⧸ AddAction.stabilizer G s) (QuotientAddGroup.mk '' s) = ⊥
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₁ = F.map f.hom₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₂ = F.map f.hom₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>T : CategoryTheory.Pretriangulated.Triangle C<GOAL>F.mapTriangle.obj T = CategoryTheory.Pretriangulated.Triangle.mk (F.map T.mor₁) (F.map T.mor₂) (CategoryTheory.CategoryStruct.comp (F.map T.mor₃) ((F.commShiftIso 1).hom.app T.obj₁))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<GOAL>∀ {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), (F.mapTriangle.map f).hom₃ = F.map f.hom₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>n : ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCommShiftIso n).hom.app X).hom₃ = (F.commShiftIso n).hom.app X.obj₃
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>n : ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCommShiftIso n).inv.app X).hom₁ = (F.commShiftIso n).inv.app X.obj₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>n : ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCommShiftIso n).hom.app X).hom₁ = (F.commShiftIso n).hom.app X.obj₁
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>n : ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCommShiftIso n).hom.app X).hom₂ = (F.commShiftIso n).hom.app X.obj₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_4, u_1} C<VAR>CategoryTheory.Category.{u_5, u_2} D<VAR>CategoryTheory.HasShift C ℤ<VAR>CategoryTheory.HasShift D ℤ<VAR>F : CategoryTheory.Functor C D<VAR>F.CommShift ℤ<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Preadditive D<VAR>F.Additive<VAR>n : ℤ<VAR>X : CategoryTheory.Pretriangulated.Triangle C<GOAL>((F.mapTriangleCommShiftIso n).inv.app X).hom₃ = (F.commShiftIso n).inv.app X.obj₃