ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex ℝ t<VAR>ht₂ : IsClosed t<VAR>disj : Disjoint s t<VAR>hs : s.Nonempty<VAR>_ht : t.Nonempty<VAR>U V : Set E<VAR>hU : IsOpen U<VAR>hV : IsOpen V<VAR>hU₁ : Convex ℝ U<VAR>hV₁ : Convex ℝ V<VAR>sU : s ⊆ U<VAR>tV : t ⊆ V<VAR>disj' : Disjoint U V<VAR>f : E →L[ℝ] ℝ<VAR>u : ℝ<VAR>hf₁ : ∀ a ∈ U, f a < u<VAR>hf₂ : ∀ b ∈ V, u < f b<GOAL>∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : TopologicalAddGroup E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>s t : Set E<VAR>x✝ y : E<VAR>inst✝ : LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex ℝ t<VAR>ht₂ : IsClosed t<VAR>disj : Disjoint s t<VAR>hs : s.Nonempty<VAR>_ht : t.Nonempty<VAR>U V : Set E<VAR>hU : IsOpen U<VAR>hV : IsOpen V<VAR>hU₁ : Convex ℝ U<VAR>hV₁ : Convex ℝ V<VAR>sU : s ⊆ U<VAR>tV : t ⊆ V<VAR>disj' : Disjoint U V<VAR>f : E →L[ℝ] ℝ<VAR>u : ℝ<VAR>hf₁ : ∀ a ∈ U, f a < u<VAR>hf₂ : ∀ b ∈ V, u < f b<VAR>x : E<VAR>hx₁ : x ∈ s<VAR>hx₂ : IsMaxOn (⇑f) s x<GOAL>∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>i : I<VAR>ho : ord I i < Ordinal.type fun x x_1 => x < x_1<GOAL>term I ho = i
<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>f : R →+* S₁<VAR>hf : Injective ⇑f<VAR>p q : MvPolynomial σ R<VAR>h : (map f) p = (map f) q<GOAL>p = q
<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>f : R →+* S₁<VAR>hf : Injective ⇑f<VAR>p q : MvPolynomial σ R<VAR>h : ∀ (m : σ →₀ ℕ), f (coeff m p) = f (coeff m q)<GOAL>∀ (m : σ →₀ ℕ), coeff m p = coeff m q
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>A B : Submodule R M<VAR>hAB : A ≤ B<VAR>f : Submodule R ↥B ≃o ↑(Set.Iic B) := B.mapIic<VAR>hf : f = B.mapIic<GOAL>A ⋖ B ↔ IsSimpleModule R (↥B ⧸ Submodule.comap B.subtype A)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>A B : Submodule R M<VAR>hAB : A ≤ B<VAR>f : Submodule R ↥B ≃o ↑(Set.Iic B) := B.mapIic<VAR>hf : f = B.mapIic<GOAL>IsCoatom ⟨A, hAB⟩ ↔ IsCoatom (B.mapIic (Submodule.comap B.subtype A))
<VAR>α : Type u<VAR>inst✝ : Nonempty α<VAR>l : List α<VAR>h : l.rotate 1 = l<VAR>n✝ n : ℕ<VAR>hn : l.rotate n = l<GOAL>l.rotate n.succ = l
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : Integrable f μ<GOAL>0 < μ {x | ∫ (a : α), f a ∂μ ≤ f x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>f✝ : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>M₀ : Type u_4<VAR>inst✝ : Zero M₀<VAR>f : X → M₀<GOAL>f =ᶠ[𝓝 x] 0 ↔ x ∉ closure (Function.support f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>f✝ : X → Y<VAR>s : Set X<VAR>x : X<VAR>y : Y<VAR>M₀ : Type u_4<VAR>inst✝ : Zero M₀<VAR>f : X → M₀<GOAL>{x | f x = 0 x} ∈ 𝓝 x ↔ {x | f x = 0} ∈ 𝓝 x
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝¹ : S.HasLeftHomology<VAR>inst✝ : HasKernel S.g<VAR>h : S.LeftHomologyData := S.leftHomologyData<VAR>this : HasColimit (parallelPair h.f' 0)<GOAL>HasCokernel (kernel.lift S.g S.f ⋯)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝¹ : S.HasLeftHomology<VAR>inst✝ : HasKernel S.g<VAR>h : S.LeftHomologyData := S.leftHomologyData<VAR>this : HasColimit (parallelPair h.f' 0)<VAR>e : parallelPair (kernel.lift S.g S.f ⋯) 0 ≅ parallelPair h.f' 0 := parallelPair.ext (Iso.refl ((parallelPair (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero)) ((kernelIsKernel S.g).conePointUniqueUpToIso h.hi) ⋯ ⋯<GOAL>HasCokernel (kernel.lift S.g S.f ⋯)
<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>x : R<VAR>hpq : p * q ≠ 0<GOAL>rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (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>x : R<VAR>hpq : p * q ≠ 0<GOAL>(X - C x) ^ rootMultiplicity x p * (X - C x) ^ rootMultiplicity x q ∣ p * q
<VAR>C : Type u_1<VAR>inst✝³ : Category.{v, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Finite J<VAR>F : J → Karoubi C<VAR>j✝¹ j✝ : J<GOAL>biproduct.ι (fun j => (F j).X) j✝ ≫ ((biproduct.map fun j => (F j).p) ≫ biproduct.map fun j => (F j).p) ≫ biproduct.π (fun j => (F j).X) j✝¹ = biproduct.ι (fun j => (F j).X) j✝ ≫ (biproduct.map fun j => (F j).p) ≫ biproduct.π (fun j => (F j).X) j✝¹
<VAR>C : Type u_1<VAR>inst✝³ : Category.{v, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Finite J<VAR>F : J → Karoubi C<VAR>j : J<GOAL>(biproduct.map fun j => (F j).p) ≫ (biproduct.bicone fun j => (F j).X).π j = { X := ⨁ fun j => (F j).X, p := biproduct.map fun j => (F j).p, idem := ⋯ }.p ≫ ((biproduct.map fun j => (F j).p) ≫ (biproduct.bicone fun j => (F j).X).π j) ≫ (F j).p
<VAR>C : Type u_1<VAR>inst✝³ : Category.{v, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Finite J<VAR>F : J → Karoubi C<VAR>j : J<GOAL>(biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p) = (F j).p ≫ (biproduct.ι (fun j => (F j).X) j ≫ biproduct.map fun j => (F j).p) ≫ { X := ⨁ fun j => (F j).X, p := biproduct.map fun j => (F j).p, idem := ⋯ }.p
<VAR>x : ℝ<GOAL>LiouvilleWith 1 x
<VAR>x : ℝ<GOAL>∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
<VAR>x : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
<VAR>x : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hn' : 0 < ↑n<GOAL>∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
<VAR>x : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hn' : 0 < ↑n<VAR>this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n<GOAL>∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < 2 / ↑n ^ 1
<VAR>x : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hn' : 0 < ↑n<VAR>this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n<GOAL>|x - ↑(⌊x * ↑n⌋ + 1) / ↑n| < 2 / ↑n ^ 1
<VAR>x : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hn' : 0 < ↑n<VAR>this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n<GOAL>↑(⌊x * ↑n⌋ + 1) / ↑n < (x * ↑n + 2) / ↑n
<VAR>x : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hn' : 0 < ↑n<VAR>this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n<GOAL>↑(⌊x * ↑n⌋ + 1) < x * ↑n + 2
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>K : Type u_2<VAR>inst✝ : Group K<VAR>ϕ : G →* K<GOAL>IsPGroup p ↥(Subgroup.map ϕ H)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H : Subgroup G<VAR>hH : IsPGroup p ↥H<VAR>K : Type u_2<VAR>inst✝ : Group K<VAR>ϕ : G →* K<GOAL>IsPGroup p ↥(ϕ.comp H.subtype).range
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<VAR>f : α → β<GOAL>f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>S : Set (Set α)<VAR>f : α → β<GOAL>f '' ⋂ i ∈ S, i ⊆ ⋂ s ∈ S, f '' s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>x : M ⊗[R] N<GOAL>∃ S, x = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum
<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : Applicative G<VAR>inst✝¹ : LawfulApplicative G<VAR>inst✝ : LawfulApplicative F<VAR>η : ApplicativeTransformation F G<VAR>α : Type u_1<VAR>β : Type u<VAR>f : α → F β<VAR>x : List α<GOAL>(fun {α} => η.app α) (List.traverse f x) = List.traverse ((fun {α} => η.app α) ∘ f) x
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort u_5<VAR>f : Filter α✝<VAR>g : Filter β✝<VAR>α : Type u_6<VAR>β : Type u_7<VAR>ι : Type u_8<VAR>a : α<VAR>b : β<VAR>i : ι<GOAL>(map (fun x => b) (𝓟 {a})).coprod (map id (𝓟 {i})) = 𝓟 ({b} ×ˢ univ ∪ univ ×ˢ {i})
<VAR>v : PrimeMultiset<VAR>p : ℕ+<VAR>h : p ∈ v.toPNatMultiset<GOAL>p.Prime
<VAR>v : PrimeMultiset<VAR>p : ℕ+<VAR>h : p ∈ v.toPNatMultiset<VAR>val✝ : ℕ<VAR>hp' : Nat.Prime val✝<VAR>left✝ : ⟨val✝, hp'⟩ ∈ v<VAR>h_eq : Coe.coe ⟨val✝, hp'⟩ = p<GOAL>p.Prime
<VAR>R : Type u<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>x : R<GOAL>IsRegular (star x) ↔ IsRegular x
<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✝² : Monoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>m : MeasurableSpace α<VAR>l : List (α → M)<VAR>hl : ∀ f ∈ l, StronglyMeasurable f<GOAL>StronglyMeasurable fun x => (List.map (fun f => f x) l).prod
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>x z : P<VAR>a : ℝ<VAR>ha₀ : 0 ≤ a<VAR>ha₁ : a ≤ 1<GOAL>dist x ((AffineMap.lineMap x z) a) + dist ((AffineMap.lineMap x z) a) z = dist x z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Rel β γ<VAR>t : Set γ<GOAL>(r • s).preimage t = r.preimage (s.preimage t)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a : R[X]<GOAL>wronskian 0 a = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a : R[X]<GOAL>0 a = 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.59648, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j✝ k✝ : ι<VAR>inst✝ : K.HasHomology i<VAR>A : C<VAR>k : K.X i ⟶ A<VAR>j : ι<VAR>hj : c.prev i = j<VAR>i' : ι<VAR>x : K.X i' ⟶ A<VAR>hx : k = K.d i i' ≫ x<GOAL>K.d j i ≫ k = 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DecidableEq α<VAR>i j : α<VAR>σ : Perm α<GOAL>swap i j * σ = σ ↔ i = j
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<GOAL>IsBoundedLinearMap 𝕜 fun x => x.2
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>x : E × F<GOAL>‖(LinearMap.snd 𝕜 E F) x‖ ≤ 1 * ‖x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>x : E × F<GOAL>‖(LinearMap.snd 𝕜 E F) x‖ ≤ ‖x‖
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<GOAL>T R ↑n.natAbs = T R n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℤ<VAR>h : n = -↑n.natAbs<GOAL>T R ↑n.natAbs = T R (-↑n.natAbs)
<VAR>R : Type u<VAR>inst✝ : EuclideanDomain R<VAR>a b c : R<VAR>h : c ∣ b<GOAL>c ∣ a % b ↔ c ∣ a
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a b : α<GOAL>∂ a ≤ ∂ (a ⊔ b) ⊔ ∂ (a ⊓ b)
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a b : α<GOAL>((a ⊓ ￢a ≤ a ⊔ (a ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ ￢(a ⊔ b)) ∧ a ⊓ ￢a ≤ a ⊔ b ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ b) ∧ a ⊓ ￢a ≤ a ⊔ (b ⊔ ￢(a ⊓ b)) ∧ a ⊓ ￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a b : α<GOAL>￢a ≤ ￢(a ⊔ b) ⊔ b
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a b : α<GOAL>￢a ≤ ￢(a ⊔ b) ⊔ ￢(a ⊓ b)
<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>r : α → α → Prop<VAR>a b c d : α<VAR>r' : α → α → Prop<VAR>hr₁ : Reflexive r'<VAR>hr₂ : Transitive r'<VAR>h : ∀ (x y : α), r x y → r' x y<VAR>x y : α<VAR>hxy : ReflTransGen r x y<GOAL>r' x y
<VAR>q : ℚ<GOAL>↑q.den * q = ↑q.num
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z✝¹ X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : Mono f<VAR>g : Y ⟶ Z✝<VAR>inst✝ : Mono g<VAR>Z : C<VAR>a b : Z ⟶ X<VAR>w : a ≫ f ≫ g = b ≫ f ≫ g<GOAL>a = b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z✝¹ X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : Mono f<VAR>g : Y ⟶ Z✝<VAR>inst✝ : Mono g<VAR>Z : C<VAR>a b : Z ⟶ X<VAR>w : a ≫ f ≫ g = b ≫ f ≫ g<GOAL>a ≫ f = b ≫ f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z✝¹ X Y Z✝ : C<VAR>f : X ⟶ Y<VAR>inst✝¹ : Mono f<VAR>g : Y ⟶ Z✝<VAR>inst✝ : Mono g<VAR>Z : C<VAR>a b : Z ⟶ X<VAR>w : a ≫ f ≫ g = b ≫ f ≫ g<GOAL>(a ≫ f) ≫ g = (b ≫ f) ≫ g
<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<GOAL>Collinear k {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<GOAL>Module.rank k ↥⊥ ≤ 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>h : φ.order ≠ ψ.order<GOAL>(φ + ψ).order = φ.order ⊓ ψ.order
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>h : φ.order ≠ ψ.order<GOAL>(φ + ψ).order ≤ φ.order ⊓ ψ.order
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<VAR>h : φ.order ≠ ψ.order<VAR>H₁ : ¬φ.order < ψ.order<VAR>H₂ : ¬ψ.order < φ.order<GOAL>False
<GOAL>√2 / 2 / (√2 / 2) = 1
<VAR>h : √2 / 2 > 0<GOAL>√2 / 2 / (√2 / 2) = 1
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>s₁ s₂ : Set (Set Ω)<VAR>h : IndepSets s₁ s₂ κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ s₂<VAR>ht2 : t2 ∈ s₁<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>s₁ s₂ : Set (Set Ω)<VAR>h : IndepSets s₁ s₂ κ μ<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ s₂<VAR>ht2 : t2 ∈ s₁<VAR>a : α<VAR>ha : (κ a) (t2 ∩ t1) = (κ a) t2 * (κ a) t1<GOAL>(κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : Zero M<VAR>inst✝ : DecidableEq α<VAR>f : α →₀ M<VAR>a✝ : α<GOAL>a✝ ∈ f.toAList.keys.toFinset ↔ a✝ ∈ f.support
<VAR>a : ℕ<GOAL>(↑a)⁻¹.den = if a = 0 then 1 else a
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring A<VAR>inst✝ : Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<VAR>a : A<VAR>s : Set A<GOAL>s ∈ 𝓝 a ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ s
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring A<VAR>inst✝ : Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<VAR>a : A<VAR>s : Set A<GOAL>(∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, (fun y => a + y) '' i ⊆ s) ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ s
<VAR>A : Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Ring A<VAR>inst✝ : Nonempty ι<VAR>B : ι → AddSubgroup A<VAR>hB : RingSubgroupsBasis B<VAR>a : A<VAR>s : Set A<GOAL>(∃ i ∈ RingFilterBasis.toAddGroupFilterBasis, (fun y => a + y) '' i ⊆ s) ↔ ∃ i, {b | b - a ∈ B i} ⊆ s
<VAR>z : ℂ<GOAL>HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) (cos z)
<VAR>z : ℂ<GOAL>HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)
<VAR>z : ℂ<VAR>this : HasSum (fun i => ((z * I) ^ i / ↑i ! + (-z * I) ^ i / ↑i !) / 2) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)<GOAL>HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)
<VAR>z : ℂ<VAR>this : HasSum ((fun i => ((z * I) ^ i / ↑i ! + (-z * I) ^ i / ↑i !) / 2) ∘ ⇑(Nat.divModEquiv 2).symm) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)<GOAL>HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2)! + (-z * I) ^ (x.1 * 2 + ↑x.2) / ↑(x.1 * 2 + ↑x.2)!) / 2) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)<GOAL>HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)<GOAL>HasSum (fun n => (z * I) ^ (2 * n) / ↑(2 * n)!) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)<VAR>k : ℕ<GOAL>HasSum (fun c => ((z * I) ^ (2 * (k, c).1 + ↑(k, c).2) / ↑(2 * (k, c).1 + ↑(k, c).2)! + (-z * I) ^ (2 * (k, c).1 + ↑(k, c).2) / ↑(2 * (k, c).1 + ↑(k, c).2)!) / 2) ((z * I) ^ (2 * k) / ↑(2 * k)!)
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)<VAR>k : ℕ<GOAL>HasSum (fun c => ((z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)! + (-z * I) ^ (2 * k + ↑c) / ↑(2 * k + ↑c)!) / 2) ((z * I) ^ (2 * k) / ↑(2 * k)!)
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)<VAR>k : ℕ<GOAL>(z * I) ^ (2 * k) / ↑(2 * k)! = ∑ b : Fin 2, ((z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)! + (-z * I) ^ (2 * k + ↑b) / ↑(2 * k + ↑b)!) / 2
<VAR>z : ℂ<VAR>this : HasSum (fun x => ((z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)! + (-z * I) ^ (2 * x.1 + ↑x.2) / ↑(2 * x.1 + ↑x.2)!) / 2) ((NormedSpace.exp ℂ (z * I) + NormedSpace.exp ℂ (-z * I)) / 2)<VAR>k : ℕ<GOAL>(z * I) ^ (2 * k) / ↑(2 * k)! = ((z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)! + (-z * I) ^ (2 * k + ↑0) / ↑(2 * k + ↑0)!) / 2 + ((z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)! + (-z * I) ^ (2 * k + ↑1) / ↑(2 * k + ↑1)!) / 2
<VAR>l m r : List Char<VAR>x✝ : Substring<VAR>h : ValidFor l m r x✝<GOAL>Iterator.ValidFor l.reverse (m ++ r) { s := x✝.str, i := x✝.startPos }
<GOAL>StableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral
<GOAL>∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T], (algebraMap R T).IsIntegral → includeLeftRingHom.IsIntegral
<VAR>R S T : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : CommRing T<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra R T<VAR>h : (algebraMap R T).IsIntegral<VAR>x : S ⊗[R] T<GOAL>includeLeftRingHom.IsIntegralElem x
<VAR>R S T : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : CommRing T<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra R T<VAR>h : (algebraMap R T).IsIntegral<VAR>x : S ⊗[R] T<GOAL>includeLeftRingHom.IsIntegralElem 0
<VAR>R S T : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : CommRing T<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra R T<VAR>h : (algebraMap R T).IsIntegral<VAR>x : S ⊗[R] T<GOAL>∀ (x : S) (y : T), includeLeftRingHom.IsIntegralElem (x ⊗ₜ[R] y)
<VAR>R S T : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : CommRing T<VAR>inst✝¹ : Algebra R S<VAR>inst✝ : Algebra R T<VAR>h : (algebraMap R T).IsIntegral<VAR>x : S ⊗[R] T<GOAL>∀ (x y : S ⊗[R] T), includeLeftRingHom.IsIntegralElem x → includeLeftRingHom.IsIntegralElem y → includeLeftRingHom.IsIntegralElem (x + y)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>hB₁ : M.Base B₁<VAR>hB₂ : M.Base B₂<GOAL>B₁.ncard = B₂.ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (LowerSet α)<VAR>s t : LowerSet α<VAR>a : α<GOAL>(∃ i, ∃ (_ : i ∈ S), a ∈ ↑i) ↔ ∃ s ∈ S, a ∈ s
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>(a * a₁⁻¹).x < a.x
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a.x * a₁.x < d * (a.y * a₁.y) + a.x
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a₁.y * (a.x * a₁.x) < a₁.y * (d * (a.y * a₁.y) + a.x)
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a.x * a₁.y * a₁.x < a₁.y * (d * (a.y * a₁.y) + a.x)
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a.y * a₁.x * a₁.x < a₁.y * (d * (a.y * a₁.y) + a.x)
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a.y * (1 + d * a₁.y ^ 2) - a₁.y * (d * (a.y * a₁.y) + a.x) < 0
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a.y - a.x * a₁.y < 0
<VAR>d : ℤ<VAR>a₁ : Solution₁ d<VAR>h : IsFundamental a₁<VAR>a : Solution₁ d<VAR>hax : 1 < a.x<VAR>hay : 0 < a.y<GOAL>a.y ^ 2 < (1 + d * a.y ^ 2) * a₁.y ^ 2
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommRing R<VAR>t : Multiset R<VAR>ht : 0 < Multiset.card t<VAR>a✝ : Nontrivial R<GOAL>(Multiset.map (fun x => X - C x) t).prod.coeff (Multiset.card t - 1) = -t.sum
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommRing R<VAR>t : Multiset R<VAR>ht : 0 < Multiset.card t<VAR>a✝ : Nontrivial R<GOAL>(Multiset.map (fun x => X - C x) t).prod.coeff (Multiset.card t - 1) = (Multiset.map (fun x => X - C x) t).prod.nextCoeff
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommRing R<VAR>t : Multiset R<VAR>ht : 0 < Multiset.card t<VAR>a✝ : Nontrivial R<GOAL>(Multiset.map (fun x => X - C x) t).prod.coeff (Multiset.card t - 1) = (Multiset.map (fun x => X - C x) t).prod.coeff ((Multiset.map (fun x => X - C x) t).prod.natDegree - 1)
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommRing R<VAR>t : Multiset R<VAR>ht : 0 < Multiset.card t<VAR>a✝ : Nontrivial R<GOAL>¬(Multiset.map (fun x => X - C x) t).prod.natDegree = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>hr : ↑r < p.radius<VAR>k : ℕ<GOAL>Summable fun s => ‖p (k + s.fst)‖₊ * r ^ s.fst