ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ<VAR>p : α → Prop<VAR>h' : ∀ u ∈ supp x, p u<GOAL>∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ<VAR>p : α → Prop<VAR>h' : ∀ u ∈ supp x, p u<GOAL>∀ (i : (P F).B a), p (f i)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ<VAR>p : α → Prop<VAR>h' : ∀ u ∈ supp x, p u<VAR>i : (P F).B a<GOAL>f i ∈ supp x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ<VAR>p : α → Prop<VAR>h' : ∀ u ∈ supp x, p u<VAR>i : (P F).B a<GOAL>∀ (a : (P F).A) (f_1 : (P F).B a → α), abs ⟨a, f_1⟩ = x → f i ∈ f_1 '' univ
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>xeq : abs ⟨a, f⟩ = x<VAR>h : ∀ (a' : (P F).A) (f' : (P F).B a' → α), abs ⟨a', f'⟩ = x → f '' univ ⊆ f' '' univ<VAR>p : α → Prop<VAR>h' : ∀ u ∈ supp x, p u<VAR>i : (P F).B a<VAR>a' : (P F).A<VAR>f' : (P F).B a' → α<VAR>xeq' : abs ⟨a', f'⟩ = x<GOAL>f i ∈ f '' univ
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>S T : Set F<VAR>hT : IsSubfield T<VAR>H : S ⊆ T<VAR>p : F<VAR>hp : p ∈ Ring.closure S<VAR>q : F<VAR>hq : q ∈ Ring.closure S<GOAL>p / q ∈ T
<VAR>a : UnitAddCircle<GOAL>Tendsto (fun s => hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZetaEven a 1))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.17460, u_5} C₅<VAR>inst✝ : Category.{?u.17464, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ≌ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ≌ C₄<VAR>h : CatCommSq T.functor L R B.functor<VAR>X : C₁<GOAL>iso'.hom.app X = iso'.hom.app X
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.17460, u_5} C₅<VAR>inst✝ : Category.{?u.17464, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ≌ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ≌ C₄<VAR>h : CatCommSq T.functor L R B.functor<VAR>X : C₁<GOAL>(B.symm.unitIso.hom.app (R.obj (T.symm.inverse.obj X)) ≫ B.symm.inverse.map (B.inverse.map (R.map (T.counitIso.inv.app (T.symm.inverse.obj X))) ≫ B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.symm.inverse.obj X))) ≫ B.unitIso.inv.app (L.obj (T.inverse.obj (T.symm.inverse.obj X)))) ≫ B.symm.inverse.map (L.map (T.symm.counitIso.hom.app X))) ≫ B.functor.map (L.map (T.unitIso.hom.app X)) = (T.functor ⋙ R).map (T.unitIso.hom.app X) ≫ iso'.hom.app ((T.functor ⋙ T.inverse).obj X)
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.17460, u_5} C₅<VAR>inst✝ : Category.{?u.17464, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ≌ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ≌ C₄<VAR>h : CatCommSq T.functor L R B.functor<VAR>X : C₁<GOAL>(B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫ B.functor.map (B.inverse.map (R.map (T.counitIso.inv.app (T.functor.obj X))) ≫ B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X))) ≫ B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X)))) ≫ B.functor.map (L.map (T.unitIso.inv.app X))) ≫ B.functor.map (L.map (T.unitIso.hom.app X)) = R.map (T.functor.map (T.unitIso.hom.app X)) ≫ iso'.hom.app (T.inverse.obj (T.functor.obj X))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.17460, u_5} C₅<VAR>inst✝ : Category.{?u.17464, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ≌ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ≌ C₄<VAR>h : CatCommSq T.functor L R B.functor<VAR>X : C₁<GOAL>B.counitIso.inv.app (R.obj (T.functor.obj X)) ≫ B.functor.map (B.inverse.map (R.map (T.functor.map (T.unit.app X))) ≫ B.inverse.map ((iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X))) ≫ B.unitIso.inv.app (L.obj (T.inverse.obj (T.functor.obj X))) ≫ 𝟙 (L.obj (T.inverse.obj (T.functor.obj X)))) = R.map (T.functor.map (T.unitIso.hom.app X)) ≫ iso'.hom.app (T.inverse.obj (T.functor.obj X))
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₅ : Type u_5<VAR>C₆ : Type u_6<VAR>inst✝⁵ : Category.{u_8, u_1} C₁<VAR>inst✝⁴ : Category.{u_9, u_2} C₂<VAR>inst✝³ : Category.{u_10, u_3} C₃<VAR>inst✝² : Category.{u_7, u_4} C₄<VAR>inst✝¹ : Category.{?u.17460, u_5} C₅<VAR>inst✝ : Category.{?u.17464, u_6} C₆<VAR>T✝ : C₁ ⥤ C₂<VAR>L✝ : C₁ ⥤ C₃<VAR>R✝ : C₂ ⥤ C₄<VAR>B✝ : C₃ ⥤ C₄<VAR>T : C₁ ≌ C₂<VAR>L : C₁ ⥤ C₃<VAR>R : C₂ ⥤ C₄<VAR>B : C₃ ≌ C₄<VAR>h : CatCommSq T.functor L R B.functor<VAR>X : C₁<GOAL>R.map (T.functor.map (T.unit.app X)) ≫ (iso T.functor L R B.functor).hom.app (T.inverse.obj (T.functor.obj X)) = R.map (T.functor.map (T.unitIso.hom.app X)) ≫ iso'.hom.app (T.inverse.obj (T.functor.obj X))
<VAR>m n✝ n : ℕ<GOAL>val 1 = 1 % n
<VAR>α : Type u_1<VAR>inst✝ : CancelMonoidWithZero α<VAR>a b c : α<VAR>ha : a ≠ 0<VAR>d : α<GOAL>a * c = a * b * d ↔ c = b * d
<VAR>n : ℕ<VAR>r : ℝ<GOAL>r.toNNReal < ↑n ↔ r < ↑n ∧ n ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : Nonempty γ<VAR>ι : Sort u_4<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iSup g)<VAR>Af : Antitone f<VAR>bdd : autoParam (BddAbove (range g)) _auto✝<GOAL>f (⨆ i, g i) = ⨅ i, f (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderClosedTopology β<VAR>inst✝¹ : Nonempty γ<VAR>ι : Sort u_4<VAR>inst✝ : Nonempty ι<VAR>f : α → β<VAR>g : ι → α<VAR>Cf : ContinuousAt f (iSup g)<VAR>Af : Antitone f<VAR>bdd : autoParam (BddAbove (range g)) _auto✝<GOAL>sInf (range (f ∘ g)) = sInf (range fun i => f (g i))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y z : X<VAR>ι : Type u_3<VAR>F : Set X<GOAL>JoinedIn univ x y ↔ Joined x y
<VAR>P : Type u_1<VAR>inst✝¹ : SemilatticeSup P<VAR>inst✝ : IsDirected P fun x x_1 => x ≥ x_1<VAR>x : P<VAR>I J K s t : Ideal P<VAR>hx : x ∉ I<VAR>h : I = I ⊔ principal x<GOAL>x ∈ I
<VAR>ι : Type u_1<VAR>κ✝¹ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>κ✝ : Type u_6<VAR>κ : Type u_7<VAR>s : Finset ι<VAR>t : ι → Set κ<VAR>f : κ → β<GOAL>(↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a => ∏ i ∈ s, (t i).mulIndicator f a
<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>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>X P Q ◁ T.mul ≫ actRight P Q = (α_ (X P Q) T.X T.X).inv ≫ actRight P Q ▷ T.X ≫ actRight P Q
<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>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(tensorRight (T.X ⊗ T.X)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ X P Q ◁ T.mul ≫ actRight P Q = (tensorRight (T.X ⊗ T.X)).map (coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫ (α_ (X P Q) T.X T.X).inv ≫ actRight P Q ▷ T.X ≫ actRight P Q
<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>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ (T.X ⊗ T.X) ≫ coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ◁ T.mul ≫ actRight P Q = coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ (T.X ⊗ T.X) ≫ (α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X T.X).inv ≫ actRight P Q ▷ T.X ≫ actRight P Q
<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>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>((P.X ⊗ Q.X) ◁ T.mul ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X) ≫ actRight P Q = coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ (T.X ⊗ T.X) ≫ (α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X T.X).inv ≫ actRight P Q ▷ T.X ≫ actRight P Q
<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>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(P.X ⊗ Q.X) ◁ T.mul ≫ (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ (T.X ⊗ T.X) ≫ (α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X T.X).inv ≫ actRight P Q ▷ T.X ≫ actRight P Q
<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>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(((α_ P.X Q.X (T.X ⊗ T.X)).hom ≫ P.X ◁ Q.X ◁ T.mul) ≫ P.X ◁ Q.actRight) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ (T.X ⊗ T.X) ≫ (α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X T.X).inv ≫ actRight P Q ▷ T.X ≫ actRight P Q
<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>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(α_ P.X Q.X (T.X ⊗ T.X)).hom ≫ (P.X ◁ (α_ Q.X T.X T.X).inv ≫ P.X ◁ Q.actRight ▷ T.X ≫ P.X ◁ Q.actRight) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ (T.X ⊗ T.X) ≫ (α_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) T.X T.X).inv ≫ actRight P Q ▷ T.X ≫ actRight P Q
<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>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(α_ P.X Q.X (T.X ⊗ T.X)).hom ≫ (P.X ◁ (α_ Q.X T.X T.X).inv ≫ P.X ◁ Q.actRight ▷ T.X ≫ P.X ◁ Q.actRight) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (((α_ (P.X ⊗ Q.X) T.X T.X).inv ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X ▷ T.X) ≫ actRight P Q ▷ T.X) ≫ actRight P Q
<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>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(α_ P.X Q.X (T.X ⊗ T.X)).hom ≫ (P.X ◁ (α_ Q.X T.X T.X).inv ≫ P.X ◁ Q.actRight ▷ T.X ≫ P.X ◁ Q.actRight) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (α_ (P.X ⊗ Q.X) T.X T.X).inv ≫ ((α_ P.X Q.X T.X).hom ▷ T.X ≫ (P.X ◁ Q.actRight) ▷ T.X ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ▷ T.X) ≫ actRight P Q
<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>R S T : Mon_ C<VAR>P : Bimod R S<VAR>Q : Bimod S T<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(α_ P.X Q.X (T.X ⊗ T.X)).hom ≫ (P.X ◁ (α_ Q.X T.X T.X).inv ≫ P.X ◁ Q.actRight ▷ T.X ≫ P.X ◁ Q.actRight) ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) = (α_ (P.X ⊗ Q.X) T.X T.X).inv ≫ (α_ P.X Q.X T.X).hom ▷ T.X ≫ (P.X ◁ Q.actRight) ▷ T.X ≫ (α_ P.X Q.X T.X).hom ≫ P.X ◁ Q.actRight ≫ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<GOAL>MeasurableSet {ω | i ≤ τ ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>this : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω}<GOAL>MeasurableSet {ω | i ≤ τ ω}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝³ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>inst✝² : TopologicalSpace ι<VAR>inst✝¹ : OrderTopology ι<VAR>inst✝ : FirstCountableTopology ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>this : {ω | i ≤ τ ω} = {ω | τ ω = i} ∪ {ω | i < τ ω}<GOAL>MeasurableSet ({ω | τ ω = i} ∪ {ω | i < τ ω})
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : ConditionallyCompleteLinearOrderedField β<VAR>inst✝¹ : ConditionallyCompleteLinearOrderedField γ<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>b✝ : β<VAR>q : ℚ<VAR>b : β<GOAL>inducedMap γ β (inducedMap β γ b) = b
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>hf : ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑f<VAR>h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z<GOAL>∀ᶠ (x : X) in 𝓝ˢ A, P x ↑g
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f<VAR>h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y<GOAL>∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑g
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x✝ : X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f<VAR>h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y<VAR>x : X<VAR>hx : x ∈ A<GOAL>∀ᶠ (y : X) in 𝓝 x, P y ↑g
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x✝ : X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f<VAR>h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y<VAR>x : X<VAR>hx : x ∈ A<GOAL>∀ (x : X), (P x ↑f ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x ↑g
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x✝ : X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f<VAR>h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y<VAR>x : X<VAR>hx : x ∈ A<VAR>y : X<VAR>hy : P y ↑f ∧ ∀ᶠ (x : X) in 𝓝 y, g x = f x<GOAL>P y ↑g
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x✝ : X<VAR>P : (x : X) → (𝓝 x).Germ Y → Prop<VAR>hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f<VAR>h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y<VAR>x : X<VAR>hx : x ∈ A<VAR>y : X<VAR>hy : P y ↑f ∧ ∀ᶠ (x : X) in 𝓝 y, g x = f x<GOAL>↑g = ↑f
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a✝ b✝ c✝ d✝ x y z : P<VAR>r R : ℝ<VAR>a b c d : P<GOAL>dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b✝ c✝ d✝ x y z : P<VAR>r R : ℝ<VAR>b c d : P<GOAL>dist b c * dist b d ≤ dist b b * dist c d + dist b c * dist b d
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a✝ b✝ c✝ d✝ x y z : P<VAR>r R : ℝ<VAR>a b c d : P<VAR>hb : b ≠ a<GOAL>dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b✝ c✝ d✝ x y z : P<VAR>r R : ℝ<VAR>b c d : P<VAR>hb : b ≠ c<GOAL>dist c c * dist b d ≤ dist c b * dist c d + dist b c * dist c d
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a✝ b✝ c✝ d✝ x y z : P<VAR>r R : ℝ<VAR>a b c d : P<VAR>hb : b ≠ a<VAR>hc : c ≠ a<GOAL>dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a b✝ c✝ d✝ x y z : P<VAR>r R : ℝ<VAR>b c d : P<VAR>hb : b ≠ d<VAR>hc : c ≠ d<GOAL>dist d c * dist b d ≤ dist d b * dist c d + dist b c * dist d d
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a✝ b✝ c✝ d✝ x y z : P<VAR>r R : ℝ<VAR>a b c d : P<VAR>hb : b ≠ a<VAR>hc : c ≠ a<VAR>hd : d ≠ a<GOAL>dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a✝ b✝ c✝ d✝ x y z : P<VAR>r R : ℝ<VAR>a b c d : P<VAR>hb : b ≠ a<VAR>hc : c ≠ a<VAR>hd : d ≠ a<VAR>H : dist (inversion a 1 b) (inversion a 1 d) ≤ dist (inversion a 1 b) (inversion a 1 c) + dist (inversion a 1 c) (inversion a 1 d)<GOAL>dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a✝ b✝ c✝ d✝ x y z : P<VAR>r R : ℝ<VAR>a b c d : P<VAR>hb : b ≠ a<VAR>hc : c ≠ a<VAR>hd : d ≠ a<VAR>H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d<GOAL>dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a✝ b✝ c✝ d✝ x y z : P<VAR>r R : ℝ<VAR>a b c d : P<VAR>hb : 0 < dist b a<VAR>hc : 0 < dist c a<VAR>hd : 0 < dist d a<VAR>H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d<GOAL>dist a c * dist b d ≤ dist a b * dist c d + dist b c * dist a d
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>a✝ b✝ c✝ d✝ x y z : P<VAR>r R : ℝ<VAR>a b c d : P<VAR>hb : 0 < dist b a<VAR>hc : 0 < dist c a<VAR>hd : 0 < dist d a<VAR>H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d<GOAL>dist a c * dist b d / (dist b a * (dist c a * dist d a)) ≤ (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : InnerProductSpace ℝ E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>volume (Metric.closedBall x r) = ENNReal.ofReal r ^ finrank ℝ E * ENNReal.ofReal (√π ^ finrank ℝ E / Gamma (↑(finrank ℝ E) / 2 + 1))
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → X → α<VAR>u : α → β<VAR>hu : UniformInducing u<VAR>x : X<GOAL>EquicontinuousAt F x ↔ EquicontinuousAt ((fun x => u ∘ x) ∘ F) x
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : Real.Angle<GOAL>↑(↑r * (↑θ.cos + ↑θ.sin * I)).arg = θ
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<GOAL>↑(↑r * (↑(↑θ).cos + ↑(↑θ).sin * I)).arg = ↑θ
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<GOAL>∃ k, (↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)).arg - θ = 2 * π * ↑k
<VAR>a x z : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<GOAL>(↑r * (↑(Real.cos θ) + ↑(Real.sin θ) * I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
<VAR>G : Type u_1<VAR>inst✝ : CommGroup G<VAR>a b : G<GOAL>a⁻¹ * b * a = b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>inst✝¹ : IsIso a<VAR>inst✝ : Mono f<GOAL>IsPullback a a f f