ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasPullbacks C<VAR>A : C<VAR>f₁ : MonoOver A<VAR>f₂ : Subobject A<GOAL>(inf.obj (Quotient.mk'' f₁)).obj f₂ = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : HasPullbacks C<VAR>A : C<VAR>f₁ f₂ : MonoOver A<GOAL>(inf.obj (Quotient.mk'' f₁)).obj (Quotient.mk'' f₂) = (map f₁.arrow).obj ((pullback f₁.arrow).obj (Quotient.mk'' f₂))
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>p : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : CharP K p<VAR>x : K<VAR>n : ℕ<VAR>ih : (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x<GOAL>(⇑(frobenius (PerfectClosure K p) p))^[n + 1] (mk K p (n + 1, x)) = (of K p) x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : D<GOAL>(whiskerLeft G (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x = adj1.counit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : D<GOAL>F.map (adj2.unit.app (G.obj x)) ≫ adj1.counit.app (F'.obj (G.obj x)) ≫ adj2.counit.app x = adj1.counit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : D<GOAL>F.map (adj2.unit.app (G.obj x) ≫ G.map (adj2.counit.app x)) ≫ adj1.counit.app x = adj1.counit.app x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>h₀ : 0 ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<GOAL>‖↑(approxOn f hf s 0 h₀ n) x‖ ≤ ‖f x‖ + ‖f x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>h₀ : 0 ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<VAR>this : edist 0 (↑(approxOn f hf s 0 h₀ n) x) ≤ edist 0 (f x) + edist 0 (f x)<GOAL>‖↑(approxOn f hf s 0 h₀ n) x‖ ≤ ‖f x‖ + ‖f x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>f : β → E<VAR>hf : Measurable f<VAR>s : Set E<VAR>h₀ : 0 ∈ s<VAR>inst✝ : SeparableSpace ↑s<VAR>x : β<VAR>n : ℕ<VAR>this : ↑‖↑(approxOn f hf s 0 h₀ n) x‖₊ ≤ ↑‖f x‖₊ + ↑‖f x‖₊<GOAL>‖↑(approxOn f hf s 0 h₀ n) x‖ ≤ ‖f x‖ + ‖f x‖
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>f : ℝ → ℝ<VAR>hA' : IsSelfAdjoint A<GOAL>cfc f A = hA.cfc f
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>f : ℝ → ℝ<VAR>hA' : IsSelfAdjoint A<VAR>this : cfcHom hA' = hA.cfcAux<GOAL>cfc f A = hA.cfc f
<VAR>n : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n 𝕜<VAR>hA : A.IsHermitian<VAR>f : ℝ → ℝ<VAR>hA' : IsSelfAdjoint A<VAR>this : cfcHom hA' = hA.cfcAux<GOAL>hA.cfcAux { toFun := (spectrum ℝ A).restrict f, continuous_toFun := ⋯ } = hA.cfc f
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>s : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<GOAL>Module.rank R ↥(span R s) = #↑s
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type w<VAR>ι' : Type w'<VAR>inst✝ : StrongRankCondition R<VAR>s : Set M<VAR>hs : LinearIndependent R fun (x : ↑s) => ↑x<GOAL>Module.rank R ↥(span R (range Subtype.val)) = #↑(range Subtype.val)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₂p₃ : p₂ ≠ p₃<VAR>hp₁ : p₁ ∉ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<GOAL>AffineIndependent k ![p₁, p₂, p₃]
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₂p₃ : p₂ ≠ p₃<VAR>hp₁ : p₁ ∉ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<GOAL>AffineIndependent k (![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 0 2))
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>s : AffineSubspace k P<VAR>p₁ p₂ p₃ : P<VAR>hp₂p₃ : p₂ ≠ p₃<VAR>hp₁ : p₁ ∉ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<GOAL>![p₁, p₂, p₃] ∘ ⇑(Equiv.swap 0 2) = ![p₃, p₂, p₁]
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹² : RingHomInvPair σ σ'<VAR>inst✝¹¹ : RingHomInvPair σ' σ<VAR>inst✝¹⁰ : RingHomIsometric σ<VAR>inst✝⁹ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace 𝕜' F✝<VAR>f : E →SL[σ] F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x<GOAL>Continuous ⇑g
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹² : RingHomInvPair σ σ'<VAR>inst✝¹¹ : RingHomInvPair σ' σ<VAR>inst✝¹⁰ : RingHomIsometric σ<VAR>inst✝⁹ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace 𝕜' F✝<VAR>f : E →SL[σ] F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x<GOAL>IsSeqClosed ↑g.graph
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹² : RingHomInvPair σ σ'<VAR>inst✝¹¹ : RingHomInvPair σ' σ<VAR>inst✝¹⁰ : RingHomIsometric σ<VAR>inst✝⁹ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace 𝕜' F✝<VAR>f : E →SL[σ] F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x<VAR>φ : ℕ → E × F<VAR>x : E<VAR>y : F<VAR>hφg : ∀ (n : ℕ), φ n ∈ ↑g.graph<VAR>hφ : Tendsto φ atTop (𝓝 (x, y))<GOAL>(x, y) ∈ ↑g.graph
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹² : RingHomInvPair σ σ'<VAR>inst✝¹¹ : RingHomInvPair σ' σ<VAR>inst✝¹⁰ : RingHomIsometric σ<VAR>inst✝⁹ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace 𝕜' F✝<VAR>f : E →SL[σ] F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x<VAR>φ : ℕ → E × F<VAR>x : E<VAR>y : F<VAR>hφg : ∀ (n : ℕ), φ n ∈ ↑g.graph<VAR>hφ : Tendsto φ atTop (𝓝 (x, y))<GOAL>Tendsto (⇑g ∘ Prod.fst ∘ φ) atTop (𝓝 y)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹² : RingHomInvPair σ σ'<VAR>inst✝¹¹ : RingHomInvPair σ' σ<VAR>inst✝¹⁰ : RingHomIsometric σ<VAR>inst✝⁹ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace 𝕜' F✝<VAR>f : E →SL[σ] F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x<VAR>φ : ℕ → E × F<VAR>x : E<VAR>y : F<VAR>hφg : ∀ (n : ℕ), φ n ∈ ↑g.graph<VAR>hφ : Tendsto φ atTop (𝓝 (x, y))<VAR>this : ⇑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ<GOAL>Tendsto (⇑g ∘ Prod.fst ∘ φ) atTop (𝓝 y)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝¹² : RingHomInvPair σ σ'<VAR>inst✝¹¹ : RingHomInvPair σ' σ<VAR>inst✝¹⁰ : RingHomIsometric σ<VAR>inst✝⁹ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F✝ : Type u_4<VAR>inst✝⁶ : NormedAddCommGroup F✝<VAR>inst✝⁵ : NormedSpace 𝕜' F✝<VAR>f : E →SL[σ] F✝<VAR>inst✝⁴ : CompleteSpace F✝<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_5<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>g : E →ₗ[𝕜] F<VAR>hg : ∀ (u : ℕ → E) (x : E) (y : F), Tendsto u atTop (𝓝 x) → Tendsto (⇑g ∘ u) atTop (𝓝 y) → y = g x<VAR>φ : ℕ → E × F<VAR>x : E<VAR>y : F<VAR>hφg : ∀ (n : ℕ), φ n ∈ ↑g.graph<VAR>hφ : Tendsto φ atTop (𝓝 (x, y))<VAR>this : ⇑g ∘ Prod.fst ∘ φ = Prod.snd ∘ φ<GOAL>Tendsto (Prod.snd ∘ φ) atTop (𝓝 y)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>2⁻¹ + 2⁻¹ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>L : List (List α)<GOAL>L.reverse.join = (map reverse L).join.reverse
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B✝ I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<VAR>B : Set α<VAR>hB : M.Base B<VAR>hIB : I ⊆ B<GOAL>B ∩ X ⊆ I
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<GOAL>∃ A x, IsGalois A
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<VAR>x : ↑(F.obj X)<VAR>A : C<VAR>f : A ⟶ X<VAR>a : ↑(F.obj A)<VAR>h1 : IsGalois A<VAR>right✝ : F.map f a = x<GOAL>∃ A x, IsGalois A
<VAR>X : Type u_1<VAR>inst✝² : LinearOrder X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OrderTopology X<VAR>a b c : X<VAR>s t : Set X<VAR>hd : Disjoint s (closure t)<VAR>ha : a ∈ s<GOAL>(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
<VAR>X : Type u_1<VAR>inst✝² : LinearOrder X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OrderTopology X<VAR>a b c : X<VAR>s t : Set X<VAR>hd : Disjoint s (closure t)<VAR>ha : a ∈ s<VAR>hmem : tᶜ ∈ 𝓝[≥] a<GOAL>(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
<VAR>X : Type u_1<VAR>inst✝² : LinearOrder X<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : OrderTopology X<VAR>a b✝ c : X<VAR>s t : Set X<VAR>hd : Disjoint s (closure t)<VAR>ha : a ∈ s<VAR>hmem : tᶜ ∈ 𝓝[≥] a<VAR>b : X<VAR>hab : a ≤ b<VAR>hmem' : Icc a b ∈ 𝓝[≥] a<VAR>hsub : Icc a b ⊆ tᶜ<GOAL>(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x y : E<GOAL>(o.kahler (φ x)) (φ y) = (o.kahler x) y
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<GOAL>LinearMap.lTensor V (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V) = ↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(mk K K V).compr₂ (LinearMap.lTensor V (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V)) = (mk K K V).compr₂ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<GOAL>((mk K K V).compr₂ (LinearMap.lTensor V (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V))) 1 = ((mk K K V).compr₂ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))) 1
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<GOAL>∀ (i : ↑(Basis.ofVectorSpaceIndex K V)), (((mk K K V).compr₂ (LinearMap.lTensor V (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V))) 1) ((Basis.ofVectorSpace K V) i) = (((mk K K V).compr₂ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))) 1) ((Basis.ofVectorSpace K V) i)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(((mk K K V).compr₂ (LinearMap.lTensor V (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V))) 1) ((Basis.ofVectorSpace K V) j) = (((mk K K V).compr₂ (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V))) 1) ((Basis.ofVectorSpace K V) j)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.lTensor V (contractLeft K V) ∘ₗ ↑(TensorProduct.assoc K V (Module.Dual K V) V) ∘ₗ LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j) = (↑(TensorProduct.rid K V).symm ∘ₗ ↑(TensorProduct.lid K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.lTensor V (contractLeft K V)) ((TensorProduct.assoc K V (Module.Dual K V) V) ((LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))) = (TensorProduct.rid K V).symm ((TensorProduct.lid K V) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.lTensor V (contractLeft K V)) ((TensorProduct.assoc K V (Module.Dual K V) V) ((LinearMap.rTensor V (coevaluation K V)) (1 ⊗ₜ[K] (Basis.ofVectorSpace K V) j))) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.lTensor V (contractLeft K V)) ((TensorProduct.assoc K V (Module.Dual K V) V) ((∑ i : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) i ⊗ₜ[K] (Basis.ofVectorSpace K V).coord i) ⊗ₜ[K] (Basis.ofVectorSpace K V) j)) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.lTensor V (contractLeft K V)) (∑ x : ↑(Basis.ofVectorSpaceIndex K V), (TensorProduct.assoc K V (Module.Dual K V) V) (((Basis.ofVectorSpace K V) x ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x) ⊗ₜ[K] (Basis.ofVectorSpace K V) j)) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.lTensor V (contractLeft K V)) (∑ x : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) x ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x ⊗ₜ[K] (Basis.ofVectorSpace K V) j) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>∑ x : ↑(Basis.ofVectorSpaceIndex K V), (LinearMap.lTensor V (contractLeft K V)) ((Basis.ofVectorSpace K V) x ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x ⊗ₜ[K] (Basis.ofVectorSpace K V) j) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>∑ x : ↑(Basis.ofVectorSpaceIndex K V), (Basis.ofVectorSpace K V) x ⊗ₜ[K] ((Basis.ofVectorSpace K V).coord x) ((Basis.ofVectorSpace K V) j) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(∑ x : ↑(Basis.ofVectorSpaceIndex K V), if j = x then (Basis.ofVectorSpace K V) x ⊗ₜ[K] 1 else 0) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(if j ∈ Finset.univ then (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1 else 0) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>X₁ X₂ : C<GOAL>binaryBiproductTriangle X₁ X₂ ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>X₁ X₂ Y : C<VAR>g : X₁ ⟶ Y<VAR>h : Y ⟶ X₂<VAR>mem : Triangle.mk g h 0 ∈ distinguishedTriangles<GOAL>binaryBiproductTriangle X₁ X₂ ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>X₁ X₂ Y : C<VAR>g : X₁ ⟶ Y<VAR>h : Y ⟶ X₂<VAR>mem : Triangle.mk g h 0 ∈ distinguishedTriangles<VAR>e : (Triangle.mk g h 0).obj₂ ≅ (Triangle.mk g h 0).obj₁ ⊞ (Triangle.mk g h 0).obj₃<VAR>he₁ : (Triangle.mk g h 0).mor₁ ≫ e.hom = biprod.inl<VAR>he₂ : (Triangle.mk g h 0).mor₂ = e.hom ≫ biprod.snd<GOAL>binaryBiproductTriangle X₁ X₂ ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>X₁ X₂ Y : C<VAR>g : X₁ ⟶ Y<VAR>h : Y ⟶ X₂<VAR>mem : Triangle.mk g h 0 ∈ distinguishedTriangles<VAR>e : (Triangle.mk g h 0).obj₂ ≅ (Triangle.mk g h 0).obj₁ ⊞ (Triangle.mk g h 0).obj₃<VAR>he₁ : g ≫ e.hom = biprod.inl<VAR>he₂ : h = e.hom ≫ biprod.snd<GOAL>binaryBiproductTriangle X₁ X₂ ∈ distinguishedTriangles
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>X₁ X₂ Y : C<VAR>g : X₁ ⟶ Y<VAR>h : Y ⟶ X₂<VAR>mem : Triangle.mk g h 0 ∈ distinguishedTriangles<VAR>e : (Triangle.mk g h 0).obj₂ ≅ (Triangle.mk g h 0).obj₁ ⊞ (Triangle.mk g h 0).obj₃<VAR>he₁ : g ≫ e.hom = biprod.inl<VAR>he₂ : h = e.hom ≫ biprod.snd<GOAL>Triangle.mk g h 0 ≅ binaryBiproductTriangle X₁ X₂
<VAR>m n✝ n : ℕ<VAR>hi : 3 ≤ n<VAR>this : 0 < n<GOAL>n < n !
<VAR>m n✝ n : ℕ<VAR>hi : 3 ≤ n<VAR>this : 0 < n<VAR>hn : 1 < n.pred<GOAL>n < n !
<VAR>m n✝ n : ℕ<VAR>hi : 3 ≤ n<VAR>this : 0 < n<VAR>hn : 1 < n.pred<GOAL>n.pred.succ < (n.pred + 1) * n.pred !
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : Semiquot α<VAR>p : q.IsPure<GOAL>q.get p ∈ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : Semiquot α<VAR>p : q.IsPure<VAR>a : α<VAR>h : a ∈ q<GOAL>q.get p ∈ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : Semiquot α<VAR>p : q.IsPure<VAR>a : α<VAR>h : a ∈ q<GOAL>q.liftOn id p ∈ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>q : Semiquot α<VAR>p : q.IsPure<VAR>a : α<VAR>h : a ∈ q<GOAL>id a ∈ q
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<GOAL>1 < o.card ↔ 1 < o
<VAR>f g : ℕ → ℂ<VAR>s a b : ℂ<VAR>hf : LSeriesHasSum f s a<VAR>hg : LSeriesHasSum g s b<GOAL>LSeriesHasSum (f + g) s (a + b)
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>pb : PowerBasis R S<VAR>I : Ideal R<VAR>g : R[X]<GOAL>(pb.quotientEquivQuotientMinpolyMap I).symm ((Ideal.Quotient.mk (span {Polynomial.map (Ideal.Quotient.mk I) (minpoly R pb.gen)})) (Polynomial.map (Ideal.Quotient.mk I) g)) = (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ((aeval pb.gen) g)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>sq sq₁ sq₂ : Square C<VAR>h : sq₁.IsPushout<VAR>e : sq₁ ≅ sq₂<GOAL>sq₂.IsPushout
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>sq sq₁ sq₂ : Square C<VAR>h : sq₁.IsPushout<VAR>e : sq₁ ≅ sq₂<GOAL>sq₁.f₁₂ ≫ (evaluation₂.mapIso e).hom = (evaluation₁.mapIso e).hom ≫ sq₂.f₁₂