ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : NormedRing R<VAR>inst✝¹ : IsAbsoluteValue norm<VAR>inst✝ : ProperSpace R<VAR>p : R[X]<VAR>hp0 : ¬0 < p.degree<GOAL>∀ (y : R), ‖eval (p.coeff 0) p‖ ≤ ‖eval y p‖
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : NormedRing R<VAR>inst✝¹ : IsAbsoluteValue norm<VAR>inst✝ : ProperSpace R<VAR>p : R[X]<VAR>hp0 : ¬0 < p.degree<GOAL>∀ (y : R), ‖eval ((C (p.coeff 0)).coeff 0) (C (p.coeff 0))‖ ≤ ‖eval y (C (p.coeff 0))‖
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Preorder α<VAR>a✝ b c : α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<GOAL>⋃ b, Ico a b = Ici a
<VAR>a : ℕ<GOAL>Nat.cast '' Iio a = Ico 0 ↑a
<VAR>a : ℕ<GOAL>Ico ↑⊥ ↑a = Ico 0 ↑a
<VAR>α : Type u_1<VAR>a b c : ZNum<GOAL>a ≤ b → c + a ≤ c + b
<VAR>α : Type u_1<VAR>a b c : ZNum<GOAL>↑a ≤ ↑b → ↑c + ↑a ≤ ↑c + ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>f : α →ₛ ℝ≥0∞<VAR>g : β →ₛ ℝ≥0∞<VAR>ν : Measure β<VAR>H : ∀ (y : ℝ≥0∞), μ (↑f ⁻¹' {y}) = ν (↑g ⁻¹' {y})<GOAL>∑ x ∈ f.range, x * μ (↑f ⁻¹' {x}) = ∑ x ∈ g.range, x * μ (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>f : α →ₛ ℝ≥0∞<VAR>g : β →ₛ ℝ≥0∞<VAR>ν : Measure β<VAR>H : ∀ (y : ℝ≥0∞), μ (↑f ⁻¹' {y}) = ν (↑g ⁻¹' {y})<GOAL>∀ (x : α), ↑f x ≠ 0 → μ (↑f ⁻¹' {↑f x}) ≠ 0 → ↑f x ∈ g.range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν✝ : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>f : α →ₛ ℝ≥0∞<VAR>g : β →ₛ ℝ≥0∞<VAR>ν : Measure β<VAR>H : ∀ (y : ℝ≥0∞), μ (↑f ⁻¹' {y}) = ν (↑g ⁻¹' {y})<VAR>x✝ : α<VAR>a✝¹ : ↑f x✝ ≠ 0<VAR>a✝ : ν (↑g ⁻¹' {↑f x✝}) ≠ 0<GOAL>↑f x✝ ∈ g.range
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>C₁ C₂ : Set X<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>h : C₁ ∪ C₂ = univ<VAR>f : LocallyConstant (↑C₁) Z<VAR>g : LocallyConstant (↑C₂) Z<VAR>hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩<VAR>inst✝ : DecidablePred fun x => x ∈ C₁<VAR>x : X<VAR>hx : x ∈ C₂<GOAL>(piecewise h₁ h₂ h f g hfg) x = g ⟨x, hx⟩
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X<VAR>C₁ C₂ : Set X<VAR>h₁ : IsClosed C₁<VAR>h₂ : IsClosed C₂<VAR>h : C₁ ∪ C₂ = univ<VAR>f : LocallyConstant (↑C₁) Z<VAR>g : LocallyConstant (↑C₂) Z<VAR>hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩<VAR>inst✝ : DecidablePred fun x => x ∈ C₁<VAR>x : X<VAR>hx : x ∈ C₂<GOAL>(if hi : x ∈ C₁ then f ⟨x, hi⟩ else g ⟨x, ⋯⟩) = g ⟨x, hx⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Lattice α<VAR>inst✝ : Group α<VAR>a : α<VAR>ha : 1 < a<GOAL>1 < a⁺ᵐ
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l₁ l₂ : List Γ<VAR>i j : ℕ<VAR>e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default<VAR>h : l₁.length ≤ l₂.length<GOAL>BlankExtends l₁ l₂
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l₁ l₂ : List Γ<VAR>i j : ℕ<VAR>e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default<VAR>h : l₁.length ≤ l₂.length<GOAL>l₂ = l₁ ++ List.replicate (i - j) default
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l₁ l₂ : List Γ<VAR>i j : ℕ<VAR>e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default<VAR>h : l₁.length ≤ l₂.length<GOAL>l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j) default ++ List.replicate j default
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l₁ l₂ : List Γ<VAR>i j : ℕ<VAR>e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default<VAR>h : l₁.length ≤ l₂.length<GOAL>j ≤ i
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l₁ l₂ : List Γ<VAR>i j : ℕ<VAR>h : l₁.length ≤ l₂.length<VAR>e : (l₁ ++ List.replicate i default).length = (l₂ ++ List.replicate j default).length<GOAL>j ≤ i
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>l₁ l₂ : List Γ<VAR>i j : ℕ<VAR>h : l₁.length ≤ l₂.length<VAR>e : l₁.length + i = l₂.length + j<GOAL>j ≤ i
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>B✝ : Type u<VAR>inst✝³ : CommRing B✝<VAR>inst✝² : Algebra R B✝<VAR>I✝ : Ideal B✝<VAR>B : Type u<VAR>inst✝¹ : CommRing B<VAR>inst✝ : FormallyUnramified R A<VAR>I : Ideal B<VAR>hI : IsNilpotent I<GOAL>∀ [_RB : Algebra R B], Function.Injective (Ideal.Quotient.mkₐ R I).comp
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>B✝ : Type u<VAR>inst✝³ : CommRing B✝<VAR>inst✝² : Algebra R B✝<VAR>I✝ : Ideal B✝<VAR>B : Type u<VAR>inst✝¹ : CommRing B<VAR>inst✝ : FormallyUnramified R A<VAR>I : Ideal B<VAR>hI : IsNilpotent I<GOAL>∀ ⦃S : Type u⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → ∀ [_RB : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R I).comp
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra R A<VAR>B✝ : Type u<VAR>inst✝³ : CommRing B✝<VAR>inst✝² : Algebra R B✝<VAR>I✝ : Ideal B✝<VAR>B : Type u<VAR>inst✝¹ : CommRing B<VAR>inst✝ : FormallyUnramified R A<VAR>I : Ideal B<VAR>hI : IsNilpotent I<GOAL>∀ ⦃S : Type u⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → (∀ [_RB : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R I).comp) → (∀ [_RB : Algebra R (S ⧸ I)], Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) → ∀ [_RB : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R J).comp
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocDiv hp (a - p) b = toIocDiv hp a b + 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>f : Z → X<GOAL>IsOpenMap (⇑h ∘ f) ↔ IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>f : Z → X<GOAL>IsOpenMap (⇑h ∘ f) → IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>f : Z → X<VAR>hf : IsOpenMap (⇑h ∘ f)<GOAL>IsOpenMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>f : Z → X<VAR>hf : IsOpenMap (⇑h ∘ f)<GOAL>IsOpenMap (⇑h.symm ∘ ⇑h ∘ f)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>e : G ≃L[𝕜] E<GOAL>ContDiffAt 𝕜 n (f ∘ ⇑e) (e.symm x) ↔ ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>e : G ≃L[𝕜] E<GOAL>ContDiffWithinAt 𝕜 n (f ∘ ⇑e) (?m.434150 ⁻¹' univ) (e.symm x) ↔ ContDiffWithinAt 𝕜 n f univ x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>e : G ≃L[𝕜] E<GOAL>Type ?u.434146
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>e : G ≃L[𝕜] E<GOAL>G → ?m.434149
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>(((κ + η).withDensity fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal) a) s = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : γ) in s, ↑(κ.rnDerivAux (κ + η) a b).toNNReal ∂(κ + η) a = (κ a) s
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>Measurable (Function.uncurry fun a x => ↑(κ.rnDerivAux (κ + η) a x).toNNReal)
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>inst✝¹ : IsFiniteKernel κ<VAR>inst✝ : IsFiniteKernel η<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<VAR>this : ∀ (b : ℝ), ↑b.toNNReal = ENNReal.ofReal b<GOAL>∫⁻ (b : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) ∂(κ + η) a = (κ a) s
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : CharZero K<VAR>α : Weight K (↥H) L<GOAL>↑(corootSpace ⇑α) = span K {coroot α}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<GOAL>Independent t ↔ ∀ (i : ι), Disjoint (t i) (sSup (t '' {j | j ≠ i}))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>ι' : Type u_4<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<VAR>hs : SetIndependent s<VAR>t : ι → α<VAR>ht : Independent t<GOAL>Independent t ↔ ∀ (i : ι), Disjoint (t i) (⨆ a ∈ {j | j ≠ i}, t a)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set (PrimeSpectrum R)<GOAL>(vanishingIdeal s).IsRadical
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set (PrimeSpectrum R)<GOAL>(vanishingIdeal s).radical.IsRadical
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedField R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>_i : FiniteDimensional R M<VAR>x₁ x₂ : Orientation R M ι<VAR>h : Fintype.card ι = finrank R M<VAR>e : Basis ι R M<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>orientation_neg_neg : ∀ (f : Basis ι R M), - -f.orientation = f.orientation<GOAL>x₁ = x₂ ∨ x₁ = -x₂
<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>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P Q : Cᵒᵖ ⥤ Type v₁<VAR>f : P ⟶ Q<VAR>X : C<VAR>p : yoneda.obj X ⟶ P<GOAL>yonedaEquiv (p ≫ presheafHom φ P ≫ whiskerLeft F.op (G.map f)) = yonedaEquiv (p ≫ f ≫ presheafHom φ Q)
<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>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P Q : Cᵒᵖ ⥤ Type v₁<VAR>f : P ⟶ Q<VAR>X : C<VAR>p : yoneda.obj X ⟶ P<GOAL>(G.map f).app (F.op.obj (Opposite.op X)) ((G.map p).app (Opposite.op (F.obj X)) ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X)))))) = (G.map f).app (Opposite.op (F.obj X)) ((G.map p).app (Opposite.op (F.obj X)) ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X))))))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : ↑((inhomogeneousCochains A).X 2)<VAR>y : G × G × G<GOAL>(A.ρ y.1) (x (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim))) - x (Fin.cons (y.1 * y.2.1) (Fin.cons y.2.2 finZeroElim)) + x (Fin.cons y.1 (Fin.cons (y.2.1 * y.2.2) finZeroElim)) - x (Fin.cons y.1 (Fin.cons y.2.1 finZeroElim)) = (A.ρ ((Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y) 0)) (x fun i => (Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y) i.succ) + ∑ j : Fin 3, (-1) ^ (↑j + 1) • x (j.contractNth (fun x x_1 => x * x_1) ((Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y)))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : ↑((inhomogeneousCochains A).X 2)<VAR>y : G × G × G<GOAL>(A.ρ y.1) (x (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim))) - x (Fin.cons (y.1 * y.2.1) (Fin.cons y.2.2 finZeroElim)) + x (Fin.cons y.1 (Fin.cons (y.2.1 * y.2.2) finZeroElim)) - x (Fin.cons y.1 (Fin.cons y.2.1 finZeroElim)) = (A.ρ ((Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y) 0)) (x fun i => (Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y) i.succ) + ((-1) ^ (↑0 + 1) • x (Fin.contractNth 0 (fun x x_1 => x * x_1) ((Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) + (-1) ^ (↑1 + 1) • x (Fin.contractNth 1 (fun x x_1 => x * x_1) ((Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) + (-1) ^ (↑2 + 1) • x (Fin.contractNth 2 (fun x x_1 => x * x_1) ((Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : ↑((inhomogeneousCochains A).X 2)<VAR>y : G × G × G<GOAL>(A.ρ y.1) (x (Fin.cons y.2.1 (Fin.cons y.2.2 finZeroElim))) + (-x (Fin.cons (y.1 * y.2.1) (Fin.cons y.2.2 finZeroElim)) + (x (Fin.cons y.1 (Fin.cons (y.2.1 * y.2.2) finZeroElim)) + -x (Fin.cons y.1 (Fin.cons y.2.1 finZeroElim)))) = (A.ρ ((Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y) 0)) (x fun i => (Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y) i.succ) + (-x (Fin.contractNth 0 (fun x x_1 => x * x_1) ((Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) + (x (Fin.contractNth 1 (fun x x_1 => x * x_1) ((Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y))) + -x (Fin.contractNth 2 (fun x x_1 => x * x_1) ((Equiv.piFinSucc 2 G).symm (Prod.map id (fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)) y)))))
<VAR>k : ℕ<GOAL>W k ≤ π / 2
<VAR>k : ℕ<GOAL>(π / 2)⁻¹ * W k ≤ 1
<VAR>k : ℕ<GOAL>∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k + 1) ≤ ∫ (x : ℝ) in 0 ..π, sin x ^ (2 * k)
<VAR>K : Type u_1<VAR>n : ℕ<VAR>g : GenContFract K<VAR>s : Stream'.Seq (Pair K)<VAR>inst✝ : DivisionRing K<VAR>terminatedAt_n : g.TerminatedAt n<GOAL>g.squashGCF n = g
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>deriv^[2] (fun x => x * log x) x = x⁻¹
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>deriv (deriv fun x => x * log x) x = x⁻¹
<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>∀ᶠ (y : ℝ) in 𝓝 x, deriv (fun x => x * log x) y = log y + 1
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : WeierstrassCurve R<VAR>inst✝ : NoZeroDivisors R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>(W.ΨSq n).leadingCoeff = ↑n ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>hab : a < b<GOAL>Ioo a b ∪ {a} = Ico a b
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ L₃ : C ⥤ D<VAR>R₁ R₂ R₃ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : L₂ ⟶ L₁<VAR>β : L₁ ⟶ L₂<VAR>βα : β ≫ α = 𝟙 L₁<GOAL>(conjugateEquiv adj₁ adj₂) α ≫ (conjugateEquiv adj₂ adj₁) β = 𝟙 R₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>f : α × β → σ<GOAL>Primrec₂ (Function.curry f) ↔ Primrec f
<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>inst✝⁶ : HasZeroMorphisms C<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁴ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝³ : F.PreservesZeroMorphisms<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : F.PreservesRightHomologyOf S<GOAL>(S.mapHomologyIso' F).hom = (S.mapHomologyIso F).hom
<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>inst✝⁶ : HasZeroMorphisms C<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁴ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝³ : F.PreservesZeroMorphisms<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : F.PreservesRightHomologyOf S<GOAL>((S.homologyData.right.map F).homologyIso ≪≫ F.mapIso S.homologyData.right.homologyIso.symm).hom = ((S.homologyData.left.map F).homologyIso ≪≫ F.mapIso S.homologyData.left.homologyIso.symm).hom
<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>inst✝⁶ : HasZeroMorphisms C<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁴ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝³ : F.PreservesZeroMorphisms<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : F.PreservesRightHomologyOf S<GOAL>(((S.map F).homologyData.iso.hom ≫ (rightHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ } (S.map F).rightHomologyData (S.map F).homologyData.right).inv) ≫ (rightHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ } (S.map F).rightHomologyData (S.homologyData.right.map F)).hom) ≫ F.map ((rightHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.rightHomologyData S.homologyData.right).inv ≫ (rightHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.rightHomologyData S.homologyData.right).hom ≫ S.homologyData.iso.inv) = ((leftHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ } (S.map F).leftHomologyData (S.map F).homologyData.left).inv ≫ (leftHomologyMapIso' { hom := 𝟙 (S.map F), inv := 𝟙 (S.map F), hom_inv_id := ⋯, inv_hom_id := ⋯ } (S.map F).leftHomologyData (S.homologyData.left.map F)).hom) ≫ F.map ((leftHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.leftHomologyData S.homologyData.left).inv ≫ (leftHomologyMapIso' { hom := 𝟙 S, inv := 𝟙 S, hom_inv_id := ⋯, inv_hom_id := ⋯ } S.leftHomologyData S.homologyData.left).hom)
<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>inst✝⁶ : HasZeroMorphisms C<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁴ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝³ : F.PreservesZeroMorphisms<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : F.PreservesRightHomologyOf S<GOAL>(S.map F).homologyData.iso.hom ≫ rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.right.map F) ≫ F.map S.homologyData.iso.inv = leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.left.map F)
<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>inst✝⁶ : HasZeroMorphisms C<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁴ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝³ : F.PreservesZeroMorphisms<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : F.PreservesRightHomologyOf S<VAR>γ : HomologyMapData (𝟙 (S.map F)) (S.map F).homologyData (S.homologyData.map F)<GOAL>(S.map F).homologyData.iso.hom ≫ rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.right.map F) ≫ F.map S.homologyData.iso.inv = leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.left.map F)