ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M₁<VAR>inst✝ : Module R M₁<VAR>I I' : R →+* R<VAR>B : M →ₗ[R] M →ₗ[R] M₁<VAR>hB : B.IsRefl<VAR>hB' : B.SeparatingRight<GOAL>ker B.flip = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S✝ S : IntermediateField K L<VAR>x✝ : L<GOAL>x✝ ∈ S.toIntermediateField' ⋯ ↔ x✝ ∈ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<GOAL>1 ≤ s.chainHeight ↔ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<GOAL>(∃ l ∈ s.subchain, l.length = 1) ↔ s.Nonempty
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<GOAL>(whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom).app X = ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F)).app X
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<GOAL>∀ (j : (J.Cover (unop X))ᵒᵖ), (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫ (whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom).app X = (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫ ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F)).app X
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>F.map (colimit.ι (J.diagram P (unop X)) W) ≫ F.map (colimMap (J.diagramNatTrans η (unop X))) ≫ (J.plusCompIso F Q).hom.app X = F.map (colimit.ι (J.diagram P (unop X)) W) ≫ (J.plusCompIso F P).hom.app X ≫ colimMap (J.diagramNatTrans (whiskerRight η F) (unop X))
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>F.map (colimit.ι (J.diagram P (unop X)) W) ≫ F.map (colimMap (J.diagramNatTrans η (unop X))) ≫ (J.plusCompIso F Q).hom.app X = (J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (Q ⋙ F)) ((J.diagram (P ⋙ F) (unop X)).obj W) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ F.map (η.app (op i.Y))) ⋯ ≫ colimit.ι (J.diagram (Q ⋙ F) (unop X)) W
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>F.map (colimit.ι (J.diagram P (unop X)) W ≫ colimMap (J.diagramNatTrans η (unop X))) ≫ (J.plusCompIso F Q).hom.app X = ((J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (Q ⋙ F)) ((J.diagram (P ⋙ F) (unop X)).obj W) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ F.map (η.app (op i.Y))) ⋯) ≫ colimit.ι (J.diagram (Q ⋙ F) (unop X)) W
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>F.map (colimit.ι (J.diagram P (unop X)) W ≫ colimit.desc (J.diagram P (unop X)) ((Cocones.precompose (J.diagramNatTrans η (unop X))).obj (colimit.cocone (J.diagram Q (unop X))))) ≫ (J.plusCompIso F Q).hom.app X = ((J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F))) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ F.map (η.app (op i.Y))) ⋯) ≫ colimit.ι (J.diagram (Q ⋙ F) (unop X)) W
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>F.map (((Cocones.precompose (J.diagramNatTrans η (unop X))).obj (colimit.cocone (J.diagram Q (unop X)))).ι.app W) ≫ (J.plusCompIso F Q).hom.app X = ((J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F))) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ F.map (η.app (op i.Y))) ⋯) ≫ colimit.ι (J.diagram (Q ⋙ F) (unop X)) W
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>F.map (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P)) (fun i => Multiequalizer.ι ((unop W).index P) i ≫ η.app (op i.Y)) ⋯ ≫ colimit.ι (J.diagram Q (unop X)) W) ≫ (J.plusCompIso F Q).hom.app X = ((J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F))) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ F.map (η.app (op i.Y))) ⋯) ≫ colimit.ι (J.diagram (Q ⋙ F) (unop X)) W
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>F.map (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P)) (fun i => Multiequalizer.ι ((unop W).index P) i ≫ η.app (op i.Y)) ⋯) ≫ (J.diagramCompIso F Q (unop X)).hom.app W ≫ colimit.ι (J.diagram (Q ⋙ F) (unop X)) W = (J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F))) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ F.map (η.app (op i.Y))) ⋯ ≫ colimit.ι (J.diagram (Q ⋙ F) (unop X)) W
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>(F.map (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P)) (fun i => Multiequalizer.ι ((unop W).index P) i ≫ η.app (op i.Y)) ⋯) ≫ (J.diagramCompIso F Q (unop X)).hom.app W) ≫ colimit.ι (J.diagram (Q ⋙ F) (unop X)) W = ((J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F))) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ F.map (η.app (op i.Y))) ⋯) ≫ colimit.ι (J.diagram (Q ⋙ F) (unop X)) W
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>F.map (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P)) (fun i => Multiequalizer.ι ((unop W).index P) i ≫ η.app (op i.Y)) ⋯) ≫ (J.diagramCompIso F Q (unop X)).hom.app W = (J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F))) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ F.map (η.app (op i.Y))) ⋯
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<GOAL>∀ (a : ((unop W).index (Q ⋙ F)).L), (F.map (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P)) (fun i => Multiequalizer.ι ((unop W).index P) i ≫ η.app (op i.Y)) ⋯) ≫ (J.diagramCompIso F Q (unop X)).hom.app W) ≫ Multiequalizer.ι ((unop W).index (Q ⋙ F)) a = ((J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F))) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ F.map (η.app (op i.Y))) ⋯) ≫ Multiequalizer.ι ((unop W).index (Q ⋙ F)) a
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<VAR>a : ((unop W).index (Q ⋙ F)).L<GOAL>(F.map (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P)) (fun i => Multiequalizer.ι ((unop W).index P) i ≫ η.app (op i.Y)) ⋯) ≫ (J.diagramCompIso F Q (unop X)).hom.app W) ≫ Multiequalizer.ι ((unop W).index (Q ⋙ F)) a = ((J.diagramCompIso F P (unop X)).hom.app W ≫ Multiequalizer.lift ((unop W).index (Q ⋙ F)) (multiequalizer ((unop W).index (P ⋙ F))) (fun i => Multiequalizer.ι ((unop W).index (P ⋙ F)) i ≫ F.map (η.app (op i.Y))) ⋯) ≫ Multiequalizer.ι ((unop W).index (Q ⋙ F)) a
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P✝ : Cᵒᵖ ⥤ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>P Q : Cᵒᵖ ⥤ D<VAR>η : P ⟶ Q<VAR>X : Cᵒᵖ<VAR>W : (J.Cover (unop X))ᵒᵖ<VAR>a : ((unop W).index (Q ⋙ F)).L<GOAL>F.map (Multiequalizer.lift ((unop W).index Q) (multiequalizer ((unop W).index P)) (fun i => Multiequalizer.ι ((unop W).index P) i ≫ η.app (op i.Y)) ⋯) ≫ F.map (Multiequalizer.ι ((unop W).index Q) a) = F.map (Multiequalizer.ι ((unop W).index P) a) ≫ F.map (η.app (op a.Y))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<GOAL>((optionEquivLeft R (n × n)).symm (univ R n)).IsHomogeneous (Fintype.card n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<VAR>aux : Fintype.card n = 0 + ∑ i : n, 1<GOAL>((optionEquivLeft R (n × n)).symm (univ R n)).IsHomogeneous (Fintype.card n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<VAR>aux : Fintype.card n = 0 + ∑ i : n, 1<GOAL>(∑ x : Equiv.Perm n, ↑↑(Equiv.Perm.sign x) * ∏ x_1 : n, ((Polynomial.aevalTower (rename some) (X none)) (if x x_1 = x_1 then Polynomial.X else 0) - X (some (x x_1, x_1)))).IsHomogeneous (0 + ∑ i : n, 1)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<VAR>aux : Fintype.card n = 0 + ∑ i : n, 1<GOAL>∀ i ∈ Finset.univ, (↑↑(Equiv.Perm.sign i) * ∏ x : n, ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) - X (some (i x, x)))).IsHomogeneous (0 + ∑ i : n, 1)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<VAR>aux : Fintype.card n = 0 + ∑ i : n, 1<VAR>i : Equiv.Perm n<GOAL>(↑↑(Equiv.Perm.sign i) * ∏ x : n, ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) - X (some (i x, x)))).IsHomogeneous (0 + ∑ i : n, 1)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<VAR>aux : Fintype.card n = 0 + ∑ i : n, 1<VAR>i : Equiv.Perm n<GOAL>(↑↑(Equiv.Perm.sign i)).IsHomogeneous 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<VAR>aux : Fintype.card n = 0 + ∑ i : n, 1<VAR>i : Equiv.Perm n<GOAL>(∏ x : n, ((Polynomial.aevalTower (rename some) (X none)) (if i x = x then Polynomial.X else 0) - X (some (i x, x)))).IsHomogeneous (∑ i : n, 1)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.803, u_1} C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : IndexSet Δ<VAR>Δ₁ : SimplexCategoryᵒᵖ<VAR>α₁ : unop Δ ⟶ unop Δ₁<VAR>hα₁ : Epi α₁<VAR>α₂ : unop Δ ⟶ unop Δ₁<VAR>hα₂ : Epi α₂<VAR>h₂ : e ⟨Δ₁, ⟨α₁, hα₁⟩⟩ ≫ eqToHom ⋯ = e ⟨Δ₁, ⟨α₂, hα₂⟩⟩<GOAL>⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₁, ⟨α₂, hα₂⟩⟩
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.803, u_1} C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A : IndexSet Δ<VAR>Δ₁ : SimplexCategoryᵒᵖ<VAR>α₁ : unop Δ ⟶ unop Δ₁<VAR>hα₁ : Epi α₁<VAR>α₂ : unop Δ ⟶ unop Δ₁<VAR>hα₂ : Epi α₂<VAR>h₂ : α₁ = α₂<GOAL>⟨Δ₁, ⟨α₁, hα₁⟩⟩ = ⟨Δ₁, ⟨α₂, hα₂⟩⟩
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : Algebra R S<VAR>f : A →ₐ[R] S<VAR>g : B →ₐ[R] S<GOAL>(productMap f g).range = f.range ⊔ g.range
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>(derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ Finsupp.total S (Ω[S⁄R]) S ⇑(D R S) = (kerTotal R S).mkQ
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>∀ (a b : S), ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) (single a b) = b𝖣a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>a b : S<GOAL>((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) (single a b) = b𝖣a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>a b : S<GOAL>((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) (single a b) = b • 1𝖣a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>f : ℕ → α<VAR>hf : Monotone f<VAR>n : ℕ<GOAL>disjointed f (n + 1) = f (n + 1) \ f n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>m k : ℤ<GOAL>2 * T R m * T R k = T R (m + k) + T R (m - k)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>inst✝³ : Fintype V<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : Fintype (Sym2 V)<VAR>inst✝ : DecidableEq V<VAR>v : V<GOAL>(filter (fun d => d.toProd.1 = v) univ).card = G.degree v
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasFDerivAtFilter f f' x L<VAR>hg : HasFDerivAtFilter g g' x L<VAR>x✝ : E<GOAL>f x✝ - f x - f' (x✝ - x) + (g x✝ - g x - g' (x✝ - x)) = f x✝ + g x✝ - (f x + g x) - (f' + g') (x✝ - x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hf : HasFDerivAtFilter f f' x L<VAR>hg : HasFDerivAtFilter g g' x L<VAR>x✝ : E<GOAL>f x✝ - f x - (f' x✝ - f' x) + (g x✝ - g x - (g' x✝ - g' x)) = f x✝ + g x✝ - (f x + g x) - (f' x✝ + g' x✝ - (f' x + g' x))