ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n✝ : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>n : ℕ∞<VAR>h : ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s<GOAL>∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝ : AddGroup G<VAR>T : AddTorsor G P<VAR>g₁ g₂ : G<VAR>p : P<VAR>h : g₁ +ᵥ p = g₂ +ᵥ p<GOAL>g₁ = g₂
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>S✝ S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>A : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>inst✝ : Category.{v₄, u₄} B<VAR>S : C<VAR>F : B ⥤ C<VAR>G : C ⥤ D<VAR>X✝ Y✝ : StructuredArrow S F<VAR>f : X✝ ⟶ Y✝<GOAL>((fun X => mk (G.map X.hom)) X✝).hom ≫ (F ⋙ G).map f.right = ((fun X => mk (G.map X.hom)) Y✝).hom
<VAR>x : 𝓞 ℚ<GOAL>IsUnit x ↔ ↑x = 1 ∨ ↑x = -1
<VAR>x : 𝓞 ℚ<GOAL>↑x = ↑1 ∨ ↑x = ↑(-1) ↔ ↑x = 1 ∨ ↑x = -1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h : σ.IsThreeCycle<GOAL>σ.support.card = 3
<VAR>n ν : ℕ<VAR>x : ↑I<GOAL>0 ≤ (bernstein n ν) x
<VAR>n ν : ℕ<VAR>x : ↑I<GOAL>0 ≤ ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
<VAR>n ν : ℕ<VAR>x : ↑I<VAR>h₁ : 0 ≤ ↑x<GOAL>0 ≤ ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
<VAR>n ν : ℕ<VAR>x : ↑I<VAR>h₁ : 0 ≤ ↑x<VAR>h₂ : 0 ≤ 1 - ↑x<GOAL>0 ≤ ↑(n.choose ν) * ↑x ^ ν * (1 - ↑x) ^ (n - ν)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>R : D ⥤ C<VAR>inst✝¹ : Coreflective R<VAR>inst✝ : HasLimitsOfShape J C<VAR>F : J ⥤ D<VAR>c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))<VAR>this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := PreservesLimitsOfSize.preservesLimitsOfShape<VAR>t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit (F ⋙ R))<GOAL>HasLimit F
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>J : Type u<VAR>inst✝² : Category.{v, u} J<VAR>R : D ⥤ C<VAR>inst✝¹ : Coreflective R<VAR>inst✝ : HasLimitsOfShape J C<VAR>F : J ⥤ D<VAR>c : Cone ((F ⋙ R) ⋙ comonadicRightAdjoint R) := (comonadicRightAdjoint R).mapCone (limit.cone (F ⋙ R))<VAR>this : PreservesLimitsOfShape J (comonadicRightAdjoint R) := PreservesLimitsOfSize.preservesLimitsOfShape<VAR>t : IsLimit c := isLimitOfPreserves (comonadicRightAdjoint R) (limit.isLimit (F ⋙ R))<GOAL>(F ⋙ R) ⋙ comonadicRightAdjoint R ≅ F
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ<VAR>n : ℕ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>(∑ x ∈ s, f x) ^ (n + 1) / ↑s.card ^ n ≤ ∑ x ∈ s, f x ^ (n + 1)
<VAR>ι : Type u<VAR>f : ι → ℝ<VAR>n : ℕ<VAR>hf : ∀ a ∈ ∅, 0 ≤ f a<GOAL>(∑ x ∈ ∅, f x) ^ (n + 1) / ↑∅.card ^ n ≤ ∑ x ∈ ∅, f x ^ (n + 1)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ<VAR>n : ℕ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<VAR>hs : s.Nonempty<GOAL>(∑ x ∈ s, f x) ^ (n + 1) / ↑s.card ^ n ≤ ∑ x ∈ s, f x ^ (n + 1)
<VAR>x y : ℝ*<GOAL>x.InfiniteNeg → ¬y.InfinitePos → (x + y).InfiniteNeg
<VAR>x y : ℝ*<GOAL>(-x).InfinitePos → ¬(-y).InfiniteNeg → (-x + -y).InfinitePos
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<GOAL>s * ↑(upperClosure t) = ↑(upperClosure (s * t))
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<GOAL>⋃ a ∈ s, a • ↑(upperClosure t) = ⋃ i ∈ s, ↑(i • upperClosure t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hsu : VectorMeasure.restrict s u ≤ VectorMeasure.restrict 0 u<VAR>hsv : VectorMeasure.restrict s v ≤ VectorMeasure.restrict 0 v<VAR>hs : ↑s (u ∆ v) = 0<GOAL>↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hsu : VectorMeasure.restrict 0 u ≤ (-s).restrict u<VAR>hsv : VectorMeasure.restrict s v ≤ VectorMeasure.restrict 0 v<VAR>hs : ↑s (u ∆ v) = 0<GOAL>↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hsu : VectorMeasure.restrict 0 u ≤ (-s).restrict u<VAR>hsv : VectorMeasure.restrict 0 v ≤ (-s).restrict v<VAR>hs : ↑s (u ∆ v) = 0<GOAL>↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hsu : VectorMeasure.restrict 0 u ≤ (-s).restrict u<VAR>hsv : VectorMeasure.restrict 0 v ≤ (-s).restrict v<VAR>hs : ↑s (u ∆ v) = 0<VAR>this : ↑(-s) (u ∆ v) = 0 → ↑(-s) (u \ v) = 0 ∧ ↑(-s) (v \ u) = 0<GOAL>↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>μ ν : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure ν<VAR>u v w : Set α<VAR>hu : MeasurableSet u<VAR>hv : MeasurableSet v<VAR>hsu : VectorMeasure.restrict 0 u ≤ (-s).restrict u<VAR>hsv : VectorMeasure.restrict 0 v ≤ (-s).restrict v<VAR>hs : ↑s (u ∆ v) = 0<VAR>this : ↑s (u ∆ v) = 0 → ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0<GOAL>↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>K : Type u_1<VAR>inst✝ : DivisionRing K<VAR>p : K[X]<GOAL>p.degree + (C p.leadingCoeff⁻¹).degree = p.degree
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>p q : K[X]<GOAL>RatFunc.mk p q = { toFractionRing := (algebraMap K[X] (FractionRing K[X])) p / (algebraMap K[X] (FractionRing K[X])) q }
<VAR>G : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝² : SeminormedAddCommGroup H<VAR>inst✝¹ : T0Space H<VAR>inst✝ : CompleteSpace H<VAR>f : NormedAddGroupHom G H<VAR>g : NormedAddGroupHom (Completion G) H<VAR>hg : ∀ (v : G), f v = g (↑G v)<VAR>v : Completion G<GOAL>f.extension v = g v
<VAR>ι : Type u_1<VAR>inst✝ : LinearOrder ι<VAR>i : ι<GOAL>i ≤ succFn i
<VAR>ι : Type u_1<VAR>inst✝ : LinearOrder ι<VAR>i : ι<GOAL>∀ x ∈ Set.Ioi i, i ≤ x
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'<VAR>C : ℝ<VAR>H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖<GOAL>‖{ toFun := fun x => (f x).mkContinuous (C * ‖x‖) ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (max C 0) ⋯‖ ≤ max C 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k l : ℕ<VAR>ζ✝ : M<VAR>f : F<VAR>h : IsPrimitiveRoot ζ✝ k<VAR>ζ : Mˣ<GOAL>IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>left✝ : x ∈ {x | IsUnit ((X.presheaf.germ x) f)}<GOAL>↑x ∈ ↑U
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>i j j' : ι<VAR>rij : c.Rel i j<VAR>rij' : c.Rel i j'<GOAL>C.d i j' ≫ eqToHom ⋯ = C.d i j
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex V c<VAR>i j : ι<VAR>rij rij' : c.Rel i j<GOAL>C.d i j ≫ eqToHom ⋯ = C.d i j
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>I : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>inst✝ : NoZeroSMulDivisors A B<GOAL>↑(differentIdeal A B) ≤ I ↔ Submodule.map (↑A (Algebra.trace K L)) (restrictScalars A ↑I⁻¹) ≤ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>I : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>inst✝ : NoZeroSMulDivisors A B<GOAL>↑I⁻¹ ≤ traceDual A K 1 ↔ Submodule.map (↑A (Algebra.trace K L)) (restrictScalars A ↑I⁻¹) ≤ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>I : FractionalIdeal B⁰ L<VAR>hI : I ≠ 0<VAR>inst✝ : NoZeroSMulDivisors A B<GOAL>Submodule.map (↑A (Algebra.trace K L)) (restrictScalars A (↑I⁻¹ * 1)) ≤ 1 ↔ Submodule.map (↑A (Algebra.trace K L)) (restrictScalars A ↑I⁻¹) ≤ 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>s : Set X<VAR>inst✝ : DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<GOAL>{x} ∈ 𝓝[s] x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>s : Set X<VAR>inst✝ : DiscreteTopology ↑s<VAR>x : X<VAR>hx : x ∈ s<VAR>this : {⟨x, hx⟩} ∈ 𝓝 ⟨x, hx⟩<GOAL>{x} ∈ 𝓝[s] x
<VAR>B : Type u₁<VAR>inst✝⁴ : Bicategory B<VAR>C : Type u₂<VAR>inst✝³ : Bicategory C<VAR>D : Type u₃<VAR>inst✝² : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : OplaxFunctor B C<VAR>inst✝¹ : ∀ (a : B), IsIso (F.mapId a)<VAR>inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)<VAR>a✝ b✝ c✝ : B<VAR>f : a✝ ⟶ b✝<VAR>g h : b✝ ⟶ c✝<VAR>η : g ⟶ h<GOAL>F.map₂ (f ◁ η) = F.mapComp f g ≫ F.map f ◁ F.map₂ η ≫ inv (F.mapComp f h)
<VAR>B : Type u₁<VAR>inst✝⁴ : Bicategory B<VAR>C : Type u₂<VAR>inst✝³ : Bicategory C<VAR>D : Type u₃<VAR>inst✝² : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : OplaxFunctor B C<VAR>inst✝¹ : ∀ (a : B), IsIso (F.mapId a)<VAR>inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)<VAR>a✝ b✝ c✝ : B<VAR>f✝ g✝ : a✝ ⟶ b✝<VAR>η : f✝ ⟶ g✝<VAR>h : b✝ ⟶ c✝<GOAL>F.map₂ (η ▷ h) = F.mapComp f✝ h ≫ F.map₂ η ▷ F.map h ≫ inv (F.mapComp g✝ h)
<VAR>B : Type u₁<VAR>inst✝⁴ : Bicategory B<VAR>C : Type u₂<VAR>inst✝³ : Bicategory C<VAR>D : Type u₃<VAR>inst✝² : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : OplaxFunctor B C<VAR>inst✝¹ : ∀ (a : B), IsIso (F.mapId a)<VAR>inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)<VAR>a✝ b✝ c✝ d✝ : B<VAR>f : a✝ ⟶ b✝<VAR>g : b✝ ⟶ c✝<VAR>h : c✝ ⟶ d✝<GOAL>F.map₂ (α_ f g h).hom = F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h ≫ (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ inv (F.mapComp g h) ≫ inv (F.mapComp f (g ≫ h))
<VAR>B : Type u₁<VAR>inst✝⁴ : Bicategory B<VAR>C : Type u₂<VAR>inst✝³ : Bicategory C<VAR>D : Type u₃<VAR>inst✝² : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : OplaxFunctor B C<VAR>inst✝¹ : ∀ (a : B), IsIso (F.mapId a)<VAR>inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)<VAR>a✝ b✝ c✝ d✝ : B<VAR>f : a✝ ⟶ b✝<VAR>g : b✝ ⟶ c✝<VAR>h : c✝ ⟶ d✝<GOAL>F.map₂ (α_ f g h).hom = (((F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom) ≫ F.map f ◁ inv (F.mapComp g h)) ≫ inv (F.mapComp f (g ≫ h))
<VAR>B : Type u₁<VAR>inst✝⁴ : Bicategory B<VAR>C : Type u₂<VAR>inst✝³ : Bicategory C<VAR>D : Type u₃<VAR>inst✝² : Bicategory D<VAR>F✝ : Pseudofunctor B C<VAR>F : OplaxFunctor B C<VAR>inst✝¹ : ∀ (a : B), IsIso (F.mapId a)<VAR>inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)<VAR>a✝ b✝ c✝ d✝ : B<VAR>f : a✝ ⟶ b✝<VAR>g : b✝ ⟶ c✝<VAR>h : c✝ ⟶ d✝<GOAL>(F.map₂ (α_ f g h).hom ≫ F.mapComp f (g ≫ h)) ≫ F.map f ◁ F.mapComp g h = (F.mapComp (f ≫ g) h ≫ F.mapComp f g ▷ F.map h) ≫ (α_ (F.map f) (F.map g) (F.map h)).hom
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<GOAL>Inseparable x y ↔ edist x y = 0
<VAR>𝕜₁ : Type u_1<VAR>inst✝²⁰ : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝¹⁸ : NormedAddCommGroup F₁<VAR>inst✝¹⁷ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹³ : NormedAddCommGroup F₂<VAR>inst✝¹² : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁸ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁶ : FiberBundle F₁ E₁<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁴ : FiberBundle F₂ E₂<VAR>inst✝³ : Trivialization.IsLinear 𝕜₁ e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜₁ e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜₂ e₂'<VAR>b : B<VAR>hb : b ∈ e₁.baseSet ∩ e₂.baseSet<VAR>L : F₁ →SL[σ] F₂<GOAL>(continuousLinearMap σ e₁ e₂).symm b L = (Trivialization.symmL 𝕜₂ e₂ b).comp (L.comp (Trivialization.continuousLinearMapAt 𝕜₁ e₁ b))
<VAR>𝕜₁ : Type u_1<VAR>inst✝²⁰ : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝¹⁸ : NormedAddCommGroup F₁<VAR>inst✝¹⁷ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹³ : NormedAddCommGroup F₂<VAR>inst✝¹² : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁸ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁶ : FiberBundle F₁ E₁<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁴ : FiberBundle F₂ E₂<VAR>inst✝³ : Trivialization.IsLinear 𝕜₁ e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜₁ e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜₂ e₂'<VAR>b : B<VAR>hb : b ∈ e₁.baseSet ∩ e₂.baseSet<VAR>L : F₁ →SL[σ] F₂<GOAL>cast ⋯ (↑(continuousLinearMap σ e₁ e₂).symm (b, L)).snd = (Trivialization.symmL 𝕜₂ e₂ b).comp (L.comp (Trivialization.continuousLinearMapAt 𝕜₁ e₁ b))
<VAR>𝕜₁ : Type u_1<VAR>inst✝²⁰ : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝¹⁸ : NormedAddCommGroup F₁<VAR>inst✝¹⁷ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁶ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁵ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁴ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹³ : NormedAddCommGroup F₂<VAR>inst✝¹² : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹¹ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹⁰ : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝⁹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝⁸ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁶ : FiberBundle F₁ E₁<VAR>inst✝⁵ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁴ : FiberBundle F₂ E₂<VAR>inst✝³ : Trivialization.IsLinear 𝕜₁ e₁<VAR>inst✝² : Trivialization.IsLinear 𝕜₁ e₁'<VAR>inst✝¹ : Trivialization.IsLinear 𝕜₂ e₂<VAR>inst✝ : Trivialization.IsLinear 𝕜₂ e₂'<VAR>b : B<VAR>hb : b ∈ e₁.baseSet ∩ e₂.baseSet<VAR>L : F₁ →SL[σ] F₂<GOAL>b ∈ (continuousLinearMap σ e₁ e₂).baseSet
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>ha : ∀ (x : α), x ∈ zpowers a<GOAL>image (fun i => a ^ i) (range (orderOf a)) = univ
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>ha : ∀ (x : α), x ∈ ↑(zpowers a)<GOAL>image (fun i => a ^ i) (range (orderOf a)) = univ
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort u_1<VAR>inst✝ : Group G<VAR>t₁ t₂ : TopologicalSpace G<VAR>h₁ : TopologicalGroup G<VAR>h₂ : TopologicalGroup G<GOAL>TopologicalGroup G
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort u_1<VAR>inst✝ : Group G<VAR>t₁ t₂ : TopologicalSpace G<VAR>h₁ : TopologicalGroup G<VAR>h₂ : TopologicalGroup G<VAR>b : Bool<GOAL>TopologicalGroup G
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>(whiskerRight f { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight N P, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }).hom = ((isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).inv ≫ whiskerRight (whiskerRight f N) P ≫ (isoOfIso { hom := AssociatorBimod.hom M' N P, inv := AssociatorBimod.inv M' N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>coequalizer.π (M.actRight ▷ { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight N P, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X) ((α_ M.X X.X { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight N P, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫ M.X ◁ { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight N P, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actLeft) ≫ (whiskerRight f { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight N P, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }).hom = coequalizer.π (M.actRight ▷ { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight N P, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X) ((α_ M.X X.X { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight N P, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫ M.X ◁ { X := TensorBimod.X N P, actLeft := TensorBimod.actLeft N P, one_actLeft := ⋯, left_assoc := ⋯, actRight := TensorBimod.actRight N P, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actLeft) ≫ ((isoOfIso { hom := AssociatorBimod.hom M N P, inv := AssociatorBimod.inv M N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).inv ≫ whiskerRight (whiskerRight f N) P ≫ (isoOfIso { hom := AssociatorBimod.hom M' N P, inv := AssociatorBimod.inv M' N P, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯ ⋯).hom).hom
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M✝ : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<VAR>W X Y Z : Mon_ C<VAR>M M' : Bimod W X<VAR>f : M ⟶ M'<VAR>N : Bimod X Y<VAR>P : Bimod Y Z<GOAL>coequalizer.π (M.actRight ▷ TensorBimod.X N P) ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P) ≫ colimMap (parallelPairHom (M.actRight ▷ TensorBimod.X N P) ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P) (M'.actRight ▷ TensorBimod.X N P) ((α_ M'.X X.X (TensorBimod.X N P)).hom ≫ M'.X ◁ TensorBimod.actLeft N P) (f.hom ▷ X.X ▷ TensorBimod.X N P) (f.hom ▷ TensorBimod.X N P) ⋯ ⋯) = coequalizer.π (M.actRight ▷ TensorBimod.X N P) ((α_ M.X X.X (TensorBimod.X N P)).hom ≫ M.X ◁ TensorBimod.actLeft N P) ≫ AssociatorBimod.inv M N P ≫ colimMap (parallelPairHom (TensorBimod.actRight M N ▷ P.X) ((α_ (TensorBimod.X M N) Y.X P.X).hom ≫ TensorBimod.X M N ◁ P.actLeft) (TensorBimod.actRight M' N ▷ P.X) ((α_ (TensorBimod.X M' N) Y.X P.X).hom ≫ TensorBimod.X M' N ◁ P.actLeft) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ Y.X ▷ P.X) (colimMap (parallelPairHom (M.actRight ▷ N.X) ((α_ M.X X.X N.X).hom ≫ M.X ◁ N.actLeft) (M'.actRight ▷ N.X) ((α_ M'.X X.X N.X).hom ≫ M'.X ◁ N.actLeft) (f.hom ▷ X.X ▷ N.X) (f.hom ▷ N.X) ⋯ ⋯) ▷ P.X) ⋯ ⋯) ≫ AssociatorBimod.hom M' N P