ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>h : H.Normal<VAR>a : G<VAR>_ha : a ∈ ⊤<VAR>b : G<VAR>hb : a * b * a⁻¹ ∈ H<GOAL>b ∈ H
<VAR>E : Type u<VAR>F : Type v<VAR>inst✝¹ : PseudoEMetricSpace F<VAR>inst✝ : TopologicalSpace E<VAR>f : E → F<VAR>D : Set E<VAR>x : E<VAR>hD : D ∈ 𝓝 x<GOAL>oscillationWithin f D x = oscillation f x
<VAR>n m : ℕ<VAR>P : MvPFunctor.{u} n<VAR>Q : Fin2 n → MvPFunctor.{u} m<VAR>α✝ β : TypeVec.{u} m<VAR>α : TypeVec.{u} n<VAR>p : ⦃i : Fin2 n⦄ → α i → Prop<VAR>a : P.A<VAR>f : P.B a ⟹ α<GOAL>LiftP p ⟨a, f⟩ ↔ ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
<VAR>n m : ℕ<VAR>P : MvPFunctor.{u} n<VAR>Q : Fin2 n → MvPFunctor.{u} m<VAR>α✝ β : TypeVec.{u} m<VAR>α : TypeVec.{u} n<VAR>p : ⦃i : Fin2 n⦄ → α i → Prop<VAR>a : P.A<VAR>f : P.B a ⟹ α<GOAL>(∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : P.B a_1 i), p (f_1 i j)) ↔ ∀ (i : Fin2 n) (x : P.B a i), p (f i x)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : Zero R<VAR>inst✝¹ : Zero M<VAR>inst✝ : SMulWithZero R M<VAR>f : α → R<VAR>f' : α → M<VAR>x : α<VAR>hf : HasCompactSupport f<GOAL>HasCompactSupport (f • f')
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : Zero R<VAR>inst✝¹ : Zero M<VAR>inst✝ : SMulWithZero R M<VAR>f : α → R<VAR>f' : α → M<VAR>x : α<VAR>hf : f =ᶠ[coclosedCompact α] 0<GOAL>f • f' =ᶠ[coclosedCompact α] 0
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ ε : ℝ<VAR>s t : Set α<VAR>x : α<GOAL>thickening δ (closure s) = thickening δ s
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>count p (n + 1) = count p n + if p n then 1 else 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<VAR>x : A<GOAL>⅟2 • (x + star x) ∈ selfAdjoint A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<VAR>x y : A<GOAL>↑((fun x => ⟨⅟2 • (x + star x), ⋯⟩) (x + y)) = ↑((fun x => ⟨⅟2 • (x + star x), ⋯⟩) x + (fun x => ⟨⅟2 • (x + star x), ⋯⟩) y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : StarMul R<VAR>inst✝⁵ : TrivialStar R<VAR>inst✝⁴ : AddCommGroup A<VAR>inst✝³ : Module R A<VAR>inst✝² : StarAddMonoid A<VAR>inst✝¹ : StarModule R A<VAR>inst✝ : Invertible 2<VAR>r : R<VAR>x : A<GOAL>↑({ toFun := fun x => ⟨⅟2 • (x + star x), ⋯⟩, map_add' := ⋯ }.toFun (r • x)) = ↑((RingHom.id R) r • { toFun := fun x => ⟨⅟2 • (x + star x), ⋯⟩, map_add' := ⋯ }.toFun x)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Ring K<VAR>inst✝² : NoZeroDivisors K<VAR>inst✝¹ : Nontrivial K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>n : ℕ := Fintype.card ↥G<VAR>nzero : ↑(Fintype.card ↥G) = 0<GOAL>False
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Ring K<VAR>inst✝² : NoZeroDivisors K<VAR>inst✝¹ : Nontrivial K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>n : ℕ := Fintype.card ↥G<VAR>nzero : ↑(Fintype.card ↥G) = 0<VAR>p : ℕ<VAR>char_p : CharP K p<GOAL>False
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Ring K<VAR>inst✝² : NoZeroDivisors K<VAR>inst✝¹ : Nontrivial K<VAR>G : Subgroup Kˣ<VAR>inst✝ : Fintype ↥G<VAR>n : ℕ := Fintype.card ↥G<VAR>nzero : ↑(Fintype.card ↥G) = 0<VAR>p : ℕ<VAR>char_p : CharP K p<VAR>hd : p ∣ n<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>a b : R<VAR>h : Commute a b<GOAL>a * a - b * b = (a - b) * (a + b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>b ⊔ c \ a = c
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι✝ : Type y<VAR>a b : R✝<VAR>m n : ℕ<VAR>inst✝³ : CommSemiring R✝<VAR>p✝ q : R✝[X]<VAR>x✝ : R✝<VAR>inst✝² : CommSemiring S<VAR>f : R✝ →+* S<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>p : ι → R[X]<VAR>x : R<GOAL>(∏ j ∈ s, p j).IsRoot x ↔ ∃ i ∈ s, (p i).IsRoot x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : Preorder Y<VAR>inst✝ : OrderClosedTopology Y<VAR>f g : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsLocalMaxOn f s a<VAR>hc : ContinuousOn f (closure s)<GOAL>IsLocalMaxOn f (closure s) a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : Preorder Y<VAR>inst✝ : OrderClosedTopology Y<VAR>f g : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsLocalMaxOn f s a<VAR>hc : ContinuousOn f (closure s)<VAR>U : Set X<VAR>Uo : IsOpen U<VAR>aU : a ∈ U<VAR>hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}<GOAL>IsLocalMaxOn f (closure s) a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : Preorder Y<VAR>inst✝ : OrderClosedTopology Y<VAR>f g : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsLocalMaxOn f s a<VAR>hc : ContinuousOn f (closure s)<VAR>U : Set X<VAR>Uo : IsOpen U<VAR>aU : a ∈ U<VAR>hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}<GOAL>U ∩ closure s ⊆ {x | (fun x => f x ≤ f a) x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : Preorder Y<VAR>inst✝ : OrderClosedTopology Y<VAR>f g : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsLocalMaxOn f s a<VAR>hc : ContinuousOn f (closure s)<VAR>U : Set X<VAR>Uo : IsOpen U<VAR>aU : a ∈ U<VAR>hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}<VAR>x : X<VAR>hxU : x ∈ U<VAR>hxs : x ∈ closure s<GOAL>x ∈ {x | (fun x => f x ≤ f a) x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : Preorder Y<VAR>inst✝ : OrderClosedTopology Y<VAR>f g : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsLocalMaxOn f s a<VAR>hc : ContinuousOn f (closure s)<VAR>U : Set X<VAR>Uo : IsOpen U<VAR>aU : a ∈ U<VAR>hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}<VAR>x : X<VAR>hxU : x ∈ U<VAR>hxs : x ∈ closure s<GOAL>x ∈ closure (U ∩ s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : Preorder Y<VAR>inst✝ : OrderClosedTopology Y<VAR>f g : X → Y<VAR>s : Set X<VAR>a : X<VAR>h : IsLocalMaxOn f s a<VAR>hc : ContinuousOn f (closure s)<VAR>U : Set X<VAR>Uo : IsOpen U<VAR>aU : a ∈ U<VAR>hU : U ∩ s ⊆ {x | (fun x => f x ≤ f a) x}<VAR>x : X<VAR>hxU : x ∈ U<VAR>hxs : x ∈ closure s<GOAL>ContinuousWithinAt f (U ∩ s) x
<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>f : M₁ →SL[σ₁₂] M₂<VAR>hf : f ≠ 0<GOAL>∃ x, f x ≠ 0
<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>f : M₁ →SL[σ₁₂] M₂<VAR>hf : f ≠ 0<VAR>h : ∀ (x : M₁), f x = 0<GOAL>False
<VAR>R : Type u<VAR>inst✝¹ : EuclideanDomain R<VAR>inst✝ : DecidableEq R<VAR>x : R<GOAL>lcm x 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ✝ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t : Set α<VAR>μ ν : Measure α<VAR>s : Set α<GOAL>∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s ∧ ν t = ν s
<VAR>x y : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>num (x * y) z / denom (x * y) z = (↑(↑↑x 0 0) * (num y z / denom y z) + ↑(↑↑x 0 1)) / denom x (smulAux y z)
<VAR>x y : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>num (x * y) z / (denom x (smulAux y z) * denom y z) = (↑(↑↑x 0 0) * (num y z / denom y z) + ↑(↑↑x 0 1)) / denom x (smulAux y z)
<VAR>x y : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>num (x * y) z * (denom y z * denom x (smulAux y z)) = (↑(↑↑x 0 0) * num y z + ↑(↑↑x 0 1) * denom y z) * (denom x (smulAux y z) * denom y z)
<VAR>x y : ↥GL(2, ℝ)⁺<VAR>z : ℍ<GOAL>((↑(↑↑x 0 0) * ↑(↑↑y 0 0) + ↑(↑↑x 0 1) * ↑(↑↑y 1 0)) * ↑z + (↑(↑↑x 0 0) * ↑(↑↑y 0 1) + ↑(↑↑x 0 1) * ↑(↑↑y 1 1))) * ((↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1)) * (↑(↑↑x 1 0) * ↑(smulAux y z) + ↑(↑↑x 1 1))) = (↑(↑↑x 0 0) * (↑(↑↑y 0 0) * ↑z + ↑(↑↑y 0 1)) + ↑(↑↑x 0 1) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1))) * ((↑(↑↑x 1 0) * ↑(smulAux y z) + ↑(↑↑x 1 1)) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1)))
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>u v : E<GOAL>‖u‖ ≤ ‖v‖ + ‖u / v‖
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>u v : E<GOAL>‖u‖ ≤ ‖u / v‖ + ‖v‖
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>u v : E<GOAL>‖u‖ = ‖u / v * v‖
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝ : FormallyEtale R S<GOAL>FormallyEtale Rₘ Sₘ
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝ : FormallyEtale R S<VAR>this : FormallyEtale S Sₘ<GOAL>FormallyEtale Rₘ Sₘ
<VAR>R S Rₘ Sₘ : Type u<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : CommRing Rₘ<VAR>inst✝¹⁰ : CommRing Sₘ<VAR>M : Submonoid R<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R Sₘ<VAR>inst✝⁷ : Algebra S Sₘ<VAR>inst✝⁶ : Algebra R Rₘ<VAR>inst✝⁵ : Algebra Rₘ Sₘ<VAR>inst✝⁴ : IsScalarTower R Rₘ Sₘ<VAR>inst✝³ : IsScalarTower R S Sₘ<VAR>inst✝² : IsLocalization M Rₘ<VAR>inst✝¹ : IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ<VAR>inst✝ : FormallyEtale R S<VAR>this✝ : FormallyEtale S Sₘ<VAR>this : FormallyEtale R Sₘ<GOAL>FormallyEtale Rₘ Sₘ
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<VAR>h : Wbtw R x y z<VAR>hne : x ≠ y<GOAL>z ∈ affineSpan R {x, y}
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y : P<VAR>hne : x ≠ y<VAR>r : R<VAR>h : Wbtw R x y ((lineMap x y) r)<GOAL>(lineMap x y) r ∈ affineSpan R {x, y}
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>a : α<VAR>inst✝ : PredOrder α<VAR>ha : ¬IsMin a<GOAL>¬IsPredLimit (pred a)
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>a : α<VAR>inst✝ : PredOrder α<VAR>ha : IsPredLimit (pred a)<GOAL>IsMin a
<VAR>R✝ : Type u_1<VAR>inst✝¹ : Rack R✝<VAR>R : Type u_2<VAR>inst✝ : Rack R<VAR>h : IsInvolutory R<VAR>x y : R<GOAL>x ◃⁻¹ y = x ◃ y
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝² : (a : α) → DecidablePred (r a)<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ interedges r s t ↔ (x, y) ∈ s.biUnion fun x => map { toFun := fun x_1 => (x, x_1), inj' := ⋯ } (filter (r x) t)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n✝ m n : ℤ<VAR>z₂ : Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>((ofHom (𝟙 F)).comp z₂ ⋯).v p q hpq = z₂.v p q hpq
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a✝ : α<VAR>inst✝ : IsSFiniteKernel η<VAR>s : Set (β × γ)<VAR>hs : MeasurableSet s<VAR>a : α<VAR>this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}<GOAL>Measurable fun b => (η (a, b)) {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a✝ : α<VAR>inst✝ : IsSFiniteKernel η<VAR>s : Set (β × γ)<VAR>hs : MeasurableSet s<VAR>a : α<VAR>this : ∀ (b : β), Prod.mk b ⁻¹' s = {c | ((a, b), c) ∈ {p | (p.1.2, p.2) ∈ s}}<GOAL>MeasurableSet {p | (p.1.2, p.2) ∈ s}
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>n₁ n₂ : ℤ<VAR>K : CochainComplex C ℤ<VAR>x✝² x✝¹ : ℤ<VAR>x✝ : (ComplexShape.up ℤ).Rel x✝² x✝¹<GOAL>(XIsoOfEq K ⋯).hom ≫ (n₂.negOnePow • n₁.negOnePow • K.d (x✝² + n₂ + n₁) (x✝¹ + n₂ + n₁)) = ((n₁ + n₂).negOnePow • K.d (x✝² + (n₁ + n₂)) (x✝¹ + (n₁ + n₂))) ≫ (XIsoOfEq K ⋯).hom
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝ : NormedRing R<VAR>f g : ℕ → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>Summable fun n => ‖∑ k ∈ range (n + 1), f k * g (n - k)‖
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>inst✝ : NormedRing R<VAR>f g : ℕ → R<VAR>hf : Summable fun x => ‖f x‖<VAR>hg : Summable fun x => ‖g x‖<GOAL>Summable fun n => ‖∑ ij ∈ antidiagonal n, f ij.1 * g ij.2‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>x : α<GOAL>x ∉ ∅
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>δ i.succ ≫ σ i = 𝟙 [n]
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝² : Ring R₂<VAR>inst✝¹ : AddCommGroup M₂<VAR>inst✝ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>h : p ≤ ker f<GOAL>map p.mkQ (comap f q) ≤ comap (p.liftQ f h) q
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t s : Set X<VAR>H : s ∈ irreducibleComponents X<GOAL>IsClosed s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t s : Set X<VAR>H : s ∈ irreducibleComponents X<GOAL>s = closure s
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_2<VAR>s : Finset ι<VAR>v : ι → R<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>nodal (insert i s) v = (X - C (v i)) * nodal s v
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>y \ x ⊓ x = ⊥
<VAR>α : Type u<VAR>l₁ l₂ : List α<VAR>H : l₁.length ≤ l₂.length<GOAL>Lex (fun x x_1 => x ≠ x_1) l₁ l₂ ↔ l₁ ≠ l₂
<VAR>o : ONote<VAR>f : ℕ → ONote<VAR>h : o.fundamentalSequence = Sum.inr f<GOAL>o.fastGrowing = fun i => (f i).fastGrowing i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>f : R[M]<GOAL>∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>m : M<GOAL>∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = (of R M) (Multiplicative.ofAdd m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>f g : R[M]<VAR>ihf : ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = f<VAR>ihg : ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = g<GOAL>∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = f + g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : AddMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>r : R<VAR>f : R[M]<VAR>ih : ∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = f<GOAL>∃ a, ((FreeAlgebra.lift R) fun s => of' R M ↑s) a = r • f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s s₁ s₂ : Finset β<VAR>f✝ g : β → α<VAR>a : α<VAR>f : β → α<VAR>S : Finset β<GOAL>S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<VAR>s : Set Γ₀<GOAL>IsOpen s ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s
<VAR>α : Type u_1<VAR>Γ₀ : Type u_2<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>γ γ₁ γ₂ : Γ₀<VAR>l : Filter α<VAR>f : α → Γ₀<VAR>s : Set Γ₀<GOAL>((0 ∈ s → s ∈ 𝓝 0) ∧ ∀ (b : Γ₀), b ≠ 0 → b ∈ s → s ∈ 𝓝 b) ↔ 0 ∉ s ∨ ∃ γ, γ ≠ 0 ∧ Iio γ ⊆ s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Ring R<VAR>p q r : R[X]<VAR>n : ℤ<VAR>x : R<GOAL>eval x ↑n = ↑n
<VAR>a b : ℤ<VAR>b0 : b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a /. b = { num := n, den := d, den_nz := h, reduced := c }<GOAL>{ num := n, den := d, den_nz := h, reduced := c }.num ∣ a
<VAR>a b : ℤ<VAR>b0 : b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a * ↑d = n * b<GOAL>{ num := n, den := d, den_nz := h, reduced := c }.num ∣ a
<VAR>a b : ℤ<VAR>b0 : b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a * ↑d = n * b<GOAL>n.natAbs ∣ a.natAbs * d
<VAR>a b : ℤ<VAR>b0 : b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a * ↑d = n * b<VAR>this : (a * ↑d).natAbs = (n * b).natAbs<GOAL>n.natAbs ∣ a.natAbs * d
<VAR>a b : ℤ<VAR>b0 : b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a * ↑d = n * b<VAR>this : a.natAbs * d = n.natAbs * b.natAbs<GOAL>n.natAbs ∣ a.natAbs * d
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>u₁ u₂ : UniformSpace α<VAR>h : 𝓤 α = 𝓤 α<GOAL>u₁ = u₂
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>u₁ u₂ : UniformSpace α<VAR>h : 𝓤 α = 𝓤 α<VAR>this : toTopologicalSpace = toTopologicalSpace<GOAL>u₁ = u₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>x : α<GOAL>(l ++ [x]).rdrop (n + 1) = l.rdrop n
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Finset E<VAR>x : E<GOAL>x ∈ (convexHull R) ↑s ↔ ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x
<VAR>𝕜 : Type u_1<VAR>inst✝³² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³¹ : NormedAddCommGroup E<VAR>inst✝³⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁸ : TopologicalSpace M<VAR>inst✝²⁷ : ChartedSpace H M<VAR>inst✝²⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²² : TopologicalSpace M'<VAR>inst✝²¹ : ChartedSpace H' M'<VAR>inst✝²⁰ : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>f✝ f₁ : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>g : M → F₁ →L[𝕜] F₂<VAR>f : M → F₁<VAR>s : Set M<VAR>x : M<VAR>hg : ContMDiffWithinAt I 𝓘(𝕜, F₁ →L[𝕜] F₂) n g s x<VAR>hf : ContMDiffWithinAt I 𝓘(𝕜, F₁) n f s x<GOAL>ContDiffWithinAt 𝕜 n (fun x => x.1 x.2) ?m.116039 ((fun x => (g x, f x)) x)