ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedAddCommGroup E'<VAR>inst✝¹⁵ : NormedAddCommGroup E''<VAR>inst✝¹⁴ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>inst✝¹¹ : NormedSpace 𝕜 E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E''<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁸ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : AddGroup G<VAR>inst✝⁵ : TopologicalSpace G<VAR>inst✝⁴ : TopologicalAddGroup G<VAR>inst✝³ : BorelSpace G<VAR>inst✝² : TopologicalSpace P<VAR>inst✝¹ : FirstCountableTopology G<VAR>inst✝ : SecondCountableTopologyEither G E'<VAR>hbg : BddAbove (range fun x => ‖g x‖)<VAR>hf : Integrable f μ<VAR>hg : Continuous g<VAR>x₀ : G<VAR>this : ∀ᶠ (x : G) in 𝓝 x₀, ∀ᵐ (t : G) ∂μ, ‖(L (f t)) (g (x - t))‖ ≤ ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖<GOAL>∀ᵐ (a : G) ∂μ, ContinuousAt (fun x => (L (f a)) (g (x - a))) x₀
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : DivisionMonoid M<VAR>a b : M<VAR>ha : a ∈ center M<GOAL>a⁻¹ ∈ center M
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : DivisionMonoid M<VAR>a b : M<VAR>ha : a ∈ center M<GOAL>∀ (g : M), g * a⁻¹ = a⁻¹ * g
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : DivisionMonoid M<VAR>a b : M<VAR>ha : a ∈ center M<VAR>g✝ : M<GOAL>g✝ * a⁻¹ = a⁻¹ * g✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n n' m : ℕ<VAR>s : Sym α n<VAR>a b : α<VAR>m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - ↑i)<VAR>h : ↑m₁.snd = ↑m₂.snd<GOAL>↑m₁.fst = ↑m₂.fst
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f : L.obj X ⟶ L.obj Y<GOAL>add' W f (L.map 0) = f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction X Y<VAR>hα : f = α.map L ⋯<GOAL>add' W f (L.map 0) = f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction X Y<VAR>hα : f = α.map L ⋯<GOAL>(LeftFraction₂.mk α.f 0 α.s ⋯).add.map L ⋯ = α.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction X Y<VAR>hα : f = α.map L ⋯<GOAL>L.map 0 = (LeftFraction₂.mk α.f 0 α.s ⋯).snd.map L ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>inst✝² : Preadditive C<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>f : L.obj X ⟶ L.obj Y<VAR>α : W.LeftFraction X Y<VAR>hα : f = α.map L ⋯<GOAL>(LeftFraction.mk (α.f + 0) α.s ⋯).map L ⋯ = α.map L ⋯
<VAR>J K : Type v<VAR>inst✝⁵ : SmallCategory J<VAR>inst✝⁴ : SmallCategory K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>inst✝² : HasLimitsOfShape K C<VAR>inst✝¹ : HasLimit (uncurry.obj F)<VAR>inst✝ : HasLimit (F ⋙ lim)<VAR>j : J<VAR>k : K<GOAL>(limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) = limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k
<VAR>J K : Type v<VAR>inst✝⁵ : SmallCategory J<VAR>inst✝⁴ : SmallCategory K<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>F : J ⥤ K ⥤ C<VAR>inst✝² : HasLimitsOfShape K C<VAR>inst✝¹ : HasLimit (uncurry.obj F)<VAR>inst✝ : HasLimit (F ⋙ lim)<VAR>j : J<VAR>k : K<GOAL>(limitUncurryIsoLimitCompLim F).hom ≫ (limitUncurryIsoLimitCompLim F).inv ≫ limit.π (uncurry.obj F) (j, k) = (limitUncurryIsoLimitCompLim F).hom ≫ limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝³ : CommRing A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : IsDomain B<VAR>p : A[X]<VAR>f : A →+* B<VAR>hf : Function.Injective ⇑f<VAR>hp0 : ¬p = 0<GOAL>Multiset.map (⇑f) p.roots ≤ (map f p).roots
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p q : Multiset (Associates α)<GOAL>(∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p q : Multiset (Associates α)<GOAL>∀ (s : Multiset α), (∀ a ∈ Multiset.map (Quot.mk Setoid.r) s, Irreducible a) → (∀ a ∈ q, Irreducible a) → (Multiset.map (Quot.mk Setoid.r) s).prod = q.prod → Multiset.map (Quot.mk Setoid.r) s = q
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p q : Multiset (Associates α)<GOAL>∀ (s s_1 : Multiset α), (∀ a ∈ Multiset.map (Quot.mk Setoid.r) s_1, Irreducible a) → (∀ a ∈ Multiset.map (Quot.mk Setoid.r) s, Irreducible a) → (Multiset.map (Quot.mk Setoid.r) s_1).prod = (Multiset.map (Quot.mk Setoid.r) s).prod → Multiset.map (Quot.mk Setoid.r) s_1 = Multiset.map (Quot.mk Setoid.r) s
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p q : Multiset (Associates α)<VAR>s t : Multiset α<VAR>hs : ∀ a ∈ Multiset.map (Quot.mk Setoid.r) t, Irreducible a<VAR>ht : ∀ a ∈ Multiset.map (Quot.mk Setoid.r) s, Irreducible a<VAR>eq : (Multiset.map (Quot.mk Setoid.r) t).prod = (Multiset.map (Quot.mk Setoid.r) s).prod<GOAL>Multiset.map (Quot.mk Setoid.r) t = Multiset.map (Quot.mk Setoid.r) s
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p q : Multiset (Associates α)<VAR>s t : Multiset α<VAR>hs : ∀ a ∈ Multiset.map (Quot.mk Setoid.r) t, Irreducible a<VAR>ht : ∀ a ∈ Multiset.map (Quot.mk Setoid.r) s, Irreducible a<VAR>eq : (Multiset.map (Quot.mk Setoid.r) t).prod = (Multiset.map (Quot.mk Setoid.r) s).prod<GOAL>∀ x ∈ t, Irreducible x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p q : Multiset (Associates α)<VAR>s t : Multiset α<VAR>hs : ∀ a ∈ Multiset.map (Quot.mk Setoid.r) t, Irreducible a<VAR>ht : ∀ a ∈ Multiset.map (Quot.mk Setoid.r) s, Irreducible a<VAR>eq : (Multiset.map (Quot.mk Setoid.r) t).prod = (Multiset.map (Quot.mk Setoid.r) s).prod<GOAL>∀ x ∈ s, Irreducible x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p q : Multiset (Associates α)<VAR>s t : Multiset α<VAR>hs : ∀ a ∈ Multiset.map (Quot.mk Setoid.r) t, Irreducible a<VAR>ht : ∀ a ∈ Multiset.map (Quot.mk Setoid.r) s, Irreducible a<VAR>eq : (Multiset.map (Quot.mk Setoid.r) t).prod = (Multiset.map (Quot.mk Setoid.r) s).prod<GOAL>t.prod ~ᵤ s.prod
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>p q : Multiset (Associates α)<VAR>s t : Multiset α<VAR>hs : ∀ a ∈ Multiset.map (Quot.mk Setoid.r) t, Irreducible a<VAR>ht : ∀ a ∈ Multiset.map (Quot.mk Setoid.r) s, Irreducible a<VAR>eq : (Multiset.map (Quot.mk Setoid.r) t).prod = (Multiset.map (Quot.mk Setoid.r) s).prod<VAR>eq' : Quot.mk Setoid.r = Associates.mk<GOAL>t.prod ~ᵤ s.prod
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : Nontrivial R<VAR>y : R[X]<GOAL>(Y - C y).natDegree < W.polynomial.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>inst✝ : Nontrivial R<VAR>y : R[X]<GOAL>1 < 2
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<GOAL>∑ k ∈ Ico 1 (n + 1), ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<GOAL>∑ k ∈ Ico 1 (n + 1), ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli' i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑p.succ
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<VAR>f : ℕ → ℚ := fun i => bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<VAR>f' : ℕ → ℚ := fun i => bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<GOAL>∑ k ∈ Ico 1 n.succ, ↑k ^ p.succ = ∑ i ∈ range p.succ.succ, f' i
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<VAR>f : ℕ → ℚ := fun i => bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<VAR>f' : ℕ → ℚ := fun i => bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<VAR>hle : 1 ≤ n + 1<GOAL>∑ k ∈ Ico 1 n.succ, ↑k ^ p.succ = ∑ i ∈ range p.succ.succ, f' i
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<VAR>f : ℕ → ℚ := fun i => bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<VAR>f' : ℕ → ℚ := fun i => bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<VAR>hle : 1 ≤ n + 1<VAR>hne : ↑p + 1 + 1 ≠ 0<GOAL>∑ k ∈ Ico 1 n.succ, ↑k ^ p.succ = ∑ i ∈ range p.succ.succ, f' i
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<VAR>f : ℕ → ℚ := fun i => bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<VAR>f' : ℕ → ℚ := fun i => bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<VAR>hle : 1 ≤ n + 1<VAR>hne : ↑p + 1 + 1 ≠ 0<VAR>h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ<GOAL>∑ k ∈ Ico 1 n.succ, ↑k ^ p.succ = ∑ i ∈ range p.succ.succ, f' i
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<VAR>f : ℕ → ℚ := fun i => bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<VAR>f' : ℕ → ℚ := fun i => bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<VAR>hle : 1 ≤ n + 1<VAR>hne : ↑p + 1 + 1 ≠ 0<VAR>h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ<VAR>h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ<GOAL>∑ k ∈ Ico 1 n.succ, ↑k ^ p.succ = ∑ i ∈ range p.succ.succ, f' i
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n p : ℕ<VAR>f : ℕ → ℚ := fun i => bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<VAR>f' : ℕ → ℚ := fun i => bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ<VAR>hle : 1 ≤ n + 1<VAR>hne : ↑p + 1 + 1 ≠ 0<VAR>h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ<VAR>h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ<VAR>this : ∑ i ∈ range p, bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) = ∑ i ∈ range p, bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)<GOAL>∑ k ∈ Ico 1 n.succ, ↑k ^ p.succ = ∑ i ∈ range p.succ.succ, f' i
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>(-x).IsOption (-y) ↔ x.IsOption y
<VAR>α : Type u<VAR>t✝ : TopologicalSpace α<VAR>β : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set (Set α)<VAR>hs : IsTopologicalBasis s<VAR>t : Set (Set β)<VAR>ht : IsTopologicalBasis t<GOAL>IsTopologicalBasis ((fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t)
<VAR>α : Type u<VAR>t✝ : TopologicalSpace α<VAR>β : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set (Set α)<VAR>hs : IsTopologicalBasis s<VAR>t : Set (Set β)<VAR>ht : IsTopologicalBasis t<GOAL>∀ u ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, IsOpen u
<VAR>α : Type u<VAR>t✝ : TopologicalSpace α<VAR>β : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalSpace β<VAR>s : Set (Set α)<VAR>hs : IsTopologicalBasis s<VAR>t : Set (Set β)<VAR>ht : IsTopologicalBasis t<GOAL>∀ (a : α ⊕ β) (u : Set (α ⊕ β)), a ∈ u → IsOpen u → ∃ v ∈ (fun u => Sum.inl '' u) '' s ∪ (fun u => Sum.inr '' u) '' t, a ∈ v ∧ v ⊆ u
<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 : ℤ<VAR>z₁ z₂ : Cochain F G 0<VAR>h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯<VAR>p q : ℤ<VAR>hpq : p + 0 = q<GOAL>z₁.v p q hpq = z₂.v p q hpq
<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 : ℤ<VAR>z₁ z₂ : Cochain F G 0<VAR>h : ∀ (p : ℤ), z₁.v p p ⋯ = z₂.v p p ⋯<VAR>q : ℤ<VAR>hpq : q + 0 = q<GOAL>z₁.v q q hpq = z₂.v q q hpq
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>h : Disjoint s t<GOAL>⨆ a ∈ s, LinearMap.range (lsingle a) ≤ ⨅ a ∈ t, ker (lapply a)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>h : Disjoint s t<VAR>a₁ : α<VAR>h₁ : a₁ ∈ s<GOAL>comap (lsingle a₁) (⨅ a ∈ t, ker (lapply a)) = ⊤
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>h : Disjoint s t<VAR>a₁ : α<VAR>h₁ : a₁ ∈ s<GOAL>∀ ⦃x : M⦄, x ∈ ⊤ → ∀ i ∈ t, (lapply i ∘ₗ lsingle a₁) x = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>h : Disjoint s t<VAR>a₁ : α<VAR>h₁ : a₁ ∈ s<VAR>b : M<VAR>a✝ : b ∈ ⊤<VAR>a₂ : α<VAR>h₂ : a₂ ∈ t<GOAL>(lapply a₂ ∘ₗ lsingle a₁) b = 0
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>h : Disjoint s t<VAR>a₁ : α<VAR>h₁ : a₁ ∈ s<VAR>b : M<VAR>a✝ : b ∈ ⊤<VAR>a₂ : α<VAR>h₂ : a₂ ∈ t<VAR>this : a₁ ≠ a₂<GOAL>(lapply a₂ ∘ₗ lsingle a₁) b = 0
<VAR>n : ℕ+<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hn : 2 < n<GOAL>NrRealPlaces K = 0
<VAR>n : ℕ+<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hn : 2 < n<VAR>this : NumberField K<GOAL>NrRealPlaces K = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>f : R⟦X⟧<VAR>inst✝ : Invertible f<GOAL>(d⁄dX R) ⅟f = -⅟f ^ 2 * (d⁄dX R) f
<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>↑(nnabs x) = ↑x.toNNReal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra A B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R A B<VAR>x : A<VAR>p : R[X]<GOAL>(aeval ((algebraMap A B) x)) p = (algebraMap A B) ((aeval x) p)
<GOAL>Tendsto (fun n => ↑(harmonic n) - log ↑n) atTop (𝓝 eulerMascheroniConstant)
<GOAL>eulerMascheroniSeq' =ᶠ[atTop] fun n => ↑(harmonic n) - log ↑n
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>eulerMascheroniSeq' n = ↑(harmonic n) - log ↑n
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>h_mf : Measurable f<GOAL>∀ {g : α → ℝ≥0∞}, Measurable g → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>h_mf : Measurable f<GOAL>∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → ∫⁻ (a : α), s.indicator (fun x => c) a ∂μ.withDensity f = ∫⁻ (a : α), (f * s.indicator fun x => c) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>h_mf : Measurable f<GOAL>∀ ⦃f_1 g : α → ℝ≥0∞⦄, Disjoint (Function.support f_1) (Function.support g) → Measurable f_1 → Measurable g → ∫⁻ (a : α), f_1 a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1) a ∂μ → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ → ∫⁻ (a : α), (f_1 + g) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (f_1 + g)) a ∂μ
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ✝ μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>h_mf : Measurable f<GOAL>∀ ⦃f_1 : ℕ → α → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f_1 n)) → Monotone f_1 → (∀ (n : ℕ), ∫⁻ (a : α), f_1 n a ∂μ.withDensity f = ∫⁻ (a : α), (f * f_1 n) a ∂μ) → ∫⁻ (a : α), (fun x => ⨆ n, f_1 n x) a ∂μ.withDensity f = ∫⁻ (a : α), (f * fun x => ⨆ n, f_1 n x) a ∂μ
<VAR>a b : Ordinal.{u_1}<GOAL>a + b ≤ b ↔ a * ω ≤ b
<VAR>a b : Ordinal.{u_1}<GOAL>a + b ≤ b ↔ a + b = b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b ≠ 0<GOAL>P.toPoly.natDegree = 2
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>α : Sort u_5<VAR>E : α → Sort u_4<GOAL>IsEmpty (PSigma E) ↔ ∀ (a : α), IsEmpty (E a)
<VAR>g : SL(2, ℤ)<GOAL>↑(T * g) 1 = ↑g 1
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : Y → Prop<VAR>s : Set X<VAR>hx : x ∈ e.source<GOAL>(∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (x : X) in 𝓝[s] x, p (↑e x)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>p : Y → Prop<VAR>s : Set X<VAR>hx : x ∈ e.source<GOAL>(∀ᶠ (y : Y) in 𝓝[↑e.symm ⁻¹' s] ↑e x, p y) ↔ ∀ᶠ (b : Y) in map (↑e) (𝓝[s] x), p b
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>h : S.HomologyData<GOAL>leftRightHomologyComparison' h.left h.right = h.iso.hom
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CompleteLattice α<VAR>h : IsAtomistic αᵒᵈ<VAR>b : α<GOAL>∃ s, b = sInf s ∧ ∀ a ∈ s, IsCoatom a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CompleteLattice α<VAR>h : IsCoatomistic α<VAR>b : αᵒᵈ<GOAL>∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>x : S<VAR>i : Fin f.natDegree<GOAL>(h.basis.repr x) i = (h.modByMonicHom x).coeff ↑i
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>x : S<VAR>i : Fin f.natDegree<GOAL>(Finsupp.comapDomain Fin.val (h.modByMonicHom x).toFinsupp ⋯) i = (h.modByMonicHom x).coeff ↑i
<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>inst✝ : Nonempty ι<VAR>s : ι → Set α<VAR>f : α → β<VAR>h : InjOn f (⋃ i, s i)<VAR>inhabited_h : Inhabited ι<GOAL>f '' ⋂ i, s i = ⋂ i, f '' s i
<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>inst✝ : Nonempty ι<VAR>s : ι → Set α<VAR>f : α → β<VAR>h : InjOn f (⋃ i, s i)<VAR>inhabited_h : Inhabited ι<VAR>y : β<VAR>hy : y ∈ ⋂ i, f '' s i<GOAL>y ∈ f '' ⋂ i, s i
<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>inst✝ : Nonempty ι<VAR>s : ι → Set α<VAR>f : α → β<VAR>h : InjOn f (⋃ i, s i)<VAR>inhabited_h : Inhabited ι<VAR>y : β<VAR>hy : ∀ (i : ι), ∃ x ∈ s i, f x = y<GOAL>y ∈ f '' ⋂ i, s i
<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>inst✝ : Nonempty ι<VAR>s : ι → Set α<VAR>f : α → β<VAR>h : InjOn f (⋃ i, s i)<VAR>inhabited_h : Inhabited ι<VAR>y : β<VAR>x : ι → α<VAR>hx : ∀ (i : ι), x i ∈ s i<VAR>hy : ∀ (i : ι), f (x i) = y<GOAL>y ∈ f '' ⋂ i, s i
<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>inst✝ : Nonempty ι<VAR>s : ι → Set α<VAR>f : α → β<VAR>h : InjOn f (⋃ i, s i)<VAR>inhabited_h : Inhabited ι<VAR>y : β<VAR>x : ι → α<VAR>hx : ∀ (i : ι), x i ∈ s i<VAR>hy : ∀ (i : ι), f (x i) = y<VAR>i : ι<GOAL>x default ∈ s i
<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>inst✝ : Nonempty ι<VAR>s : ι → Set α<VAR>f : α → β<VAR>h : InjOn f (⋃ i, s i)<VAR>inhabited_h : Inhabited ι<VAR>y : β<VAR>x : ι → α<VAR>hx : ∀ (i : ι), x i ∈ s i<VAR>hy : ∀ (i : ι), f (x i) = y<VAR>i : ι<GOAL>x default = x i
<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>inst✝ : Nonempty ι<VAR>s : ι → Set α<VAR>f : α → β<VAR>h : InjOn f (⋃ i, s i)<VAR>inhabited_h : Inhabited ι<VAR>y : β<VAR>x : ι → α<VAR>hy : ∀ (i : ι), f (x i) = y<VAR>i : ι<VAR>hx : ∀ (i : ι), x i ∈ ⋃ j, s j<GOAL>x default = x i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a b c d : α<VAR>h : a⁻¹ * b = 1<GOAL>a = b
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝¹ : NonAssocSemiring α<VAR>inst✝ : DecidableEq m<VAR>a : α<GOAL>MulOpposite.op a • 1 = diagonal fun x => a
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>A : Type u_2<VAR>inst✝¹ : Category.{?u.74494, u_2} A<VAR>inst✝ : Abelian A<VAR>X Y : CosimplicialObject C<VAR>n : ℕ<GOAL>objD X n = (AlternatingFaceMapComplex.objD ((cosimplicialSimplicialEquiv C).functor.obj (op X)) n).unop
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>A : Type u_2<VAR>inst✝¹ : Category.{?u.74494, u_2} A<VAR>inst✝ : Abelian A<VAR>X Y : CosimplicialObject C<VAR>n : ℕ<GOAL>∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i = ∑ x : Fin (n + 2), (-1) ^ ↑x • (((cosimplicialSimplicialEquiv C).functor.obj (op X)).δ x).unop