ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>E : EllipticCurve R<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>j : F<VAR>inst✝ : DecidableEq F<VAR>h3 : 3 = 0<GOAL>ofJ 1728 = ofJ1728 F
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>N : Submodule R M<VAR>h : IsNoetherian R M<GOAL>IsNoetherian R ↥N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>N : Submodule R M<VAR>h : WellFounded fun x x_1 => x > x_1<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>κ : Kernel α β<VAR>hf : MeasurableEmbedding f<VAR>hκ : ∀ (a : α), (κ a) (Set.range f) = 1<VAR>a : α<GOAL>((κ.comapRight hf) a) Set.univ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>κ : Kernel α β<VAR>hf : MeasurableEmbedding f<VAR>hκ : ∀ (a : α), (κ a) (Set.range f) = 1<VAR>a : α<GOAL>(κ a) (f '' Set.univ) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : γ → β<VAR>κ : Kernel α β<VAR>hf : MeasurableEmbedding f<VAR>hκ : ∀ (a : α), (κ a) (Set.range f) = 1<VAR>a : α<GOAL>(κ a) (Set.range f) = 1
<VAR>R : Type u<VAR>S : Type v<VAR>S' : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : CommSemiring S'<VAR>inst✝² : Algebra S' R<VAR>inst✝¹ : Algebra S S'<VAR>inst✝ : IsScalarTower S S' R<VAR>I : Ideal R<VAR>x : ↥I<GOAL>x ∈ LinearMap.ker I.toCotangent ↔ ↑x ∈ I ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>S' : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S R<VAR>inst✝³ : CommSemiring S'<VAR>inst✝² : Algebra S' R<VAR>inst✝¹ : Algebra S S'<VAR>inst✝ : IsScalarTower S S' R<VAR>I : Ideal R<VAR>x : ↥I<GOAL>x ∈ LinearMap.ker I.toCotangent ↔ ↑x ∈ Submodule.map (Submodule.subtype I) (LinearMap.ker I.toCotangent)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p✝ q p : R[X]<VAR>hp0 : ¬p = 0<GOAL>Multiset.card p.roots ≤ p.natDegree
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M₁<VAR>inst✝⁸ : Module R M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : AddCommMonoid N₂<VAR>inst✝⁴ : Module R N₂<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Fintype m<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] N₂<VAR>i : n<VAR>j : m<GOAL>(toMatrix₂ b₁ b₂) B i j = (B (b₁ i)) (b₂ j)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<GOAL>a ^ n ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd n<GOAL>n ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring R<VAR>a b : R<VAR>m : ℕ<VAR>inst✝ : ExistsAddOfLE R<VAR>hn : Odd 0<GOAL>False
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : DifferentiableAt 𝕜' h₂ (h x)<VAR>hh : DifferentiableAt 𝕜 h x<VAR>hy : y = h x<GOAL>deriv (h₂ ∘ h) x = deriv h₂ (h x) * deriv h x
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<GOAL>minkowskiBound K I < ⊤
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<GOAL>volume (fundamentalDomain (fractionalIdealLatticeBasis K I)) ≠ ⊤
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<GOAL>2 ^ finrank ℝ (({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)) ≠ ⊤
<VAR>ι✝ : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>π : ι → Type u<VAR>f : (i : ι) → π i<VAR>inst✝¹ : (i : ι) → PartialOrder (π i)<VAR>inst✝ : (i : ι) → OrderBot (π i)<GOAL>IsAtom f ↔ ∃ i, IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>x : G<GOAL>fderiv 𝕜 (⇑iso ∘ f) x = (↑iso).comp (fderiv 𝕜 f x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>x : G<GOAL>fderivWithin 𝕜 (⇑iso ∘ f) univ x = (↑iso).comp (fderivWithin 𝕜 f univ x)
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H : G.Subgraph<GOAL>H.Connected ↔ H.Preconnected ∧ H.verts.Nonempty
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>f g✝ : α → β✝<VAR>μ ν : Measure α<VAR>β : Type u_7<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>x : α<VAR>g : α → β<VAR>g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))<VAR>this : Nonempty α<GOAL>AEMeasurable g (μ.restrict (Ioi x))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>f g✝ : α → β✝<VAR>μ ν : Measure α<VAR>β : Type u_7<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>x : α<VAR>g : α → β<VAR>g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))<VAR>this : Nonempty α<VAR>u : ℕ → α<VAR>hu_tendsto : Tendsto u atTop atTop<GOAL>AEMeasurable g (μ.restrict (Ioi x))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>f g✝ : α → β✝<VAR>μ ν : Measure α<VAR>β : Type u_7<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>x : α<VAR>g : α → β<VAR>g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))<VAR>this : Nonempty α<VAR>u : ℕ → α<VAR>hu_tendsto : Tendsto u atTop atTop<VAR>Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)<GOAL>AEMeasurable g (μ.restrict (Ioi x))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>f g✝ : α → β✝<VAR>μ ν : Measure α<VAR>β : Type u_7<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>x : α<VAR>g : α → β<VAR>g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))<VAR>this : Nonempty α<VAR>u : ℕ → α<VAR>hu_tendsto : Tendsto u atTop atTop<VAR>Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)<GOAL>∀ (i : ℕ), AEMeasurable g (μ.restrict (Ioc x (u i)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>f g✝ : α → β✝<VAR>μ ν : Measure α<VAR>β : Type u_7<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>x : α<VAR>g : α → β<VAR>g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))<VAR>this : Nonempty α<VAR>u : ℕ → α<VAR>hu_tendsto : Tendsto u atTop atTop<VAR>Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)<VAR>n : ℕ<GOAL>AEMeasurable g (μ.restrict (Ioc x (u n)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>f g✝ : α → β✝<VAR>μ ν : Measure α<VAR>β : Type u_7<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>x : α<VAR>g : α → β<VAR>g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))<VAR>this : Nonempty α<VAR>u : ℕ → α<VAR>hu_tendsto : Tendsto u atTop atTop<VAR>Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)<VAR>n : ℕ<VAR>h : x < u n<GOAL>AEMeasurable g (μ.restrict (Ioc x (u n)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>f g✝ : α → β✝<VAR>μ ν : Measure α<VAR>β : Type u_7<VAR>mβ : MeasurableSpace β<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : atTop.IsCountablyGenerated<VAR>x : α<VAR>g : α → β<VAR>g_meas : ∀ t > x, AEMeasurable g (μ.restrict (Ioc x t))<VAR>this : Nonempty α<VAR>u : ℕ → α<VAR>hu_tendsto : Tendsto u atTop atTop<VAR>Ioi_eq_iUnion : Ioi x = ⋃ n, Ioc x (u n)<VAR>n : ℕ<VAR>h : u n ≤ x<GOAL>AEMeasurable g (μ.restrict (Ioc x (u n)))
<VAR>V : Type<VAR>G : SimpleGraph V<VAR>e : ↑G.end<VAR>K : (Finset V)ᵒᵖ<GOAL>(ComponentCompl.supp (↑e K)).Infinite
<VAR>V : Type<VAR>G : SimpleGraph V<VAR>e : ↑G.end<VAR>K : (Finset V)ᵒᵖ<VAR>L : Finset V<VAR>h : Opposite.unop K ⊆ L<GOAL>∃ D, ComponentCompl.hom h D = ↑e K
<VAR>V : Type<VAR>G : SimpleGraph V<VAR>e : ↑G.end<VAR>K : (Finset V)ᵒᵖ<VAR>L : Finset V<VAR>h : Opposite.unop K ⊆ Opposite.unop (Opposite.op L)<GOAL>∃ D, ComponentCompl.hom h D = ↑e K
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>h : s.Countable<VAR>default : α<VAR>h_mem : default ∈ s<VAR>n : ℕ<GOAL>enumerateCountable h default n ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>s : Set α<VAR>h : s.Countable<VAR>default : α<VAR>h_mem : default ∈ s<VAR>n : ℕ<GOAL>enumerateCountable h default n ∈ range (enumerateCountable h default)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>f : WithLp p (α × β)<GOAL>edist f f = 0
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>f : WithLp 0 (α × β)<GOAL>edist f f = 0
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>f : WithLp ⊤ (α × β)<GOAL>edist f f = 0
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>f : WithLp p (α × β)<VAR>h : 0 < p.toReal<GOAL>edist f f = 0
<VAR>n₁ n₂ : Int<VAR>d₁ d₂ : Nat<VAR>z₁ : d₁ ≠ 0<VAR>z₂ : d₂ ≠ 0<GOAL>mkRat n₁ d₁ + mkRat n₂ d₂ = mkRat (n₁ * ↑d₂ + n₂ * ↑d₁) (d₁ * d₂)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m' mΩ : MeasurableSpace Ω<VAR>inst✝² : StandardBorelSpace Ω<VAR>inst✝¹ : Nonempty Ω<VAR>hm' : m' ≤ mΩ<VAR>s : ι → Set Ω<VAR>hs : ∀ (i : ι), MeasurableSet (s i)<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<GOAL>iCondIndepSet m' hm' s μ ↔ ∀ (S : Finset ι), μ[(⋂ i ∈ S, s i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ S, μ[(s i).indicator fun ω => 1|m']
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>f : α → α<VAR>hs : s.Finite<VAR>hm : MapsTo f s s<GOAL>SurjOn f s s ↔ BijOn f s s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>f : α → α<VAR>hs : s.Finite<VAR>hm : MapsTo f s s<VAR>h : SurjOn f s s<GOAL>InjOn f s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>f : α → α<VAR>hs : s.Finite<VAR>hm : MapsTo f s s<VAR>h : SurjOn f s s<VAR>this : Finite ↑s<GOAL>InjOn f s
<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>d : D<GOAL>(𝟙 (R₁.obj d) ≫ (adj₂.unit.app (R₁.obj d) ≫ R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫ 𝟙 (R₂.obj d)) ≫ 𝟙 (R₂.obj d) ≫ (adj₃.unit.app (R₂.obj d) ≫ R₃.map (𝟙 (L₃.obj (R₂.obj d)) ≫ β.app (R₂.obj d) ≫ 𝟙 (L₂.obj (R₂.obj d))) ≫ R₃.map (adj₂.counit.app d)) ≫ 𝟙 (R₃.obj d) = 𝟙 (R₁.obj d) ≫ (adj₃.unit.app (R₁.obj d) ≫ R₃.map (𝟙 (L₃.obj (R₁.obj d)) ≫ (β.app (R₁.obj d) ≫ α.app (R₁.obj d)) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₃.map (adj₁.counit.app d)) ≫ 𝟙 (R₃.obj d)
<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>d : D<VAR>vcomp : (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) = rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))<GOAL>(𝟙 (R₁.obj d) ≫ (adj₂.unit.app (R₁.obj d) ≫ R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫ 𝟙 (R₂.obj d)) ≫ 𝟙 (R₂.obj d) ≫ (adj₃.unit.app (R₂.obj d) ≫ R₃.map (𝟙 (L₃.obj (R₂.obj d)) ≫ β.app (R₂.obj d) ≫ 𝟙 (L₂.obj (R₂.obj d))) ≫ R₃.map (adj₂.counit.app d)) ≫ 𝟙 (R₃.obj d) = 𝟙 (R₁.obj d) ≫ (adj₃.unit.app (R₁.obj d) ≫ R₃.map (𝟙 (L₃.obj (R₁.obj d)) ≫ (β.app (R₁.obj d) ≫ α.app (R₁.obj d)) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₃.map (adj₁.counit.app d)) ≫ 𝟙 (R₃.obj d)
<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>d : D<VAR>vcomp : (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) = rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))<VAR>vcompd : ((mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))).app d = (rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))).app d<GOAL>(𝟙 (R₁.obj d) ≫ (adj₂.unit.app (R₁.obj d) ≫ R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫ 𝟙 (R₂.obj d)) ≫ 𝟙 (R₂.obj d) ≫ (adj₃.unit.app (R₂.obj d) ≫ R₃.map (𝟙 (L₃.obj (R₂.obj d)) ≫ β.app (R₂.obj d) ≫ 𝟙 (L₂.obj (R₂.obj d))) ≫ R₃.map (adj₂.counit.app d)) ≫ 𝟙 (R₃.obj d) = 𝟙 (R₁.obj d) ≫ (adj₃.unit.app (R₁.obj d) ≫ R₃.map (𝟙 (L₃.obj (R₁.obj d)) ≫ (β.app (R₁.obj d) ≫ α.app (R₁.obj d)) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₃.map (adj₁.counit.app d)) ≫ 𝟙 (R₃.obj d)
<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>d : D<VAR>vcomp : (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) = rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))<VAR>vcompd : adj₃.unit.app (R₁.obj d) ≫ R₃.map (β.app (R₁.obj d)) ≫ R₃.map (α.app (R₁.obj d)) ≫ R₃.map (adj₁.counit.app d) = adj₂.unit.app (R₁.obj d) ≫ R₂.map (α.app (R₁.obj d)) ≫ R₂.map (adj₁.counit.app d) ≫ adj₃.unit.app (R₂.obj d) ≫ R₃.map (β.app (R₂.obj d)) ≫ R₃.map (adj₂.counit.app d)<GOAL>(𝟙 (R₁.obj d) ≫ (adj₂.unit.app (R₁.obj d) ≫ R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫ 𝟙 (R₂.obj d)) ≫ 𝟙 (R₂.obj d) ≫ (adj₃.unit.app (R₂.obj d) ≫ R₃.map (𝟙 (L₃.obj (R₂.obj d)) ≫ β.app (R₂.obj d) ≫ 𝟙 (L₂.obj (R₂.obj d))) ≫ R₃.map (adj₂.counit.app d)) ≫ 𝟙 (R₃.obj d) = 𝟙 (R₁.obj d) ≫ (adj₃.unit.app (R₁.obj d) ≫ R₃.map (𝟙 (L₃.obj (R₁.obj d)) ≫ (β.app (R₁.obj d) ≫ α.app (R₁.obj d)) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₃.map (adj₁.counit.app d)) ≫ 𝟙 (R₃.obj d)
<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>d : D<VAR>vcomp : (mateEquiv adj₁ adj₃) (leftAdjointSquare.vcomp (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)) = rightAdjointSquare.vcomp ((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)) ((mateEquiv adj₂ adj₃) (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv))<VAR>vcompd : adj₃.unit.app (R₁.obj d) ≫ R₃.map (β.app (R₁.obj d)) ≫ R₃.map (α.app (R₁.obj d)) ≫ R₃.map (adj₁.counit.app d) = adj₂.unit.app (R₁.obj d) ≫ R₂.map (α.app (R₁.obj d)) ≫ R₂.map (adj₁.counit.app d) ≫ adj₃.unit.app (R₂.obj d) ≫ R₃.map (β.app (R₂.obj d)) ≫ R₃.map (adj₂.counit.app d)<GOAL>adj₂.unit.app (R₁.obj d) ≫ R₂.map (α.app (R₁.obj d)) ≫ R₂.map (adj₁.counit.app d) ≫ adj₃.unit.app (R₂.obj d) ≫ R₃.map (β.app (R₂.obj d)) ≫ R₃.map (adj₂.counit.app d) = adj₃.unit.app (R₁.obj d) ≫ R₃.map (β.app (R₁.obj d)) ≫ R₃.map (α.app (R₁.obj d)) ≫ R₃.map (adj₁.counit.app d)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m✝ n : ℕ∞<VAR>p✝ : E → FormalMultilinearSeries 𝕜 E F<VAR>h : ContDiffWithinAt 𝕜 n f s x<VAR>t : Set E<VAR>hst : s ∈ 𝓝[t] x<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>H : HasFTaylorSeriesUpToOn (↑m) f p u<GOAL>∃ u ∈ 𝓝[insert x t] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a = ⊤<GOAL>(a + b).toReal ≤ a.toReal + b.toReal
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : ¬a = ⊤<VAR>hb : b = ⊤<GOAL>(a + b).toReal ≤ a.toReal + b.toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : BoundedOrder β<VAR>x y : α × β<GOAL>IsCompl x y ↔ IsCompl x.1 y.1 ∧ IsCompl x.2 y.2
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hp : 1 ≤ p<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 = p<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q✝ : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>q : ℝ := p / (p - 1)<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q✝ : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>q : ℝ := p / (p - 1)<VAR>hpq : p.IsConjExponent q<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q✝ : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>q : ℝ := p / (p - 1)<VAR>hpq : p.IsConjExponent q<VAR>hp₁ : 1 / p * p = 1<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0∞<VAR>p q✝ : ℝ<VAR>hp✝ : 1 ≤ p<VAR>hp : 1 < p<VAR>q : ℝ := p / (p - 1)<VAR>hpq : p.IsConjExponent q<VAR>hp₁ : 1 / p * p = 1<VAR>hq : 1 / q * p = p - 1<GOAL>(∑ i ∈ s, f i) ^ p ≤ ↑s.card ^ (p - 1) * ∑ i ∈ s, f i ^ p
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>n : ℕ<GOAL>⌈a - ↑n⌉ = ⌈a⌉ - ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<VAR>n : ℕ<GOAL>⌈a - ↑n⌉ = ⌈a - ↑↑n⌉
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁴ : Primcodable α<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Primcodable γ<VAR>inst✝¹ : Primcodable δ<VAR>inst✝ : Primcodable σ<VAR>f : α → β → Option σ<VAR>h : Primrec₂ fun a n => (decode n).bind (f a)<GOAL>Primrec₂ f
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasBinaryCoproducts C<VAR>A : C<VAR>X✝ Y✝ : Over A<VAR>k : X✝ ⟶ Y✝<VAR>g : Over A<GOAL>coprod.map k.left (𝟙 g.left) ≫ coprod.desc Y✝.hom g.hom = coprod.desc X✝.hom g.hom
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J : FractionalIdeal S P<GOAL>I * J = ⟨↑I * ↑J, ⋯⟩
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝ : Epi f<VAR>h : Y ⟶ Y<GOAL>f ≫ h = f ↔ h = 𝟙 Y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝ : Epi f<VAR>h : Y ⟶ Y<GOAL>f = f ≫ 𝟙 Y
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>B : BilinMap R M N<VAR>x y : M<GOAL>polar (⇑B.toQuadraticMap) x y = (B x) y + (B y) 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>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>this : Preadditive D := preadditive L W<GOAL>∀ {X Y : C} {f g : X ⟶ Y}, L.map (f + g) = L.map f + L.map g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>a ⇔ a = ⊤
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>H : Type u_2<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type u_3<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>γ γ' : ℝ → M<VAR>v : (x : M) → TangentSpace I x<VAR>s s' : Set ℝ<VAR>t₀ : ℝ<VAR>hγ : IsIntegralCurve γ v<VAR>dt : ℝ<GOAL>IsIntegralCurve (γ ∘ fun x => x + dt) v