ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>l : LocalizedModule S M →ₗ[R] M''<VAR>hl : l ∘ₗ mkLinearMap S M = g<VAR>m : M<VAR>s : ↥S<GOAL>1 • s • m = 1 • 1 • ↑s • m
<VAR>p n k : ℕ<VAR>hp' : p ≠ 2<VAR>hk : p ≤ k<VAR>hk' : p ≤ n - k<VAR>hn : n < 3 * p<GOAL>(n.choose k).factorization p = 0
<VAR>p n k : ℕ<VAR>hp' : p ≠ 2<VAR>hk : p ≤ k<VAR>hk' : p ≤ n - k<VAR>hn : n < 3 * p<VAR>hp : ¬Prime p<GOAL>(n.choose k).factorization p = 0
<VAR>p n k : ℕ<VAR>hp' : p ≠ 2<VAR>hk : p ≤ k<VAR>hk' : p ≤ n - k<VAR>hn : n < 3 * p<VAR>hp : Prime p<GOAL>(n.choose k).factorization p = 0
<VAR>p n k : ℕ<VAR>hp' : p ≠ 2<VAR>hk : p ≤ k<VAR>hk' : p ≤ n - k<VAR>hn : n < 3 * p<VAR>hp : Prime p<VAR>hnk : n < k<GOAL>(n.choose k).factorization p = 0
<VAR>p n k : ℕ<VAR>hp' : p ≠ 2<VAR>hk : p ≤ k<VAR>hk' : p ≤ n - k<VAR>hn : n < 3 * p<VAR>hp : Prime p<VAR>hkn : k ≤ n<GOAL>(n.choose k).factorization p = 0
<VAR>p n k : ℕ<VAR>hp' : p ≠ 2<VAR>hk : p ≤ k<VAR>hk' : p ≤ n - k<VAR>hn : n < 3 * p<VAR>hp : Prime p<VAR>hkn : k ≤ n<GOAL>(multiplicity p (n.choose k)).get ⋯ = 0
<VAR>p n k : ℕ<VAR>hp' : p ≠ 2<VAR>hk : p ≤ k<VAR>hk' : p ≤ n - k<VAR>hn : n < 3 * p<VAR>hp : Prime p<VAR>hkn : k ≤ n<GOAL>∀ ⦃x : ℕ⦄, x ∈ Finset.Ico 1 (log p n + 1) → k % p ^ x + (n - k) % p ^ x < p ^ x
<VAR>p n k : ℕ<VAR>hp' : p ≠ 2<VAR>hk : p ≤ k<VAR>hk' : p ≤ n - k<VAR>hn : n < 3 * p<VAR>hp : Prime p<VAR>hkn : k ≤ n<VAR>i : ℕ<VAR>hi : i ∈ Finset.Ico 1 (log p n + 1)<GOAL>k % p ^ i + (n - k) % p ^ i < p ^ i
<VAR>p n k : ℕ<VAR>hp' : p ≠ 2<VAR>hk : p ≤ k<VAR>hk' : p ≤ n - k<VAR>hn : n < 3 * p<VAR>hp : Prime p<VAR>hkn : k ≤ n<VAR>hi : 1 ∈ Finset.Ico 1 (log p n + 1)<GOAL>k % p ^ 1 + (n - k) % p ^ 1 < p ^ 1
<VAR>p n k : ℕ<VAR>hp' : p ≠ 2<VAR>hk : p ≤ k<VAR>hk' : p ≤ n - k<VAR>hn : n < 3 * p<VAR>hp : Prime p<VAR>hkn : k ≤ n<VAR>i : ℕ<VAR>hi✝ : i ∈ Finset.Ico 1 (log p n + 1)<VAR>hi : 1 < i<GOAL>k % p ^ i + (n - k) % p ^ i < p ^ i
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_6, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>H : Type u_3<VAR>inst✝¹ : Category.{u_5, u_3} H<VAR>inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F<VAR>G : D ⥤ H<GOAL>L.lanUnit.app (L ⋙ G) ≫ whiskerLeft L ((L.lanAdjunction H).counit.app G) = 𝟙 (L ⋙ G)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Ring α<VAR>I : Ideal α<VAR>a b x x✝ : α<GOAL>x✝ ∈ span {-x} ↔ x✝ ∈ span {x}
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Ring α<VAR>I : Ideal α<VAR>a b x x✝ : α<GOAL>(∃ a, a * -x = x✝) ↔ ∃ a, a * x = x✝
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<GOAL>α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<GOAL>(𝟙 F).app X = 𝟙 (F.obj X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<GOAL>α.inv.app X ≫ α.hom.app X = 𝟙 (G.obj X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>X : C<GOAL>(𝟙 G).app X = 𝟙 (G.obj X)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝¹ : CommRing R<VAR>P : R[X]<VAR>inst✝ : IsReduced R<VAR>p : R[X]<VAR>hpl : 0 < p.natDegree<GOAL>¬IsUnit p
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝¹ : CommRing R<VAR>P : R[X]<VAR>inst✝ : IsReduced R<VAR>p : R[X]<VAR>hpl : 0 < p.natDegree<GOAL>IsUnit (p.coeff 0) → ∃ x, ¬x = 0 ∧ ¬p.coeff x = 0
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝¹ : CommRing R<VAR>P : R[X]<VAR>inst✝ : IsReduced R<VAR>p : R[X]<VAR>hpl : 0 < p.natDegree<VAR>a✝ : IsUnit (p.coeff 0)<GOAL>∃ x, ¬x = 0 ∧ ¬p.coeff x = 0
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝¹ : CommRing R<VAR>P : R[X]<VAR>inst✝ : IsReduced R<VAR>p : R[X]<VAR>hpl : 0 < p.natDegree<VAR>a✝ : IsUnit (p.coeff 0)<GOAL>¬p.coeff p.natDegree = 0
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝¹ : CommRing R<VAR>P : R[X]<VAR>inst✝ : IsReduced R<VAR>p : R[X]<VAR>a✝ : IsUnit (p.coeff 0)<VAR>hpl : p.coeff p.natDegree = 0<GOAL>p.natDegree ≤ 0
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝¹ : CommRing R<VAR>P : R[X]<VAR>inst✝ : IsReduced R<VAR>p : R[X]<VAR>a✝ : IsUnit (p.coeff 0)<VAR>hpl : p = 0<GOAL>p.natDegree ≤ 0
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x : V<GOAL>↑e (-x) = ↑‖-1‖₊ * ↑e x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n] x < g^[n] x ↔ f x < g x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>H : f x < g x<GOAL>f^[n] x < g^[n] x ↔ f x < g x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>H : f x = g x<GOAL>f^[n] x < g^[n] x ↔ f x < g x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrder α<VAR>f g : α → α<VAR>h : Commute f g<VAR>hf : Monotone f<VAR>hg : StrictMono g<VAR>x : α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>H : g x < f x<GOAL>f^[n] x < g^[n] x ↔ f x < g x
<VAR>x y : ℝ<GOAL>↑(sin x - sin y) = ↑(2 * sin ((x - y) / 2) * cos ((x + y) / 2))
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>x : PiLp 2 β<GOAL>‖x‖ ^ 2 = ∑ i : ι, ‖x i‖ ^ 2
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>x : PiLp 2 β<GOAL>‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2
<VAR>S : Set Ordinal.{u}<VAR>a b : Ordinal.{u}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<VAR>ha : a ∈ S<VAR>hb : enumOrd S b < a<GOAL>enumOrd S (succ b) ≤ a
<VAR>S : Set Ordinal.{u}<VAR>a b : Ordinal.{u}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<VAR>ha : a ∈ S<VAR>hb : enumOrd S b < a<GOAL>sInf (S ∩ {b_1 | ∀ c < succ b, enumOrd S c < b_1}) ≤ a
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_indep : IndepFun X Y μ<VAR>hX : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ<VAR>hY : AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ<GOAL>mgf (X + Y) μ t = mgf X μ t * mgf Y μ t
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>X Y : Ω → ℝ<VAR>h_indep : IndepFun X Y μ<VAR>hX : AEStronglyMeasurable (fun ω => rexp (t * X ω)) μ<VAR>hY : AEStronglyMeasurable (fun ω => rexp (t * Y ω)) μ<GOAL>∫ (x : Ω), rexp (t * X x) * rexp (t * Y x) ∂μ = (∫ (x : Ω), rexp (t * X x) ∂μ) * ∫ (x : Ω), rexp (t * Y x) ∂μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>U : Opens α<GOAL>¬(↑U).Nonempty ↔ U = ⊥
<VAR>α : Type u<VAR>a : α<VAR>s✝ t s : Set α<GOAL>Nontrivial ↑s ↔ s.Nontrivial
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>g : Y → Z<VAR>s : Set X<VAR>t : Set Y<VAR>x : X<VAR>hx : x ∈ s<VAR>f : PartialHomeomorph X Y<VAR>hxf : x ∈ f.source<VAR>hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s<VAR>hf : IsLocalHomeomorphOn (↑f) s<VAR>gf : PartialHomeomorph X Z<VAR>hgf : x ∈ gf.source<VAR>he : g ∘ ↑f = ↑gf<GOAL>∃ e, ↑f x ∈ e.source ∧ Set.EqOn g (↑e) e.source
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>g : Y → Z<VAR>s : Set X<VAR>t : Set Y<VAR>x : X<VAR>hx : x ∈ s<VAR>f : PartialHomeomorph X Y<VAR>hxf : x ∈ f.source<VAR>hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s<VAR>hf : IsLocalHomeomorphOn (↑f) s<VAR>gf : PartialHomeomorph X Z<VAR>hgf : x ∈ gf.source<VAR>he : g ∘ ↑f = ↑gf<GOAL>↑f x ∈ ↑f.symm.symm.symm ⁻¹' gf.source
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>g : Y → Z<VAR>s : Set X<VAR>t : Set Y<VAR>x : X<VAR>hx : x ∈ s<VAR>f : PartialHomeomorph X Y<VAR>hxf : x ∈ f.source<VAR>hgf✝ : IsLocalHomeomorphOn (g ∘ ↑f) s<VAR>hf : IsLocalHomeomorphOn (↑f) s<VAR>gf : PartialHomeomorph X Z<VAR>hgf : x ∈ gf.source<VAR>he : g ∘ ↑f = ↑gf<VAR>y : Y<VAR>hy : y ∈ (f.symm.trans gf).source<GOAL>g y = ↑(f.symm.trans gf) y
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>Scheme.Γ.map (f ∣_ U).op = Y.presheaf.map (eqToHom ⋯).op ≫ Scheme.Hom.app f U ≫ X.presheaf.map (eqToHom ⋯).op
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>Scheme.Hom.app f (U.ι ''ᵁ ⊤) ≫ X.presheaf.map (eqToHom ⋯).op = Scheme.Hom.app f (⋯.functor.obj ⊤) ≫ X.presheaf.map (((Opens.map f.val.base).map (eqToHom ⋯).op.unop).op ≫ (eqToHom ⋯).op)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : E<VAR>a b : 𝕜<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hfx : f x ≤ f (a • x + b • y)<GOAL>f (a • x + b • y) ≤ f y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : E<VAR>a b : 𝕜<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : b + a = 1<VAR>hfx : f x ≤ f (b • y + a • x)<GOAL>f (b • y + a • x) ≤ f y
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<GOAL>⨆ k, LieSubmodule.ucs k ⊥ ≤ weightSpace M 0
<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 : R[X]<VAR>inst✝⁷ : CommRing T<VAR>p : T[X]<VAR>S : Type u_1<VAR>S' : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : Algebra T S<VAR>inst✝³ : CommRing S'<VAR>inst✝² : IsDomain S'<VAR>inst✝¹ : Algebra T S'<VAR>inst✝ : NoZeroSMulDivisors T S'<VAR>f : S →ₐ[T] S'<GOAL>Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')
<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 : R[X]<VAR>inst✝⁷ : CommRing T<VAR>p : T[X]<VAR>S : Type u_1<VAR>S' : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : Algebra T S<VAR>inst✝³ : CommRing S'<VAR>inst✝² : IsDomain S'<VAR>inst✝¹ : Algebra T S'<VAR>inst✝ : NoZeroSMulDivisors T S'<VAR>f : S →ₐ[T] S'<VAR>h₀ : map (algebraMap T S') p = 0<GOAL>map (algebraMap T S) p = 0
<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 : R[X]<VAR>inst✝⁷ : CommRing T<VAR>S : Type u_1<VAR>S' : Type u_2<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : Algebra T S<VAR>inst✝³ : CommRing S'<VAR>inst✝² : IsDomain S'<VAR>inst✝¹ : Algebra T S'<VAR>inst✝ : NoZeroSMulDivisors T S'<VAR>f : S →ₐ[T] S'<VAR>h₀ : map (algebraMap T S') 0 = 0<GOAL>map (algebraMap T S) 0 = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑Y<VAR>hU : ↑U ⊆ Set.range ⇑f.base<GOAL>IsIso (f.c.app (op U))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : PresheafedSpace C<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑↑Y<VAR>hU : ↑U ⊆ Set.range ⇑f.base<VAR>this : U = ⋯.functor.obj ((Opens.map f.base).obj U)<GOAL>IsIso (f.c.app (op U))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a : α<VAR>s : Set α<GOAL>s.ncard ≤ (insert a s).ncard
<VAR>m n k : ℕ<GOAL>m.Coprime (n + m * k) ↔ m.Coprime n
<VAR>σ : Type u_1<VAR>M : Type u_2<VAR>w : σ → M<VAR>d : σ →₀ ℕ<GOAL>d.degree = (weight 1) d
<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>p q : R[X]<GOAL>(p + q).natDegree ≤ max p.natDegree q.natDegree
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : Cofix F → Cofix F → Prop<VAR>h' : ∀ (x : Cofix F), r x x<VAR>h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest<VAR>x✝ : Cofix F<VAR>x : (P F).M<VAR>y✝ : Cofix F<VAR>y : (P F).M<VAR>rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)<VAR>r' : (P F).M → (P F).M → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)<GOAL>Mcongr x y
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>r : Cofix F → Cofix F → Prop<VAR>h' : ∀ (x : Cofix F), r x x<VAR>h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest<VAR>x✝ : Cofix F<VAR>x : (P F).M<VAR>y✝ : Cofix F<VAR>y : (P F).M<VAR>rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)<VAR>r' : (P F).M → (P F).M → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)<VAR>this : IsPrecongr r'<GOAL>Mcongr x y
<VAR>α : Type u_1<VAR>M N : Matroid α<VAR>h : Disjoint M.E N.E<VAR>B : Set α<GOAL>(M.disjointSum N h).Base B ↔ M.Base (B ∩ M.E) ∧ N.Base (B ∩ N.E) ∧ B ⊆ M.E ∪ N.E
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b : α<VAR>s : Set α<VAR>a : α<VAR>ha : (Iio a).Nonempty<GOAL>interior (Ici a) = Ioi a
<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.HasLeftHomology<VAR>A : C<VAR>f₁ f₂ : S.leftHomology ⟶ A<GOAL>f₁ = f₂ ↔ S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : Nat.Prime (orderOf σ)<GOAL>∃ n, σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : Nat.Prime (orderOf σ)<GOAL>card σ.cycleType = card σ.cycleType - 1 + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>hσ : Nat.Prime (orderOf σ)<VAR>n : ℕ<VAR>hn : n ∈ σ.cycleType<GOAL>n = orderOf σ
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{u_2}<VAR>H : c.IsRegular<GOAL>0 < c.ord
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>c : Cardinal.{u_2}<VAR>H : c.IsRegular<GOAL>0 < c
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp (a - m • p) b = toIocMod hp a b - m • p
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : Lattice α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : ComplementedLattice α<VAR>h : IsCoatomic α<GOAL>IsStronglyAtomic α
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : Lattice α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : IsModularLattice α<VAR>inst✝ : ComplementedLattice α<VAR>h : IsAtomic α<GOAL>IsStronglyAtomic α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hn : IsPeriodicPt f (n + m) x<VAR>hm : IsPeriodicPt f m x<GOAL>IsPeriodicPt f n x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<VAR>hn : IsFixedPt (f^[n] ∘ f^[m]) x<VAR>hm : IsPeriodicPt f m x<GOAL>IsPeriodicPt f n x
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : Zero N<VAR>f g : α →₀ N<VAR>x✝ : α<GOAL>x✝ ∈ ↑(f.neLocus g) ↔ x✝ ∈ {x | f x ≠ g x}
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>a z : ℂ<VAR>hz : z ≠ 0<GOAL>(fun z => abs z ^ a.re) z = (fun z => Real.exp (a.re * Real.log (abs z))) z
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>hP : P.IsEquipartition<VAR>hu : u ∈ P.parts<GOAL>4 ^ P.parts.card * m ≤ u.card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>P : Finpartition univ<VAR>u : Finset α<VAR>ε : ℝ<VAR>hP : P.IsEquipartition<VAR>hu : u ∈ P.parts<GOAL>4 ^ P.parts.card * (Fintype.card α / P.parts.card / 4 ^ P.parts.card) ≤ u.card
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>h : x + ↑m ≤ f x<VAR>n : ℕ<GOAL>x + ↑n * ↑m ≤ (⇑f)^[n] x
<VAR>a✝ b✝ c p q : ℚ<VAR>a b : ℤ<VAR>ha : 0 ≤ a<VAR>hb✝ : 0 ≤ b<VAR>hb : 0 < b<GOAL>0 ≤ a /. b
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>3 * (eval P) W.polynomial = P 0 * (eval P) W.polynomialX + P 1 * (eval P) W.polynomialY + P 2 * (eval P) W.polynomialZ
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<VAR>P : Fin 3 → R<GOAL>3 * (P 1 ^ 2 * P 2 + W.a₁ * P 0 * P 1 * P 2 + W.a₃ * P 1 * P 2 ^ 2 - (P 0 ^ 3 + W.a₂ * P 0 ^ 2 * P 2 + W.a₄ * P 0 * P 2 ^ 2 + W.a₆ * P 2 ^ 3)) = P 0 * (W.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2)) + P 1 * (2 * P 1 * P 2 + W.a₁ * P 0 * P 2 + W.a₃ * P 2 ^ 2) + P 2 * (P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 - (W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2))
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w : V<VAR>e✝ : Sym2 V<VAR>inst✝ : DecidableEq V<VAR>v : V<VAR>e : Sym2 V<VAR>h : e ∈ G.incidenceSet v<GOAL>e ∈ G.incidenceSet (G.otherVertexOfIncident h)
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w : V<VAR>e✝ : Sym2 V<VAR>inst✝ : DecidableEq V<VAR>v : V<VAR>e : Sym2 V<VAR>h : e ∈ G.incidenceSet v<GOAL>G.otherVertexOfIncident h ∈ e
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>h : I ≤ J<GOAL>Tendsto (⇑(embedBox I J h)) (l.toFilteriUnion I ⊤) (l.toFilteriUnion J (Prepartition.single J I h))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>h : I ≤ J<GOAL>∀ (i : ℝ≥0), Tendsto (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I i ⊤) (⨆ c, l.toFilterDistortioniUnion J c (Prepartition.single J I h))
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c✝ c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>h : I ≤ J<VAR>c : ℝ≥0<VAR>π₀ : Prepartition J := Prepartition.single J I h<GOAL>Tendsto (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I c ⊤) (⨆ c, l.toFilterDistortioniUnion J c π₀)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c✝ c₁ c₂ : ℝ≥0<VAR>r r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>h : I ≤ J<VAR>c : ℝ≥0<VAR>π₀ : Prepartition J := Prepartition.single J I h<GOAL>Filter.map (⇑(embedBox I J h)) (l.toFilterDistortioniUnion I c ⊤) ≤ l.toFilterDistortioniUnion J (max c π₀.compl.distortion) π₀
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c✝ c₁ c₂ : ℝ≥0<VAR>r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>h : I ≤ J<VAR>c : ℝ≥0<VAR>π₀ : Prepartition J := Prepartition.single J I h<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hr : l.RCond r<GOAL>∃ ia, l.RCond ia ∧ ∀ x ∈ {π | l.MemBaseSet I c ia π ∧ π.iUnion = ⊤.iUnion}, (embedBox I J h) x ∈ {π | l.MemBaseSet J (max c π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c✝ c₁ c₂ : ℝ≥0<VAR>r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π✝ π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>h : I ≤ J<VAR>c : ℝ≥0<VAR>π₀ : Prepartition J := Prepartition.single J I h<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hr : l.RCond r<VAR>π : TaggedPrepartition I<VAR>hπ : π ∈ {π | l.MemBaseSet I c r π ∧ π.iUnion = ⊤.iUnion}<GOAL>(embedBox I J h) π ∈ {π | l.MemBaseSet J (max c π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c✝ c₁ c₂ : ℝ≥0<VAR>r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π✝ π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>h : I ≤ J<VAR>c : ℝ≥0<VAR>π₀ : Prepartition J := Prepartition.single J I h<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hr : l.RCond r<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I<GOAL>(embedBox I J h) π ∈ {π | l.MemBaseSet J (max c π₀.compl.distortion) r π ∧ π.iUnion = π₀.iUnion}
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c✝ c₁ c₂ : ℝ≥0<VAR>r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π✝ π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>h : I ≤ J<VAR>c : ℝ≥0<VAR>π₀ : Prepartition J := Prepartition.single J I h<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hr : l.RCond r<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I<VAR>x✝ : l.bDistortion = true<GOAL>∃ π', π'.iUnion = ↑J \ ((embedBox I J h) π).iUnion ∧ π'.distortion ≤ max c π₀.compl.distortion
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>I J : Box ι<VAR>c✝ c₁ c₂ : ℝ≥0<VAR>r✝ r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>π✝ π₁ π₂ : TaggedPrepartition I<VAR>l✝ l₁ l₂ l : IntegrationParams<VAR>h : I ≤ J<VAR>c : ℝ≥0<VAR>π₀ : Prepartition J := Prepartition.single J I h<VAR>r : (ι → ℝ) → ↑(Set.Ioi 0)<VAR>hr : l.RCond r<VAR>π : TaggedPrepartition I<VAR>hπ : l.MemBaseSet I c r π ∧ π.iUnion = ↑I<GOAL>((embedBox I J h) π).iUnion = π₀.iUnion