ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>inst✝³ : Algebra R Rₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : Algebra S Sₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>p : Rₘ[X]<VAR>hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range<VAR>n : ℕ<GOAL>(p.scaleRoots ((algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff))).coeff n ∈ Set.range ⇑(algebraMap R Rₘ)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>Rₘ : Type u_4<VAR>Sₘ : Type u_5<VAR>inst✝⁵ : CommRing Rₘ<VAR>inst✝⁴ : CommRing Sₘ<VAR>inst✝³ : Algebra R Rₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : Algebra S Sₘ<VAR>inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ<VAR>p : Rₘ[X]<VAR>hp : p.leadingCoeff ∈ (algebraMap R Rₘ).range<VAR>n : ℕ<GOAL>p.coeff n * (algebraMap R Rₘ) ↑(commonDenom M p.support p.coeff) ^ (p.natDegree - n) ∈ Set.range ⇑(algebraMap R Rₘ)
<VAR>d x y a b : ℕ<VAR>hu : x % d = 0<VAR>hv : y % d = 0<VAR>h : x * a = y * b + d<GOAL>x.gcd y = d
<VAR>d x y a b : ℕ<VAR>hu : x % d = 0<VAR>hv : y % d = 0<VAR>h : x * a = y * b + d<GOAL>(↑x).gcd ↑y = d
<VAR>d x y a b : ℕ<VAR>hu : x % d = 0<VAR>hv : y % d = 0<VAR>h : x * a = y * b + d<GOAL>↑x * ↑a + ↑y * -↑b = ↑d
<VAR>d x y a b : ℕ<VAR>hu : x % d = 0<VAR>hv : y % d = 0<VAR>h : x * a = y * b + d<GOAL>↑x * ↑a = ↑y * ↑b + ↑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>y : E<GOAL>ContDiffWithinAt 𝕜 n f (insert y s) x ↔ ContDiffWithinAt 𝕜 n f s x
<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>y : E<VAR>h : x ≠ y<GOAL>ContDiffWithinAt 𝕜 n f (insert y s) x ↔ ContDiffWithinAt 𝕜 n f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>r : ℝ≥0∞<GOAL>∫⁻ (x : α) in {x | f x = r}, f x ∂μ = r * μ {x | f x = r}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>r : ℝ≥0∞<VAR>this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r<GOAL>∫⁻ (x : α) in {x | f x = r}, f x ∂μ = r * μ {x | f x = r}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>r : ℝ≥0∞<VAR>this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r<GOAL>∫⁻ (x : α) in {x | f x = r}, r ∂μ = r * μ {x | f x = r}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>r : ℝ≥0∞<VAR>this : ∀ᵐ (x : α) ∂μ, x ∈ {x | f x = r} → f x = r<GOAL>MeasurableSet {x | f x = r}
<VAR>α : Type u_1<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>⋂ n, Ioi ↑n = {⊤}
<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✝³ : InnerProductSpace 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>T : E →ₗ.[𝕜] F<VAR>S : F →ₗ.[𝕜] E<VAR>hT✝ : Dense ↑T.domain<VAR>inst✝ : CompleteSpace E<VAR>hT : ¬Dense ↑T.domain<VAR>y : ↥T†.domain<GOAL>(if hT : Dense ↑T.domain then adjointAux hT else 0) y = 0
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hB : IsBlock G B<VAR>g : G<GOAL>g • B = B ∨ Disjoint (g • B) B
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>X : Type u_2<VAR>inst✝ : MulAction G X<VAR>B : Set X<VAR>hB : ∀ (g g' : G), g • B = g' • B ∨ Disjoint (g • B) (g' • B)<VAR>g : G<GOAL>g • B = B ∨ Disjoint (g • B) B
<VAR>C : Type u_1<VAR>inst✝¹⁰ : Category.{u_2, u_1} C<VAR>inst✝⁹ : HasZeroMorphisms C<VAR>S₁✝ S₂✝ S₃ S₄ : ShortComplex C<VAR>inst✝⁸ : S₁✝.HasHomology<VAR>inst✝⁷ : S₂✝.HasHomology<VAR>inst✝⁶ : S₃.HasHomology<VAR>inst✝⁵ : S₄.HasHomology<VAR>S₁ S₂ : ShortComplex Cᵒᵖ<VAR>inst✝⁴ : S₁.HasHomology<VAR>inst✝³ : S₂.HasHomology<VAR>inst✝² : S₁.unop.HasHomology<VAR>inst✝¹ : S₂.unop.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>inst✝ : QuasiIso φ<GOAL>QuasiIso (unopMap φ)
<VAR>C : Type u_1<VAR>inst✝¹⁰ : Category.{u_2, u_1} C<VAR>inst✝⁹ : HasZeroMorphisms C<VAR>S₁✝ S₂✝ S₃ S₄ : ShortComplex C<VAR>inst✝⁸ : S₁✝.HasHomology<VAR>inst✝⁷ : S₂✝.HasHomology<VAR>inst✝⁶ : S₃.HasHomology<VAR>inst✝⁵ : S₄.HasHomology<VAR>S₁ S₂ : ShortComplex Cᵒᵖ<VAR>inst✝⁴ : S₁.HasHomology<VAR>inst✝³ : S₂.HasHomology<VAR>inst✝² : S₁.unop.HasHomology<VAR>inst✝¹ : S₂.unop.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>inst✝ : QuasiIso φ<GOAL>QuasiIso (opMap (unopMap φ))
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>p q : ℕ<VAR>hpq : q < p<GOAL>Tendsto (fun x => x ^ p / x ^ q) atTop atTop
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>p q : ℕ<VAR>hpq : q < p<GOAL>Tendsto (fun x => x ^ (↑p - ↑q)) atTop atTop
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>p q : ℕ<VAR>hpq : q < p<GOAL>0 < ↑p - ↑q
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>a : α<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>hs.toFinset ⊂ ht.toFinset ↔ s ⊂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>J J' : Set α<VAR>h : J' ∈ R.leftFixedPoints<VAR>h₁ : J ≤ J'<GOAL>R.rightDual (R.leftDual J) ≤ R.rightDual (R.leftDual J')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>J J' : Set α<VAR>h : J' ∈ R.leftFixedPoints<VAR>h₁ : J ≤ J'<GOAL>(fun b => ∀ ⦃a : α⦄, a ∈ J → R a b) ≤ fun b => ∀ ⦃a : α⦄, a ∈ J' → R a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Rel α β<VAR>J J' : Set α<VAR>h : J' ∈ R.leftFixedPoints<VAR>h₁ : J ≤ J'<GOAL>J ≤ J'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c d a b : α<GOAL>a ⊔ b ⇨ b = a ⇨ b
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>inst✝⁶ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : PreservesFilteredColimits (forget C)<VAR>inst✝³ : HasLimits C<VAR>inst✝² : PreservesLimits (forget C)<VAR>inst✝¹ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.val)<GOAL>IsIso f
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>inst✝⁶ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : PreservesFilteredColimits (forget C)<VAR>inst✝³ : HasLimits C<VAR>inst✝² : PreservesLimits (forget C)<VAR>inst✝¹ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.val)<GOAL>IsIso ((Sheaf.forget C X).map f)
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>inst✝⁶ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : PreservesFilteredColimits (forget C)<VAR>inst✝³ : HasLimits C<VAR>inst✝² : PreservesLimits (forget C)<VAR>inst✝¹ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.val)<GOAL>∀ (U : (Opens ↑X)ᵒᵖ), IsIso (f.val.app U)
<VAR>C : Type u<VAR>inst✝⁷ : Category.{v, u} C<VAR>inst✝⁶ : HasColimits C<VAR>X Y Z : TopCat<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : PreservesFilteredColimits (forget C)<VAR>inst✝³ : HasLimits C<VAR>inst✝² : PreservesLimits (forget C)<VAR>inst✝¹ : (forget C).ReflectsIsomorphisms<VAR>F G : Sheaf C X<VAR>f : F ⟶ G<VAR>inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.val)<VAR>X✝ : Opens ↑X<GOAL>IsIso (f.val.app (op X✝))
<VAR>α : Type u_1<VAR>inst✝¹ : Inv α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm x⁻¹ = ((equivShrink α).symm x)⁻¹
<VAR>α : Type u_1<VAR>inst✝¹ : Inv α<VAR>inst✝ : Small.{u_2, u_1} α<VAR>x : Shrink.{u_2, u_1} α<GOAL>(equivShrink α).symm ((equivShrink α).symm.symm ((equivShrink α).symm x)⁻¹) = ((equivShrink α).symm x)⁻¹
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>p₁ p₂ : MvPolynomial σ R<GOAL>∃ s q₁ q₂, p₁ = (rename Subtype.val) q₁ ∧ p₂ = (rename Subtype.val) q₂
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>p₂ : MvPolynomial σ R<VAR>s₁ : Finset σ<VAR>q₁ : MvPolynomial { x // x ∈ s₁ } R<GOAL>∃ s q₁_1 q₂, (rename Subtype.val) q₁ = (rename Subtype.val) q₁_1 ∧ p₂ = (rename Subtype.val) q₂
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s₁ : Finset σ<VAR>q₁ : MvPolynomial { x // x ∈ s₁ } R<VAR>s₂ : Finset σ<VAR>q₂ : MvPolynomial { x // x ∈ s₂ } R<GOAL>∃ s q₁_1 q₂_1, (rename Subtype.val) q₁ = (rename Subtype.val) q₁_1 ∧ (rename Subtype.val) q₂ = (rename Subtype.val) q₂_1
<VAR>s : ℂ<GOAL>completedRiemannZeta s = completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup γ<VAR>f g : α → γ<VAR>hf : Tendsto f atTop atTop<VAR>hg : Tendsto g atTop atTop<GOAL>Tendsto (Prod.map f g) atTop atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : SemilatticeSup γ<VAR>f g : α → γ<VAR>hf : Tendsto f atTop atTop<VAR>hg : Tendsto g atTop atTop<GOAL>Tendsto (Prod.map f g) (atTop ×ˢ atTop) atTop
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ : SimplicialObject C<VAR>X Y : Augmented C<VAR>f : X ⟶ Y<GOAL>(drop.map f).app (op [0]) ≫ Y.hom.app (op [0]) = X.hom.app (op [0]) ≫ point.map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>P : Karoubi C<GOAL>(F.map P.p).f ≫ (φ.app P.X).f = ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ ((obj G).obj P).p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>P : Karoubi C<VAR>h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p<GOAL>(F.map P.p).f ≫ (φ.app P.X).f = ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ ((obj G).obj P).p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>P : Karoubi C<VAR>h : F.map P.p ≫ φ.app P.X = φ.app P.X ≫ G.map P.p<VAR>h' : F.map (P.p ≫ P.p) = F.map P.p<GOAL>(F.map P.p).f ≫ (φ.app P.X).f = ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ ((obj G).obj P).p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>P : Karoubi C<VAR>h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f<VAR>h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f<GOAL>(F.map P.p).f ≫ (φ.app P.X).f = ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ ((obj G).obj P).p
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>P : Karoubi C<VAR>h : (F.map P.p).f ≫ (φ.app P.X).f = (φ.app P.X).f ≫ (G.map P.p).f<VAR>h' : (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).f<GOAL>(F.map P.p).f ≫ (φ.app P.X).f = (F.map P.p).f ≫ (F.map P.p).f ≫ (F.map P.p).f ≫ (φ.app P.X).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>x✝¹ x✝ : Karoubi C<VAR>f : x✝¹ ⟶ x✝<GOAL>(F.map f.f).f ≫ (F.map x✝.p).f ≫ (φ.app x✝.X).f = ((F.map x✝¹.p).f ≫ (φ.app x✝¹.X).f) ≫ (G.map f.f).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>x✝¹ x✝ : Karoubi C<VAR>f : x✝¹ ⟶ x✝<VAR>h : F.map f.f ≫ φ.app x✝.X = φ.app x✝¹.X ≫ G.map f.f<GOAL>(F.map f.f).f ≫ (F.map x✝.p).f ≫ (φ.app x✝.X).f = ((F.map x✝¹.p).f ≫ (φ.app x✝¹.X).f) ≫ (G.map f.f).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>x✝¹ x✝ : Karoubi C<VAR>f : x✝¹ ⟶ x✝<VAR>h : F.map f.f ≫ φ.app x✝.X = φ.app x✝¹.X ≫ G.map f.f<VAR>h' : F.map (f.f ≫ x✝.p) = F.map f.f<GOAL>(F.map f.f).f ≫ (F.map x✝.p).f ≫ (φ.app x✝.X).f = ((F.map x✝¹.p).f ≫ (φ.app x✝¹.X).f) ≫ (G.map f.f).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>x✝¹ x✝ : Karoubi C<VAR>f : x✝¹ ⟶ x✝<VAR>h : F.map f.f ≫ φ.app x✝.X = φ.app x✝¹.X ≫ G.map f.f<VAR>h' : F.map (f.f ≫ x✝.p) = F.map f.f<VAR>h'' : F.map (x✝¹.p ≫ f.f) = F.map f.f<GOAL>(F.map f.f).f ≫ (F.map x✝.p).f ≫ (φ.app x✝.X).f = ((F.map x✝¹.p).f ≫ (φ.app x✝¹.X).f) ≫ (G.map f.f).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>x✝¹ x✝ : Karoubi C<VAR>f : x✝¹ ⟶ x✝<VAR>h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f<VAR>h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f<VAR>h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f<GOAL>(F.map f.f).f ≫ (F.map x✝.p).f ≫ (φ.app x✝.X).f = ((F.map x✝¹.p).f ≫ (φ.app x✝¹.X).f) ≫ (G.map f.f).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>x✝¹ x✝ : Karoubi C<VAR>f : x✝¹ ⟶ x✝<VAR>h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f<VAR>h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f<VAR>h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f<GOAL>(F.map f.f).f ≫ (F.map x✝.p).f ≫ (φ.app x✝.X).f = (F.map x✝¹.p).f ≫ (F.map f.f).f ≫ (φ.app x✝.X).f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝² : Category.{?u.6113, u_1} C<VAR>inst✝¹ : Category.{?u.6117, u_2} D<VAR>inst✝ : Category.{?u.6121, u_3} E<VAR>F G : C ⥤ Karoubi D<VAR>φ : F ⟶ G<VAR>x✝¹ x✝ : Karoubi C<VAR>f : x✝¹ ⟶ x✝<VAR>h : (F.map f.f).f ≫ (φ.app x✝.X).f = (φ.app x✝¹.X).f ≫ (G.map f.f).f<VAR>h' : (F.map f.f).f ≫ (F.map x✝.p).f = (F.map f.f).f<VAR>h'' : (F.map x✝¹.p).f ≫ (F.map f.f).f = (F.map f.f).f<GOAL>(F.map f.f).f ≫ (φ.app x✝.X).f = (F.map x✝¹.p).f ≫ (F.map f.f).f ≫ (φ.app x✝.X).f
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Add α<VAR>b c d : WithTop α<VAR>x y : α<VAR>inst✝ : IsLeftCancelAdd α<VAR>a : α<GOAL>↑a + b = ↑a + c ↔ b = c
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Add α<VAR>c d : WithTop α<VAR>x y : α<VAR>inst✝ : IsLeftCancelAdd α<VAR>a : α<GOAL>↑a + ⊤ = ↑a + c ↔ ⊤ = c
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Add α<VAR>b c d : WithTop α<VAR>x y : α<VAR>inst✝ : IsLeftCancelAdd α<VAR>a : α<VAR>hb : b ≠ ⊤<GOAL>↑a + b = ↑a + c ↔ b = c
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Add α<VAR>c d : WithTop α<VAR>x y : α<VAR>inst✝ : IsLeftCancelAdd α<VAR>a b : α<GOAL>↑a + ↑b = ↑a + c ↔ ↑b = c
<VAR>f : ℂ →ₗᵢ[ℝ] ℂ<VAR>h₃ : ∀ (z : ℂ), z + (starRingEnd ℂ) z = f z + (starRingEnd ℂ) (f z)<VAR>z : ℂ<GOAL>(f z).re = z.re
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>n m : ℕ<VAR>h : n = m<VAR>x : ⨂[R]^n M<GOAL>GradedMonoid.mk m ((PiTensorProduct.reindex R (fun x => M) (finCongr h)) x) = GradedMonoid.mk n x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p✝ p₀✝ p₁ p₂ p₀ p : P<GOAL>∠ p p₀ p₀ = π / 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<GOAL>⊥.image s = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<GOAL>∀ (x : β), x ∉ ⊥.image s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<VAR>x : β<VAR>h : x ∈ ⊥.image s<GOAL>False
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>inrX φ i ≫ fstX φ i j hij = 0
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i : ι<VAR>hij : c.Rel i (c.next i)<GOAL>inrX φ i ≫ fstX φ i (c.next i) hij = 0
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<GOAL>0 < a - b ↔ ¬a ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>inst✝ : Countable ι<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((Kernel.sum fun x => 0) a) s = (0 a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>inst✝ : Countable ι<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∑' (n : ι), (0 a) s = (0 a) s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X : C<VAR>p : Subobject X → Subobject X → Prop<VAR>h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)<VAR>P Q : Subobject X<GOAL>p P Q
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X✝ Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X : C<VAR>p : Subobject X → Subobject X → Prop<VAR>h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)<VAR>P Q : Subobject X<GOAL>∀ (a₁ a₂ : MonoOver X), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<GOAL>UnifIntegrable (-f) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup β<VAR>f g : ι → α → β<VAR>p : ℝ≥0∞<VAR>hf : UnifIntegrable f p μ<GOAL>∀ ⦃ε : ℝ⦄, 0 < ε → ∃ δ, ∃ (_ : 0 < δ), ∀ (i : ι) (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : LocallyConnectedSpace α<VAR>x : α<GOAL>IsOpen (connectedComponent x)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : LocallyConnectedSpace α<VAR>x : α<GOAL>IsOpen (connectedComponentIn univ x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>a✝ a' : α<VAR>b✝ : M<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : M<GOAL>⇑(single a b) = update 0 a b
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>x y : ℕ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>f (x.lcm y) * f (x.gcd y) = f x * f y
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>x y : ℕ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hgcd_ne_zero : x.gcd y ≠ 0<GOAL>f (x.lcm y) * f (x.gcd y) = f x * f y
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>x y : ℕ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hgcd_ne_zero : x.gcd y ≠ 0<VAR>hlcm_ne_zero : x.lcm y ≠ 0<GOAL>f (x.lcm y) * f (x.gcd y) = f x * f y
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>x y : ℕ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hgcd_ne_zero : x.gcd y ≠ 0<VAR>hlcm_ne_zero : x.lcm y ≠ 0<VAR>hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1<GOAL>f (x.lcm y) * f (x.gcd y) = f x * f y
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>x y : ℕ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hgcd_ne_zero : x.gcd y ≠ 0<VAR>hlcm_ne_zero : x.lcm y ≠ 0<VAR>hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1<GOAL>(∏ x_1 ∈ x.primeFactors ⊔ y.primeFactors, f (x_1 ^ (x.lcm y).factorization x_1)) * ∏ x_1 ∈ x.primeFactors ⊔ y.primeFactors, f (x_1 ^ (x.gcd y).factorization x_1) = (∏ x_1 ∈ x.primeFactors ⊔ y.primeFactors, f (x_1 ^ x.factorization x_1)) * ∏ x ∈ x.primeFactors ⊔ y.primeFactors, f (x ^ y.factorization x)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>x y : ℕ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hgcd_ne_zero : x.gcd y ≠ 0<VAR>hlcm_ne_zero : x.lcm y ≠ 0<VAR>hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1<GOAL>y.factorization.support ⊆ x.primeFactors ⊔ y.primeFactors
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>x y : ℕ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hgcd_ne_zero : x.gcd y ≠ 0<VAR>hlcm_ne_zero : x.lcm y ≠ 0<VAR>hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1<GOAL>x.factorization.support ⊆ x.primeFactors ⊔ y.primeFactors
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>x y : ℕ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hgcd_ne_zero : x.gcd y ≠ 0<VAR>hlcm_ne_zero : x.lcm y ≠ 0<VAR>hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1<GOAL>(x.gcd y).factorization.support ⊆ x.primeFactors ⊔ y.primeFactors
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>f : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>x y : ℕ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<VAR>hgcd_ne_zero : x.gcd y ≠ 0<VAR>hlcm_ne_zero : x.lcm y ≠ 0<VAR>hfi_zero : ∀ {i : ℕ}, f (i ^ 0) = 1<GOAL>(x.lcm y).factorization.support ⊆ x.primeFactors ⊔ y.primeFactors
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Icc a b = ∅ ↔ ¬a ≤ b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring S<VAR>inst✝⁶ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : IsDomain B<VAR>inst✝² : Algebra A B<VAR>K : Type u_6<VAR>inst✝¹ : Field K<VAR>inst✝ : Nontrivial S<VAR>pb : PowerBasis R S<VAR>y : S<GOAL>y ∈ Submodule.span R (Set.range fun i => pb.gen ^ ↑i)
<VAR>a✝ b✝ a b : Prop<GOAL>Xor' a b = Xor' b a