ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>inst✝ : FunLike F α β<VAR>e : α ≃ β<VAR>s : Set β<GOAL>(fun s => ⇑e '' s) ((fun s => ⇑e.symm '' s) s) = s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>inst✝ : FunLike F α β<VAR>e : α ≃ β<VAR>a✝ b✝ : Set α<VAR>h : { toFun := fun s => ⇑e '' s, invFun := fun s => ⇑e.symm '' s, left_inv := ⋯, right_inv := ⋯ } a✝ ≤ { toFun := fun s => ⇑e '' s, invFun := fun s => ⇑e.symm '' s, left_inv := ⋯, right_inv := ⋯ } b✝<GOAL>a✝ ≤ b✝
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C₁<VAR>inst✝⁷ : Category.{u_5, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{u_6, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) := TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv<VAR>this : Nonempty (w.CostructuredArrowDownwards y)<GOAL>IsConnected ((TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv).CostructuredArrowDownwards y)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C₁<VAR>inst✝⁷ : Category.{u_5, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{u_6, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) := TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv<VAR>this : Nonempty (w.CostructuredArrowDownwards y)<GOAL>∀ (X : w.CostructuredArrowDownwards y), ∃ Y, Zigzag X ((fromRightResolution Φ L y).obj Y)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C₁<VAR>inst✝⁷ : Category.{u_5, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{u_6, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) := TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv<VAR>this : Nonempty (w.CostructuredArrowDownwards y)<VAR>X : w.CostructuredArrowDownwards y<GOAL>∃ Y, Zigzag X ((fromRightResolution Φ L y).obj Y)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C₁<VAR>inst✝⁷ : Category.{u_5, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{u_6, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) := TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv<VAR>this : Nonempty (w.CostructuredArrowDownwards y)<VAR>c : C₁<VAR>g : X₂ ⟶ Φ.functor.obj c<VAR>x : (Φ.functor ⋙ L).obj c ⟶ X₃<VAR>fac : L.map g ≫ w.app c ≫ (𝟭 D).map x = y<GOAL>∃ Y, Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac) ((fromRightResolution Φ L y).obj Y)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C₁<VAR>inst✝⁷ : Category.{u_5, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{u_6, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) := TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv<VAR>this : Nonempty (w.CostructuredArrowDownwards y)<VAR>c : C₁<VAR>g : X₂ ⟶ Φ.functor.obj c<VAR>x : L.obj (Φ.functor.obj c) ⟶ X₃<VAR>fac : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y<GOAL>∃ Y, Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac) ((fromRightResolution Φ L y).obj Y)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C₁<VAR>inst✝⁷ : Category.{u_5, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{u_6, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) := TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv<VAR>this : Nonempty (w.CostructuredArrowDownwards y)<VAR>c : C₁<VAR>g : X₂ ⟶ Φ.functor.obj c<VAR>x : L.obj (Φ.functor.obj c) ⟶ X₃<VAR>fac✝ : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y<VAR>fac : L.map g ≫ x = y<GOAL>∃ Y, Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac✝) ((fromRightResolution Φ L y).obj Y)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C₁<VAR>inst✝⁷ : Category.{u_5, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{u_6, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) := TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv<VAR>this : Nonempty (w.CostructuredArrowDownwards y)<VAR>c : C₁<VAR>g : X₂ ⟶ Φ.functor.obj c<VAR>x : L.obj (Φ.functor.obj c) ⟶ X₃<VAR>fac✝ : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y<VAR>fac : L.map g ≫ x = y<VAR>ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary (Φ.arrow.RightResolution (Arrow.mk g))<GOAL>∃ Y, Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac✝) ((fromRightResolution Φ L y).obj Y)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C₁<VAR>inst✝⁷ : Category.{u_5, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{u_6, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) := TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv<VAR>this : Nonempty (w.CostructuredArrowDownwards y)<VAR>c : C₁<VAR>g : X₂ ⟶ Φ.functor.obj c<VAR>x : L.obj (Φ.functor.obj c) ⟶ X₃<VAR>fac✝ : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y<VAR>fac : L.map g ≫ x = y<VAR>ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary (Φ.arrow.RightResolution (Arrow.mk g))<GOAL>Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac✝) ((fromRightResolution Φ L y).obj (RightResolution.mk ρ.w.left ⋯))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C₁<VAR>inst✝⁷ : Category.{u_5, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{u_6, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) := TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv<VAR>this✝ : Nonempty (w.CostructuredArrowDownwards y)<VAR>c : C₁<VAR>g : X₂ ⟶ Φ.functor.obj c<VAR>x : L.obj (Φ.functor.obj c) ⟶ X₃<VAR>fac✝ : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y<VAR>fac : L.map g ≫ x = y<VAR>ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary (Φ.arrow.RightResolution (Arrow.mk g))<VAR>this : Zigzag ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk (𝟙 (Φ.functor.obj c)) ⋯)) ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk ρ.w.right ⋯))<GOAL>Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac✝) ((fromRightResolution Φ L y).obj (RightResolution.mk ρ.w.left ⋯))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C₁<VAR>inst✝⁷ : Category.{u_5, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{u_6, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) := TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv<VAR>this✝ : Nonempty (w.CostructuredArrowDownwards y)<VAR>c : C₁<VAR>g : X₂ ⟶ Φ.functor.obj c<VAR>x : L.obj (Φ.functor.obj c) ⟶ X₃<VAR>fac✝ : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y<VAR>fac : L.map g ≫ x = y<VAR>ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary (Φ.arrow.RightResolution (Arrow.mk g))<VAR>this : Zigzag ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk (𝟙 (Φ.functor.obj c)) ⋯)) ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk ρ.w.right ⋯))<GOAL>Zigzag (TwoSquare.CostructuredArrowDownwards.mk w y c g x fac✝) ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk (𝟙 (Φ.functor.obj c)) ⋯))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>inst✝⁸ : Category.{u_4, u_1} C₁<VAR>inst✝⁷ : Category.{u_5, u_2} C₂<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>inst✝⁶ : Φ.IsLocalizedEquivalence<VAR>inst✝⁵ : W₁.IsMultiplicative<VAR>inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)<VAR>inst✝³ : Φ.arrow.HasRightResolutions<VAR>inst✝² : W₂.ContainsIdentities<VAR>D : Type u_3<VAR>inst✝¹ : Category.{u_6, u_3} D<VAR>L : C₂ ⥤ D<VAR>inst✝ : L.IsLocalization W₂<VAR>X₂ : C₂<VAR>X₃ : D<VAR>y : L.obj X₂ ⟶ X₃<VAR>w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) := TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv<VAR>this✝ : Nonempty (w.CostructuredArrowDownwards y)<VAR>c : C₁<VAR>g : X₂ ⟶ Φ.functor.obj c<VAR>x : L.obj (Φ.functor.obj c) ⟶ X₃<VAR>fac✝ : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y<VAR>fac : L.map g ≫ x = y<VAR>ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary (Φ.arrow.RightResolution (Arrow.mk g))<VAR>this : Zigzag ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk (𝟙 (Φ.functor.obj c)) ⋯)) ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk ρ.w.right ⋯))<GOAL>Zigzag ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj (RightResolution.mk ρ.w.right ⋯)) ((fromRightResolution Φ L y).obj (RightResolution.mk ρ.w.left ⋯))
<VAR>x : ℝ<VAR>h : x ∈ Ioo (-1) 1<GOAL>arcsin x = arctan (x / √(1 - x ^ 2))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : HeytingAlgebra α<VAR>a✝ b c a : α<GOAL>a ⇨ aᶜ = aᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f g : C(α, β)<VAR>ι : Type u_5<VAR>S : ι → Set α<VAR>φ : (i : ι) → C(↑(S i), β)<VAR>hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩<VAR>hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x<VAR>A : Set (Set α)<VAR>F : (s : Set α) → s ∈ A → C(↑s, β)<VAR>hF : ∀ (s : Set α) (hs : s ∈ A) (t : Set α) (ht : t ∈ A) (x : α) (hxi : x ∈ s) (hxj : x ∈ t), (F s hs) ⟨x, hxi⟩ = (F t ht) ⟨x, hxj⟩<VAR>hA : ∀ (x : α), ∃ i ∈ A, i ∈ 𝓝 x<VAR>s : Set α<VAR>hs : s ∈ A<VAR>x : ↑s<VAR>x' : ↑↑⟨s, hs⟩ := x<GOAL>(let S := Subtype.val; let F_1 := fun i => F ↑i ⋯; liftCover S F_1 ⋯ ⋯) ↑x = (F s hs) x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s u : Set P<VAR>hu : IsOpen u<VAR>hsu : s ⊆ u<VAR>h : AffineIndependent ℝ Subtype.val<VAR>q : P<VAR>hq : q ∈ s<GOAL>∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s u : Set P<VAR>hu : IsOpen u<VAR>hsu : s ⊆ u<VAR>h : AffineIndependent ℝ Subtype.val<VAR>q : P<VAR>hq : q ∈ s<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hεu : Metric.closedBall q ε ⊆ u<GOAL>∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s u : Set P<VAR>hu : IsOpen u<VAR>hsu : s ⊆ u<VAR>h : AffineIndependent ℝ Subtype.val<VAR>q : P<VAR>hq : q ∈ s<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hεu : Metric.closedBall q ε ⊆ u<VAR>t : Set P<VAR>ht₁ : s ⊆ t<VAR>ht₂ : AffineIndependent ℝ fun p => ↑p<VAR>ht₃ : affineSpan ℝ t = ⊤<GOAL>∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s u : Set P<VAR>hu : IsOpen u<VAR>hsu : s ⊆ u<VAR>h : AffineIndependent ℝ Subtype.val<VAR>q : P<VAR>hq : q ∈ s<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hεu : Metric.closedBall q ε ⊆ u<VAR>t : Set P<VAR>ht₁ : s ⊆ t<VAR>ht₂ : AffineIndependent ℝ fun p => ↑p<VAR>ht₃ : affineSpan ℝ t = ⊤<VAR>f : P → P := fun y => (lineMap q y) (ε / dist y q)<GOAL>∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s u : Set P<VAR>hu : IsOpen u<VAR>hsu : s ⊆ u<VAR>h : AffineIndependent ℝ Subtype.val<VAR>q : P<VAR>hq : q ∈ s<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hεu : Metric.closedBall q ε ⊆ u<VAR>t : Set P<VAR>ht₁ : s ⊆ t<VAR>ht₂ : AffineIndependent ℝ fun p => ↑p<VAR>ht₃ : affineSpan ℝ t = ⊤<VAR>f : P → P := fun y => (lineMap q y) (ε / dist y q)<VAR>hf : ∀ (y : P), f y ∈ u<GOAL>∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s u : Set P<VAR>hu : IsOpen u<VAR>hsu : s ⊆ u<VAR>h : AffineIndependent ℝ Subtype.val<VAR>q : P<VAR>hq : q ∈ s<VAR>ε : ℝ<VAR>ε0 : 0 < ε<VAR>hεu : Metric.closedBall q ε ⊆ u<VAR>t : Set P<VAR>ht₁ : s ⊆ t<VAR>ht₂ : AffineIndependent ℝ fun p => ↑p<VAR>ht₃ : affineSpan ℝ t = ⊤<VAR>f : P → P := fun y => (lineMap q y) (ε / dist y q)<VAR>hf : ∀ (y : P), f y ∈ u<VAR>hεyq : ∀ y ∉ s, ε / dist y q ≠ 0<GOAL>∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Lattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ a₁ a₂ b✝ b₁ b₂ c x a b : α<GOAL>[[a, b]] = [[b, a]]
<VAR>i : ℤ<GOAL>(natAbs 1).lcm i.natAbs = i.natAbs
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁹ : _root_.RCLike 𝕜<VAR>E : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : InnerProductSpace 𝕜 E<VAR>E' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : InnerProductSpace 𝕜 E'<VAR>F : Type u_6<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>F' : Type u_7<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : InnerProductSpace ℝ F'<VAR>inst✝ : Fintype ι<VAR>b : OrthonormalBasis ι 𝕜 E<VAR>v : E<VAR>i : ι<GOAL>b.repr v i = ⟪b i, v⟫_𝕜
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Mul α<VAR>s t u : Set α<VAR>a : α<GOAL>op '' s • t = t * s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Mul α<VAR>s t u : Set α<VAR>a : α<GOAL>image2 (fun a b => SMul.smul (op b) a) t s = image2 (fun x x_1 => x * x_1) t s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x : α<VAR>hx : x ∈ Icc a b<GOAL>projIcc a b h x = ⟨x, hx⟩
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>hf : Tendsto f atBot (𝓝 m)<GOAL>∫ (x : ℝ) in Iic a, f' x = f a - m
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x<VAR>f'int : IntegrableOn f' (Iic a) volume<VAR>hf : Tendsto f atBot (𝓝 m)<GOAL>ContinuousWithinAt f (Iic a) a
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<VAR>r : R<GOAL>((gradedMul R 𝒜 ℬ) x) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = r • x
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<VAR>r : R<GOAL>(gradedMul R 𝒜 ℬ).flip ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = DistribMulAction.toLinearMap R (DirectSum ι 𝒜 ⊗[R] DirectSum ι ℬ) r
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<VAR>r : R<VAR>i✝¹ : ι<VAR>x✝¹ : 𝒜 i✝¹<VAR>i✝ : ι<VAR>x✝ : ℬ i✝<GOAL>((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝)) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = r • (lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<VAR>r : R<VAR>i✝¹ : ι<VAR>x✝¹ : 𝒜 i✝¹<VAR>i✝ : ι<VAR>x✝ : ℬ i✝<GOAL>(-1) ^ (i✝ * 0) • ((lof R ι 𝒜 i✝¹) x✝¹ * (lof R ι 𝒜 0) (DirectSum.GAlgebra.toFun r)) ⊗ₜ[R] ((lof R ι ℬ i✝) x✝ * 1) = r • (lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<VAR>r : R<VAR>i✝¹ : ι<VAR>x✝¹ : 𝒜 i✝¹<VAR>i✝ : ι<VAR>x✝ : ℬ i✝<GOAL>((lof R ι 𝒜 i✝¹) x✝¹ * (lof R ι 𝒜 0) (DirectSum.GAlgebra.toFun r)) ⊗ₜ[R] ((lof R ι ℬ i✝) x✝ * 1) = (r • (lof R ι 𝒜 i✝¹) x✝¹) ⊗ₜ[R] (lof R ι ℬ i✝) x✝
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>𝒜 : ι → Type u_5<VAR>ℬ : ι → Type u_6<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)<VAR>inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)<VAR>inst✝⁵ : (i : ι) → Module R (𝒜 i)<VAR>inst✝⁴ : (i : ι) → Module R (ℬ i)<VAR>inst✝³ : DirectSum.GRing 𝒜<VAR>inst✝² : DirectSum.GRing ℬ<VAR>inst✝¹ : DirectSum.GAlgebra R 𝒜<VAR>inst✝ : DirectSum.GAlgebra R ℬ<VAR>x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i<VAR>r : R<VAR>i✝¹ : ι<VAR>x✝¹ : 𝒜 i✝¹<VAR>i✝ : ι<VAR>x✝ : ℬ i✝<GOAL>((lof R ι 𝒜 i✝¹) x✝¹ * (lof R ι 𝒜 0) (DirectSum.GAlgebra.toFun r)) ⊗ₜ[R] (lof R ι ℬ i✝) x✝ = ((lof R ι 𝒜 i✝¹) x✝¹ * (algebraMap R (⨁ (i : ι), 𝒜 i)) r) ⊗ₜ[R] (lof R ι ℬ i✝) x✝
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u✝ v✝ ua ub va vb : ι → ℝ<VAR>inst✝² : FTCFilter a la la'<VAR>inst✝¹ : FTCFilter b lb lb'<VAR>inst✝ : FTCFilter a l l'<VAR>hfm : StronglyMeasurableAtFilter f l' volume<VAR>hf : Tendsto f (l' ⊓ ae volume) (𝓝 c)<VAR>u v : ι → ℝ<VAR>hu : Tendsto u lt l<VAR>hv : Tendsto v lt l<GOAL>(fun t => (∫ (x : ℝ) in u t..v t, f x) - (v t - u t) • c) =o[lt] (v - u)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁶ : DecidableEq α<VAR>inst✝⁵ : DecidableEq β<VAR>inst✝⁴ : SemilatticeInf α<VAR>inst✝³ : SemilatticeInf β<VAR>inst✝² : FunLike F α β<VAR>inst✝¹ : InfHomClass F α β<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α<VAR>a✝ b c : α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<GOAL>filter (fun x => a ≤ x) (s ⊼ t) = filter (fun x => a ≤ x) s ⊼ filter (fun x => a ≤ x) t
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<GOAL>dist ((starRingEnd ℂ) z) z = 2 * |z.im|