ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁰ : Category.{u_4, u_1} C<VAR>inst✝⁹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁸ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝⁷ : G.IsCocontinuous J K<VAR>inst✝⁶ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝⁵ : G.IsCocontinuous J K<VAR>inst✝⁴ : G.IsContinuous J K<VAR>inst✝³ : HasWeakSheafify J A<VAR>inst✝² : HasWeakSheafify K A<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<VAR>adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A<VAR>adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A<VAR>adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A<VAR>adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K<VAR>eq : adj₁.unit.app F ≫ G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫ G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) = adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))<GOAL>(adj₁.homEquiv ((𝟭 (Dᵒᵖ ⥤ A)).obj F) ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)).val).symm (adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))) = (adj₁.homEquiv ((𝟭 (Dᵒᵖ ⥤ A)).obj F) ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)).val).symm ((adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F))) (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F)))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁰ : Category.{u_4, u_1} C<VAR>inst✝⁹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁸ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝⁷ : G.IsCocontinuous J K<VAR>inst✝⁶ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝⁵ : G.IsCocontinuous J K<VAR>inst✝⁴ : G.IsContinuous J K<VAR>inst✝³ : HasWeakSheafify J A<VAR>inst✝² : HasWeakSheafify K A<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<VAR>adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A<VAR>adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A<VAR>adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A<VAR>adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K<VAR>eq : adj₁.unit.app F ≫ G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫ G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) = adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))<GOAL>((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F) ≫ ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map ((sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))) ≫ adj₁.counit.app ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)).val = ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F) ≫ ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₁.unit.app ((presheafToSheaf K A ⋙ sheafToPresheaf K A).obj F)) ≫ adj₁.counit.app ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)).val
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹⁰ : Category.{u_4, u_1} C<VAR>inst✝⁹ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝⁸ : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝⁷ : G.IsCocontinuous J K<VAR>inst✝⁶ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>inst✝⁵ : G.IsCocontinuous J K<VAR>inst✝⁴ : G.IsContinuous J K<VAR>inst✝³ : HasWeakSheafify J A<VAR>inst✝² : HasWeakSheafify K A<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : G.IsContinuous J K<VAR>F : Dᵒᵖ ⥤ A<VAR>adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A<VAR>adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A<VAR>adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A<VAR>adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K<VAR>eq : adj₁.unit.app F ≫ G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫ G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) = adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))<GOAL>(sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F)) = adj₁.unit.app ((presheafToSheaf K A ⋙ sheafToPresheaf K A).obj F)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>s : Set α<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hfi : Integrable f μ<GOAL>↑↑(condexpL1 hm μ f) =ᶠ[ae μ] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>s : Set α<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hfi : Integrable f μ<GOAL>↑↑((condexpL1CLM F' hm μ) (Integrable.toL1 f hfi)) =ᶠ[ae μ] f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>s : Set α<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hfi : Integrable f μ<GOAL>↑↑((condexpL1CLM F' hm μ) (Integrable.toL1 f hfi)) =ᶠ[ae μ] ↑↑(Integrable.toL1 f hfi)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace 𝕜 F'<VAR>inst✝⁶ : NormedSpace ℝ F'<VAR>inst✝⁵ : CompleteSpace F'<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedAddCommGroup G'<VAR>inst✝² : NormedSpace ℝ G'<VAR>inst✝¹ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>inst✝ : SigmaFinite (μ.trim hm)<VAR>f g : α → F'<VAR>s : Set α<VAR>hfm : AEStronglyMeasurable' m f μ<VAR>hfi : Integrable f μ<GOAL>AEStronglyMeasurable' m (↑↑(Integrable.toL1 f hfi)) μ
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>n : ℕ<GOAL>exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1
<VAR>G : Type u<VAR>inst✝ : Monoid G<GOAL>exponent G ∣ 0 ↔ ∀ (g : G), g ^ 0 = 1
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>n : ℕ<VAR>hpos : n > 0<GOAL>exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddMonoid R<VAR>x : (HahnSeries Γ R)ᵃᵒᵖ<GOAL>(addOppositeEquiv.symm x).support = (AddOpposite.unop x).support
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A : Type u_2<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_3<VAR>inst✝ : Group N<VAR>z : ℤ<GOAL>z ∈ AddSubgroup.zmultiples 1 ↔ z ∈ ⊤
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>i : (Quotient.out (aleph 1).ord).α<VAR>f : ℕ → Set α<VAR>hf : ∀ (n : ℕ), ∃ j < i, f n ∈ generateMeasurableRec s j<GOAL>⋃ n, f n ∈ let i := i; let S := ⋃ j, generateMeasurableRec s ↑j; s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ n, ↑(f n)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s✝ : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x y z : E<VAR>s : Finset E<VAR>hf : ConvexOn 𝕜 ((convexHull 𝕜) ↑s) f<VAR>hx : x ∈ (convexHull 𝕜) ↑s<GOAL>f x ≤ s.sup' ⋯ f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s✝ : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w✝ : ι → 𝕜<VAR>p : ι → E<VAR>y z : E<VAR>s : Finset E<VAR>hf : ConvexOn 𝕜 ((convexHull 𝕜) ↑s) f<VAR>w : E → 𝕜<VAR>hw₀ : ∀ y ∈ s, 0 ≤ w y<VAR>hw₁ : ∑ y ∈ s, w y = 1<VAR>hx : s.centerMass w _root_.id ∈ (convexHull 𝕜) ↑s<GOAL>f (s.centerMass w _root_.id) ≤ s.sup' ⋯ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : Measurable f<VAR>a : α<GOAL>IsRatStieltjesPoint (toRatCDF f) a
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x - y) x).tan * ‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle x (x - y)).tan * ‖x‖ = ‖y‖
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>s : σ<VAR>x : List α<VAR>a : α<GOAL>M.evalFrom s (x ++ [a]) = M.step (M.evalFrom s x) a
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>x : M<GOAL>(lift S g h) (mk x 1) = g x
<VAR>R : Type u_1<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁷ : CommSemiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Module A M'<VAR>inst✝⁴ : IsLocalization S A<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>inst✝ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>x : M<GOAL>↑⋯.unit⁻¹ (g x) = g x
<VAR>α : Type u<VAR>o n m : ℕ<VAR>m' : Type uₘ<VAR>n' : Type uₙ<VAR>o' : Type uₒ<VAR>a b : ℕ<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : Mul α<VAR>a₀ a₁ a₂ b₀ b₁ b₂ : α<GOAL>![a₀, a₁, a₂] ⬝ᵥ ![b₀, b₁, b₂] = a₀ * b₀ + a₁ * b₁ + a₂ * b₂
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : q.degree < p.degree<GOAL>(p + q).coeff p.natDegree ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : q.degree < p.degree<GOAL>p.coeff p.natDegree ≠ 0
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : SimplicialObject C<VAR>s : Splitting X<VAR>f g : X ⟶ Y<VAR>h : ∀ (n : ℕ), s.φ f n = s.φ g n<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>f.app Δ = g.app Δ
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : SimplicialObject C<VAR>s : Splitting X<VAR>f g : X ⟶ Y<VAR>h : ∀ (n : ℕ), s.φ f n = s.φ g n<VAR>Δ : SimplexCategoryᵒᵖ<GOAL>∀ (A : IndexSet Δ), (s.cofan Δ).inj A ≫ f.app Δ = (s.cofan Δ).inj A ≫ g.app Δ
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X Y : SimplicialObject C<VAR>s : Splitting X<VAR>f g : X ⟶ Y<VAR>h : ∀ (n : ℕ), s.φ f n = s.φ g n<VAR>n : ℕ<VAR>A : IndexSet (op [n])<GOAL>(s.cofan (op [n])).inj A ≫ f.app (op [n]) = (s.cofan (op [n])).inj A ≫ g.app (op [n])
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hm : φ.IsHomogeneous m<VAR>hn : φ.IsHomogeneous n<VAR>hφ : φ ≠ 0<GOAL>m = n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hm : φ.IsHomogeneous m<VAR>hn : φ.IsHomogeneous n<VAR>hφ : φ ≠ 0<VAR>d : σ →₀ ℕ<VAR>hd : coeff d φ ≠ 0<GOAL>m = n
<VAR>n : Type u_1<VAR>inst✝⁶ : Fintype n<VAR>R : Type u_2<VAR>M✝ : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>A : Type u_4<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing A<VAR>inst✝ : IsDomain A<VAR>M : Matrix n n A<GOAL>M.Nondegenerate ↔ M.det ≠ 0
<VAR>n : Type u_1<VAR>inst✝⁶ : Fintype n<VAR>R : Type u_2<VAR>M✝ : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M✝<VAR>inst✝³ : Module R M✝<VAR>A : Type u_4<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing A<VAR>inst✝ : IsDomain A<VAR>M : Matrix n n A<GOAL>M.Nondegenerate ↔ ¬∃ v, v ≠ 0 ∧ v ᵥ* M = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommRing S<VAR>inst✝ : Nontrivial R<VAR>abv : AbsoluteValue R S<VAR>x : ℤˣ<GOAL>abv ↑↑x = 1
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : (C ⥤ D)ᵒᵖ<VAR>f : F ⟶ G<GOAL>f ≫ (NatIso.ofComponents (fun X => Iso.refl ((unop G).obj X)) ⋯).hom.op = (NatIso.ofComponents (fun X => Iso.refl ((unop F).obj X)) ⋯).hom.op ≫ Quiver.Hom.op { app := fun X => f.unop.app X, naturality := ⋯ }
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G : (C ⥤ D)ᵒᵖ<VAR>f : F ⟶ G<GOAL>((NatIso.ofComponents (fun X => Iso.refl ((unop G).obj X)) ⋯).hom ≫ f.unop).op = ({ app := fun X => f.unop.op.unop.app X, naturality := ⋯ } ≫ (NatIso.ofComponents (fun X => Iso.refl ((unop F).obj X)) ⋯).hom).op
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>S : Set (Set X)<GOAL>interior (⋂₀ S) = interior (⋂ s ∈ S, s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : LT α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b : α<GOAL>a * b < a ↔ a * b < a * 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : LinearOrderedRing α<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>inst✝ : Fintype ι<VAR>hfg : Antivary f g<GOAL>Fintype.card ι • ∑ i : ι, f i • g i ≤ (∑ i : ι, f i) • ∑ i : ι, g i
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>p q : ℤ<VAR>hpq : p + n' = q<GOAL>((γ₁ + γ₂).leftShift a n' hn').v p q hpq = (γ₁.leftShift a n' hn').v p q hpq + (γ₂.leftShift a n' hn').v p q hpq
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>t₁ t₂ : Triangle ℝ P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h₁ : t₁.points i₁ = t₂.points i₁<VAR>h₃ : t₁.points i₃ = t₂.points i₃<VAR>h₂ : 2 • ∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) = 2 • ∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)<GOAL>Simplex.circumsphere t₁ = Simplex.circumsphere t₂
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y<GOAL>∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u v s : Set α<VAR>hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y<VAR>this : ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∪ v ∧ (s ∩ u).Nonempty ∧ (s ∩ v).Nonempty ∧ s ∩ (u ∩ v) = ∅<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y<VAR>u v : Set α<VAR>u_op : IsOpen u<VAR>v_op : IsOpen v<VAR>hsuv : s ⊆ u ∪ v<VAR>x : α<VAR>x_in_s : x ∈ s<VAR>x_in_u : x ∈ u<VAR>H : s ∩ (u ∩ v) = ∅<VAR>y : α<VAR>y_in_s : y ∈ s<VAR>y_in_v : y ∈ v<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y<VAR>u v : Set α<VAR>u_op : IsOpen u<VAR>v_op : IsOpen v<VAR>hsuv : s ⊆ u ∪ v<VAR>x : α<VAR>x_in_s : x ∈ s<VAR>x_in_u : x ∈ u<VAR>H : s ∩ (u ∩ v) = ∅<VAR>y : α<VAR>y_in_s : y ∈ s<VAR>y_in_v : y ∈ v<VAR>hy : y ∉ u<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t u✝ v✝ s : Set α<VAR>hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y<VAR>u v : Set α<VAR>u_op : IsOpen u<VAR>v_op : IsOpen v<VAR>hsuv : s ⊆ u ∪ v<VAR>x : α<VAR>x_in_s : x ∈ s<VAR>x_in_u : x ∈ u<VAR>H : s ∩ (u ∩ v) = ∅<VAR>y : α<VAR>y_in_s : y ∈ s<VAR>y_in_v : y ∈ v<VAR>hy : y ∉ u<VAR>this : ContinuousOn u.boolIndicator s<GOAL>False
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝ : NonUnitalNonAssocSemiring α<VAR>g f₁ f₂ : CentroidHom α<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>α : Type u_1<VAR>inst✝ : Fintype α<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hα : ¬p ∣ Fintype.card α<VAR>σ : Perm α<VAR>hσ : σ ^ p ^ n = 1<GOAL>∃ a, σ a = a
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s t : Set α<VAR>hst : t ⊆ s<GOAL>eVariationOn f t ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s t : Set α<VAR>hst : t ⊆ s<GOAL>∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ t }), ∑ i_1 ∈ Finset.range i.1, edist (f (↑i.2 (i_1 + 1))) (f (↑i.2 i_1)) ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s t : Set α<VAR>hst : t ⊆ s<VAR>n : ℕ<VAR>u : ℕ → α<VAR>hu : Monotone u<VAR>ut : ∀ (i : ℕ), u i ∈ t<GOAL>∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist (f (↑(n, ⟨u, ⋯⟩).2 (i + 1))) (f (↑(n, ⟨u, ⋯⟩).2 i)) ≤ eVariationOn f s
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<VAR>F : ℕ → R := fun n => ∑' (e : ℕ), f (n ^ e)<GOAL>HasProd (F ∘ Subtype.val) (∑' (n : ℕ), f n)
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<VAR>F : ℕ → R := fun n => ∑' (e : ℕ), f (n ^ e)<GOAL>∀ ε > 0, ∃ N, ∀ n ≥ N, dist (∏ b ∈ n, {p | Nat.Prime p}.mulIndicator F b) (∑' (n : ℕ), f n) < ε
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<VAR>F : ℕ → R := fun n => ∑' (e : ℕ), f (n ^ e)<VAR>ε : ℝ<VAR>hε : ε > 0<GOAL>∃ N, ∀ n ≥ N, dist (∏ b ∈ n, {p | Nat.Prime p}.mulIndicator F b) (∑' (n : ℕ), f n) < ε
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<VAR>F : ℕ → R := fun n => ∑' (e : ℕ), f (n ^ e)<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>N₀ : ℕ<VAR>hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε<GOAL>∃ N, ∀ n ≥ N, dist (∏ b ∈ n, {p | Nat.Prime p}.mulIndicator F b) (∑' (n : ℕ), f n) < ε
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<VAR>F : ℕ → R := fun n => ∑' (e : ℕ), f (n ^ e)<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>N₀ : ℕ<VAR>hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε<VAR>s : Finset ℕ<VAR>hs : s ≥ range N₀<GOAL>dist (∏ b ∈ s, {p | Nat.Prime p}.mulIndicator F b) (∑' (n : ℕ), f n) < ε
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<VAR>F : ℕ → R := fun n => ∑' (e : ℕ), f (n ^ e)<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>N₀ : ℕ<VAR>hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε<VAR>s : Finset ℕ<VAR>hs : s ≥ range N₀<VAR>this : ∏ p ∈ s, {p | Nat.Prime p}.mulIndicator F p = ∏ p ∈ filter Nat.Prime s, F p<GOAL>dist (∏ b ∈ s, {p | Nat.Prime p}.mulIndicator F b) (∑' (n : ℕ), f n) < ε
<VAR>R : Type u_1<VAR>inst✝¹ : NormedCommRing R<VAR>inst✝ : CompleteSpace R<VAR>f : ℕ → R<VAR>hf₁ : f 1 = 1<VAR>hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n<VAR>hsum : Summable fun x => ‖f x‖<VAR>hf₀ : f 0 = 0<VAR>F : ℕ → R := fun n => ∑' (e : ℕ), f (n ^ e)<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>N₀ : ℕ<VAR>hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ≤ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε<VAR>s : Finset ℕ<VAR>hs : s ≥ range N₀<VAR>this : ∏ p ∈ s, {p | Nat.Prime p}.mulIndicator F p = ∏ p ∈ filter Nat.Prime s, F p<GOAL>‖∑' (n : ℕ), f n - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype ι'<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹¹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁸ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁷ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace 𝕜 G<VAR>inst✝⁴ : SeminormedAddCommGroup G'<VAR>inst✝³ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝² : NormedField 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' G<VAR>inst✝ : SMulCommClass 𝕜 𝕜' G<GOAL>IsLeast {C | ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ C * ∏ i : ι, ‖m i‖₊} ‖f‖₊