ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>hs : IsOpen s<VAR>hf : AnalyticWithinOn 𝕜 f s<VAR>x : E<VAR>m : x ∈ s<GOAL>AnalyticAt 𝕜 f x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>hs : IsOpen s<VAR>hf : AnalyticWithinOn 𝕜 f s<VAR>x : E<VAR>m : x ∈ s<VAR>r : ℝ<VAR>r0 : r > 0<VAR>rs : Metric.ball x r ⊆ s<GOAL>AnalyticAt 𝕜 f x
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>H : Type u_6<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : E → F<VAR>s : Set E<VAR>hs : IsOpen s<VAR>hf : AnalyticWithinOn 𝕜 f s<VAR>x : E<VAR>m : x ∈ s<VAR>r : ℝ<VAR>r0 : r > 0<VAR>rs : Metric.ball x r ⊆ s<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>t : ℝ≥0∞<VAR>fp : HasFPowerSeriesWithinOnBall f p s x t<GOAL>AnalyticAt 𝕜 f x
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>θ : Δ ⟶ Δ'<GOAL>((N₁ ⋙ Γ₂).obj X).X.map θ ≫ (fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op) Δ' = (fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op) Δ ≫ ((toKaroubi (SimplicialObject C)).obj X).X.map θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>θ : Δ ⟶ Δ'<GOAL>∀ (A : Splitting.IndexSet Δ), ((Γ₀.splitting K[X]).cofan Δ).inj A ≫ ((N₁ ⋙ Γ₂).obj X).X.map θ ≫ (fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op) Δ' = ((Γ₀.splitting K[X]).cofan Δ).inj A ≫ (fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op) Δ ≫ ((toKaroubi (SimplicialObject C)).obj X).X.map θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>θ : Δ ⟶ Δ'<VAR>A : Splitting.IndexSet Δ<GOAL>((Γ₀.splitting K[X]).cofan Δ).inj A ≫ (Γ₀.obj K[X]).map θ ≫ (fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op) Δ' = ((Γ₀.splitting K[X]).cofan Δ).inj A ≫ (fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op) Δ ≫ ((toKaroubi (SimplicialObject C)).obj X).X.map θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>θ : Δ ⟶ Δ'<VAR>A : Splitting.IndexSet Δ<GOAL>Γ₀.Obj.Termwise.mapMono K[X] (image.ι (θ.unop ≫ A.e)) ≫ PInfty.f (unop (A.pull θ).fst).len ≫ X.map (A.pull θ).e.op = PInfty.f (unop A.fst).len ≫ X.map A.e.op ≫ ((toKaroubi (SimplicialObject C)).obj X).X.map θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>θ : Δ ⟶ Δ'<VAR>A : Splitting.IndexSet Δ<GOAL>PInfty.f (unop A.fst).len ≫ X.map (image.ι (θ.unop ≫ A.e)).op ≫ X.map (A.pull θ).e.op = PInfty.f (unop A.fst).len ≫ X.map A.e.op ≫ X.map θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>θ : Δ ⟶ Δ'<VAR>A : Splitting.IndexSet Δ<GOAL>PInfty.f (unop A.fst).len ≫ X.map ((image.ι (θ.unop ≫ A.e)).op ≫ (A.pull θ).e.op) = PInfty.f (unop A.fst).len ≫ X.map (A.e.op ≫ θ)
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>θ : Δ ⟶ Δ'<VAR>A : Splitting.IndexSet Δ<GOAL>(image.ι (θ.unop ≫ A.e)).op ≫ (A.pull θ).e.op = A.e.op ≫ θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>θ : Δ ⟶ Δ'<VAR>A : Splitting.IndexSet Δ<GOAL>((A.pull θ).e ≫ image.ι (θ.unop ≫ A.e)).op = A.e.op ≫ θ
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>{ app := fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ } = ((N₁ ⋙ Γ₂).obj X).p ≫ { app := fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ } ≫ ((toKaroubi (SimplicialObject C)).obj X).p
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<GOAL>∀ (n : ℕ), (Γ₀.splitting K[X]).φ { app := fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ } n = (Γ₀.splitting K[X]).φ (((N₁ ⋙ Γ₂).obj X).p ≫ { app := fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ } ≫ ((toKaroubi (SimplicialObject C)).obj X).p) n
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : SimplicialObject C<VAR>n : ℕ<GOAL>((Γ₀.splitting K[X]).ι n ≫ (Γ₀.splitting K[X]).desc (op [n]) fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op) = (Γ₀.splitting K[X]).ι n ≫ ((Γ₀.splitting K[X]).desc (op [n]) fun A => PInfty.f (unop A.fst).len ≫ ((Γ₀.splitting K[X]).cofan (op [n])).inj A) ≫ ((Γ₀.splitting K[X]).desc (op [n]) fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op) ≫ 𝟙 (X _[n])
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X Y : SimplicialObject C<VAR>f : X ⟶ Y<GOAL>((N₁ ⋙ Γ₂).map f ≫ (fun X => { f := { app := fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ }, comm := ⋯ }) Y).f = ((fun X => { f := { app := fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ }, comm := ⋯ }) X ≫ (toKaroubi (SimplicialObject C)).map f).f
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X Y : SimplicialObject C<VAR>f : X ⟶ Y<GOAL>∀ (n : ℕ), (Γ₀.splitting K[X]).φ ((N₁ ⋙ Γ₂).map f ≫ (fun X => { f := { app := fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ }, comm := ⋯ }) Y).f n = (Γ₀.splitting K[X]).φ ((fun X => { f := { app := fun Δ => (Γ₀.splitting K[X]).desc Δ fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ }, comm := ⋯ }) X ≫ (toKaroubi (SimplicialObject C)).map f).f n
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.26563, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X Y : SimplicialObject C<VAR>f : X ⟶ Y<VAR>n : ℕ<GOAL>((Γ₀.splitting K[X]).ι n ≫ ((Γ₀.splitting K[X]).desc (op [n]) fun A => (PInfty.f (unop A.fst).len ≫ f.app A.fst) ≫ ((Γ₀.splitting K[Y]).cofan (op [n])).inj A) ≫ (Γ₀.splitting K[Y]).desc (op [n]) fun A => PInfty.f (unop A.fst).len ≫ Y.map A.e.op) = (Γ₀.splitting K[X]).ι n ≫ ((Γ₀.splitting K[X]).desc (op [n]) fun A => PInfty.f (unop A.fst).len ≫ X.map A.e.op) ≫ f.app (op [n])
<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>c c₁ c₂ p₁✝ p₂✝ p₁ p₂ : P<GOAL>(perpBisector p₁ p₂).direction = (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ
<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>c c₁ c₂ p₁✝ p₂✝ p₁ p₂ : P<GOAL>LinearMap.ker ((innerₛₗ ℝ) (p₂ -ᵥ p₁)) = (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ
<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>c c₁ c₂ p₁✝ p₂✝ p₁ p₂ : P<VAR>x : V<GOAL>x ∈ LinearMap.ker ((innerₛₗ ℝ) (p₂ -ᵥ p₁)) ↔ x ∈ (Submodule.span ℝ {p₂ -ᵥ p₁})ᗮ
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(deriv fun z => z ^ p * (1 - ε z)) =Θ[atTop] fun z => z ^ (p - 1)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s✝ t✝ A B : Set β<VAR>a : α<VAR>x✝ : β<VAR>s t : Set α<VAR>x : αᵐᵒᵖ<GOAL>x • s ∩ t ≠ ∅ ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Group α<VAR>inst✝ : MulAction α β<VAR>s✝ t✝ A B : Set β<VAR>a : α<VAR>x✝ : β<VAR>s t : Set α<VAR>x : αᵐᵒᵖ<GOAL>(x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x
<VAR>α β γ : Type u<VAR>F : Type u → Type v<VAR>inst✝¹ : Applicative F<VAR>inst✝ : LawfulApplicative F<VAR>f : β → γ<VAR>x : F (α → β)<VAR>y : F α<GOAL>(f <$> Seq.seq x fun x => y) = Seq.seq ((fun x => f ∘ x) <$> x) fun x => y
<VAR>α β γ : Type u<VAR>F : Type u → Type v<VAR>inst✝¹ : Applicative F<VAR>inst✝ : LawfulApplicative F<VAR>f : β → γ<VAR>x : F (α → β)<VAR>y : F α<GOAL>(Seq.seq (pure f) fun x_1 => Seq.seq x fun x => y) = Seq.seq (Seq.seq (pure fun x => f ∘ x) fun x_1 => x) fun x => y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>t✝ : γ → γ → Prop<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder γ t<VAR>f : r ≺i s<VAR>g : s ≺i t<VAR>h : r ≺i t<GOAL>t h.top g.top
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r✝ : α → α → Prop<VAR>s✝ : β → β → Prop<VAR>t✝ : γ → γ → Prop<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder γ t<VAR>f : r ≺i s<VAR>g : s ≺i t<VAR>h : r ≺i t<GOAL>t (f.trans g).top g.top
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖ ≤ re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>y : F<GOAL>‖⟪0, y⟫_𝕜‖ * ‖⟪y, 0⟫_𝕜‖ ≤ re ⟪0, 0⟫_𝕜 * re ⟪y, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<VAR>hx : x ≠ 0<GOAL>‖⟪x, y⟫_𝕜‖ * ‖⟪y, x⟫_𝕜‖ ≤ re ⟪x, x⟫_𝕜 * re ⟪y, y⟫_𝕜
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝¹ : FunLike 𝓕 E F<VAR>inst✝ : MonoidHomClass 𝓕 E F<VAR>f : 𝓕<VAR>C : ℝ<VAR>h : ∀ (x : E), ‖f x‖ ≤ C * ‖x‖<VAR>x y : E<GOAL>dist (f x) (f y) ≤ C * dist x y
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>j₃ : J<VAR>x' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, x⟩.fst ⟶ l<VAR>g : ⟨j₃, x'⟩.fst ⟶ l<VAR>hfg : (F ⋙ forget MonCat).map f ⟨j₁, x⟩.snd = (F ⋙ forget MonCat).map g ⟨j₃, x'⟩.snd<GOAL>colimitMulAux F ⟨j₁, x⟩ ⟨j₂, y⟩ = colimitMulAux F ⟨j₃, x'⟩ ⟨j₂, y⟩
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>j₃ : J<VAR>x' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, x⟩.fst ⟶ l<VAR>g : ⟨j₃, x'⟩.fst ⟶ l<VAR>hfg : (F.map f) x = (F.map g) x'<GOAL>colimitMulAux F ⟨j₁, x⟩ ⟨j₂, y⟩ = colimitMulAux F ⟨j₃, x'⟩ ⟨j₂, y⟩
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>j₃ : J<VAR>x' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, x⟩.fst ⟶ l<VAR>g : ⟨j₃, x'⟩.fst ⟶ l<VAR>hfg : (F.map f) x = (F.map g) x'<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₃ j₂ ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ<VAR>h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β<GOAL>colimitMulAux F ⟨j₁, x⟩ ⟨j₂, y⟩ = colimitMulAux F ⟨j₃, x'⟩ ⟨j₂, y⟩
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>j₃ : J<VAR>x' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, x⟩.fst ⟶ l<VAR>g : ⟨j₃, x'⟩.fst ⟶ l<VAR>hfg : (F.map f) x = (F.map g) x'<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₃ j₂ ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ<VAR>h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β<GOAL>∃ k f g, (F.map f) ⟨IsFiltered.max ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst, (F.map (IsFiltered.leftToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst)) ⟨j₁, x⟩.snd * (F.map (IsFiltered.rightToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst)) ⟨j₂, y⟩.snd⟩.snd = (F.map g) ⟨IsFiltered.max ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst, (F.map (IsFiltered.leftToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst)) ⟨j₃, x'⟩.snd * (F.map (IsFiltered.rightToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst)) ⟨j₂, y⟩.snd⟩.snd
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>j₃ : J<VAR>x' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, x⟩.fst ⟶ l<VAR>g : ⟨j₃, x'⟩.fst ⟶ l<VAR>hfg : (F.map f) x = (F.map g) x'<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₃ j₂ ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ<VAR>h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β<GOAL>(F.map α) ⟨IsFiltered.max ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst, (F.map (IsFiltered.leftToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst)) ⟨j₁, x⟩.snd * (F.map (IsFiltered.rightToMax ⟨j₁, x⟩.fst ⟨j₂, y⟩.fst)) ⟨j₂, y⟩.snd⟩.snd = (F.map γ) ⟨IsFiltered.max ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst, (F.map (IsFiltered.leftToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst)) ⟨j₃, x'⟩.snd * (F.map (IsFiltered.rightToMax ⟨j₃, x'⟩.fst ⟨j₂, y⟩.fst)) ⟨j₂, y⟩.snd⟩.snd
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>j₃ : J<VAR>x' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, x⟩.fst ⟶ l<VAR>g : ⟨j₃, x'⟩.fst ⟶ l<VAR>hfg : (F.map f) x = (F.map g) x'<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₃ j₂ ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ<VAR>h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β<GOAL>(F.map α) ((F.map (IsFiltered.leftToMax j₁ j₂)) x * (F.map (IsFiltered.rightToMax j₁ j₂)) y) = (F.map γ) ((F.map (IsFiltered.leftToMax j₃ j₂)) x' * (F.map (IsFiltered.rightToMax j₃ j₂)) y)
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>j₃ : J<VAR>x' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, x⟩.fst ⟶ l<VAR>g : ⟨j₃, x'⟩.fst ⟶ l<VAR>hfg : (F.map f) x = (F.map g) x'<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₃ j₂ ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ<VAR>h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β<GOAL>(F.map α) ((F.map (IsFiltered.leftToMax j₁ j₂)) x) * (F.map α) ((F.map (IsFiltered.rightToMax j₁ j₂)) y) = (F.map γ) ((F.map (IsFiltered.leftToMax j₃ j₂)) x') * (F.map γ) ((F.map (IsFiltered.rightToMax j₃ j₂)) y)
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>j₃ : J<VAR>x' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, x⟩.fst ⟶ l<VAR>g : ⟨j₃, x'⟩.fst ⟶ l<VAR>hfg : (F.map f) x = (F.map g) x'<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₃ j₂ ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ<VAR>h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β<GOAL>(F.map (IsFiltered.leftToMax j₁ j₂) ≫ F.map α) x * (F.map (IsFiltered.rightToMax j₁ j₂) ≫ F.map α) y = (F.map (IsFiltered.leftToMax j₃ j₂) ≫ F.map γ) x' * (F.map (IsFiltered.rightToMax j₃ j₂) ≫ F.map γ) y
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>x : ↑(F.obj j₁)<VAR>j₂ : J<VAR>y : ↑(F.obj j₂)<VAR>j₃ : J<VAR>x' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, x⟩.fst ⟶ l<VAR>g : ⟨j₃, x'⟩.fst ⟶ l<VAR>hfg : (F.map f) x = (F.map g) x'<VAR>s : J<VAR>α : IsFiltered.max j₁ j₂ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₃ j₂ ⟶ s<VAR>h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ<VAR>h₃ : IsFiltered.leftToMax j₃ j₂ ≫ γ = g ≫ β<GOAL>(F.map f ≫ F.map β) x * (F.map (IsFiltered.rightToMax j₃ j₂) ≫ F.map γ) y = (F.map g ≫ F.map β) x' * (F.map (IsFiltered.rightToMax j₃ j₂) ≫ F.map γ) y
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y : R<GOAL>x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y
<VAR>R : Type u_1<VAR>inst✝ : Rack R<VAR>x y : R<VAR>h : op x ◃ op x = op y ◃ op y ↔ op x = op y<GOAL>x ◃⁻¹ x = y ◃⁻¹ y ↔ x = y
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Nontrivial R<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → M<VAR>hb : LinearIndependent R b<GOAL>Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : StrongRankCondition R<VAR>inst✝¹ : Nontrivial R<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → M<VAR>hb : LinearIndependent R b<VAR>this : Module.rank R ↥(span R (range b)) = #↑(range b)<GOAL>Module.rank R ↥(span R (range b)) = ↑(Fintype.card ι)
<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 : Mon_ C<VAR>P : Bimod R S<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)<GOAL>((PreservesCoequalizer.iso (tensorLeft R.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)).inv ≫ colimMap (parallelPairHom (R.X ◁ P.actRight ▷ S.X) (R.X ◁ ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ((α_ R.X (P.X ⊗ S.X) S.X).inv ≫ (α_ R.X P.X S.X).inv ▷ S.X ≫ P.actLeft ▷ S.X ▷ S.X) ((α_ R.X P.X S.X).inv ≫ P.actLeft ▷ S.X) ⋯ ⋯)) ≫ coequalizer.desc P.actRight ⋯ = R.X ◁ coequalizer.desc P.actRight ⋯ ≫ P.actLeft
<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 : Mon_ C<VAR>P : Bimod R S<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)<GOAL>(tensorLeft R.X).map (coequalizer.π (P.actRight ▷ { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X) ((α_ P.X S.X { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫ P.X ◁ { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actLeft)) ≫ ((PreservesCoequalizer.iso (tensorLeft R.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)).inv ≫ colimMap (parallelPairHom (R.X ◁ P.actRight ▷ S.X) (R.X ◁ ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ((α_ R.X (P.X ⊗ S.X) S.X).inv ≫ (α_ R.X P.X S.X).inv ▷ S.X ≫ P.actLeft ▷ S.X ▷ S.X) ((α_ R.X P.X S.X).inv ≫ P.actLeft ▷ S.X) ⋯ ⋯)) ≫ coequalizer.desc P.actRight ⋯ = (tensorLeft R.X).map (coequalizer.π (P.actRight ▷ { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X) ((α_ P.X S.X { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫ P.X ◁ { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actLeft)) ≫ R.X ◁ coequalizer.desc P.actRight ⋯ ≫ P.actLeft
<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 : Mon_ C<VAR>P : Bimod R S<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)<GOAL>R.X ◁ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ ((PreservesCoequalizer.iso (tensorLeft R.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)).inv ≫ colimMap (parallelPairHom (R.X ◁ P.actRight ▷ S.X) (R.X ◁ ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ((α_ R.X (P.X ⊗ S.X) S.X).inv ≫ (α_ R.X P.X S.X).inv ▷ S.X ≫ P.actLeft ▷ S.X ▷ S.X) ((α_ R.X P.X S.X).inv ≫ P.actLeft ▷ S.X) ⋯ ⋯)) ≫ coequalizer.desc P.actRight ⋯ = R.X ◁ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ R.X ◁ coequalizer.desc P.actRight ⋯ ≫ P.actLeft
<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 : Mon_ C<VAR>P : Bimod R S<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)<GOAL>((α_ R.X P.X S.X).inv ≫ P.actLeft ▷ S.X) ≫ P.actRight = R.X ◁ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ R.X ◁ coequalizer.desc P.actRight ⋯ ≫ P.actLeft
<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 : Mon_ C<VAR>P : Bimod R S<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)<GOAL>(α_ R.X P.X S.X).inv ≫ (α_ R.X P.X S.X).hom ≫ R.X ◁ P.actRight ≫ P.actLeft = R.X ◁ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ R.X ◁ coequalizer.desc P.actRight ⋯ ≫ P.actLeft