ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<VAR>j : (J.Cover (unop (op X)))ᵒᵖ<GOAL>Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F))) (fun i => Multiequalizer.ι ((unop j).index (limit F)) i ≫ (limit.π F k).app (op i.Y)) ⋯ ≫ colimit.ι (J.diagram (F.obj k) X) j = (limit.lift (F ⋙ J.diagramFunctor D X) ((J.diagramFunctor D X).mapCone (limit.cone F))).app j ≫ colimit.ι (limit (F ⋙ J.diagramFunctor D X)) j ≫ (colimitLimitIso (F ⋙ J.diagramFunctor D X)).hom ≫ limit.lift (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) ((Cones.postcompose (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) ⋯).hom).obj (limit.cone (colimit (F ⋙ J.diagramFunctor D X).flip))) ≫ limit.π (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) k
<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>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<VAR>j : (J.Cover (unop (op X)))ᵒᵖ<GOAL>Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F))) (fun i => Multiequalizer.ι ((unop j).index (limit F)) i ≫ (limit.π F k).app (op i.Y)) ⋯ ≫ colimit.ι (J.diagram (F.obj k) X) j = (limit.lift (F ⋙ J.diagramFunctor D X) ((J.diagramFunctor D X).mapCone (limit.cone F))).app j ≫ colimit.ι (limit (F ⋙ J.diagramFunctor D X)) j ≫ (colimitLimitIso (F ⋙ J.diagramFunctor D X)).hom ≫ ((Cones.postcompose (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) ⋯).hom).obj (limit.cone (colimit (F ⋙ J.diagramFunctor D X).flip))).π.app k
<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>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<VAR>j : (J.Cover (unop (op X)))ᵒᵖ<GOAL>Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F))) (fun i => Multiequalizer.ι ((unop j).index (limit F)) i ≫ (limit.π F k).app (op i.Y)) ⋯ ≫ colimit.ι (J.diagram (F.obj k) X) j = (limit.lift (F ⋙ J.diagramFunctor D X) ((J.diagramFunctor D X).mapCone (limit.cone F))).app j ≫ (limit.π (F ⋙ J.diagramFunctor D X) k).app j ≫ (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k ≫ (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).hom
<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>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<VAR>j : (J.Cover (unop (op X)))ᵒᵖ<GOAL>Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F))) (fun i => Multiequalizer.ι ((unop j).index (limit F)) i ≫ (limit.π F k).app (op i.Y)) ⋯ ≫ colimit.ι (J.diagram (F.obj k) X) j = ((limit.lift (F ⋙ J.diagramFunctor D X) ((J.diagramFunctor D X).mapCone (limit.cone F)) ≫ limit.π (F ⋙ J.diagramFunctor D X) k).app j ≫ (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k) ≫ (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).hom
<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>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<VAR>j : (J.Cover (unop (op X)))ᵒᵖ<GOAL>Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F))) (fun i => Multiequalizer.ι ((unop j).index (limit F)) i ≫ (limit.π F k).app (op i.Y)) ⋯ ≫ colimit.ι (J.diagram (F.obj k) X) j = (((J.diagramFunctor D X).mapCone (limit.cone F)).π.app k).app j ≫ (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k ≫ (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).hom
<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>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<VAR>j : (J.Cover (unop (op X)))ᵒᵖ<GOAL>colimit.ι (J.diagram (F.obj k) X) j = (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k ≫ (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).hom
<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>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<VAR>j : (J.Cover (unop (op X)))ᵒᵖ<GOAL>colimit.ι (J.diagram (F.obj k) X) j ≫ (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).inv = (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k
<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>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<VAR>j : (J.Cover (unop (op X)))ᵒᵖ<GOAL>(((evaluation K D).obj k).mapCocone (colimit.cocone (F ⋙ J.diagramFunctor D X).flip)).ι.app j = (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k
<VAR>x y : PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x ⧏ y → ¬y ⧏ x
<VAR>x y : PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>hx : ∀ (i : xl) (j : xr), xL i < xR j<VAR>_oxl : ∀ (i : xl), (xL i).Numeric<VAR>_oxr : ∀ (i : xr), (xR i).Numeric<VAR>IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)<VAR>IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)<GOAL>(fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (mk xl xr xL xR)
<VAR>x y : PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>hx : ∀ (i : xl) (j : xr), xL i < xR j<VAR>_oxl : ∀ (i : xl), (xL i).Numeric<VAR>_oxr : ∀ (i : xr), (xR i).Numeric<VAR>IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)<VAR>IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>hy : ∀ (i : yl) (j : yr), yL i < yR j<VAR>oyl : ∀ (i : yl), (yL i).Numeric<VAR>oyr : ∀ (i : yr), (yR i).Numeric<VAR>_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR<VAR>_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR<GOAL>mk xl xr xL xR ⧏ mk yl yr yL yR → ¬mk yl yr yL yR ⧏ mk xl xr xL xR
<VAR>x y : PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>hx : ∀ (i : xl) (j : xr), xL i < xR j<VAR>_oxl : ∀ (i : xl), (xL i).Numeric<VAR>_oxr : ∀ (i : xr), (xR i).Numeric<VAR>IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)<VAR>IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>hy : ∀ (i : yl) (j : yr), yL i < yR j<VAR>oyl : ∀ (i : yl), (yL i).Numeric<VAR>oyr : ∀ (i : yr), (yR i).Numeric<VAR>_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR<VAR>_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR<GOAL>((∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR) → ¬((∃ i, mk yl yr yL yR ≤ xL i) ∨ ∃ j, yR j ≤ mk xl xr xL xR)
<VAR>n : ℕ<VAR>c : ℂ<GOAL>(iteratedDeriv n fun s => cexp (c * s)) = fun s => c ^ n * cexp (c * s)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H : Subgroup G<VAR>a✝ b✝ : G<GOAL>(setoid ↑H.toSubmonoid ↑⊥).Rel a✝ b✝ ↔ (QuotientGroup.rightRel H).Rel a✝ b✝
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H : Subgroup G<VAR>a✝ b✝ : G<GOAL>(setoid ↑H.toSubmonoid ↑⊥).Rel a✝ b✝ ↔ (setoid ↑H ↑⊥).Rel a✝ b✝
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>(W.variableChange C).Δ = ↑C.u⁻¹ ^ 12 * W.Δ
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>C : VariableChange R<GOAL>-((↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 + 4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2))) ^ 2 * ((↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 * (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) + 4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2)) * (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)) - ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) * (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) + ↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 - (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) ^ 2) - 8 * (2 * (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) + ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t))) ^ 3 - 27 * ((↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 + 4 * (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁))) ^ 2 + 9 * ((↑C.u⁻¹ * (W.a₁ + 2 * C.s)) ^ 2 + 4 * (↑C.u⁻¹ ^ 2 * (W.a₂ - C.s * W.a₁ + 3 * C.r - C.s ^ 2))) * (2 * (↑C.u⁻¹ ^ 4 * (W.a₄ - C.s * W.a₃ + 2 * C.r * W.a₂ - (C.t + C.r * C.s) * W.a₁ + 3 * C.r ^ 2 - 2 * C.s * C.t)) + ↑C.u⁻¹ * (W.a₁ + 2 * C.s) * (↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t))) * ((↑C.u⁻¹ ^ 3 * (W.a₃ + C.r * W.a₁ + 2 * C.t)) ^ 2 + 4 * (↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁))) = ↑C.u⁻¹ ^ 12 * (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 2 * (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) - 8 * (2 * W.a₄ + W.a₁ * W.a₃) ^ 3 - 27 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 + 9 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) * (W.a₃ ^ 2 + 4 * W.a₆))
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x✝ : E<VAR>h : StrictConvex 𝕜 s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>(a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x✝ : E<VAR>h : StrictConvex 𝕜 s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>a / (a + b) + b / (a + b) = 1
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x✝ : E<VAR>h : StrictConvex 𝕜 s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>(a + b) / (a + b) = 1
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x✝ : E<VAR>h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ interior s
<VAR>X : Scheme<VAR>R : CommRingCat<VAR>h : IsReduced (Spec R)<GOAL>_root_.IsReduced ↑R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : CommSemiring β<VAR>inst✝ : ContinuousAdd β<VAR>hf : SuperpolynomialDecay l k f<VAR>hg : SuperpolynomialDecay l k g<VAR>z : ℕ<GOAL>Tendsto (fun a => k a ^ z * (f + g) a) l (𝓝 0)
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝¹ : Monoid M<VAR>a : M<VAR>inst✝ : Invertible a<VAR>ha : a ∈ center M<GOAL>⅟a ∈ center M
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝¹ : Monoid M<VAR>a : M<VAR>inst✝ : Invertible a<VAR>ha : ∀ (g : M), g * a = a * g<GOAL>∀ (g : M), g * ⅟a = ⅟a * g
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>jacobiTheta τ = 1 + 2 * ∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * τ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>s✝ : Set α<VAR>a✝ : α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α<VAR>s : Set α<GOAL>s ∈ ae (dirac a) ↔ s ∈ pure a
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f g : V →ₗ[K] V<VAR>hfg : f * g = 1<GOAL>g * f = 1
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f g : V →ₗ[K] V<VAR>hfg : f * g = 1<VAR>ginj : Injective ⇑g<GOAL>g * f = 1
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f g : V →ₗ[K] V<VAR>hfg : f * g = 1<VAR>ginj : Injective ⇑g<VAR>i : V →ₗ[K] V<VAR>hi : g ∘ₗ i = id<GOAL>g * f = 1
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f g : V →ₗ[K] V<VAR>hfg : f * g = 1<VAR>ginj : Injective ⇑g<VAR>i : V →ₗ[K] V<VAR>hi : g ∘ₗ i = id<VAR>this : f * (g * i) = f * 1<GOAL>g * f = 1
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>inst✝ : FiniteDimensional K V<VAR>f g : V →ₗ[K] V<VAR>hfg : f * g = 1<VAR>ginj : Injective ⇑g<VAR>i : V →ₗ[K] V<VAR>hi : g ∘ₗ i = id<VAR>this : i = f<GOAL>g * f = 1
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x₁ x₂ L : A<GOAL>(baseChange W B).toAffine.addX (f x₁) (f x₂) (f L) = f ((baseChange W A).toAffine.addX x₁ x₂ L)
<VAR>R✝ : Type u<VAR>inst✝¹¹ : CommRing R✝<VAR>W✝ : Affine R✝<VAR>R : Type r<VAR>inst✝¹⁰ : CommRing R<VAR>W : Affine R<VAR>S : Type s<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>x₁ x₂ L : A<GOAL>(baseChange W B).toAffine.addX (f x₁) (f x₂) (f L) = (baseChange W B).toAffine.addX (f.toRingHom x₁) (f.toRingHom x₂) (f.toRingHom L)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Group M<VAR>inst✝¹ : Group N<VAR>inst✝ : Group P<VAR>c : Con M<VAR>x✝ y : M<VAR>h : c x✝ y<VAR>x : M<GOAL>c (x⁻¹ * x) 1
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<GOAL>Disjoint (⨆ k, (f.genEigenspace μ₁) k) (⨆ k, (f.genEigenspace μ₂) k)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ μ₂ : R<VAR>hμ : μ₁ ≠ μ₂<GOAL>∀ (i i_1 : ℕ), Disjoint ((f.genEigenspace μ₁) i) ((f.genEigenspace μ₂) i_1)
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝³ : Category.{?u.49535, u_1} E<VAR>F : D ⥤ E<VAR>G✝ : E ⥤ D<VAR>inst✝² : HasWeakSheafify J D<VAR>inst✝¹ : ConcreteCategory D<VAR>inst✝ : J.HasSheafCompose (forget D)<VAR>G : Type (max v₁ u₁) ⥤ D<VAR>adj : G ⊣ forget D<VAR>X : Sheaf J D<GOAL>((adjunctionToTypes J adj).counit.app X).val = sheafifyLift J ((X.1.associator (forget D) G).hom ≫ (Adjunction.whiskerRight Cᵒᵖ adj).counit.app X.1) ⋯
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝³ : Category.{?u.49535, u_1} E<VAR>F : D ⥤ E<VAR>G✝ : E ⥤ D<VAR>inst✝² : HasWeakSheafify J D<VAR>inst✝¹ : ConcreteCategory D<VAR>inst✝ : J.HasSheafCompose (forget D)<VAR>G : Type (max v₁ u₁) ⥤ D<VAR>adj : G ⊣ forget D<VAR>X : Sheaf J D<GOAL>toSheafify J (((whiskeringRight Cᵒᵖ (Type (max u₁ v₁)) D).obj G).obj ((sheafToPresheaf J (Type (max u₁ v₁))).obj ((sheafEquivSheafOfTypes J).inverse.obj ((sheafForget J).obj X)))) ≫ ((adjunctionToTypes J adj).counit.app X).val = (X.1.associator (forget D) G).hom ≫ (Adjunction.whiskerRight Cᵒᵖ adj).counit.app X.1
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝³ : Category.{?u.49535, u_1} E<VAR>F : D ⥤ E<VAR>G✝ : E ⥤ D<VAR>inst✝² : HasWeakSheafify J D<VAR>inst✝¹ : ConcreteCategory D<VAR>inst✝ : J.HasSheafCompose (forget D)<VAR>G : Type (max v₁ u₁) ⥤ D<VAR>adj : G ⊣ forget D<VAR>X : Sheaf J D<GOAL>toSheafify J (((whiskeringRight Cᵒᵖ (Type (max u₁ v₁)) D).obj G).obj ((sheafToPresheaf J (Type (max u₁ v₁))).obj ((sheafEquivSheafOfTypes J).inverse.obj ((sheafForget J).obj X)))) ≫ (((sheafCompose J (forget D)).associator (sheafEquivSheafOfTypes J).symm.inverse ((sheafEquivSheafOfTypes J).symm.functor ⋙ composeAndSheafify J G)).hom.app X).val ≫ ((whiskerLeft (sheafCompose J (forget D)) (whiskerRight (sheafEquivSheafOfTypes J).symm.toAdjunction.counit (composeAndSheafify J G))).app X).val ≫ ((adjunction J adj).counit.app X).val = (X.1.associator (forget D) G).hom ≫ (Adjunction.whiskerRight Cᵒᵖ adj).counit.app X.1
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝³ : Category.{?u.49535, u_1} E<VAR>F : D ⥤ E<VAR>G✝ : E ⥤ D<VAR>inst✝² : HasWeakSheafify J D<VAR>inst✝¹ : ConcreteCategory D<VAR>inst✝ : J.HasSheafCompose (forget D)<VAR>G : Type (max v₁ u₁) ⥤ D<VAR>adj : G ⊣ forget D<VAR>X : Sheaf J D<GOAL>toSheafify J (((whiskeringRight Cᵒᵖ (Type (max u₁ v₁)) D).obj G).obj ((sheafToPresheaf J (Type (max u₁ v₁))).obj ((sheafEquivSheafOfTypes J).inverse.obj ((sheafForget J).obj X)))) ≫ (((sheafCompose J (forget D)).associator (sheafEquivSheafOfTypes J).symm.inverse ((sheafEquivSheafOfTypes J).symm.functor ⋙ composeAndSheafify J G)).hom.app X).val ≫ ((whiskerLeft (sheafCompose J (forget D)) (whiskerRight (sheafEquivSheafOfTypes J).symm.toAdjunction.counit (composeAndSheafify J G))).app X).val ≫ sheafifyLift J (((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv (X.val ⋙ forget D) X.val).symm (𝟙 (X.val ⋙ forget D))) ⋯ = (X.1.associator (forget D) G).hom ≫ (Adjunction.whiskerRight Cᵒᵖ adj).counit.app X.1