ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<VAR>l l' : List ι<VAR>hl : l.Perm l'<VAR>hs : ∀ i ∈ l, s i ≠ 0<VAR>co : List.Pairwise (Coprime on s) l<VAR>z : { k // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯<GOAL>↑(chineseRemainderOfList a s l co) = ↑(chineseRemainderOfList a s l' ⋯)
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<VAR>l l' : List ι<VAR>hl : l.Perm l'<VAR>hs : ∀ i ∈ l, s i ≠ 0<VAR>co : List.Pairwise (Coprime on s) l<VAR>z : { k // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯<VAR>hlp : (List.map s l).prod = (List.map s l').prod<GOAL>↑(chineseRemainderOfList a s l co) = ↑(chineseRemainderOfList a s l' ⋯)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f : ι → ℝ≥0<VAR>n : ℕ<GOAL>↑(∑ x ∈ s, f x) ^ (n + 1) / ↑s.card ^ n ≤ ↑(∑ x ∈ s, f x ^ (n + 1))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_6, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>E : Type u_3<VAR>inst✝¹ : Category.{u_5, u_3} E<VAR>inst✝ : L.IsLocalization W<VAR>F : C ⥤ E<VAR>F' : D ⥤ E<VAR>h : Lifting L W F F'<VAR>X : C<GOAL>(liftNatTrans L W F F F' F' (𝟙 F)).app (L.obj X) = (𝟙 F').app (L.obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_6, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>E : Type u_3<VAR>inst✝¹ : Category.{u_5, u_3} E<VAR>inst✝ : L.IsLocalization W<VAR>F : C ⥤ E<VAR>F' : D ⥤ E<VAR>h : Lifting L W F F'<VAR>X : C<GOAL>𝟙 ((L ⋙ F').obj X) = 𝟙 (F'.obj (L.obj X))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>n : ℤ<GOAL>‖x‖ < ↑p ^ n ↔ ‖x‖ ≤ ↑p ^ (n - 1)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>h : 𝓝[s \ {x}] x = ⊥<GOAL>derivWithin f s x = 0
<VAR>p q✝ : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>q : ℚ≥0<GOAL>↑q * ↑q.den = ↑q.num
<VAR>p q✝ : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>q : ℚ≥0<GOAL>↑q * ↑↑(↑q).den = ↑(↑q).num
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite G<GOAL>IsPGroup p G ↔ ∃ n, Nat.card G = p ^ n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite G<VAR>hG : Nat.card G ≠ 0<GOAL>IsPGroup p G ↔ ∃ n, Nat.card G = p ^ n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite G<VAR>hG : Nat.card G ≠ 0<VAR>h : IsPGroup p G<GOAL>∃ n, Nat.card G = p ^ n
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite G<VAR>hG : Nat.card G ≠ 0<VAR>h : IsPGroup p G<GOAL>∀ q ∈ (Nat.card G).primeFactorsList, q = p
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite G<VAR>hG : Nat.card G ≠ 0<VAR>h : IsPGroup p G<VAR>q : ℕ<VAR>hq : q ∈ (Nat.card G).primeFactorsList<GOAL>q = p
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite G<VAR>hG : Nat.card G ≠ 0<VAR>h : IsPGroup p G<VAR>q : ℕ<VAR>hq : q ∈ (Nat.card G).primeFactorsList<VAR>hq1 : Nat.Prime q<VAR>hq2 : q ∣ Nat.card G<GOAL>q = p
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite G<VAR>hG : Nat.card G ≠ 0<VAR>h : IsPGroup p G<VAR>q : ℕ<VAR>hq : q ∈ (Nat.card G).primeFactorsList<VAR>hq1 : Nat.Prime q<VAR>hq2 : q ∣ Nat.card G<VAR>this : Fact (Nat.Prime q)<GOAL>q = p
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite G<VAR>hG : Nat.card G ≠ 0<VAR>h : IsPGroup p G<VAR>q : ℕ<VAR>hq : q ∈ (Nat.card G).primeFactorsList<VAR>hq1 : Nat.Prime q<VAR>hq2 : q ∣ Nat.card G<VAR>this : Fact (Nat.Prime q)<VAR>g : G<VAR>hg : orderOf g = q<GOAL>q = p
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Finite G<VAR>hG : Nat.card G ≠ 0<VAR>h : IsPGroup p G<VAR>q : ℕ<VAR>hq : q ∈ (Nat.card G).primeFactorsList<VAR>hq1 : Nat.Prime q<VAR>hq2 : q ∣ Nat.card G<VAR>this : Fact (Nat.Prime q)<VAR>g : G<VAR>hg : orderOf g = q<VAR>k : ℕ<VAR>hk : orderOf g = p ^ k<GOAL>q = p
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝² : Ring R<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Ring S<VAR>r : S<GOAL>(X - C r).leadingCoeff = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s t : Set α<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>x : α<VAR>hx : x ∈ Icc a b ∩ s<VAR>y : α<VAR>hy : y ∈ Icc a b ∩ t<GOAL>(Icc a b ∩ (s ∩ t)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s t : Set α<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>x : α<VAR>hx : x ∈ Icc a b ∩ s<VAR>y : α<VAR>hy : y ∈ Icc a b ∩ t<VAR>h : x ≤ y<GOAL>(Icc a b ∩ (s ∩ t)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b : α<VAR>s t : Set α<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>x : α<VAR>hx : x ∈ Icc a b ∩ s<VAR>y : α<VAR>hy : y ∈ Icc a b ∩ t<VAR>h : y ≤ x<GOAL>(Icc a b ∩ (s ∩ t)).Nonempty
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<GOAL>LipschitzWith 1 negPart
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f : (x : α) → p x → β<VAR>g : (x : α) → ¬p x → β<VAR>x : { x // x ∈ filter p s }<GOAL>p ↑x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f : (x : α) → p x → β<VAR>g : (x : α) → ¬p x → β<VAR>x : { x // x ∈ filter (fun x => ¬p x) s }<GOAL>¬p ↑x
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>s : Finset α<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f : (x : α) → p x → β<VAR>g : (x : α) → ¬p x → β<GOAL>(∏ x ∈ s, if hx : p x then f x hx else g x hx) = (∏ x ∈ (filter p s).attach, f ↑x ⋯) * ∏ x ∈ (filter (fun x => ¬p x) s).attach, g ↑x ⋯
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<VAR>m n : ℕ<GOAL>x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<GOAL>a / 1 = a
<VAR>a b : ℝ≥0<VAR>h : a < b<GOAL>a / b < 1
<VAR>a b : ℝ≥0<VAR>h : a < b<GOAL>b ≠ 0
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>p : α<VAR>hp : p ≠ 0<GOAL>(span {p}).IsPrime ↔ Prime p
<VAR>α : Type u_1<VAR>l l₁✝ l₂✝ : List α<VAR>p : α → Prop<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>b : α<VAR>l₁ l₂ : List α<GOAL>(b :: l₁).bagInter l₂ <+ b :: l₁
<VAR>α : Type u_1<VAR>l l₁✝ l₂✝ : List α<VAR>p : α → Prop<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>b : α<VAR>l₁ l₂ : List α<VAR>h : b ∈ l₂<GOAL>b :: l₁.bagInter (l₂.erase b) <+ b :: l₁
<VAR>α : Type u_1<VAR>l l₁✝ l₂✝ : List α<VAR>p : α → Prop<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>b : α<VAR>l₁ l₂ : List α<VAR>h : ¬b ∈ l₂<GOAL>l₁.bagInter l₂ <+ b :: l₁
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<VAR>f : σ → τ<VAR>h : Injective f<GOAL>((rename f) p).degrees = Multiset.map f p.degrees
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : Q.degree < P.degree<VAR>hneg : P.leadingCoeff / Q.leadingCoeff < 0<GOAL>Tendsto (fun x => eval x P / eval x Q) atTop atBot
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : Q.degree < P.degree<VAR>hneg : P.leadingCoeff / Q.leadingCoeff < 0<VAR>hQ : Q ≠ 0<GOAL>Tendsto (fun x => eval x P / eval x Q) atTop atBot
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : Q.natDegree < P.natDegree<VAR>hneg : P.leadingCoeff / Q.leadingCoeff < 0<VAR>hQ : Q ≠ 0<GOAL>Tendsto (fun x => eval x P / eval x Q) atTop atBot
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : Q.natDegree < P.natDegree<VAR>hneg : P.leadingCoeff / Q.leadingCoeff < 0<VAR>hQ : Q ≠ 0<GOAL>Tendsto (fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) atTop atBot
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : Q.natDegree < P.natDegree<VAR>hneg : P.leadingCoeff / Q.leadingCoeff < 0<VAR>hQ : Q ≠ 0<GOAL>Tendsto (fun x => x ^ (↑P.natDegree - ↑Q.natDegree)) atTop atTop
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : Q.natDegree < P.natDegree<VAR>hneg : P.leadingCoeff / Q.leadingCoeff < 0<VAR>hQ : Q ≠ 0<GOAL>0 < ↑P.natDegree - ↑Q.natDegree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>a ∈ Icc a b ↔ a ≤ b
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>L : IntermediateField F E<VAR>h : L ≤ separableClosure F E<VAR>x : ↥L<GOAL>IsSeparable F x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : OrderedCancelAddCommMonoid α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<GOAL>image (fun x => c + x) (Ioo a b) = Ioo (c + a) (c + b)
<VAR>a : ℤ<VAR>b p : ℕ<VAR>hp : p ∈ b.primeFactorsList<VAR>h₁✝ h₂ : Nat.Prime p<VAR>this : Fact (Nat.Prime p) := { out := h₂ }<GOAL>legendreSym p a = legendreSym p (a % ↑b)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>μ : Measure ℝ<VAR>u v ua va ub vb : ι → ℝ<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : FTCFilter a la la'<VAR>inst✝¹ : FTCFilter b lb lb'<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>hab : IntervalIntegrable f μ a b<VAR>hmeas : StronglyMeasurableAtFilter f la' μ<VAR>hf : Tendsto f (la' ⊓ ae μ) (𝓝 c)<VAR>hu : Tendsto u lt la<VAR>hv : Tendsto v lt la<GOAL>(fun t => ∫ (x : ℝ) in v t..b, f x ∂μ - ∫ (x : ℝ) in u t..b, f x ∂μ + ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt] fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
<VAR>E : Type u_1<VAR>inst✝ : MeasurableSpace E<VAR>m μ : Measure E<VAR>Ω : Type u_2<VAR>x✝ : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>X : Ω → E<VAR>s : Set E<VAR>hns : μ s ≠ 0<VAR>hnt : μ s ≠ ⊤<VAR>hu : IsUniform X s ℙ μ<VAR>A : Set E<VAR>hA : MeasurableSet A<GOAL>ℙ (X ⁻¹' A) = μ (s ∩ A) / μ s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsReflexive R M<VAR>e : N ≃ₗ[R] Dual R M<VAR>p : Submodule R M<VAR>x✝ : N<GOAL>x✝ ∈ (map e.flip p).dualCoannihilator ↔ x✝ ∈ map e.symm p.dualAnnihilator
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>D : I ⥤ C<VAR>F : C ⥤ Type u₂<VAR>inst✝¹ : HasColimit (D.op ⋙ coyoneda)<VAR>inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))<VAR>f : colimit (D.op ⋙ coyoneda) ⟶ F<VAR>i : I<GOAL>((colimitCoyonedaHomIsoLimit' D F).hom ≫ limit.π (D ⋙ F ⋙ uliftFunctor.{u₁, u₂}) i) f = { down := f.app (D.obj i) ((colimit.ι (D.op ⋙ coyoneda) (op i)).app (D.obj i) (𝟙 (D.obj i))) }
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>D : I ⥤ C<VAR>F : C ⥤ Type u₂<VAR>inst✝¹ : HasColimit (D.op ⋙ coyoneda)<VAR>inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))<VAR>f : colimit (D.op ⋙ coyoneda) ⟶ F<VAR>i : I<GOAL>((colimitHomIsoLimitYoneda' (D.op ⋙ coyoneda) F).hom ≫ limit.π ((D.op ⋙ coyoneda).rightOp ⋙ yoneda.obj F) i ≫ (isoWhiskerLeft (D ⋙ Prod.sectl C F) (coyonedaLemma C)).hom.app i) f = { down := f.app (D.obj i) ((colimit.ι (D.op ⋙ coyoneda) (op i)).app (D.obj i) (𝟙 (D.obj i))) }
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>D : I ⥤ C<VAR>F : C ⥤ Type u₂<VAR>inst✝¹ : HasColimit (D.op ⋙ coyoneda)<VAR>inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))<VAR>f : colimit (D.op ⋙ coyoneda) ⟶ F<VAR>i : I<GOAL>((coyoneda.map (colimit.ι (D.op ⋙ coyoneda) (op i)).op).app F ≫ (isoWhiskerLeft (D ⋙ Prod.sectl C F) (coyonedaLemma C)).hom.app i) f = { down := f.app (D.obj i) ((colimit.ι (D.op ⋙ coyoneda) (op i)).app (D.obj i) (𝟙 (D.obj i))) }
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>D : I ⥤ C<VAR>F : C ⥤ Type u₂<VAR>inst✝¹ : HasColimit (D.op ⋙ coyoneda)<VAR>inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))<VAR>f : colimit (D.op ⋙ coyoneda) ⟶ F<VAR>i : I<GOAL>Equiv.ulift.symm (coyonedaEquiv (colimit.ι (D.op ⋙ coyoneda) (op i) ≫ f)) = { down := f.app (D.obj i) ((colimit.ι (D.op ⋙ coyoneda) (op i)).app (D.obj i) (𝟙 (D.obj i))) }
<VAR>C : Type u₁<VAR>inst✝³ : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝² : Category.{v₂, v₁} I<VAR>D : I ⥤ C<VAR>F : C ⥤ Type u₂<VAR>inst✝¹ : HasColimit (D.op ⋙ coyoneda)<VAR>inst✝ : HasLimitsOfShape I (Type (max u₁ u₂))<VAR>f : colimit (D.op ⋙ coyoneda) ⟶ F<VAR>i : I<GOAL>Equiv.ulift.symm (f.app (D.obj i) ((colimit.ι (D.op ⋙ coyoneda) (op i)).app (D.obj i) (𝟙 (D.obj i)))) = { down := f.app (D.obj i) ((colimit.ι (D.op ⋙ coyoneda) (op i)).app (D.obj i) (𝟙 (D.obj i))) }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a✝ b✝ : α<VAR>f : β → α<VAR>a b : β<GOAL>⨆ x ∈ {a, b}, f x = f a ⊔ f b
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>h : ¬IsField R<GOAL>[DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime, Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) = 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>h : ¬IsField R<VAR>this : finrank (ResidueField R) (CotangentSpace R) = 1 ↔ finrank (ResidueField R) (CotangentSpace R) ≤ 1<GOAL>[DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime, Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) = 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>h : ¬IsField R<VAR>this : finrank (ResidueField R) (CotangentSpace R) = 1 ↔ finrank (ResidueField R) (CotangentSpace R) ≤ 1<GOAL>[DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime, Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) ≤ 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>h : ¬IsField R<VAR>this✝ : finrank (ResidueField R) (CotangentSpace R) = 1 ↔ finrank (ResidueField R) (CotangentSpace R) ≤ 1<VAR>this : maximalIdeal R ≠ ⊥<GOAL>[DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime, Submodule.IsPrincipal (maximalIdeal R), finrank (ResidueField R) (CotangentSpace R) ≤ 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n].TFAE
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>h : ¬IsField R<VAR>this✝ : finrank (ResidueField R) (CotangentSpace R) = 1 ↔ finrank (ResidueField R) (CotangentSpace R) ≤ 1<VAR>this : maximalIdeal R ≠ ⊥<GOAL>DiscreteValuationRing R ↔ IsPrincipalIdealRing R
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>K : Type u_2<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra R K<VAR>inst✝³ : IsFractionRing R K<VAR>inst✝² : IsNoetherianRing R<VAR>inst✝¹ : LocalRing R<VAR>inst✝ : IsDomain R<VAR>h : ¬IsField R<VAR>this✝ : finrank (ResidueField R) (CotangentSpace R) = 1 ↔ finrank (ResidueField R) (CotangentSpace R) ≤ 1<VAR>this : maximalIdeal R ≠ ⊥<GOAL>(∃! P, P ≠ ⊥ ∧ P.IsPrime) ↔ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β<VAR>inst✝ : Nonempty ι<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t<GOAL>(iInf f).lift g = ⨅ i, (f i).lift g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β<VAR>inst✝ : Nonempty ι<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t<VAR>s : Set β<GOAL>s ∈ (iInf f).lift g → s ∈ ⨅ i, (f i).lift g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β<VAR>inst✝ : Nonempty ι<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t<VAR>s : Set β<VAR>H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t<GOAL>s ∈ (iInf f).lift g → s ∈ ⨅ i, (f i).lift g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β<VAR>inst✝ : Nonempty ι<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t<VAR>s : Set β<VAR>H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t<GOAL>∀ x ∈ iInf f, s ∈ g x → s ∈ ⨅ i, (f i).lift g
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x y : M<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>SameRay R x y ∨ SameRay R x (-y) ↔ ¬LinearIndependent R ![x, y]
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>x y : M<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>SameRay R x y ∨ SameRay R x (-y) ↔ ∃ g, ∑ i : Fin (Nat.succ 0).succ, g i • ![x, y] i = 0 ∧ ∃ i, g i ≠ 0
<VAR>α✝ β : Type u<VAR>c : Cardinal.{?u.225789}<VAR>α : Type u_1<VAR>P Q : Set α<GOAL>#↑(P ∪ Q) ≤ ℵ₀ ↔ #↑P ≤ ℵ₀ ∧ #↑Q ≤ ℵ₀
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>p q : R[X]<VAR>inst✝ : Semiring S<VAR>hq : q.Monic<VAR>p₁ p₂ : R[X]<VAR>a✝ : Nontrivial R<VAR>f : R[X]<VAR>sub_eq : p₁ - p₂ = q * f<GOAL>p₁ %ₘ q = p₂ %ₘ q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>p q : R[X]<VAR>inst✝ : Semiring S<VAR>hq : q.Monic<VAR>p₁ p₂ : R[X]<VAR>a✝ : Nontrivial R<VAR>f : R[X]<VAR>sub_eq : p₁ - p₂ = q * f<GOAL>p₂ %ₘ q + q * (p₂ /ₘ q + f) = p₁
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<GOAL>MeasurableSet {x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<GOAL>MeasurableSet (⋂ e, ⋃ n, ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))
<VAR>F : Type u_1<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : ℝ → F<VAR>K✝ K : Set F<VAR>hK : IsComplete K<VAR>b✝⁵ b✝⁴ b✝³ : ℕ<VAR>b✝² : b✝³ ≥ b✝⁴<VAR>b✝¹ : ℕ<VAR>b✝ : b✝¹ ≥ b✝⁴<GOAL>MeasurableSet (B f K ((1 / 2) ^ b✝³) ((1 / 2) ^ b✝¹) ((1 / 2) ^ b✝⁵))
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a⁻¹ ≤ 1 ↔ 1 ≤ a
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>(a :: l).rotate 1 = l ++ [a]
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>s : Set R<GOAL>s ∈ 𝓝 0 ↔ ∃ γ, {x | v x < ↑γ} ⊆ s
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 ≤ z<GOAL>(x / y) ^ z = x ^ z / y ^ z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n i : ℕ<VAR>x : α<VAR>l : List α<GOAL>(i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l.get? (i - n) = some x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s : Set E<VAR>a b m : ℝ<VAR>x y : E<VAR>f g : E → ℝ<VAR>hf : UniformConvexOn s φ f<VAR>hφ : 0 ≤ φ<GOAL>ConvexOn ℝ s f
<VAR>x : ℝ<GOAL>DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1
<VAR>x : ℝ<VAR>h : DifferentiableWithinAt ℝ arcsin (Iic x) x<GOAL>x ≠ 1
<VAR>x : ℝ<VAR>h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)<GOAL>x ≠ 1
<VAR>x : ℝ<VAR>h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)<VAR>this : DifferentiableWithinAt ℝ (fun y => -(arcsin ∘ Neg.neg) y) (Ici (-x)) (-x)<GOAL>x ≠ 1
<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✝² : Finite ι<VAR>inst✝¹ : Ring 𝕜<VAR>inst✝ : DecidableEq ι<VAR>i : ι<GOAL>(basisFun p 𝕜 ι) i = (WithLp.equiv p (ι → 𝕜)).symm (Pi.single i 1)
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ<GOAL>p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ<VAR>hq : 0 < q - 1<GOAL>p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }
<VAR>K : Type u_1<VAR>σ : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁵ : Fintype K<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Fintype σ<VAR>inst✝² : DecidableEq σ<VAR>inst✝¹ : DecidableEq K<VAR>p : ℕ<VAR>inst✝ : CharP K p<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ K<VAR>h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ<VAR>hq : 0 < q - 1<VAR>S : Finset (σ → K) := {x | x ∈ univ ∧ ∀ i ∈ s, (eval x) (f i) = 0}.toFinset<GOAL>p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }