ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x y : P.Elements<VAR>f : x ⟶ y<VAR>eq₁ : yoneda.map (↑f).unop ≫ yonedaEquiv.symm x.snd = yonedaEquiv.symm y.snd<GOAL>yoneda.map (↑f).unop ≫ coconeApp φ x = coconeApp φ y
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x y : P.Elements<VAR>f : x ⟶ y<VAR>eq₁ : yoneda.map (↑f).unop ≫ yonedaEquiv.symm x.snd = yonedaEquiv.symm y.snd<VAR>eq₂ : ((G.obj (yoneda.obj (Opposite.unop x.1))).map (F.map (↑f).unop).op ≫ (G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop y.fst)))) ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (Opposite.unop (Opposite.op (F.obj (Opposite.unop x.fst)))))) = ((G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop x.fst))) ≫ (G.obj P).map (F.map (↑f).unop).op) ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (Opposite.unop (Opposite.op (F.obj (Opposite.unop x.fst))))))<GOAL>yoneda.map (↑f).unop ≫ coconeApp φ x = coconeApp φ y
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x y : P.Elements<VAR>f : x ⟶ y<VAR>eq₁ : yoneda.map (↑f).unop ≫ yonedaEquiv.symm x.snd = yonedaEquiv.symm y.snd<VAR>eq₂ : ((G.obj (yoneda.obj (Opposite.unop x.1))).map (F.map (↑f).unop).op ≫ (G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop y.fst)))) ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (Opposite.unop (Opposite.op (F.obj (Opposite.unop x.fst)))))) = ((G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop x.fst))) ≫ (G.obj P).map (F.map (↑f).unop).op) ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (Opposite.unop (Opposite.op (F.obj (Opposite.unop x.fst))))))<VAR>eq₃ : ((F ⋙ yoneda).map (↑f).unop ≫ φ.app (Opposite.unop x.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (Opposite.unop (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))))) = (φ.app (Opposite.unop y.fst) ≫ (yoneda ⋙ G).map (↑f).unop).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (Opposite.unop (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst)))))<GOAL>yoneda.map (↑f).unop ≫ coconeApp φ x = coconeApp φ y
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x y : P.Elements<VAR>f : x ⟶ y<VAR>eq₁ : yoneda.map (↑f).unop ≫ yonedaEquiv.symm x.snd = yonedaEquiv.symm y.snd<VAR>eq₂ : ((G.obj (yoneda.obj (Opposite.unop x.1))).map (F.map (↑f).unop).op ≫ (G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop y.fst)))) ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (Opposite.unop (Opposite.op (F.obj (Opposite.unop x.fst)))))) = ((G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop x.fst))) ≫ (G.obj P).map (F.map (↑f).unop).op) ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (Opposite.unop (Opposite.op (F.obj (Opposite.unop x.fst))))))<VAR>eq₃ : ((F ⋙ yoneda).map (↑f).unop ≫ φ.app (Opposite.unop x.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (Opposite.unop (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))))) = (φ.app (Opposite.unop y.fst) ≫ (yoneda ⋙ G).map (↑f).unop).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (Opposite.unop (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst)))))<VAR>eq₄ : ∀ (a : ((F ⋙ yoneda).obj (Opposite.unop x.fst)).obj (Opposite.op (F.obj (Opposite.unop x.fst)))), (((F ⋙ yoneda).obj (Opposite.unop x.fst)).map (F.map (↑f).unop).op ≫ (φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop y.fst)))) a = ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) ≫ ((yoneda ⋙ G).obj (Opposite.unop x.fst)).map (F.map (↑f).unop).op) a<GOAL>yoneda.map (↑f).unop ≫ coconeApp φ x = coconeApp φ y
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x y : P.Elements<VAR>f : x ⟶ y<VAR>eq₁ : yoneda.map (↑f).unop ≫ yonedaEquiv.symm x.snd = yonedaEquiv.symm y.snd<VAR>eq₂ : (G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop y.fst))) ((G.obj (yoneda.obj (Opposite.unop x.1))).map (F.map (↑f).unop).op ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (F.obj (Opposite.unop x.fst))))) = (G.obj P).map (F.map (↑f).unop).op ((G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop x.fst))) ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (F.obj (Opposite.unop x.fst)))))<VAR>eq₃ : (φ.app (Opposite.unop x.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (F.toPrefunctor.1 (Opposite.unop y.fst)) ≫ F.map (↑f).unop) = (G.map (yoneda.map (↑f).unop)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) ((φ.app (Opposite.unop y.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (F.toPrefunctor.1 (Opposite.unop y.fst))))<VAR>eq₄ : ∀ (a : F.obj (Opposite.unop x.fst) ⟶ F.obj (Opposite.unop x.fst)), (φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop y.fst))) (F.map (↑f).unop ≫ a) = (G.obj (yoneda.obj (Opposite.unop x.fst))).map (F.map (↑f).unop).op ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) a)<GOAL>yoneda.map (↑f).unop ≫ coconeApp φ x = coconeApp φ y
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x y : P.Elements<VAR>f : x ⟶ y<VAR>eq₁ : yoneda.map (↑f).unop ≫ yonedaEquiv.symm x.snd = yonedaEquiv.symm y.snd<VAR>eq₂ : (G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop y.fst))) ((G.obj (yoneda.obj (Opposite.unop x.1))).map (F.map (↑f).unop).op ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (F.obj (Opposite.unop x.fst))))) = (G.obj P).map (F.map (↑f).unop).op ((G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop x.fst))) ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (F.obj (Opposite.unop x.fst)))))<VAR>eq₃ : (φ.app (Opposite.unop x.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (F.toPrefunctor.1 (Opposite.unop y.fst)) ≫ F.map (↑f).unop) = (G.map (yoneda.map (↑f).unop)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) ((φ.app (Opposite.unop y.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (F.toPrefunctor.1 (Opposite.unop y.fst))))<VAR>eq₄ : ∀ (a : F.obj (Opposite.unop x.fst) ⟶ F.obj (Opposite.unop x.fst)), (φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop y.fst))) (F.map (↑f).unop ≫ a) = (G.obj (yoneda.obj (Opposite.unop x.fst))).map (F.map (↑f).unop).op ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) a)<GOAL>yonedaEquiv (yoneda.map (↑f).unop ≫ coconeApp φ x) = yonedaEquiv (coconeApp φ y)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x y : P.Elements<VAR>f : x ⟶ y<VAR>eq₁ : yoneda.map (↑f).unop ≫ yonedaEquiv.symm x.snd = yonedaEquiv.symm y.snd<VAR>eq₂ : (G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop y.fst))) ((G.obj (yoneda.obj (Opposite.unop x.1))).map (F.map (↑f).unop).op ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (F.obj (Opposite.unop x.fst))))) = (G.obj P).map (F.map (↑f).unop).op ((G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop x.fst))) ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (F.obj (Opposite.unop x.fst)))))<VAR>eq₃ : (φ.app (Opposite.unop x.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (F.toPrefunctor.1 (Opposite.unop y.fst)) ≫ F.map (↑f).unop) = (G.map (yoneda.map (↑f).unop)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) ((φ.app (Opposite.unop y.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (F.toPrefunctor.1 (Opposite.unop y.fst))))<VAR>eq₄ : ∀ (a : F.obj (Opposite.unop x.fst) ⟶ F.obj (Opposite.unop x.fst)), (φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop y.fst))) (F.map (↑f).unop ≫ a) = (G.obj (yoneda.obj (Opposite.unop x.fst))).map (F.map (↑f).unop).op ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) a)<GOAL>yonedaEquiv (yoneda.map (↑f).unop ≫ yonedaEquiv.symm ((G.map (yonedaEquiv.symm x.snd)).app (F.op.obj (Opposite.op (Opposite.unop x.fst))) ((φ.app (Opposite.unop x.fst)).app (F.op.obj (Opposite.op (Opposite.unop x.fst))) (𝟙 (Opposite.unop (F.op.obj (Opposite.op (Opposite.unop x.fst)))))))) = yonedaEquiv (yonedaEquiv.symm ((G.map (yonedaEquiv.symm y.snd)).app (F.op.obj (Opposite.op (Opposite.unop y.fst))) ((φ.app (Opposite.unop y.fst)).app (F.op.obj (Opposite.op (Opposite.unop y.fst))) (𝟙 (Opposite.unop (F.op.obj (Opposite.op (Opposite.unop y.fst))))))))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x y : P.Elements<VAR>f : x ⟶ y<VAR>eq₁ : yoneda.map (↑f).unop ≫ yonedaEquiv.symm x.snd = yonedaEquiv.symm y.snd<VAR>eq₂ : (G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop y.fst))) ((G.obj (yoneda.obj (Opposite.unop x.1))).map (F.map (↑f).unop).op ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (F.obj (Opposite.unop x.fst))))) = (G.obj P).map (F.map (↑f).unop).op ((G.map (yonedaEquiv.symm x.snd)).app (Opposite.op (F.obj (Opposite.unop x.fst))) ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) (𝟙 (F.obj (Opposite.unop x.fst)))))<VAR>eq₃ : (φ.app (Opposite.unop x.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (F.toPrefunctor.1 (Opposite.unop y.fst)) ≫ F.map (↑f).unop) = (G.map (yoneda.map (↑f).unop)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) ((φ.app (Opposite.unop y.fst)).app (Opposite.op (F.toPrefunctor.1 (Opposite.unop y.fst))) (𝟙 (F.toPrefunctor.1 (Opposite.unop y.fst))))<VAR>eq₄ : ∀ (a : F.obj (Opposite.unop x.fst) ⟶ F.obj (Opposite.unop x.fst)), (φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop y.fst))) (F.map (↑f).unop ≫ a) = (G.obj (yoneda.obj (Opposite.unop x.fst))).map (F.map (↑f).unop).op ((φ.app (Opposite.unop x.fst)).app (Opposite.op (F.obj (Opposite.unop x.fst))) a)<GOAL>(F.op ⋙ G.obj P).map (↑f).unop.op ((G.map (yonedaEquiv.symm x.snd)).app (F.op.obj (Opposite.op (Opposite.unop x.fst))) ((φ.app (Opposite.unop x.fst)).app (F.op.obj (Opposite.op (Opposite.unop x.fst))) (𝟙 (Opposite.unop (F.op.obj (Opposite.op (Opposite.unop x.fst))))))) = (G.map (yonedaEquiv.symm y.snd)).app (F.op.obj (Opposite.op (Opposite.unop y.fst))) ((φ.app (Opposite.unop y.fst)).app (F.op.obj (Opposite.op (Opposite.unop y.fst))) (𝟙 (Opposite.unop (F.op.obj (Opposite.op (Opposite.unop y.fst))))))
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>x : α<GOAL>Tendsto (fun n => f^[n] x) atTop (𝓝 (fixedPoint f hf))
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>x : α<GOAL>fixedPoint f hf = efixedPoint f hf x ⋯
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>K : ℝ≥0<VAR>f : α → α<VAR>hf : ContractingWith K f<VAR>inst✝¹ : Nonempty α<VAR>inst✝ : CompleteSpace α<VAR>x : α<GOAL>IsFixedPt f (efixedPoint f hf x ⋯)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁵ : OrderedSemiring 𝕜<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : AddCancelCommMonoid E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>z x : E<VAR>hx : x ∈ (fun x => z + x) ⁻¹' s<VAR>y : E<VAR>hy : y ∈ (fun x => z + x) ⁻¹' 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 ((fun x => z + x) ⁻¹' 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✝⁵ : OrderedSemiring 𝕜<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : AddCancelCommMonoid E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>z x : E<VAR>hx : x ∈ (fun x => z + x) ⁻¹' s<VAR>y : E<VAR>hy : y ∈ (fun x => z + x) ⁻¹' 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 ∈ (fun b => z + b) ⁻¹' 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✝⁵ : OrderedSemiring 𝕜<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : TopologicalSpace F<VAR>inst✝² : AddCancelCommMonoid E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : StrictConvex 𝕜 s<VAR>z x : E<VAR>hx : x ∈ (fun x => z + x) ⁻¹' s<VAR>y : E<VAR>hy : y ∈ (fun x => z + x) ⁻¹' s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>h : a • (fun x => z + x) x + b • (fun x => z + x) y ∈ interior s<GOAL>a • x + b • y ∈ (fun b => z + b) ⁻¹' interior s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<GOAL>(𝓝 0).HasBasis (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}<GOAL>(𝓝 0).HasBasis (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}<GOAL>(Filter.map mk (𝓝 0)).HasBasis (fun ε => 0 < ε) fun x => mk '' ball 0 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<GOAL>QuotientMap (⇑h ∘ ⇑h.symm)
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Sub R<VAR>inst✝ : BoundedSub R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<GOAL>∃ C, ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Sub R<VAR>inst✝ : BoundedSub R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<VAR>C : ℝ<VAR>hC : ∀ ⦃x : R⦄, x ∈ Set.range f - Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f - Set.range g → dist x y ≤ C<GOAL>∃ C, ∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Sub R<VAR>inst✝ : BoundedSub R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<VAR>C : ℝ<VAR>hC : ∀ ⦃x : R⦄, x ∈ Set.range f - Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f - Set.range g → dist x y ≤ C<GOAL>∀ (x y : X), dist ((f - g) x) ((f - g) y) ≤ C
<VAR>R : Type u_1<VAR>X : Type u_2<VAR>inst✝² : PseudoMetricSpace R<VAR>inst✝¹ : Sub R<VAR>inst✝ : BoundedSub R<VAR>f g : X → R<VAR>f_bdd : ∃ C, ∀ (x y : X), dist (f x) (f y) ≤ C<VAR>g_bdd : ∃ C, ∀ (x y : X), dist (g x) (g y) ≤ C<VAR>C : ℝ<VAR>hC : ∀ ⦃x : R⦄, x ∈ Set.range f - Set.range g → ∀ ⦃y : R⦄, y ∈ Set.range f - Set.range g → dist x y ≤ C<VAR>x y : X<GOAL>dist ((f - g) x) ((f - g) y) ≤ C
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ : R⟦X⟧<VAR>n : PartENat<GOAL>φ.order = n ↔ (∀ (i : ℕ), ↑i = n → (coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → (coeff R i) φ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ : R⟦X⟧<GOAL>φ.order = ⊤ ↔ (∀ (i : ℕ), ↑i = ⊤ → (coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ⊤ → (coeff R i) φ = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ : R⟦X⟧<VAR>n✝ : ℕ<GOAL>φ.order = ↑n✝ ↔ (∀ (i : ℕ), ↑i = ↑n✝ → (coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < ↑n✝ → (coeff R i) φ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c : β<GOAL>c ≥ fold max b f s ↔ b ≤ c ∧ ∀ x ∈ s, f x ≤ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c : β<GOAL>∀ {x y z : β}, x ≥ max y z ↔ x ≥ y ∧ x ≥ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : LinearOrder β<VAR>c x y z : β<GOAL>max y z ≤ x ↔ x ≥ y ∧ x ≥ z
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : PartialOrder A<VAR>inst✝¹ : Algebra ℝ A<VAR>inst✝ : NonnegSpectrumClass ℝ A<VAR>a : A<VAR>x : ℝ≥0<VAR>ha : autoParam (0 ≤ a) _auto✝<GOAL>↑x ∈ spectrum ℝ a ↔ x ∈ spectrum ℝ≥0 a
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<GOAL>0 ≤ p.degree ↔ p ≠ 0
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>t ⋖ s ↔ t ⊆ s ∧ (s \ t).card = 1
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>(∃ a ∉ t, insert a t = s) ↔ t ⊆ s ∧ (s \ t).card = 1
<VAR>R : Type u_1<VAR>inst✝⁹ : Ring R<VAR>E : Type u_2<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module R E<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup F<VAR>inst✝⁵ : Module R F<VAR>G : Type u_4<VAR>inst✝⁴ : AddCommGroup G<VAR>inst✝³ : Module R G<VAR>M : Type u_5<VAR>inst✝² : Monoid M<VAR>inst✝¹ : DistribMulAction M F<VAR>inst✝ : SMulCommClass R M F<VAR>y : M<VAR>f : E →ₗ.[R] F<VAR>fst✝¹ : E<VAR>snd✝¹ : F<VAR>hx : (fst✝¹, snd✝¹) ∈ f.graph<VAR>fst✝ : E<VAR>snd✝ : F<VAR>hy : (fst✝, snd✝) ∈ f.graph<VAR>hxy : (fst✝¹, snd✝¹).1 = (fst✝, snd✝).1<GOAL>(fst✝¹, snd✝¹).2 = (fst✝, snd✝).2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : CompactSpace α<GOAL>𝓝ˢ (diagonal α) = 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : CompactSpace α<GOAL>𝓤 α ≤ 𝓝ˢ (diagonal α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : CompactSpace α<VAR>this : (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U<GOAL>𝓤 α ≤ 𝓝ˢ (diagonal α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : CompactSpace α<VAR>this : (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U<VAR>U : Set (α × α)<VAR>hU : U ∈ 𝓤 α<GOAL>⋃ x ∈ diagonal α, ball x ((fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U) ∈ 𝓤 α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<GOAL>AEStronglyMeasurable f μ ↔ AEMeasurable f μ ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<GOAL>(AEMeasurable f μ ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t) → AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>H : AEMeasurable f μ<VAR>t : Set β<VAR>t_sep : IsSeparable t<VAR>ht : ∀ᵐ (x : α) ∂μ, f x ∈ t<GOAL>AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>H : AEMeasurable f μ<VAR>t_sep : IsSeparable ∅<VAR>ht : ∀ᵐ (x : α) ∂μ, f x ∈ ∅<GOAL>AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f g : α → β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : BorelSpace β<VAR>H : AEMeasurable f μ<VAR>t : Set β<VAR>t_sep : IsSeparable t<VAR>ht : ∀ᵐ (x : α) ∂μ, f x ∈ t<VAR>h₀ : t.Nonempty<GOAL>AEStronglyMeasurable f μ
<VAR>R : Type u<VAR>M : Type v<VAR>M'✝ : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid M'✝<VAR>inst✝² : Module R M'✝<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>S : Set R<VAR>T : Set M<VAR>M' : Type w<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>ι : Type u_4<VAR>s : Set ι<VAR>f : ι → M<VAR>x : M<GOAL>x ∈ I • span R (f '' s) ↔ ∃ a, ∃ (_ : ∀ (i : ↑s), a i ∈ I), (a.sum fun i c => c • f ↑i) = x