ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f : X → ↑F X<VAR>P : PFunctor.{u}<VAR>α : Type u_2<VAR>R : P.M → P.M → Prop<VAR>h : ∀ (x y : P.M), R x y → ∃ a f f', x.dest = ⟨a, f⟩ ∧ y.dest = ⟨a, f'⟩ ∧ ∀ (i : P.B a), R (f i) (f' i)<VAR>x y : P.M<VAR>h' : R x y<VAR>this : Inhabited P.A<GOAL>IsBisimulation R
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S<VAR>inst✝³ : Algebra R S<VAR>f : R[X]<VAR>T : Type u_1<VAR>inst✝² : CommRing T<VAR>inst✝¹ : Algebra R T<VAR>U : Type u_2<VAR>inst✝ : CommRing U<VAR>h : IsAdjoinRoot S f<VAR>h' : IsAdjoinRoot T f<VAR>i : R →+* U<VAR>x : U<VAR>hx : eval₂ i x f = 0<VAR>z : S<GOAL>(lift i x hx h') ((h.aequiv h') z) = (lift i x hx h) z
<VAR>G : Type u_1<VAR>X : Type u_2<VAR>inst✝ : SMul G X<VAR>B : Set X<VAR>hfB : IsFixedBlock G B<GOAL>IsBlock G B
<VAR>G : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : Archimedean G<VAR>H : AddSubgroup G<VAR>a : G<VAR>h₀ : 0 < a<VAR>hd : Disjoint (↑H) (Ioo 0 a)<GOAL>∃ b, H = closure {b}
<VAR>G : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : Archimedean G<VAR>a : G<VAR>h₀ : 0 < a<VAR>hd : Disjoint (↑⊥) (Ioo 0 a)<GOAL>∃ b, ⊥ = closure {b}
<VAR>G : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup G<VAR>inst✝ : Archimedean G<VAR>H : AddSubgroup G<VAR>a : G<VAR>h₀ : 0 < a<VAR>hd : Disjoint (↑H) (Ioo 0 a)<VAR>hbot : H ≠ ⊥<GOAL>∃ b, H = closure {b}
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>m n k : α<VAR>H : k ∣ m * n<GOAL>k ∣ m * gcd k n
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>m n k : α<VAR>H : k ∣ n * m<GOAL>k ∣ gcd k n * m
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f✝ g f : NormedAddGroupHom V₁ V₂<GOAL>‖-f‖ = ‖f‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α) in ∅, f x ∂μ = 0
<VAR>s : Finset ℕ<VAR>m : ℕ<GOAL>m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
<VAR>s : Finset ℕ<VAR>m p : ℕ<VAR>hp₁ : 1 + s.sup id ≤ p<VAR>hp₂ : Prime p<GOAL>m ∈ factoredNumbers s ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
<VAR>s : Finset ℕ<VAR>m p : ℕ<VAR>hp₁ : 1 + s.sup id ≤ p<VAR>hp₂ : Prime p<GOAL>(m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s) ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
<VAR>s : Finset ℕ<VAR>m p : ℕ<VAR>hp₁ : 1 + s.sup id ≤ p<VAR>hp₂ : Prime p<VAR>H : ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s<VAR>h : m = 0<GOAL>p < p
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<GOAL>Tendsto (fun x => r * f x) l atBot ↔ Tendsto f l atBot
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x<GOAL>map (Embedding.subtype p) (Iic a) = Iic ↑a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>a : Subtype p<VAR>hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x<GOAL>map (Embedding.subtype p) (Finset.subtype p (Iic ↑a)) = Iic ↑a
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<GOAL>(π.restrict J).iUnion = ↑J ∩ π.iUnion
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>hg : ConcaveOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>h0 : μ t ≠ 0<VAR>ht : μ t ≠ ⊤<VAR>hfs : ∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s<VAR>hfi : IntegrableOn f t μ<VAR>hgi : IntegrableOn (g ∘ f) t μ<GOAL>(⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ p.2 ≤ g p.1}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hIN : N ≤ I • N<VAR>hIjac : I ≤ J.jacobson<GOAL>N = J • N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hIN : N ≤ I • N<VAR>hIjac : I ≤ J.jacobson<GOAL>N ≤ J • N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hIN : N ≤ I • N<VAR>hIjac : I ≤ J.jacobson<VAR>n : M<VAR>hn : n ∈ N<GOAL>n ∈ J • N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hIN : N ≤ I • N<VAR>hIjac : I ≤ J.jacobson<VAR>n : M<VAR>hn : n ∈ N<VAR>r : R<VAR>hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0<GOAL>n ∈ J • N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hIN : N ≤ I • N<VAR>hIjac : I ≤ J.jacobson<VAR>n : M<VAR>hn : n ∈ N<VAR>r : R<VAR>hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0<VAR>s : R<VAR>hs : s * r - 1 ∈ J<GOAL>n ∈ J • N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hIN : N ≤ I • N<VAR>hIjac : I ≤ J.jacobson<VAR>n : M<VAR>hn : n ∈ N<VAR>r : R<VAR>hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0<VAR>s : R<VAR>hs : s * r - 1 ∈ J<VAR>this : n = -(s * r - 1) • n<GOAL>n ∈ J • N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I J : Ideal R<VAR>N : Submodule R M<VAR>hN : N.FG<VAR>hIN : N ≤ I • N<VAR>hIjac : I ≤ J.jacobson<VAR>n : M<VAR>hn : n ∈ N<VAR>r : R<VAR>hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0<VAR>s : R<VAR>hs : s * r - 1 ∈ J<VAR>this : n = -(s * r - 1) • n<GOAL>-(s * r - 1) • n ∈ J • N
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Group N<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* MulAut N<VAR>f₁ : N →* H<VAR>f₂ : G →* H<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁<VAR>f g : N ⋊[φ] G →* H<VAR>hl : f.comp inl = g.comp inl<VAR>hr : f.comp inr = g.comp inr<GOAL>f = g
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Group N<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* MulAut N<VAR>f₁ : N →* H<VAR>f₂ : G →* H<VAR>h : ∀ (g : G), f₁.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (f₂ g))).comp f₁<VAR>f g : N ⋊[φ] G →* H<VAR>hl : f.comp inl = g.comp inl<VAR>hr : f.comp inr = g.comp inr<GOAL>lift (f.comp inl) (f.comp inr) ⋯ = lift (g.comp inl) (g.comp inr) ⋯
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>x : X<GOAL>(𝓝 x).ker = {x}
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>x : R<GOAL>x ∈ I.leadingCoeff ↔ ∃ p ∈ I, p.leadingCoeff = x
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>x : R<GOAL>(∃ i, x ∈ I.leadingCoeffNth i) ↔ ∃ p ∈ I, p.leadingCoeff = x
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>x : R<GOAL>Directed (fun x x_1 => x ≤ x_1) fun n => I.leadingCoeffNth n
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Semiring S<VAR>I : Ideal R[X]<VAR>x : R<VAR>i j : ℕ<GOAL>∃ z, (fun x x_1 => x ≤ x_1) ((fun n => I.leadingCoeffNth n) i) ((fun n => I.leadingCoeffNth n) z) ∧ (fun x x_1 => x ≤ x_1) ((fun n => I.leadingCoeffNth n) j) ((fun n => I.leadingCoeffNth n) z)
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>r : R<GOAL>r ∈ N.annihilator ↔ ∀ n ∈ N, r • n = 0
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>r : R<GOAL>(∀ (a : M) (b : a ∈ N), ↑(r • ⟨a, b⟩) = ↑0) ↔ ∀ n ∈ N, r • n = 0
<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>inst✝¹ : FormallyUnramified R A<VAR>C : Type u<VAR>inst✝ : CommRing C<VAR>f : B →+* C<VAR>hf : IsNilpotent (RingHom.ker f)<VAR>g₁ g₂ : A →ₐ[R] B<VAR>h : f.comp ↑g₁ = f.comp ↑g₂<VAR>x : A<GOAL>((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₁) x = ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₂) x
<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>inst✝¹ : FormallyUnramified R A<VAR>C : Type u<VAR>inst✝ : CommRing C<VAR>f : B →+* C<VAR>hf : IsNilpotent (RingHom.ker f)<VAR>g₁ g₂ : A →ₐ[R] B<VAR>h : f.comp ↑g₁ = f.comp ↑g₂<VAR>x : A<VAR>this : (f.comp ↑g₁) x = (f.comp ↑g₂) x<GOAL>((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₁) x = ((Ideal.Quotient.mkₐ R (RingHom.ker f)).comp g₂) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<GOAL>𝓝[≠] a ⊔ pure a = 𝓝 a
<VAR>R : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>S : Subalgebra R A<GOAL>comap f (map f S) = S ⊔ adjoin R (⇑f ⁻¹' {0})
<VAR>R : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>S : Subalgebra R A<GOAL>comap f (map f S) ≤ S ⊔ adjoin R (⇑f ⁻¹' {0})
<VAR>R : Type uR<VAR>S✝ : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>S : Subalgebra R A<GOAL>S ⊔ adjoin R (⇑f ⁻¹' {0}) ≤ comap f (map f S)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x : E<VAR>a : ℝ<VAR>h : s ⊆ 0<GOAL>gauge s = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>t : Set E<VAR>x : E<VAR>a : ℝ<VAR>h : ∅ ⊆ 0<GOAL>gauge ∅ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>t : Set E<VAR>x : E<VAR>a : ℝ<VAR>h : {0} ⊆ 0<GOAL>gauge {0} = 0
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ 0<VAR>ha' : a ≠ ⊤<VAR>h : b = c / a<GOAL>a * b = c
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ha : a ≠ 0<VAR>ha' : a ≠ ⊤<VAR>h : a * b = c<GOAL>b = c / a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>a : α<VAR>l : List α<VAR>hl : l.length = n<GOAL>Tendsto (fun p => Vector.insertNth p.1 i p.2) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 (Vector.insertNth a i ⟨l, hl⟩))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>a : α<VAR>l : List α<VAR>hl : l.length = n<GOAL>Tendsto (fun x => ↑(Vector.insertNth x.1 i x.2)) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 ↑⟨insertNth (↑i) a ↑⟨l, hl⟩, ⋯⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>a : α<VAR>l : List α<VAR>hl : l.length = n<GOAL>Tendsto (fun x => insertNth (↑i) x.1 ↑x.2) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 (insertNth (↑i) a l))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>((PreservesCoequalizer.iso (tensorRight S.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)).inv ≫ colimMap (parallelPairHom (P.actRight ▷ S.X ▷ S.X) (((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ▷ S.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ((α_ (P.X ⊗ S.X) S.X S.X).hom ≫ (α_ P.X S.X (S.X ⊗ S.X)).hom ≫ P.X ◁ S.X ◁ S.mul ≫ (α_ P.X S.X S.X).inv) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ⋯ ⋯)) ≫ coequalizer.desc P.actRight ⋯ = coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(tensorRight S.X).map (coequalizer.π (P.actRight ▷ { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X) ((α_ P.X S.X { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫ P.X ◁ { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actLeft)) ≫ ((PreservesCoequalizer.iso (tensorRight S.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)).inv ≫ colimMap (parallelPairHom (P.actRight ▷ S.X ▷ S.X) (((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ▷ S.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ((α_ (P.X ⊗ S.X) S.X S.X).hom ≫ (α_ P.X S.X (S.X ⊗ S.X)).hom ≫ P.X ◁ S.X ◁ S.mul ≫ (α_ P.X S.X S.X).inv) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ⋯ ⋯)) ≫ coequalizer.desc P.actRight ⋯ = (tensorRight S.X).map (coequalizer.π (P.actRight ▷ { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X) ((α_ P.X S.X { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.X).hom ≫ P.X ◁ { X := S.X, actLeft := S.mul, one_actLeft := ⋯, left_assoc := ⋯, actRight := S.mul, actRight_one := ⋯, right_assoc := ⋯, middle_assoc := ⋯ }.actLeft)) ≫ coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ▷ S.X ≫ ((PreservesCoequalizer.iso (tensorRight S.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)).inv ≫ colimMap (parallelPairHom (P.actRight ▷ S.X ▷ S.X) (((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ▷ S.X) (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ((α_ (P.X ⊗ S.X) S.X S.X).hom ≫ (α_ P.X S.X (S.X ⊗ S.X)).hom ≫ P.X ◁ S.X ◁ S.mul ≫ (α_ P.X S.X S.X).inv) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ⋯ ⋯)) ≫ coequalizer.desc P.actRight ⋯ = coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ▷ S.X ≫ coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ≫ P.actRight = coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ▷ S.X ≫ coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(α_ P.X S.X S.X).hom ≫ (α_ P.X S.X S.X).inv ≫ P.actRight ▷ S.X ≫ P.actRight = coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul) ▷ S.X ≫ coequalizer.desc P.actRight ⋯ ▷ S.X ≫ P.actRight
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : MonoidalCategory C<VAR>A B : Mon_ C<VAR>M : Bimod A B<VAR>inst✝² : HasCoequalizers C<VAR>R S : Mon_ C<VAR>P : Bimod R S<VAR>inst✝¹ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)<VAR>inst✝ : (X : C) → PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)<GOAL>(α_ P.X S.X S.X).hom ≫ (α_ P.X S.X S.X).inv ≫ P.actRight ▷ S.X ≫ P.actRight = P.actRight ▷ S.X ≫ P.actRight
<VAR>x✝ y x : ℝ<VAR>h : x ≤ 0<GOAL>0 < rexp x
<VAR>x✝ y x : ℝ<VAR>h : x ≤ 0<GOAL>0 < (rexp (-x))⁻¹
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : CommRing T<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁴ : Fintype ι<VAR>F : Type u_6<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K S<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : FiniteDimensional K L<VAR>x : L<VAR>hF : Splits (algebraMap K F) (minpoly K x)<GOAL>(algebraMap K F) ((Algebra.trace K L) x) = finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>↑(hC.diffFinset₀ hs hI) ⊆ C
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeInf β<VAR>s✝ t✝ : Set α<VAR>a✝ b : α<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ lowerBounds s<VAR>t : Finset α<VAR>ht : t.Nonempty<VAR>hts : ↑t ⊆ s<GOAL>a ≤ t.inf' ht id
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r : ℝ<VAR>x : E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₁ : 0 < r₁<GOAL>Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x : E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₁ : 0 < r₁<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr : r₂ < r * r₁<GOAL>Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a✝ : 𝕜<VAR>r✝ : ℝ<VAR>x✝ : E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₁ : 0 < r₁<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr : r₂ < r * r₁<VAR>a : 𝕜<VAR>ha : r ≤ ‖a‖<VAR>x : E<VAR>hx : x ∈ p.ball 0 r₂<GOAL>x ∈ a • p.ball 0 r₁
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a✝ : 𝕜<VAR>r✝ : ℝ<VAR>x✝ : E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₁ : 0 < r₁<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr : r₂ < r * r₁<VAR>a : 𝕜<VAR>ha : r ≤ ‖a‖<VAR>x : E<VAR>hx : x ∈ p.ball 0 r₂<GOAL>p x < ‖a‖ * r₁
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a✝ : 𝕜<VAR>r✝ : ℝ<VAR>x✝ : E<VAR>p : Seminorm 𝕜 E<VAR>r₁ r₂ : ℝ<VAR>hr₁ : 0 < r₁<VAR>r : ℝ<VAR>hr₀ : 0 < r<VAR>hr : r₂ < r * r₁<VAR>a : 𝕜<VAR>ha : r ≤ ‖a‖<VAR>x : E<VAR>hx : p x < r₂<GOAL>p x < ‖a‖ * r₁
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : GroupWithZero α<VAR>s✝ t s : Finset α<GOAL>0 / s ⊆ 0
<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>h : Basis ι R M<GOAL>finrank R M = Nat.card ι
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : Semiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>s : Set X<VAR>f : C(X, R)<GOAL>f ∈ idealOfSet R s ↔ ∀ ⦃x : X⦄, x ∈ sᶜ → f x = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>hε : 0 < ε<GOAL>∃ n, 1 / (↑n + 1) < ε
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>hε : 0 < ε<VAR>n : ℕ<VAR>hn : 1 / ε < ↑n<GOAL>∃ n, 1 / (↑n + 1) < ε
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>hε : 0 < ε<VAR>n : ℕ<VAR>hn : 1 / ε < ↑n<GOAL>1 / (↑n + 1) < ε
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>hε : 0 < ε<VAR>n : ℕ<VAR>hn : 1 / ε < ↑n<GOAL>1 / ε < ↑n + 1
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : LinearOrderedSemifield α<VAR>inst✝¹ : Archimedean α<VAR>inst✝ : ExistsAddOfLE α<VAR>x y ε : α<VAR>hε : 0 < ε<VAR>n : ℕ<VAR>hn : 1 / ε < ↑n<GOAL>0 < ↑n + 1
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<GOAL>inverse W D ⋙ functor W D = 𝟭 (W.FunctorsInverting D)
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<GOAL>∀ (X : W.FunctorsInverting D), (inverse W D ⋙ functor W D).obj X = (𝟭 (W.FunctorsInverting D)).obj X
<VAR>C : Type uC<VAR>inst✝¹ : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<GOAL>∀ (X Y : W.FunctorsInverting D) (f : X ⟶ Y), (inverse W D ⋙ functor W D).map f = eqToHom ⋯ ≫ (𝟭 (W.FunctorsInverting D)).map f ≫ eqToHom ⋯
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>D : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>G : Type u_6<VAR>V : Type u_7<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup D<VAR>inst✝⁵ : NormedSpace ℝ D<VAR>inst✝⁴ : MeasurableSpace D<VAR>inst✝³ : BorelSpace D<VAR>inst✝² : SecondCountableTopology D<VAR>inst✝¹ : FiniteDimensional ℝ D<VAR>μ : Measure D<VAR>inst✝ : μ.HasTemperateGrowth<VAR>f : D → E<VAR>C₁ C₂ : ℝ<VAR>k : ℕ<VAR>hf : ∀ (x : D), ‖f x‖ ≤ C₁<VAR>h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂<VAR>h''f : AEStronglyMeasurable f μ<GOAL>Integrable (fun x => ‖x‖ ^ k * ‖f x‖) μ