ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>inst✝ : Nonempty ι<VAR>u : ι → UniformSpace β<VAR>l : Filter β<GOAL>l.NeBot ∧ l ×ˢ l ≤ 𝓤 β ↔ ∀ (i : ι), l.NeBot ∧ l ×ˢ l ≤ 𝓤 β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : ℕ → ℝ≥0<VAR>r : ℝ≥0<GOAL>HasSum f r ↔ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : ℕ → ℝ≥0<VAR>r : ℝ≥0<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, ↑(f i)) atTop (𝓝 ↑r) ↔ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : ℕ → ℝ≥0<VAR>r : ℝ≥0<GOAL>Tendsto (fun n => ↑(∑ a ∈ Finset.range n, f a)) atTop (𝓝 ↑r) ↔ Tendsto (fun n => ∑ a ∈ Finset.range n, f a) atTop (𝓝 r)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a✝ : α<VAR>b✝ : β<VAR>h₀ : ∀ (b : β), Antitone (swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>a : α<VAR>ha : a ∈ lowerBounds s<VAR>b : β<VAR>hb : b ∈ lowerBounds t<GOAL>BddAbove (image2 f s t)
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F P : Sheaf J A<GOAL>(sheafComposeNatIso J U (sheafificationAdjunction J A) (sheafificationAdjunction J B)).hom.app ((sheafToPresheaf J A).obj P) ≫ (sheafCompose J U).map ((sheafificationAdjunction J A).counit.app P) = (sheafificationAdjunction J B).counit.app ((sheafCompose J U).obj P)
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F P : Sheaf J A<GOAL>((sheafificationAdjunction J B).homEquiv (P.val ⋙ U) ((sheafCompose J U).obj ((presheafToSheaf J A).obj P.val))).symm (whiskerRight (toSheafify J P.val) U) ≫ (sheafCompose J U).map ((sheafificationAdjunction J A).counit.app P) = (sheafificationAdjunction J B).counit.app ((sheafCompose J U).obj P)
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F P : Sheaf J A<GOAL>((presheafToSheaf J B).map (whiskerRight (toSheafify J P.val) U) ≫ (sheafificationAdjunction J B).counit.app ((sheafCompose J U).obj ((presheafToSheaf J A).obj P.val))) ≫ (sheafCompose J U).map ((sheafificationAdjunction J A).counit.app P) = (sheafificationAdjunction J B).counit.app ((sheafCompose J U).obj P)
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F P : Sheaf J A<GOAL>(((presheafToSheaf J B).map (whiskerRight (toSheafify J P.val) U) ≫ (sheafificationAdjunction J B).counit.app ((sheafCompose J U).obj ((presheafToSheaf J A).obj P.val))) ≫ (sheafCompose J U).map ((sheafificationAdjunction J A).counit.app P)).val = ((sheafificationAdjunction J B).counit.app ((sheafCompose J U).obj P)).val
<VAR>C : Type u_1<VAR>inst✝¹³ : Category.{u_4, u_1} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_2<VAR>inst✝¹² : Category.{u_5, u_2} A<VAR>inst✝¹¹ : HasWeakSheafify J A<VAR>inst✝¹⁰ : (constantSheaf J A).Faithful<VAR>inst✝⁹ : (constantSheaf J A).Full<VAR>t : C<VAR>ht : IsTerminal t<VAR>B : Type u_3<VAR>inst✝⁸ : Category.{u_6, u_3} B<VAR>U : A ⥤ B<VAR>inst✝⁷ : HasWeakSheafify J A<VAR>inst✝⁶ : HasWeakSheafify J B<VAR>inst✝⁵ : (constantSheaf J A).Faithful<VAR>inst✝⁴ : (constantSheaf J A).Full<VAR>inst✝³ : (constantSheaf J B).Faithful<VAR>inst✝² : (constantSheaf J B).Full<VAR>inst✝¹ : J.PreservesSheafification U<VAR>inst✝ : J.HasSheafCompose U<VAR>F P : Sheaf J A<GOAL>toSheafify J (P.val ⋙ U) ≫ (((presheafToSheaf J B).map (whiskerRight (toSheafify J P.val) U) ≫ (sheafificationAdjunction J B).counit.app ((sheafCompose J U).obj ((presheafToSheaf J A).obj P.val))) ≫ (sheafCompose J U).map ((sheafificationAdjunction J A).counit.app P)).val = toSheafify J (P.val ⋙ U) ≫ ((sheafificationAdjunction J B).counit.app ((sheafCompose J U).obj P)).val
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasInitial C<VAR>h : ∀ (A : C) (f : A ⟶ ⊥_ C), IsIso f<VAR>I A : C<VAR>f : A ⟶ I<VAR>hI : IsInitial I<VAR>this : IsIso (f ≫ hI.to (⊥_ C))<GOAL>f ≫ hI.to (⊥_ C) ≫ inv (f ≫ hI.to (⊥_ C)) = 𝟙 A
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>S : L.Substructure M<VAR>f : M →[L] N<VAR>p : L.Substructure N<GOAL>f.range ≤ p ↔ comap f p = ⊤
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>f : α → β<VAR>inst✝ : Zero β<VAR>t : Set β<VAR>ht : 0 ∉ t<GOAL>t ∈ Filter.map (s.indicator f) (ae μ) ↔ μ ((f ⁻¹' t)ᶜ ∪ sᶜ) = 0
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : Finite ι<VAR>f : ι → Set X<GOAL>closure (⋃ i, f i) = ⋃ i, closure (f i)
<VAR>x y : ℝ<GOAL>↑(cos (2 * x)) = ↑(2 * cos x ^ 2 - 1)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>u : Set P<VAR>hu : IsOpen u<VAR>x : P<VAR>hx : x ∈ u<GOAL>∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>u : Set P<VAR>hu : IsOpen u<VAR>x : P<VAR>hx : x ∈ u<VAR>s : Set P<VAR>hsu : s ⊆ u<VAR>hs : AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤<GOAL>∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>n : ℕ<GOAL>count K v (↑v.asIdeal ^ n) = ↑n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f✝ : α → M<VAR>f : ℕ → M<VAR>m n k : ℕ<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<GOAL>(∏ i ∈ Ioc m n, f i) * ∏ i ∈ Ioc n k, f i = ∏ i ∈ Ioc m k, f i
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f✝ : α → M<VAR>f : ℕ → M<VAR>m n k : ℕ<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<GOAL>Disjoint (Ioc m n) (Ioc n k)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f✝ : α → M<VAR>f : ℕ → M<VAR>m n k : ℕ<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<GOAL>∀ x ∈ Ioc m n, x ∈ Ioc n k → False
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f✝ : α → M<VAR>f : ℕ → M<VAR>m n k : ℕ<VAR>hmn : m ≤ n<VAR>hnk : n ≤ k<VAR>x : ℕ<VAR>hx : x ∈ Ioc m n<VAR>h'x : x ∈ Ioc n k<GOAL>False
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hcf : ContinuousOn f (Ico a b)<VAR>hcg : ContinuousOn g (Ico a b)<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : f a = 0<VAR>hga : g a = 0<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<GOAL>Tendsto (fun x => f x / g x) (𝓝[>] a) l
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hcf : ContinuousOn f (Ico a b)<VAR>hcg : ContinuousOn g (Ico a b)<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : f a = 0<VAR>hga : g a = 0<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<GOAL>Tendsto f (𝓝[>] a) (𝓝 0)
<VAR>a b : ℝ<VAR>hab : a < b<VAR>l : Filter ℝ<VAR>f f' g g' : ℝ → ℝ<VAR>hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x<VAR>hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x<VAR>hcf : ContinuousOn f (Ico a b)<VAR>hcg : ContinuousOn g (Ico a b)<VAR>hg' : ∀ x ∈ Ioo a b, g' x ≠ 0<VAR>hfa : f a = 0<VAR>hga : g a = 0<VAR>hdiv : Tendsto (fun x => f' x / g' x) (𝓝[>] a) l<GOAL>Tendsto g (𝓝[>] a) (𝓝 0)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → F<VAR>h0 : ¬p = 0<VAR>h_top : ¬p = ⊤<GOAL>eLpNorm (-f) p μ = eLpNorm f p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>d : ℝ≥0∞<GOAL>d ≤ s.einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : F →ₗ[𝕜] G<VAR>B : E →ₗ[𝕜] F<VAR>v : G<GOAL>(adjoint (A ∘ₗ B)) v = (adjoint B ∘ₗ adjoint A) v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : F →ₗ[𝕜] G<VAR>B : E →ₗ[𝕜] F<VAR>v : G<VAR>w : E<GOAL>⟪w, (adjoint (A ∘ₗ B)) v⟫_𝕜 = ⟪w, (adjoint B ∘ₗ adjoint A) v⟫_𝕜
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a b c : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Ico a b) b ↔ ContinuousWithinAt f (Iio b) b
<GOAL>riemannZeta 1 = (↑γ - Complex.log (4 * ↑π)) / 2
<VAR>this : Tendsto (fun s => HurwitzZeta.hurwitzZetaEven 0 s - 1 / (s - 1) / s.Gammaℝ) (𝓝[≠] 1) (𝓝 (HurwitzZeta.hurwitzZetaEven 0 1))<GOAL>riemannZeta 1 = (↑γ - Complex.log (4 * ↑π)) / 2
<VAR>this : Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (riemannZeta 1))<GOAL>riemannZeta 1 = (↑γ - Complex.log (4 * ↑π)) / 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s t : SignedMeasure α<VAR>μ : Measure α<GOAL>singularPart 0 μ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s t : SignedMeasure α<VAR>μ : Measure α<GOAL>0 = 0 + μ.withDensityᵥ 0
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<GOAL>f.right.app P = g.right.app P
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<GOAL>F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) = F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<GOAL>∀ (j : P.Elementsᵒᵖ), (coconeOfRepresentable P).ι.app j ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) = (coconeOfRepresentable P).ι.app j ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x : P.Elementsᵒᵖ<GOAL>(coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) = (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x : P.Elementsᵒᵖ<VAR>eq : (𝟭 (Cᵒᵖ ⥤ Type v₁)).map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ F.op.lanUnit.app P = F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ (F.op.lan ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).map (yonedaEquiv.symm (Opposite.unop x).snd)<GOAL>(coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) = (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x : P.Elementsᵒᵖ<VAR>eq : (𝟭 (Cᵒᵖ ⥤ Type v₁)).map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ F.op.lanUnit.app P = F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ (F.op.lan ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).map (yonedaEquiv.symm (Opposite.unop x).snd)<VAR>eq₁ : (((Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom).hom ≫ ((whiskeringLeft C (Cᵒᵖ ⥤ Type v₁) (Dᵒᵖ ⥤ Type v₁)).obj yoneda).map f.right).app (Opposite.unop (Opposite.unop x).fst)).app (F.op.obj (Opposite.unop x).fst) (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (F.op.obj (Opposite.unop x).fst) (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst)))<GOAL>(coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) = (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x : P.Elementsᵒᵖ<VAR>eq : (𝟭 (Cᵒᵖ ⥤ Type v₁)).map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ F.op.lanUnit.app P = F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ (F.op.lan ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).map (yonedaEquiv.symm (Opposite.unop x).snd)<VAR>eq₁ : (((Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom).hom ≫ ((whiskeringLeft C (Cᵒᵖ ⥤ Type v₁) (Dᵒᵖ ⥤ Type v₁)).obj yoneda).map f.right).app (Opposite.unop (Opposite.unop x).fst)).app (F.op.obj (Opposite.unop x).fst) (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (F.op.obj (Opposite.unop x).fst) (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst)))<VAR>eq₂ : (((Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom).hom ≫ ((whiskeringLeft C (Cᵒᵖ ⥤ Type v₁) (Dᵒᵖ ⥤ Type v₁)).obj yoneda).map g.right).app (Opposite.unop (Opposite.unop x).fst)).app (F.op.obj (Opposite.unop x).fst) (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (F.op.obj (Opposite.unop x).fst) (𝟙 (Opposite.unop (F.op.obj (Opposite.unop x).fst)))<GOAL>(coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) = (coconeOfRepresentable P).ι.app x ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x : P.Elementsᵒᵖ<VAR>eq : yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P = F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd))<VAR>eq₁ : (f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<VAR>eq₂ : (g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<GOAL>yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (f.right.app P) = yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P ≫ whiskerLeft F.op (g.right.app P)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>Φ : yoneda.LeftExtension (F ⋙ yoneda)<VAR>f g : Functor.LeftExtension.mk F.op.lan (compYonedaIsoYonedaCompLan F).hom ⟶ Φ<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>x : P.Elementsᵒᵖ<VAR>eq : yonedaEquiv.symm (Opposite.unop x).snd ≫ F.op.lanUnit.app P = F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd))<VAR>eq₁ : (f.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<VAR>eq₂ : (g.right.app (yoneda.obj (Opposite.unop (Opposite.unop x).fst))).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (((compYonedaIsoYonedaCompLan F).hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))) = (Φ.hom.app (Opposite.unop (Opposite.unop x).fst)).app (Opposite.op (F.obj (Opposite.unop (Opposite.unop x).fst))) (𝟙 (F.obj (Opposite.unop (Opposite.unop x).fst)))<GOAL>F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ f.right.app P) = F.op.lanUnit.app (yoneda.obj (Opposite.unop (Opposite.unop x).1)) ≫ whiskerLeft F.op (F.op.lan.map (yonedaEquiv.symm (Opposite.unop x).snd) ≫ g.right.app P)