ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R✝ : Type u<VAR>A✝ : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R✝<VAR>inst✝¹⁵ : NonUnitalNonAssocSemiring A✝<VAR>inst✝¹⁴ : Module R✝ A✝<VAR>inst✝¹³ : Star A✝<VAR>inst✝¹² : NonUnitalNonAssocSemiring B<VAR>inst✝¹¹ : Module R✝ B<VAR>inst✝¹⁰ : Star B<VAR>inst✝⁹ : NonUnitalNonAssocSemiring C<VAR>inst✝⁸ : Module R✝ C<VAR>inst✝⁷ : Star C<VAR>inst✝⁶ : FunLike F A✝ B<VAR>inst✝⁵ : NonUnitalAlgHomClass F R✝ A✝ B<VAR>inst✝⁴ : NonUnitalStarAlgHomClass F R✝ A✝ B<VAR>S✝ : NonUnitalStarSubalgebra R✝ A✝<VAR>R : Type u<VAR>A : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : NonUnitalRing A<VAR>inst✝¹ : Module R A<VAR>inst✝ : Star A<VAR>S T : NonUnitalStarSubalgebra R A<VAR>h : S.toNonUnitalSubring = T.toNonUnitalSubring<VAR>x : A<GOAL>x ∈ S ↔ x ∈ T
<VAR>α : Type u<VAR>inst✝² : CommGroup α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a / b ≤ c / d ↔ a * d ≤ c * b
<VAR>c : CliffordAlgebra Q<GOAL>toComplex (involute c) = (starRingEnd ℂ) (toComplex c)
<VAR>c : CliffordAlgebra Q<VAR>this : toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))<GOAL>toComplex (involute c) = (starRingEnd ℂ) (toComplex c)
<VAR>c : CliffordAlgebra Q<VAR>this : toComplex (involute ((ι Q) 1)) = (starRingEnd ℂ) (toComplex ((ι Q) 1))<GOAL>toComplex.comp involute = (↑Complex.conjAe).comp toComplex
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r✝ : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>n : ℕ<VAR>r : R<GOAL>eval₂ f x ((monomial n) r) = f r * x ^ n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁷ : Preorder α<VAR>inst✝⁶ : Preorder β<VAR>inst✝⁵ : Preorder γ<VAR>inst✝⁴ : Preorder δ<VAR>inst✝³ : MulZeroOneClass α<VAR>inst✝² : MulZeroOneClass β<VAR>inst✝¹ : MulZeroOneClass γ<VAR>inst✝ : MulZeroOneClass δ<VAR>f g✝ : α →*₀o β<VAR>g : β →*₀o γ<VAR>f₁ f₂ : α →*₀o β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>R✝ : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R✝<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommRing R✝<VAR>p q : MvPolynomial σ R✝<VAR>inst✝ : CommRing S<VAR>f✝ : R✝ →+* S<VAR>g : σ → S<VAR>R : Type u<VAR>c : ℤ →+* S<VAR>f : MvPolynomial R ℤ →+* S<VAR>x : MvPolynomial R ℤ<GOAL>eval₂ c (⇑f ∘ X) x = f x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>β : Type u_5<VAR>mβ : MeasurableSpace β<VAR>f : α → β<VAR>g : β → E<VAR>hg : AEStronglyMeasurable g (Measure.map f μ)<VAR>hf : AEMeasurable f μ<GOAL>Memℒp g p (Measure.map f μ) ↔ Memℒp (g ∘ f) p μ
<VAR>α : Type u<VAR>l✝ l' l : List α<VAR>n : ℕ<VAR>h : n < l.cyclicPermutations.length<GOAL>l.cyclicPermutations[n] = l.rotate n
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁹ : DecidableEq α'<VAR>inst✝⁸ : DecidableEq β'<VAR>inst✝⁷ : DecidableEq γ<VAR>inst✝⁶ : DecidableEq γ'<VAR>inst✝⁵ : DecidableEq δ<VAR>inst✝⁴ : DecidableEq δ'<VAR>inst✝³ : DecidableEq ε<VAR>inst✝² : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<GOAL>image2 f (↑s ∩ ↑s') (↑t ∪ ↑t') ⊆ image2 f ↑s ↑t ∪ image2 f ↑s' ↑t'
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>inst✝¹ : Bifunctor F<VAR>inst✝ : LawfulBifunctor F<VAR>α : Type u₀<VAR>β₀ β₁ β₂ : Type u₁<VAR>g : β₀ → β₁<VAR>g' : β₁ → β₂<VAR>x : F α β₀<GOAL>snd g' (snd g x) = snd (g' ∘ g) x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : C ⥤ Type w<VAR>F : Cᵒᵖ ⥤ Type v<VAR>X Y : (CostructuredArrow yoneda F)ᵒᵖ<VAR>f : X ⟶ Y<GOAL>F.map f.unop.left.op ((fun X => ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩) X).snd = ((fun X => ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩) Y).snd
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : C ⥤ Type w<VAR>F : Cᵒᵖ ⥤ Type v<VAR>X Y : (CostructuredArrow yoneda F)ᵒᵖ<VAR>f : X ⟶ Y<VAR>e_1✝ : F.obj ((fun X => ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩) Y).fst = ((Functor.fromPUnit F).obj (unop X).right).obj (op (unop Y).left)<GOAL>((fun X => ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩) Y).snd = ((yoneda.obj (unop X).left).map f.unop.left.op ≫ (unop X).hom.app (op (unop Y).left)) (𝟙 (unop (op (unop X).left)))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : C ⥤ Type w<VAR>F : Cᵒᵖ ⥤ Type v<VAR>X Y : (CostructuredArrow yoneda F)ᵒᵖ<VAR>f : X ⟶ Y<VAR>e_1✝ : F.obj ((fun X => ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩) Y).fst = ((Functor.fromPUnit F).obj (unop X).right).obj (op (unop Y).left)<GOAL>(unop Y).hom.app (op (unop Y).left) (𝟙 (unop Y).left) = (unop X).hom.app (op (unop Y).left) f.unop.left
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : C ⥤ Type w<VAR>F : Cᵒᵖ ⥤ Type v<VAR>X Y : (CostructuredArrow yoneda F)ᵒᵖ<VAR>f : X ⟶ Y<VAR>e_1✝ : F.obj ((fun X => ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩) Y).fst = ((Functor.fromPUnit F).obj (unop X).right).obj (op (unop Y).left)<VAR>this : yoneda.map f.unop.left ≫ (unop X).hom = (unop Y).hom<GOAL>(unop Y).hom.app (op (unop Y).left) (𝟙 (unop Y).left) = (unop X).hom.app (op (unop Y).left) f.unop.left
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : C ⥤ Type w<VAR>F : Cᵒᵖ ⥤ Type v<VAR>X Y : (CostructuredArrow yoneda F)ᵒᵖ<VAR>f : X ⟶ Y<VAR>e_1✝ : F.obj ((fun X => ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩) Y).fst = ((Functor.fromPUnit F).obj (unop X).right).obj (op (unop Y).left)<VAR>this : yoneda.map f.unop.left ≫ (unop X).hom = (unop Y).hom<GOAL>(yoneda.map f.unop.left ≫ (unop X).hom).app (op (unop Y).left) (𝟙 (unop Y).left) = (unop X).hom.app (op (unop Y).left) f.unop.left
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : C ⥤ Type w<VAR>F : Cᵒᵖ ⥤ Type v<VAR>X Y : (CostructuredArrow yoneda F)ᵒᵖ<VAR>f : X ⟶ Y<VAR>e_1✝ : F.obj ((fun X => ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩) Y).fst = ((Functor.fromPUnit F).obj (unop X).right).obj (op (unop Y).left)<VAR>this : yoneda.map f.unop.left ≫ (unop X).hom = (unop Y).hom<GOAL>(unop X).hom.app (op (unop Y).left) (𝟙 (unop Y).left ≫ f.unop.left) = (unop X).hom.app (op (unop Y).left) f.unop.left
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Surjective ⇑f<GOAL>support R N ⊆ support R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p : PrimeSpectrum R<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommGroup P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Surjective ⇑f<GOAL>∀ (x : PrimeSpectrum R), (∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0
<VAR>x : ℤ[i]<GOAL>↑x.im = (toComplex x).im
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R : Sieve X<VAR>J : GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S : Sieve X<VAR>hf : S.arrows f<GOAL>J.Covers S f
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>S✝ R : Sieve X<VAR>J : GrothendieckTopology C<VAR>f : Y ⟶ X<VAR>S : Sieve X<VAR>hf : S.arrows f<GOAL>⊤ ∈ J.sieves Y
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>M : Type w'<VAR>inst✝ : L.Structure M<VAR>iM : Infinite M<VAR>κ : Cardinal.{w}<VAR>h1 : ℵ₀ ≤ κ<VAR>h2 : lift.{w, max u v} L.card ≤ lift.{max u v, w} κ<GOAL>∃ N, (Nonempty (↑N ↪ₑ[L] M) ∨ Nonempty (M ↪ₑ[L] ↑N)) ∧ #↑N = κ
<VAR>α : Type u_1<VAR>inst✝¹⁴ : Ring α<VAR>inst✝¹³ : UniformSpace α<VAR>inst✝¹² : TopologicalRing α<VAR>inst✝¹¹ : UniformAddGroup α<VAR>β : Type u<VAR>inst✝¹⁰ : UniformSpace β<VAR>inst✝⁹ : Ring β<VAR>inst✝⁸ : UniformAddGroup β<VAR>inst✝⁷ : TopologicalRing β<VAR>f : α →+* β<VAR>hf : Continuous ⇑f<VAR>A : Type u_2<VAR>inst✝⁶ : Ring A<VAR>inst✝⁵ : UniformSpace A<VAR>inst✝⁴ : UniformAddGroup A<VAR>inst✝³ : TopologicalRing A<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : UniformContinuousConstSMul R A<VAR>r : R<VAR>x : Completion A<GOAL>Completion.map (fun x => r • x) x = ↑A ((algebraMap R A) r) * x
<VAR>α : Type u_1<VAR>inst✝¹⁴ : Ring α<VAR>inst✝¹³ : UniformSpace α<VAR>inst✝¹² : TopologicalRing α<VAR>inst✝¹¹ : UniformAddGroup α<VAR>β : Type u<VAR>inst✝¹⁰ : UniformSpace β<VAR>inst✝⁹ : Ring β<VAR>inst✝⁸ : UniformAddGroup β<VAR>inst✝⁷ : TopologicalRing β<VAR>f : α →+* β<VAR>hf : Continuous ⇑f<VAR>A : Type u_2<VAR>inst✝⁶ : Ring A<VAR>inst✝⁵ : UniformSpace A<VAR>inst✝⁴ : UniformAddGroup A<VAR>inst✝³ : TopologicalRing A<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : UniformContinuousConstSMul R A<VAR>r : R<VAR>x : Completion A<GOAL>IsClosed {a | Completion.map (fun x => r • x) a = ↑A ((algebraMap R A) r) * a}
<VAR>α : Type u_1<VAR>inst✝¹⁴ : Ring α<VAR>inst✝¹³ : UniformSpace α<VAR>inst✝¹² : TopologicalRing α<VAR>inst✝¹¹ : UniformAddGroup α<VAR>β : Type u<VAR>inst✝¹⁰ : UniformSpace β<VAR>inst✝⁹ : Ring β<VAR>inst✝⁸ : UniformAddGroup β<VAR>inst✝⁷ : TopologicalRing β<VAR>f : α →+* β<VAR>hf : Continuous ⇑f<VAR>A : Type u_2<VAR>inst✝⁶ : Ring A<VAR>inst✝⁵ : UniformSpace A<VAR>inst✝⁴ : UniformAddGroup A<VAR>inst✝³ : TopologicalRing A<VAR>R : Type u_3<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : UniformContinuousConstSMul R A<VAR>r : R<VAR>x : Completion A<VAR>a : A<GOAL>Completion.map (fun x => r • x) (↑A a) = ↑A ((algebraMap R A) r) * ↑A a
<VAR>X : Scheme<VAR>inst✝ : IsAffine X<GOAL>IsAffineOpen ⊤
<VAR>X : Scheme<VAR>inst✝ : IsAffine X<GOAL>⊤ = Scheme.Hom.opensRange (𝟙 X)
<VAR>X : Scheme<VAR>inst✝ : IsAffine X<GOAL>↑⊤ = ↑(Scheme.Hom.opensRange (𝟙 X))
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>inst✝ : SemilatticeSup α<VAR>c : ClosureOperator α<VAR>x y : α<GOAL>c (c x ⊔ c y) = c (x ⊔ y)
<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>hs : ∀ (x : ↥L), IsSeparable F x<VAR>x : E<VAR>h : x ∈ L<GOAL>x ∈ separableClosure F E
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>x : K<GOAL>x ∈ ⨅ v, Localization.subalgebra.ofField K v.asIdeal.primeCompl ⋯ ↔ x ∈ ⊥
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDomain R<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>x : K<GOAL>(∀ (i : MaximalSpectrum R), x ∈ Localization.subalgebra.ofField K i.asIdeal.primeCompl ⋯) ↔ x ∈ range ⇑(algebraMap R K)
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝²⁰ : Semiring R₁<VAR>inst✝¹⁹ : Semiring R₂<VAR>inst✝¹⁸ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝¹⁷ : TopologicalSpace M₁<VAR>inst✝¹⁶ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace M'₁<VAR>inst✝¹⁴ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹³ : TopologicalSpace M₂<VAR>inst✝¹² : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : TopologicalSpace M₃<VAR>inst✝¹⁰ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝⁹ : TopologicalSpace M₄<VAR>inst✝⁸ : AddCommMonoid M₄<VAR>inst✝⁷ : Module R₁ M₁<VAR>inst✝⁶ : Module R₁ M'₁<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>F : Type u_9<VAR>inst✝² : Module R₁ M₂<VAR>inst✝¹ : TopologicalSpace R₁<VAR>inst✝ : ContinuousSMul R₁ M₂<VAR>c : R₁ →L[R₁] M₂<GOAL>(smulRight 1 (c 1)) 1 = c 1
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α✝ → α✝ → Prop<VAR>s : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u<VAR>f : α → Ordinal.{max u v}<VAR>g : β → Ordinal.{max u v}<VAR>h : range f ⊆ range g<GOAL>mex f ≤ mex g
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α✝ → α✝ → Prop<VAR>s : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u<VAR>f : α → Ordinal.{max u v}<VAR>g : β → Ordinal.{max u v}<VAR>h : range f ⊆ range g<VAR>i : α<VAR>hi : f i = mex g<GOAL>False
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α✝ → α✝ → Prop<VAR>s : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>α β : Type u<VAR>f : α → Ordinal.{max u v}<VAR>g : β → Ordinal.{max u v}<VAR>h : range f ⊆ range g<VAR>i : α<VAR>j : β<VAR>hi : g j = mex g<VAR>hj : g j = f i<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>k : ℕ<GOAL>(p ^ k).factors.prod = FactorSet.prod ↑(replicate k ⟨p, hp⟩)
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>k : ℕ<GOAL>p ^ k = match ↑(replicate k ⟨p, hp⟩) with | none => 0 | some s => (Multiset.map Subtype.val s).prod
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>inst✝ : Nontrivial α<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>k : ℕ<GOAL>p ^ k = (Multiset.map Subtype.val (replicate k ⟨p, hp⟩)).prod
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : abs z < ↑n<VAR>hn0 : 0 < ↑n<GOAL>abs z / ↑n < 1
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : abs z < ↑n<VAR>hn0 : 0 < ↑n<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>|abs (z ^ m.succ / ↑m.succ.factorial)| ≤ abs z / ↑n * |abs (z ^ m / ↑m.factorial)|
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : abs z < ↑n<VAR>hn0 : 0 < ↑n<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>abs z / ↑m.succ * abs (z ^ m / ↑m.factorial) ≤ abs z / ↑n * abs (z ^ m / ↑m.factorial)
<VAR>z : ℂ<VAR>n : ℕ<VAR>hn : abs z < ↑n<VAR>hn0 : 0 < ↑n<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>n ≤ m.succ
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>f : α ≃ α<VAR>Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s<VAR>mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs<VAR>A : Set α<GOAL>(inducedOuterMeasure m P0 m0) (⇑f ⁻¹' A) = (inducedOuterMeasure m P0 m0) A
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>f : α ≃ α<VAR>Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s<VAR>mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs<VAR>A : Set α<GOAL>⨅ t, ⨅ (ht : P t), ⨅ (_ : ⇑f ⁻¹' A ⊆ t), m t ht = ⨅ t, ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>f : α ≃ α<VAR>Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s<VAR>mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs<VAR>A : Set α<GOAL>⨅ t, ⨅ (ht : P t), ⨅ (_ : A ⊆ t), m t ht = ⨅ t, ⨅ (ht : P t), ⨅ (_ : ⇑f ⁻¹' A ⊆ t), m t ht
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>f : α ≃ α<VAR>Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s<VAR>mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs<VAR>A s : Set α<GOAL>⨅ (ht : P (⇑f ⁻¹' s)), ⨅ (_ : ⇑f ⁻¹' A ⊆ ⇑f ⁻¹' s), m (⇑f ⁻¹' s) ht = ⨅ (ht : P s), ⨅ (_ : A ⊆ s), m s ht
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>f : α ≃ α<VAR>Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s<VAR>mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs<VAR>A s : Set α<GOAL>∀ (x : P s), ⨅ (_ : ⇑f ⁻¹' A ⊆ ⇑f ⁻¹' s), m (⇑f ⁻¹' s) ⋯ = ⨅ (_ : A ⊆ s), m s x
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>f : α ≃ α<VAR>Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s<VAR>mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs<VAR>A s : Set α<VAR>hs : P s<GOAL>⨅ (_ : ⇑f ⁻¹' A ⊆ ⇑f ⁻¹' s), m (⇑f ⁻¹' s) ⋯ = ⨅ (_ : A ⊆ s), m s hs
<VAR>α : Type u_1<VAR>P : Set α → Prop<VAR>m : (s : Set α) → P s → ℝ≥0∞<VAR>P0 : P ∅<VAR>m0 : m ∅ P0 = 0<VAR>PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)<VAR>mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯<VAR>msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯<VAR>m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂<VAR>f : α ≃ α<VAR>Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s<VAR>mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs<VAR>A s : Set α<VAR>hs : P s<GOAL>A ⊆ s → m (⇑f ⁻¹' s) ⋯ = m s hs
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>hv : LinearIndependent R v<GOAL>LinearMap.ker hv.repr = ⊥
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>C : G.ComponentCompl K<VAR>c d : V<VAR>x✝ : c ∈ C<VAR>dnK : d ∉ K<VAR>cd : G.Adj c d<VAR>cnK : c ∉ K<VAR>h : G.componentComplMk cnK = C<GOAL>G.componentComplMk dnK = C
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>C : G.ComponentCompl K<VAR>c d : V<VAR>x✝ : c ∈ C<VAR>dnK : d ∉ K<VAR>cd : G.Adj c d<VAR>cnK : c ∉ K<VAR>h : G.componentComplMk cnK = C<GOAL>(induce Kᶜ G).Reachable ⟨d, dnK⟩ ⟨c, cnK⟩
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ p₄ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₃, p₄}<VAR>h₂ : p₂ ∈ affineSpan k {p₃, p₄}<GOAL>Collinear k {p₁, p₂, p₃, p₄}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p₁ p₂ p₃ p₄ : P<VAR>h₁ : p₁ ∈ affineSpan k {p₃, p₄}<VAR>h₂ : p₂ ∈ affineSpan k {p₃, p₄}<GOAL>Collinear k {p₃, p₄}
<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>i : ι<VAR>a : α<VAR>f✝ g : ι → α<VAR>inst✝¹ inst✝ : NonUnitalNonAssocSemiring α<VAR>s : Finset ι<VAR>f : ι → α<VAR>b✝ : α<VAR>h : ∀ i ∈ s, Commute b✝ (f i)<VAR>b : α<VAR>hb : b ∈ Multiset.map (fun i => f i) s.val<GOAL>Commute b✝ b
<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>i✝ : ι<VAR>a : α<VAR>f✝ g : ι → α<VAR>inst✝¹ inst✝ : NonUnitalNonAssocSemiring α<VAR>s : Finset ι<VAR>f : ι → α<VAR>b : α<VAR>h : ∀ i ∈ s, Commute b (f i)<VAR>i : ι<VAR>hi : i ∈ s.val<VAR>hb : f i ∈ Multiset.map (fun i => f i) s.val<GOAL>Commute b (f i)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>hna : IsNonarchimedean f<GOAL>IsNonarchimedean (seminormFromBounded' f)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>hna : IsNonarchimedean f<VAR>x y z : R<GOAL>f ((x + y) * z) / f z ≤ max (seminormFromBounded' f x) (seminormFromBounded' f y)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>hna : IsNonarchimedean f<VAR>x y z : R<GOAL>f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>m : ℕ<VAR>hm : m < hf.toFinset.card<VAR>n : ℕ<VAR>hn : n < hf.toFinset.card<VAR>h : m < n<GOAL>nth p m < nth p n
<VAR>p : ℕ → Prop<VAR>hf : (setOf p).Finite<VAR>m : ℕ<VAR>hm : m < hf.toFinset.card<VAR>n : ℕ<VAR>hn : n < hf.toFinset.card<VAR>h : m < n<GOAL>(⋯.toFinset.orderEmbOfFin ⋯) ⟨m, ⋯⟩ < (⋯.toFinset.orderEmbOfFin ⋯) ⟨n, ⋯⟩
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.Normal<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>inst✝¹ : (i : η) → Group (Gs i)<VAR>inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)<VAR>n : ℕ<VAR>h : ∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n<GOAL>Group.IsNilpotent ((i : η) → Gs i)
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.Normal<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>inst✝¹ : (i : η) → Group (Gs i)<VAR>inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)<VAR>n : ℕ<VAR>h : ∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n<GOAL>∃ n, lowerCentralSeries ((i : η) → Gs i) n = ⊥
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.Normal<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>inst✝¹ : (i : η) → Group (Gs i)<VAR>inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)<VAR>n : ℕ<VAR>h : ∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n<GOAL>lowerCentralSeries ((i : η) → Gs i) n = ⊥
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.Normal<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>inst✝¹ : (i : η) → Group (Gs i)<VAR>inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)<VAR>n : ℕ<VAR>h : ∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n<GOAL>lowerCentralSeries ((i : η) → Gs i) n ≤ ⊥
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.Normal<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>inst✝¹ : (i : η) → Group (Gs i)<VAR>inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)<VAR>n : ℕ<VAR>h : ∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n<GOAL>(pi Set.univ fun i => lowerCentralSeries (Gs i) n) ≤ ⊥
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>H : Subgroup G<VAR>inst✝² : H.Normal<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>inst✝¹ : (i : η) → Group (Gs i)<VAR>inst✝ : ∀ (i : η), Group.IsNilpotent (Gs i)<VAR>n : ℕ<VAR>h : ∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n<GOAL>∀ (i : η), lowerCentralSeries (Gs i) n = ⊥