ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u s : Set α<VAR>x : α<GOAL>s ⊂ {x} ↔ s = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u s : Set α<VAR>x : α<GOAL>s = ∅ → s ≠ {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NormedCommRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>x✝¹ : E<VAR>x✝ : x✝¹ ∈ s<GOAL>‖(B x✝¹) 0‖ ≤ 1
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : R →+* S<VAR>x✝ : MvPolynomial σ R<GOAL>x✝ ∈ RingHom.ker (map f) ↔ x✝ ∈ Ideal.map C (RingHom.ker f)
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>f : R →+* S<VAR>x✝ : MvPolynomial σ R<GOAL>(∀ (m : σ →₀ ℕ), coeff m ((map f) x✝) = coeff m 0) ↔ ∀ (m : σ →₀ ℕ), coeff m x✝ ∈ RingHom.ker f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : WSeq α<VAR>a : α<VAR>n : ℕ<VAR>h : some a ∈ s.get? n<GOAL>∃ a', some a' ∈ s.head
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x✝ : α<VAR>r : Ordnode α<VAR>sl : l.Sized<VAR>sr : r.Sized<GOAL>l.size + r.size + 1 = r.dual.size + l.dual.size + 1
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>f : R[X]<VAR>inst✝ : CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h : eval₂ i a f = 0<VAR>x : R<GOAL>(lift i a h) ((of f) x) = i x
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(x ^ n) ^ (↑n)⁻¹ = x
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(↑x ^ n) ^ (↑n)⁻¹ = ↑x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>hn : (↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n ≠ 0<GOAL>‖(↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n‖ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>n : ι<VAR>hn : (↑‖gramSchmidt 𝕜 f n‖)⁻¹ • gramSchmidt 𝕜 f n ≠ 0<GOAL>gramSchmidt 𝕜 f n ≠ 0
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X : C<VAR>f : J → C<VAR>j✝ : J<GOAL>(biproduct.lift fun j => X ◁ biproduct.π f j) ≫ biproduct.π (fun j => X ⊗ f j) j✝ = (∑ j : J, X ◁ biproduct.π f j ≫ biproduct.ι (fun j => X ⊗ f j) j) ≫ biproduct.π (fun j => X ⊗ f j) j✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X : C<VAR>f : J → C<VAR>j✝ : J<GOAL>X ◁ biproduct.π f j✝ = (∑ j : J, X ◁ biproduct.π f j ≫ biproduct.ι (fun j => X ⊗ f j) j) ≫ biproduct.π (fun j => X ⊗ f j) j✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSingletonClass α<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, f x * μ {x}
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>r : R<GOAL>(C r * X).eraseLead = 0
<VAR>w x✝ y✝ z✝ : ℝ<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : z ≠ 0<GOAL>x ^ (1 / z) = y ↔ x = y ^ z
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<GOAL>Function.Injective ⇑(algebraMap K[X] (RatFunc K))
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<GOAL>Function.Injective (ofFractionRing ∘ ⇑(algebraMap K[X] (FractionRing K[X])))
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>hbot : S ≠ ⊥<VAR>H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a<GOAL>Dense ↑S
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>hbot : S ≠ ⊥<VAR>H : ¬∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a<VAR>ε : G<VAR>ε0 : ε > 0<GOAL>∃ g ∈ S, g ∈ Ioo 0 ε
<VAR>G : Type u_1<VAR>inst✝³ : LinearOrderedAddCommGroup G<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : OrderTopology G<VAR>inst✝ : Archimedean G<VAR>S : AddSubgroup G<VAR>hbot : S ≠ ⊥<VAR>ε : G<VAR>ε0 : ε > 0<VAR>H : ∀ g ∈ S, g ∉ Ioo 0 ε<GOAL>∃ a, IsLeast {g | g ∈ S ∧ 0 < g} a
<VAR>x✝ y z✝ : ℝ<VAR>n : ℕ<VAR>x z : ℝ<VAR>hx1 : 0 ≤ x<VAR>hx2 : x < 1<VAR>hz : 0 < z<GOAL>x ^ z < 1
<VAR>x✝ y z✝ : ℝ<VAR>n : ℕ<VAR>x z : ℝ<VAR>hx1 : 0 ≤ x<VAR>hx2 : x < 1<VAR>hz : 0 < z<GOAL>x ^ z < 1 ^ z
<VAR>α : Type u<VAR>β : Type v<VAR>l l₁✝ l₂✝ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l₁ l₂ : List α<GOAL>(l₁ ++ l₂).Nodup ↔ (l₂ ++ l₁).Nodup
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>r : R<GOAL>eval (-r) (ascPochhammer R 0) = (-1) ^ 0 * eval r (descPochhammer R 0)
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>r : R<GOAL>eval (-r) 1 = (-1) ^ 0 * eval r 1
<VAR>R : Type u<VAR>inst✝ : Ring R<VAR>r : R<VAR>k : ℕ<GOAL>eval (-r) (ascPochhammer R (k + 1)) = (-1) ^ (k + 1) * eval r (descPochhammer R (k + 1))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : AddMonoid M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>h : FiniteType R R[M]<GOAL>AddMonoid.FG M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : AddMonoid M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>h : FiniteType R R[M]<VAR>S : Finset M<VAR>hS : adjoin R (of' R M '' ↑S) = ⊤<GOAL>AddMonoid.FG M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : AddMonoid M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>h : FiniteType R R[M]<VAR>S : Finset M<VAR>hS : adjoin R (of' R M '' ↑S) = ⊤<VAR>m : M<GOAL>m ∈ closure ↑S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : AddMonoid M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>h : FiniteType R R[M]<VAR>S : Finset M<VAR>hS : adjoin R (of' R M '' ↑S) = ⊤<VAR>m : M<VAR>hm : of' R M m ∈ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑S))<GOAL>m ∈ closure ↑S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : AddMonoid M<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>h : FiniteType R R[M]<VAR>S : Finset M<VAR>hS : adjoin R (of' R M '' ↑S) = ⊤<VAR>m : M<VAR>hm : of' R M m ∈ span R ↑(Submonoid.closure (of' R M '' ↑S))<GOAL>m ∈ closure ↑S
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R✝<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R✝ M<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : WfDvdMonoid R<VAR>f : R[X]<VAR>hf : 0 < f.natDegree<GOAL>0 < f.degree
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R✝<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R✝ M<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : WfDvdMonoid R<VAR>f : R[X]<VAR>hf : f.degree ≤ 0<GOAL>f.natDegree ≤ 0
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝⁹ : CommSemiring R✝<VAR>inst✝⁸ : NonUnitalRing A✝<VAR>inst✝⁷ : Module R✝ A✝<VAR>inst✝⁶ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁵ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : NonUnitalRing A<VAR>inst✝² : Module R A<VAR>inst✝¹ : IsScalarTower R A A<VAR>inst✝ : SMulCommClass R A A<VAR>a : A<VAR>r : R<VAR>hr : ¬IsUnit r<VAR>h : r ∈ resolventSet R ↑a<GOAL>IsUnit r
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>inst✝¹ : H.Normal<VAR>inst✝ : Group.IsNilpotent G<GOAL>Group.nilpotencyClass G = 0 ↔ Subsingleton G
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i|↑𝒢 i]<GOAL>Submartingale f 𝒢 μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i|↑𝒢 i]<VAR>i : ℕ<GOAL>f i ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i]
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝⁴ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>𝒢 : Filtration ℕ m0<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : ℕ → Ω → ℝ<VAR>hadp : Adapted 𝒢 f<VAR>hint : ∀ (i : ℕ), Integrable (f i) μ<VAR>hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f (i + 1) - f i|↑𝒢 i]<VAR>i : ℕ<GOAL>0 ≤ᶠ[ae μ] μ[f (i + 1)|↑𝒢 i] - μ[f i|↑𝒢 i]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>A B C : Set E<VAR>hAB : IsExposed 𝕜 A B<GOAL>IsExtreme 𝕜 A B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>A B C : Set E<VAR>hAB : IsExposed 𝕜 A B<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hxB : x ∈ B<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<GOAL>x₁ ∈ B ∧ x₂ ∈ B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>A C : Set E<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<VAR>l : E →L[𝕜] 𝕜<VAR>hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<VAR>hxB : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<GOAL>x₁ ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>A C : Set E<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<VAR>l : E →L[𝕜] 𝕜<VAR>hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<VAR>hxB : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<VAR>hl : ConvexOn 𝕜 univ ⇑l<GOAL>x₁ ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>A C : Set E<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<VAR>l : E →L[𝕜] 𝕜<VAR>hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<VAR>hxB : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<VAR>hl : ConvexOn 𝕜 univ ⇑l<VAR>hlx₁ : l x₁ ≤ l x<GOAL>x₁ ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : TopologicalSpace 𝕜<VAR>inst✝³ : LinearOrderedRing 𝕜<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>A C : Set E<VAR>x₁ : E<VAR>hx₁A : x₁ ∈ A<VAR>x₂ : E<VAR>hx₂A : x₂ ∈ A<VAR>x : E<VAR>hx : x ∈ openSegment 𝕜 x₁ x₂<VAR>l : E →L[𝕜] 𝕜<VAR>hAB : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<VAR>hxB : x ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}<VAR>hl : ConvexOn 𝕜 univ ⇑l<VAR>hlx₁ : l x₁ ≤ l x<VAR>hlx₂ : l x₂ ≤ l x<GOAL>x₁ ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ∧ x₂ ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.2467, u_2} D<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>inst✝ : S.HasHomology<VAR>h : S.RightHomologyData<GOAL>S.Exact ↔ IsZero h.H
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.2467, u_2} D<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>inst✝ : S.HasHomology<VAR>h : S.RightHomologyData<GOAL>IsZero S.homology ↔ IsZero h.H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂ρ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in Set.univ, f (b, ω) ∂ρ.condKernel b ∂ρ.fst
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>a b : α<VAR>m n : ℕ<VAR>h : a ≠ b<GOAL>l ~ replicate m a ++ replicate n b ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>a b : α<VAR>m n : ℕ<VAR>h : a ≠ b<GOAL>(count a l = count a (replicate m a ++ replicate n b) ∧ (b ≠ a → count b l = count b (replicate m a ++ replicate n b)) ∧ ∀ (b_1 : α), b_1 ≠ b → b_1 ≠ a → count b_1 l = count b_1 (replicate m a ++ replicate n b)) ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l₁ l₂ : List α<VAR>a✝ : α<VAR>inst✝ : DecidableEq α<VAR>l : List α<VAR>a b : α<VAR>m n : ℕ<VAR>h : a ≠ b<GOAL>l ⊆ [a, b] ↔ ∀ (c : α), c ≠ b → c ≠ a → c ∉ l
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>n : ℕ<VAR>φ ψ : MvPolynomial σ R<VAR>d : σ →₀ ℕ<GOAL>coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ) = coeff d φ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>n : ℕ<VAR>φ ψ : MvPolynomial σ R<VAR>d : σ →₀ ℕ<GOAL>φ.totalDegree < d.support.sum ⇑d → 0 = coeff d φ
<VAR>k : ℤ<GOAL>(k + k).negOnePow = 1
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<GOAL>x * y = (algebraMap K[X] (RatFunc K)) (x.num * y.num) / (algebraMap K[X] (RatFunc K)) (x.denom * y.denom)
<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>s : Finset β<VAR>t : Finset γ<VAR>f : β × γ → α<GOAL>(s ×ˢ t).sup f = t.sup fun i' => s.sup fun i => f (i, i')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>s : Finset β<VAR>f : β → α<GOAL>∏' (x : { x // x ∈ s }), f ↑x = ∏ x ∈ s, f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f✝ g : β → α<VAR>a a₁ a₂ : α<VAR>s : Finset β<VAR>f : β → α<GOAL>∏' (x : { x // x ∈ s }), f ↑x = ∏ x ∈ s.attach, f ↑x
<VAR>R : Type u<VAR>L : Type v<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>h₁ : LieAlgebra.IsNilpotent R L<VAR>f : L →ₗ⁅R⁆ L'<VAR>h₂ : Surjective ⇑f<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L L k = ⊥<GOAL>∃ k, lowerCentralSeries R L' L' k = ⊥
<VAR>R : Type u<VAR>L : Type v<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>h₁ : LieAlgebra.IsNilpotent R L<VAR>f : L →ₗ⁅R⁆ L'<VAR>h₂ : Surjective ⇑f<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L L k = ⊥<GOAL>lowerCentralSeries R L' L' k = ⊥
<VAR>R : Type u<VAR>L : Type v<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>h₁ : LieAlgebra.IsNilpotent R L<VAR>f : L →ₗ⁅R⁆ L'<VAR>h₂ : Surjective ⇑f<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L L k = ⊥<GOAL>LieIdeal.map f ⊥ = ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : (x : α) → Decidable ¬p x<GOAL>(filter p s).card + (filter (fun a => ¬p a) s).card = s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E'<VAR>g₁ g₂ : α → F'<VAR>h₁ : f₁ =o[l] g<VAR>h₂ : f₂ =o[l] g<GOAL>(fun x => f₁ x - f₂ x) =o[l] g
<VAR>E : ℕ → Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Encodable ι<VAR>F : ι → Type u_3<VAR>inst✝ : (i : ι) → MetricSpace (F i)<VAR>x y : (i : ι) → F i<GOAL>Summable fun i => min ((1 / 2) ^ encode i) (dist (x i) (y i))
<VAR>E : ℕ → Type u_1<VAR>ι : Type u_2<VAR>inst✝¹ : Encodable ι<VAR>F : ι → Type u_3<VAR>inst✝ : (i : ι) → MetricSpace (F i)<VAR>x y : (i : ι) → F i<VAR>i : ι<GOAL>0 ≤ min ((1 / 2) ^ encode i) (dist (x i) (y i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α → ℝ≥0∞<VAR>a_mble : Measurable a<VAR>c : ℝ≥0∞<VAR>tsum_le_c : ∑' (i : α), a i ≤ c<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<VAR>ε_ne_top : ε ≠ ⊤<GOAL>count {i | ε ≤ a i} ≤ c / ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α → ℝ≥0∞<VAR>a_mble : Measurable a<VAR>c : ℝ≥0∞<VAR>tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<VAR>ε_ne_top : ε ≠ ⊤<GOAL>count {i | ε ≤ a i} ≤ c / ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSingletonClass α<VAR>a : α → ℝ≥0∞<VAR>a_mble : Measurable a<VAR>c : ℝ≥0∞<VAR>tsum_le_c : ∫⁻ (a_1 : α), a a_1 ∂count ≤ c<VAR>ε : ℝ≥0∞<VAR>ε_ne_zero : ε ≠ 0<VAR>ε_ne_top : ε ≠ ⊤<GOAL>(∫⁻ (a_1 : α), a a_1 ∂count) / ε ≤ c / ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>x✝ : ℕ<GOAL>Tendsto (fun x => x.eraseIdx x✝) (𝓝 []) (𝓝 ([].eraseIdx x✝))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>x✝ : ℕ<GOAL>Tendsto (fun x => x.eraseIdx x✝) (pure []) (𝓝 ([].eraseIdx x✝))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<VAR>l : List α<GOAL>Tendsto (fun x => x.eraseIdx 0) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx 0))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>a : α<VAR>l : List α<GOAL>Tendsto (fun p => (p.1 :: p.2).eraseIdx 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx 0))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>Tendsto (fun x => x.eraseIdx (n + 1)) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx (n + 1)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>Tendsto (fun p => (p.1 :: p.2).eraseIdx (n + 1)) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx (n + 1)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>Tendsto (fun p => p.1 :: p.2.eraseIdx n) (𝓝 a ×ˢ 𝓝 l) (𝓝 (a :: l.eraseIdx n))
<VAR>s : ℝ<GOAL>Complex.Gamma ↑s = ↑(Gamma s)
<VAR>m n : Nat<VAR>H : 0 < m.gcd n<GOAL>(m / m.gcd n).Coprime (n / m.gcd n)
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>hx : x ≠ 0<VAR>θ : Real.Angle<GOAL>x = (o.rotation θ) x ↔ θ = 0
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝² : CommRing R✝<VAR>inst✝¹ : IsDomain R✝<VAR>p✝ q✝ : R✝[X]<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hmonic : q.Monic<VAR>hdegree : q.degree ≤ p.degree<VAR>a✝ : Nontrivial R<GOAL>(p /ₘ q).leadingCoeff = p.leadingCoeff
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝² : CommRing R✝<VAR>inst✝¹ : IsDomain R✝<VAR>p✝ q✝ : R✝[X]<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hmonic : q.Monic<VAR>hdegree : q.degree ≤ p.degree<VAR>a✝ : Nontrivial R<VAR>h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0<GOAL>(p /ₘ q).leadingCoeff = p.leadingCoeff
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝² : CommRing R✝<VAR>inst✝¹ : IsDomain R✝<VAR>p✝ q✝ : R✝[X]<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hmonic : q.Monic<VAR>hdegree : q.degree ≤ p.degree<VAR>a✝ : Nontrivial R<VAR>h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0<GOAL>(p /ₘ q).leadingCoeff = (p %ₘ q + q * (p /ₘ q)).leadingCoeff
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝² : CommRing R✝<VAR>inst✝¹ : IsDomain R✝<VAR>p✝ q✝ : R✝[X]<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hmonic : q.Monic<VAR>hdegree : q.degree ≤ p.degree<VAR>a✝ : Nontrivial R<VAR>h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0<GOAL>(p %ₘ q).degree < (q * (p /ₘ q)).degree
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝² : CommRing R✝<VAR>inst✝¹ : IsDomain R✝<VAR>p✝ q✝ : R✝[X]<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hmonic : q.Monic<VAR>hdegree : q.degree ≤ p.degree<VAR>a✝ : Nontrivial R<VAR>h : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0<GOAL>(p %ₘ q).degree < p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<GOAL>(C a * X ^ n).divX = if n = 0 then 0 else C a * X ^ (n - 1)
<VAR>a : ℤ<GOAL>J(a | 1) = 1
<VAR>m n : ℕ<GOAL>(finRotate n.succ) 0 = 1
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ : L → R<VAR>m : M<GOAL>m ∈ ↑(weightSpace M (χ ∘ ⇑⊤.incl)) ↔ m ∈ ↑(weightSpace M χ)