ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>U : Opens ↑X<VAR>inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.val)<GOAL>IsIso ((forget C).map (f.val.app (op 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>U : Opens ↑X<VAR>inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.val)<GOAL>Function.Bijective ((forget C).map (f.val.app (op 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>U : Opens ↑X<VAR>inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.val)<GOAL>∀ (x : ↥U), Function.Bijective ⇑((stalkFunctor C ↑x).map f.val)
<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>U : Opens ↑X<VAR>inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.val)<VAR>x : ↥U<GOAL>Function.Bijective ⇑((stalkFunctor C ↑x).map f.val)
<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>U : Opens ↑X<VAR>inst✝ : ∀ (x : ↥U), IsIso ((stalkFunctor C ↑x).map f.val)<VAR>x : ↥U<GOAL>IsIso ⇑((stalkFunctor C ↑x).map f.val)
<VAR>R : Type u<VAR>S : Type u₁<VAR>T : Type u_1<VAR>inst✝⁸ : Monoid R<VAR>inst✝⁷ : Monoid S<VAR>inst✝⁶ : Monoid T<VAR>φ : R →* S<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w₁<VAR>inst✝⁵ : NonUnitalNonAssocSemiring A<VAR>inst✝⁴ : DistribMulAction R A<VAR>inst✝³ : NonUnitalNonAssocSemiring B<VAR>inst✝² : DistribMulAction S B<VAR>inst✝¹ : NonUnitalNonAssocSemiring C<VAR>inst✝ : DistribMulAction T C<VAR>f g : A →ₛₙₐ[φ] B<VAR>h : ↑f = ↑g<VAR>a : A<GOAL>f a = g a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f✝ g : α → E<VAR>s✝ t : Set α<VAR>μ✝ ν : Measure α<VAR>inst✝ : MeasurableSpace β<VAR>e : α → β<VAR>he : MeasurableEmbedding e<VAR>f : β → E<VAR>μ : Measure β<VAR>s : Set β<VAR>hs : s ⊆ range e<GOAL>IntegrableOn f s μ ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) (Measure.comap e μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f g : α → β<VAR>M : Type u_5<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>m : MeasurableSpace α<VAR>l✝ : Multiset (α → M)<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ Quot.mk Setoid.r l, StronglyMeasurable f<GOAL>StronglyMeasurable (Multiset.prod (Quot.mk Setoid.r l))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ : List α<VAR>a : α<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<GOAL>Forall₂ r ∘r Perm = Perm ∘r Forall₂ r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁✝ l₂ : List α<VAR>a : α<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>l₁ : List α<VAR>l₃ : List β<GOAL>(Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃
<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<GOAL>0 ⧏ (mk xl xr xL xR).inv'
<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<GOAL>0 = invVal (fun i => xL ↑i) xR (fun i => (xL ↑i).inv') (fun i => (xR i).inv') (mk xl xr xL xR) InvTy.zero
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>κ : Type u_1<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>h : κ → ι<VAR>h' : ι → κ<VAR>hh' : Function.LeftInverse h' h<VAR>f g : Π₀ (i : ι), β i<VAR>i✝ : κ<GOAL>(comapDomain' h hh' (f + g)) i✝ = (comapDomain' h hh' f + comapDomain' h hh' g) i✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>f✝ g✝ : α → β<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : PseudoMetrizableSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : _root_.Embedding g<VAR>this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ<VAR>this✝³ : MeasurableSpace β := borel β<VAR>this✝² : BorelSpace β<VAR>this✝¹ : MeasurableSpace γ := borel γ<VAR>this✝ : BorelSpace γ<GOAL>(StronglyMeasurable fun x => g (f x)) ↔ StronglyMeasurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>f✝ g✝ : α → β<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : PseudoMetrizableSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : _root_.Embedding g<VAR>this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ<VAR>this✝³ : MeasurableSpace β := borel β<VAR>this✝² : BorelSpace β<VAR>this✝¹ : MeasurableSpace γ := borel γ<VAR>this✝ : BorelSpace γ<VAR>H : StronglyMeasurable fun x => g (f x)<GOAL>Measurable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>f✝ g✝ : α → β<VAR>m : MeasurableSpace α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : PseudoMetrizableSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : PseudoMetrizableSpace γ<VAR>g : β → γ<VAR>f : α → β<VAR>hg : _root_.Embedding g<VAR>this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ<VAR>this✝³ : MeasurableSpace β := borel β<VAR>this✝² : BorelSpace β<VAR>this✝¹ : MeasurableSpace γ := borel γ<VAR>this✝ : BorelSpace γ<VAR>H : StronglyMeasurable fun x => g (f x)<GOAL>IsSeparable (range f)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>j : n<VAR>c : n → R<GOAL>(A.updateRow j (∑ k : n, c k • A k)).det = c j • A.det
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>A : Matrix n n R<VAR>j : n<VAR>c : n → R<GOAL>∑ k : n, c k • A k = c j • A j + ∑ k ∈ univ.erase j, c k • A k
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonUnitalNonAssocSemiring α<VAR>inst✝ : Fintype n<VAR>L : Matrix m n α<VAR>M N : Matrix n o α<VAR>i✝ : m<VAR>j✝ : o<GOAL>(L * (M + N)) i✝ j✝ = (L * M + L * N) i✝ j✝
<VAR>k : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type v<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Semiring α<VAR>f : m ≃ m<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>(f.toPEquiv.toMatrix * M) i j = M.submatrix (⇑f) id i j
<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>F : Presheaf C X<VAR>U V : Opens ↑X<VAR>x : ↑X<VAR>mU : x ∈ U<VAR>mV : x ∈ V<VAR>s : (forget C).obj (F.obj (op U))<VAR>t : (forget C).obj (F.obj (op V))<VAR>h : (F.germ ⟨x, mU⟩) s = (F.germ ⟨x, mV⟩) t<GOAL>∃ W, ∃ (_ : x ∈ W), ∃ iU iV, (F.map iU.op) s = (F.map iV.op) t
<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>F : Presheaf C X<VAR>U V : Opens ↑X<VAR>x : ↑X<VAR>mU : x ∈ U<VAR>mV : x ∈ V<VAR>s : (forget C).obj (F.obj (op U))<VAR>t : (forget C).obj (F.obj (op V))<VAR>h : (F.germ ⟨x, mU⟩) s = (F.germ ⟨x, mV⟩) t<VAR>W : (OpenNhds x)ᵒᵖ<VAR>iU : op { obj := U, property := ⋯ } ⟶ W<VAR>iV : op { obj := V, property := ⋯ } ⟶ W<VAR>e : (((OpenNhds.inclusion x).op ⋙ F) ⋙ forget C).map iU s = (((OpenNhds.inclusion x).op ⋙ F) ⋙ forget C).map iV t<GOAL>∃ W, ∃ (_ : x ∈ W), ∃ iU iV, (F.map iU.op) s = (F.map iV.op) t
<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>α : Type u_3<VAR>inst✝ : AddCommMonoid α<VAR>n : ℕ<VAR>f : PointsWithCircumcenterIndex n → α<VAR>h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)<GOAL>∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f ((pointIndexEmbedding n) i) + f circumcenterIndex
<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>α : Type u_3<VAR>inst✝ : AddCommMonoid α<VAR>n : ℕ<VAR>f : PointsWithCircumcenterIndex n → α<VAR>h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)<GOAL>circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ
<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>α : Type u_3<VAR>inst✝ : AddCommMonoid α<VAR>n : ℕ<VAR>f : PointsWithCircumcenterIndex n → α<VAR>h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)<GOAL>∀ (x : Fin (n + 1)), ¬(x ∈ univ ∧ (pointIndexEmbedding n) x = circumcenterIndex)
<VAR>α : Type u<VAR>l l' : List α<VAR>n : ℕ<GOAL>l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)
<VAR>α : Type u<VAR>l l' : List α<VAR>n : ℕ<GOAL>l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
<VAR>α : Type u<VAR>l l' : List α<VAR>n : ℕ<VAR>hl : 0 = l'.length<GOAL>l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
<VAR>α : Type u<VAR>l l' : List α<VAR>n : ℕ<VAR>hl : 0 < l'.length<GOAL>l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : InfSet α<VAR>inst✝¹ : InfSet β<VAR>inst✝ : sInfHomClass F α β<VAR>f : F<VAR>g : (i : ι) → κ i → α<GOAL>f (⨅ i, ⨅ j, g i j) = ⨅ i, ⨅ j, f (g i j)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<GOAL>q * p %ₘ q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>hq : q.Monic<GOAL>q ∣ q * p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝² : Algebra R S₁<VAR>inst✝¹ : CommSemiring S₂<VAR>f : σ → S₁<VAR>B : Type u_2<VAR>inst✝ : CommSemiring B<VAR>g : σ → S₁<VAR>φ : S₁ →+* B<VAR>p : MvPolynomial σ R<GOAL>φ ((aeval g) p) = (eval₂Hom (φ.comp (algebraMap R S₁)) fun i => φ (g i)) p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>inst✝² : Algebra R S₁<VAR>inst✝¹ : CommSemiring S₂<VAR>f : σ → S₁<VAR>B : Type u_2<VAR>inst✝ : CommSemiring B<VAR>g : σ → S₁<VAR>φ : S₁ →+* B<VAR>p : MvPolynomial σ R<GOAL>φ ((aeval g) p) = (φ.comp (eval₂Hom (algebraMap R S₁) g)) p
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>X : C<GOAL>F.map (ρ_ X).hom = inv (F.μ X (𝟙_ C)) ≫ F.obj X ◁ inv F.ε ≫ (ρ_ (F.obj X)).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>X : C<GOAL>F.map (ρ_ X).hom = inv (F.μ X (𝟙_ C)) ≫ F.obj X ◁ inv F.ε ≫ F.obj X ◁ F.ε ≫ F.μ X (𝟙_ C) ≫ F.map (ρ_ X).hom
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : MonoidalFunctor C D<VAR>X : C<GOAL>F.map (ρ_ X).hom = inv (F.μ X (𝟙_ C)) ≫ (𝟙 (F.obj X ⊗ F.obj (𝟙_ C)) ≫ F.μ X (𝟙_ C)) ≫ F.map (ρ_ X).hom
<VAR>a b c d✝ m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hcb : c ∣ b<VAR>h : a ∣ b / c<VAR>d : ℕ<VAR>hd : b / c = a * d<GOAL>b = c * a * d
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>a₁ a₂ : A<VAR>h : (Algebra.lmul R A) a₁ = (Algebra.lmul R A) a₂<GOAL>a₁ = a₂
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>IsLieAbelian ↥↑(D k I) ↔ D (k + 1) I = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : Nonempty α<VAR>h₀ : G.FarFromTriangleFree ε<VAR>h₁ : G.CliqueFree 3<GOAL>ε ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : Nonempty α<VAR>h₀ : G.FarFromTriangleFree ε<VAR>h₁ : G.CliqueFree 3<VAR>this : (fun H => H.CliqueFree 3) (G.deleteEdges ↑∅) → ε * ↑(Fintype.card α ^ 2) ≤ ↑∅.card<GOAL>ε ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : LinearOrderedField 𝕜<VAR>G H : SimpleGraph α<VAR>ε δ : 𝕜<VAR>n : ℕ<VAR>s : Finset α<VAR>inst✝³ : Fintype α<VAR>inst✝² : DecidableRel G.Adj<VAR>inst✝¹ : DecidableRel H.Adj<VAR>inst✝ : Nonempty α<VAR>h₀ : G.FarFromTriangleFree ε<VAR>h₁ : G.CliqueFree 3<VAR>this : (fun H => H.CliqueFree 3) G → ε * ↑(Fintype.card α ^ 2) ≤ 0<GOAL>ε ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Lattice α<VAR>inst✝² : Group α<VAR>a✝ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁺ᵐ * a⁻ᵐ = mabs a
<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✝ : TopologicalSpace β<VAR>s : Set α<VAR>H : IsPreconnected s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>u v : Set β<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : f '' s ⊆ u ∪ v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : f x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : f y ∈ v<GOAL>(f '' 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✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>H : IsPreconnected s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>u v : Set β<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : f '' s ⊆ u ∪ v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : f x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : f y ∈ v<VAR>u' : Set α<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<GOAL>(f '' 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✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>H : IsPreconnected s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>u v : Set β<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : f '' s ⊆ u ∪ v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : f x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : f y ∈ v<VAR>u' : Set α<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<VAR>v' : Set α<VAR>hv' : IsOpen v'<VAR>v'_eq : f ⁻¹' v ∩ s = v' ∩ s<GOAL>(f '' 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✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>H : IsPreconnected s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>u v : Set β<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : f x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : f y ∈ v<VAR>u' : Set α<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<VAR>v' : Set α<VAR>hv' : IsOpen v'<VAR>v'_eq : f ⁻¹' v ∩ s = v' ∩ s<VAR>huv : s ⊆ u' ∪ v'<GOAL>(f '' 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✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>H : IsPreconnected s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>u v : Set β<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : f x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : f y ∈ v<VAR>u' : Set α<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<VAR>v' : Set α<VAR>hv' : IsOpen v'<VAR>v'_eq : f ⁻¹' v ∩ s = v' ∩ s<VAR>huv : s ⊆ u' ∪ v'<VAR>z : α<VAR>hz : z ∈ s ∩ (u' ∩ v')<GOAL>(f '' 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✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set α<VAR>H : IsPreconnected s<VAR>f : α → β<VAR>hf : ContinuousOn f s<VAR>u v : Set β<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>x : α<VAR>xs : x ∈ s<VAR>xu : f x ∈ u<VAR>y : α<VAR>ys : y ∈ s<VAR>yv : f y ∈ v<VAR>u' : Set α<VAR>hu' : IsOpen u'<VAR>u'_eq : f ⁻¹' u ∩ s = u' ∩ s<VAR>v' : Set α<VAR>hv' : IsOpen v'<VAR>v'_eq : f ⁻¹' v ∩ s = v' ∩ s<VAR>huv : s ⊆ u' ∪ v'<VAR>z : α<VAR>hz : z ∈ f ⁻¹' u ∩ s ∩ (f ⁻¹' v ∩ s)<GOAL>(f '' s ∩ (u ∩ v)).Nonempty
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>a : ℝ<VAR>b : ℝ≥0<VAR>ha : 0 ≤ a<GOAL>a < (↑b).toReal ↔ a < ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : CommMonoid β<VAR>s t : Multiset α<VAR>a✝ : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>a b : α<GOAL>{a, b}.prod = a * b
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Semiring R✝<VAR>r✝ : R✝<VAR>f✝ : R✝[X]<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>r : R<VAR>f : R[X]<VAR>s : R<GOAL>eval (s - r) ((taylor r) f) = eval s f
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>g : G<VAR>a : α<VAR>h : G<GOAL>h ∈ stabilizer G (g • a) ↔ h ∈ Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) (stabilizer G a)
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b : α<VAR>inst✝ : Invertible a<GOAL>a * (⅟a * b) = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>L L' : List (List α)<VAR>join_eq : L.join = L'.join<VAR>length_eq : map length L = map length L'<GOAL>L = L'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>L L' : List (List α)<VAR>join_eq : L.join = L'.join<VAR>length_eq : map length L = map length L'<GOAL>L.length = L'.length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>L L' : List (List α)<VAR>join_eq : L.join = L'.join<VAR>length_eq : map length L = map length L'<GOAL>∀ (n : ℕ) (h₁ : n < L.length) (h₂ : n < L'.length), L[n] = L'[n]
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>ι : Type u_5<VAR>ιₘ : Type u_6<VAR>inst✝¹⁷ : CommRing R<VAR>inst✝¹⁶ : Nontrivial R<VAR>inst✝¹⁵ : CommRing A<VAR>inst✝¹⁴ : Algebra R A<VAR>inst✝¹³ : LieRing L<VAR>inst✝¹² : LieAlgebra R L<VAR>inst✝¹¹ : Module.Finite R L<VAR>inst✝¹⁰ : Module.Free R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : LieRingModule L M<VAR>inst✝⁶ : LieModule R L M<VAR>inst✝⁵ : Module.Finite R M<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Fintype ι<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Fintype ιₘ<VAR>inst✝ : DecidableEq ιₘ<VAR>b : Basis ι R L<VAR>bₘ : Basis ιₘ R M<VAR>x : L<GOAL>rank R L M = ((↑(toEnd R L M)).polyCharpoly b).natTrailingDegree
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>n : ℕ<VAR>r : R<VAR>i : ℕ<GOAL>((hasseDeriv k) ((monomial n) r)).coeff i = ((monomial (n - k)) (↑(n.choose k) * r)).coeff i
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>n : ℕ<VAR>r : R<VAR>i : ℕ<GOAL>(↑((i + k).choose k) * if n = i + k then r else 0) = if n - k = i then ↑(n.choose k) * r else 0
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>F : Cᵒᵖ ⥤ Type v₁<VAR>f : yoneda.obj X ⟶ F<VAR>g : Y ⟶ X<GOAL>(f.app (op X) ≫ F.map g.op) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>F : Cᵒᵖ ⥤ Type v₁<VAR>f : yoneda.obj X ⟶ F<VAR>g : Y ⟶ X<GOAL>((yoneda.obj X).map g.op ≫ f.app (op Y)) (𝟙 X) = f.app (op Y) (𝟙 Y ≫ g)
<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>a : α<GOAL>∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}
<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 b : α<GOAL>Ico a b ⊆ closure (interior (Ico a b))
<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>K : Type u_4<VAR>inst✝² : IsLocalization M S<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors S<VAR>hM : M ≤ nonZeroDivisors R<VAR>x : S<VAR>hx : x ≠ 0<GOAL>(sec M x).1 ≠ 0
<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>K : Type u_4<VAR>inst✝² : IsLocalization M S<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors S<VAR>hM : M ≤ nonZeroDivisors R<VAR>x : S<VAR>hx : x ≠ 0<VAR>hsec : x * (algebraMap R S) ↑(sec M x).2 = (algebraMap R S) (sec M x).1<GOAL>(sec M x).1 ≠ 0
<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>K : Type u_4<VAR>inst✝² : IsLocalization M S<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors S<VAR>hM : M ≤ nonZeroDivisors R<VAR>x : S<VAR>hx : x ≠ 0<VAR>hsec : x * (algebraMap R S) ↑(sec M x).2 = (algebraMap R S) (sec M x).1<VAR>hfst : (sec M x).1 = 0<GOAL>False
<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>K : Type u_4<VAR>inst✝² : IsLocalization M S<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors S<VAR>hM : M ≤ nonZeroDivisors R<VAR>x : S<VAR>hx : x ≠ 0<VAR>hsec : x = 0 ∨ ↑(sec M x).2 = 0<VAR>hfst : (sec M x).1 = 0<GOAL>False
<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>K : Type u_4<VAR>inst✝² : IsLocalization M S<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : NoZeroDivisors S<VAR>hM : M ≤ nonZeroDivisors R<VAR>x : S<VAR>hx : x ≠ 0<VAR>hsec : x = 0 ∨ (algebraMap R S) ↑(sec M x).2 = 0<VAR>hfst : (sec M x).1 = 0<GOAL>Injective ⇑(algebraMap R S)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>inst✝ : H.Normal<VAR>x : G<VAR>n : ℕ<VAR>hxn : x ∈ lowerCentralSeries G n<VAR>g : G<GOAL>x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)
<VAR>n p : ℕ<VAR>h : p ∈ n.primeFactorsList<GOAL>p ≤ n
<VAR>p : ℕ<VAR>h : p ∈ primeFactorsList 0<GOAL>p ≤ 0
<VAR>n p : ℕ<VAR>h : p ∈ n.primeFactorsList<VAR>hn : n > 0<GOAL>p ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid β<VAR>f : Fin 2 → β<GOAL>∏ i : Fin 2, f i = f 0 * f 1