ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : PartialOrder α<VAR>s✝ : LowerSet α<VAR>a : α<VAR>s t : LowerSet α<VAR>hst : s ⊔ t = Iic a<VAR>this : a ∈ s ⊔ t<GOAL>s = Iic a ∨ t = Iic a
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f x✝¹ x✝ : RatFunc R<VAR>h : (laurent r) x✝¹ = (laurent r) x✝<GOAL>x✝¹ = x✝
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>S : Type u_3<VAR>M₀ : Type u_4<VAR>M₁ : Type u_5<VAR>R : Type u_6<VAR>G : Type u_7<VAR>G₀ : Type u_8<VAR>inst✝⁷ : Mul M<VAR>inst✝⁶ : Monoid N<VAR>inst✝⁵ : Semigroup S<VAR>inst✝⁴ : MulZeroClass M₀<VAR>inst✝³ : MulOneClass M₁<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Group G<VAR>inst✝ : CancelMonoidWithZero G₀<VAR>p : N<VAR>n✝ : ℕ<VAR>h : IsIdempotentElem p<VAR>n : ℕ<VAR>x✝ : IsIdempotentElem (p ^ n)<GOAL>p ^ n.succ * p ^ n.succ = p ^ n.succ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>S : Type u_3<VAR>M₀ : Type u_4<VAR>M₁ : Type u_5<VAR>R : Type u_6<VAR>G : Type u_7<VAR>G₀ : Type u_8<VAR>inst✝⁷ : Mul M<VAR>inst✝⁶ : Monoid N<VAR>inst✝⁵ : Semigroup S<VAR>inst✝⁴ : MulZeroClass M₀<VAR>inst✝³ : MulOneClass M₁<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Group G<VAR>inst✝ : CancelMonoidWithZero G₀<VAR>p : N<VAR>n✝ : ℕ<VAR>h : IsIdempotentElem p<VAR>n : ℕ<VAR>x✝ : IsIdempotentElem (p ^ n)<GOAL>p ^ n.succ * p ^ n.succ = (p * p) ^ n.succ
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a : α<VAR>n : ℕ<GOAL>count a (replicate n a) = n
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a : α<VAR>n : ℕ<GOAL>count a (replicate n a) = List.count a (List.replicate n a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l m : Language α<VAR>a b x✝ : List α<VAR>l₁ l₂ m₁ m₂ : Language α<VAR>h₁ : l₁ ≤ m₁<VAR>h₂ : l₂ ≤ m₂<VAR>x : List α<VAR>hx : x ∈ l₁ * l₂<GOAL>x ∈ m₁ * m₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l m : Language α<VAR>a b x✝ : List α<VAR>l₁ l₂ m₁ m₂ : Language α<VAR>h₁ : l₁ ≤ m₁<VAR>h₂ : l₂ ≤ m₂<VAR>x : List α<VAR>hx : ∃ a ∈ l₁, ∃ b ∈ l₂, a ++ b = x<GOAL>∃ a ∈ m₁, ∃ b ∈ m₂, a ++ b = x
<VAR>u v : ℤ<VAR>h : u * v = 1<GOAL>u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
<VAR>u v : ℤ<VAR>h : u * v = 1<VAR>h' : v * u = 1<GOAL>u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1
<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>f g✝ : E → F<VAR>p✝ pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x✝ : E<VAR>r✝ r' : ℝ≥0∞<VAR>n✝ m : ℕ<VAR>s : Set E<VAR>g : F →L[𝕜] G<VAR>h : CPolynomialOn 𝕜 f s<VAR>x : E<VAR>hx : x ∈ s<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>r : ℝ≥0∞<VAR>hp : HasFiniteFPowerSeriesOnBall f p x n r<GOAL>CPolynomialAt 𝕜 (⇑g ∘ f) x
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>U : Set M<VAR>a b : M<VAR>hpc : IsPreconnected U<VAR>hc : IsCompact U<VAR>ho : IsOpen U<VAR>ha : a ∈ U<VAR>hb : b ∈ U<VAR>f : M → F<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hb₀ : f b = 0<GOAL>f a = f b
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>U : Set M<VAR>a b : M<VAR>hpc : IsPreconnected U<VAR>hc✝ : IsCompact U<VAR>ho : IsOpen U<VAR>ha : a ∈ U<VAR>hb : b ∈ U<VAR>f : M → F<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hb₀ : f b = 0<VAR>c : M<VAR>hcU : c ∈ U<VAR>hc : IsMaxOn (fun x => ‖f x‖) U c<GOAL>f a = f b
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℂ E<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℂ F<VAR>H : Type u_3<VAR>inst✝⁵ : TopologicalSpace H<VAR>I : ModelWithCorners ℂ E H<VAR>inst✝⁴ : I.Boundaryless<VAR>M : Type u_4<VAR>inst✝³ : TopologicalSpace M<VAR>inst✝² : CompactSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>U : Set M<VAR>a b : M<VAR>hpc : IsPreconnected U<VAR>hc✝ : IsCompact U<VAR>ho : IsOpen U<VAR>ha : a ∈ U<VAR>hb : b ∈ U<VAR>f : M → F<VAR>hd : MDifferentiableOn I 𝓘(ℂ, F) f U<VAR>hb₀ : f b = 0<VAR>c : M<VAR>hcU : c ∈ U<VAR>hc : IsMaxOn (fun x => ‖f x‖) U c<VAR>this : ∀ x ∈ U, ‖f x‖ = ‖f c‖<GOAL>f a = f b
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>a : E<VAR>c : Fin n → ℂ<VAR>R : Fin n → ℝ<GOAL>TorusIntegrable (fun x => a) c R
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>hf : (mulSupport (f ∘ PLift.down)).Finite<VAR>s : Finset (PLift α)<VAR>hs : hf.toFinset ⊆ s<GOAL>∏ᶠ (i : α), f i = ∏ i ∈ s, f i.down
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>hf : (mulSupport (f ∘ PLift.down)).Finite<VAR>s : Finset (PLift α)<VAR>hs : hf.toFinset ⊆ s<GOAL>∏ i ∈ ?hc.toFinset, f i.down = ∏ i ∈ s, f i.down
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>hf : (mulSupport (f ∘ PLift.down)).Finite<VAR>s : Finset (PLift α)<VAR>hs : hf.toFinset ⊆ s<GOAL>(mulSupport ((fun i => f i) ∘ PLift.down)).Finite
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>hf : (mulSupport (f ∘ PLift.down)).Finite<VAR>s : Finset (PLift α)<VAR>hs : hf.toFinset ⊆ s<VAR>x : PLift α<VAR>x✝ : x ∈ s<VAR>hxf : x ∉ hf.toFinset<GOAL>f x.down = 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<GOAL>I.jacobson = I ↔ ⊥.jacobson = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>I : Ideal R<VAR>hf : Function.Surjective ⇑(Quotient.mk I)<GOAL>I.jacobson = I ↔ ⊥.jacobson = ⊥
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>G.chromaticNumber ≤ ↑n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>↑(sInf {n' | G.Colorable n'}) ≤ ↑n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>sInf {n' | G.Colorable n'} ≤ n
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>C : G.Coloring α<VAR>n : ℕ<VAR>hc : G.Colorable n<GOAL>n ∈ {n | G.Colorable n}
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : IsEmpty α<VAR>f : α → M<GOAL>∏ᶠ (i : α), f i = 1
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : IsEmpty α<VAR>f : α → M<GOAL>∏ᶠ (i : α), f i = ∏ᶠ (x : ?m.12512), 1
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : IsEmpty α<VAR>f : α → M<GOAL>Sort ?u.12509
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : IsEmpty α<VAR>f : α → M<GOAL>(fun i => f i) = fun x => 1
<VAR>z : 𝔻<GOAL>normSq ↑z < 1
<VAR>z : 𝔻<GOAL>1 = 1 ^ 2
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>m : M<VAR>h : torsionOf R M m = ⊤<GOAL>m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>m : M<VAR>h : torsionOf R M m = ⊤<GOAL>1 ∈ ⊤
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝³ : Monoid β<VAR>inst✝² : Monoid γ<VAR>inst✝¹ : FunLike F β γ<VAR>inst✝ : MonoidHomClass F β γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>g : F<GOAL>g (s.noncommProd f comm) = s.noncommProd (fun i => g (f i)) ⋯
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x✝ y✝ z x y : E<VAR>c : 𝕜<GOAL>openSegment 𝕜 x y ⊆ insert ((lineMap x y) c) (openSegment 𝕜 x ((lineMap x y) c) ∪ openSegment 𝕜 ((lineMap x y) c) y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x✝ y✝ z x y : E<VAR>c : 𝕜<GOAL>MapsTo (⇑(lineMap x y)) (Ioo 0 1) (insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x✝ y✝ z x y : E<VAR>c a : 𝕜<VAR>h₀ : 0 < a<VAR>h₁ : a < 1<GOAL>(lineMap x y) a ∈ insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x✝ y✝ z x y : E<VAR>c a : 𝕜<VAR>h₀ : 0 < a<VAR>h₁ : a < 1<VAR>hac : a < c<GOAL>(lineMap x y) a ∈ insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x✝ y✝ z x y : E<VAR>a : 𝕜<VAR>h₀ : 0 < a<VAR>h₁ : a < 1<GOAL>(lineMap x y) a ∈ insert ((lineMap x y) a) (⇑(lineMap x ((lineMap x y) a)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) a) y) '' Ioo 0 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>x✝ y✝ z x y : E<VAR>c a : 𝕜<VAR>h₀ : 0 < a<VAR>h₁ : a < 1<VAR>hca : c < a<GOAL>(lineMap x y) a ∈ insert ((lineMap x y) c) (⇑(lineMap x ((lineMap x y) c)) '' Ioo 0 1 ∪ ⇑(lineMap ((lineMap x y) c) y) '' Ioo 0 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>ho : o ≠ 0<VAR>c : α<GOAL>(o.brange fun x x => c) = {c}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>ho : o ≠ 0<VAR>c : α<GOAL>range (o.familyOfBFamily fun x x => c) = {c}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>Odd (m - n) ↔ (Odd n ↔ Even m)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>e : ι₂ ↪ ι<VAR>w : ι → k<VAR>p : ι → P<GOAL>(affineCombination k (map e s₂) p) w = (affineCombination k s₂ (p ∘ ⇑e)) (w ∘ ⇑e)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f g : α → F<VAR>hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊<GOAL>eLpNorm' f q μ = eLpNorm' g q μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f g : α → F<VAR>hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ = ‖g x‖₊<VAR>this : (fun x => ↑‖f x‖₊ ^ q) =ᶠ[ae μ] fun x => ↑‖g x‖₊ ^ q<GOAL>eLpNorm' f q μ = eLpNorm' g q μ
<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>φ : S₁ ⟶ S₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<GOAL>(leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData).op = rightHomologyMap' (𝟙 S₂.op) S₂.leftHomologyData.op S₂.op.rightHomologyData ≫ rightHomologyMap' (opMap φ) S₂.op.rightHomologyData S₁.op.rightHomologyData ≫ rightHomologyMap' (𝟙 S₁.op) S₁.op.rightHomologyData S₁.leftHomologyData.op
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<VAR>x : E<VAR>h : IsVonNBounded 𝕜 (x +ᵥ s)<GOAL>IsVonNBounded 𝕜 s
<VAR>a b : ℕ+<GOAL>(a.xgcd b).y + (a.xgcd b).zp + 1 = (a.xgcd b).y + ((a.xgcd b).zp + 1)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p₁ p₂ : P<VAR>s : AffineSubspace k P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<GOAL>affineSpan k {p₁, p₂} ≤ s
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p₁ p₂ : P<VAR>s : AffineSubspace k P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<GOAL>p₁ ∈ ↑s ∧ p₂ ∈ ↑s
<VAR>p n k : ℕ<VAR>h : ¬(n.choose k).factorization p = 0<GOAL>(n.choose k).factorization p ≤ log p n
<VAR>p n k : ℕ<VAR>h : ¬(n.choose k).factorization p = 0<VAR>hp : Prime p<GOAL>(n.choose k).factorization p ≤ log p n
<VAR>p n k : ℕ<VAR>h : ¬(n.choose k).factorization p = 0<VAR>hp : Prime p<VAR>hkn : k ≤ n<GOAL>(n.choose k).factorization p ≤ log p n
<VAR>p n k : ℕ<VAR>h : ¬(n.choose k).factorization p = 0<VAR>hp : Prime p<VAR>hkn : k ≤ n<GOAL>(multiplicity p (n.choose k)).get ⋯ ≤ log p n
<VAR>p n k : ℕ<VAR>h : ¬(n.choose k).factorization p = 0<VAR>hp : Prime p<VAR>hkn : k ≤ n<GOAL>(Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 (log p n + 1))).card ≤ log p n
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H : Subgroup G<VAR>a b : G<GOAL>(setoid ↑⊥ ↑H).Rel a b ↔ (QuotientGroup.leftRel H).Rel a b
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>α : Type u_2<VAR>inst✝ : Mul α<VAR>J : Subgroup G<VAR>g : G<VAR>H : Subgroup G<VAR>a b : G<GOAL>(∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>κ.density ν a x s ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>IsCoboundedUnder (fun x x_1 => x ≤ x_1) atTop fun n => κ.densityProcess ν n a x s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>x : γ<VAR>s : Set β<GOAL>∀ᶠ (n : ℕ) in atTop, κ.densityProcess ν n a x s ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ici a \ Ioi b = Icc a b
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<GOAL>M.Basis ∅ X ↔ X ⊆ M.closure ∅
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ c✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<VAR>g✝ h✝ : b✝ ⟶ c✝<VAR>η✝ : g✝ ⟶ h✝<GOAL>(prelaxfunctor.map₂ (Bicategory.whiskerLeft f✝ η✝)).app = (((fun {a b c} => mapComp) f✝ g✝).hom ≫ Bicategory.whiskerLeft (prelaxfunctor.map f✝) (prelaxfunctor.map₂ η✝) ≫ ((fun {a b c} => mapComp) f✝ h✝).inv).app
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ c✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<VAR>g✝ h✝ : b✝ ⟶ c✝<VAR>η✝ : g✝ ⟶ h✝<VAR>X : ↑(prelaxfunctor.obj a✝)<GOAL>(prelaxfunctor.map₂ (Bicategory.whiskerLeft f✝ η✝)).app X = (((fun {a b c} => mapComp) f✝ g✝).hom ≫ Bicategory.whiskerLeft (prelaxfunctor.map f✝) (prelaxfunctor.map₂ η✝) ≫ ((fun {a b c} => mapComp) f✝ h✝).inv).app X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ c✝ : Cat<VAR>f✝ g✝ : a✝ ⟶ b✝<VAR>η✝ : f✝ ⟶ g✝<VAR>h✝ : b✝ ⟶ c✝<GOAL>(prelaxfunctor.map₂ (Bicategory.whiskerRight η✝ h✝)).app = (((fun {a b c} => mapComp) f✝ h✝).hom ≫ Bicategory.whiskerRight (prelaxfunctor.map₂ η✝) (prelaxfunctor.map h✝) ≫ ((fun {a b c} => mapComp) g✝ h✝).inv).app
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ c✝ : Cat<VAR>f✝ g✝ : a✝ ⟶ b✝<VAR>η✝ : f✝ ⟶ g✝<VAR>h✝ : b✝ ⟶ c✝<VAR>X : ↑(prelaxfunctor.obj a✝)<GOAL>(prelaxfunctor.map₂ (Bicategory.whiskerRight η✝ h✝)).app X = (((fun {a b c} => mapComp) f✝ h✝).hom ≫ Bicategory.whiskerRight (prelaxfunctor.map₂ η✝) (prelaxfunctor.map h✝) ≫ ((fun {a b c} => mapComp) g✝ h✝).inv).app X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ c✝ d✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<VAR>g✝ : b✝ ⟶ c✝<VAR>h✝ : c✝ ⟶ d✝<GOAL>(prelaxfunctor.map₂ (Bicategory.associator f✝ g✝ h✝).hom).app = (((fun {a b c} => mapComp) (f✝ ≫ g✝) h✝).hom ≫ Bicategory.whiskerRight ((fun {a b c} => mapComp) f✝ g✝).hom (prelaxfunctor.map h✝) ≫ (Bicategory.associator (prelaxfunctor.map f✝) (prelaxfunctor.map g✝) (prelaxfunctor.map h✝)).hom ≫ Bicategory.whiskerLeft (prelaxfunctor.map f✝) ((fun {a b c} => mapComp) g✝ h✝).inv ≫ ((fun {a b c} => mapComp) f✝ (g✝ ≫ h✝)).inv).app
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ c✝ d✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<VAR>g✝ : b✝ ⟶ c✝<VAR>h✝ : c✝ ⟶ d✝<VAR>X : ↑(prelaxfunctor.obj a✝)<GOAL>(prelaxfunctor.map₂ (Bicategory.associator f✝ g✝ h✝).hom).app X = (((fun {a b c} => mapComp) (f✝ ≫ g✝) h✝).hom ≫ Bicategory.whiskerRight ((fun {a b c} => mapComp) f✝ g✝).hom (prelaxfunctor.map h✝) ≫ (Bicategory.associator (prelaxfunctor.map f✝) (prelaxfunctor.map g✝) (prelaxfunctor.map h✝)).hom ≫ Bicategory.whiskerLeft (prelaxfunctor.map f✝) ((fun {a b c} => mapComp) g✝ h✝).inv ≫ ((fun {a b c} => mapComp) f✝ (g✝ ≫ h✝)).inv).app X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<GOAL>(prelaxfunctor.map₂ (Bicategory.leftUnitor f✝).hom).app = (((fun {a b c} => mapComp) (𝟙 a✝) f✝).hom ≫ Bicategory.whiskerRight ((fun C => mapId ↑C) a✝).hom (prelaxfunctor.map f✝) ≫ (Bicategory.leftUnitor (prelaxfunctor.map f✝)).hom).app
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<VAR>X : ↑(prelaxfunctor.obj a✝)<GOAL>(prelaxfunctor.map₂ (Bicategory.leftUnitor f✝).hom).app X = (((fun {a b c} => mapComp) (𝟙 a✝) f✝).hom ≫ Bicategory.whiskerRight ((fun C => mapId ↑C) a✝).hom (prelaxfunctor.map f✝) ≫ (Bicategory.leftUnitor (prelaxfunctor.map f✝)).hom).app X
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<GOAL>(prelaxfunctor.map₂ (Bicategory.rightUnitor f✝).hom).app = (((fun {a b c} => mapComp) f✝ (𝟙 b✝)).hom ≫ Bicategory.whiskerLeft (prelaxfunctor.map f✝) ((fun C => mapId ↑C) b✝).hom ≫ (Bicategory.rightUnitor (prelaxfunctor.map f✝)).hom).app
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>a✝ b✝ : Cat<VAR>f✝ : a✝ ⟶ b✝<VAR>X : ↑(prelaxfunctor.obj a✝)<GOAL>(prelaxfunctor.map₂ (Bicategory.rightUnitor f✝).hom).app X = (((fun {a b c} => mapComp) f✝ (𝟙 b✝)).hom ≫ Bicategory.whiskerLeft (prelaxfunctor.map f✝) ((fun C => mapId ↑C) b✝).hom ≫ (Bicategory.rightUnitor (prelaxfunctor.map f✝)).hom).app X
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → α → M<VAR>x : Filter α<VAR>a : ι → M<VAR>s : Multiset ι<VAR>l : List ι<GOAL>(∀ i ∈ Quot.mk Setoid.r l, Tendsto (f i) x (𝓝 (a i))) → Tendsto (fun b => (Multiset.map (fun c => f c b) (Quot.mk Setoid.r l)).prod) x (𝓝 (Multiset.map a (Quot.mk Setoid.r l)).prod)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>L' : Type u_3<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field L'<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K L'<VAR>S✝ S : IntermediateField K L<VAR>x✝ : L<GOAL>x✝ ∈ S.toIntermediateField ⋯ ↔ x✝ ∈ S
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.121165, u_1} C<VAR>inst✝² : Category.{?u.121169, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>h : S.Splitting<GOAL>(h.s.op ≫ S.op.f + S.op.g ≫ h.r.op).unop = (𝟙 S.op.X₂).unop
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.121165, u_1} C<VAR>inst✝² : Category.{?u.121169, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>h : S.Splitting<GOAL>S.g ≫ h.s + h.r ≫ S.f = h.r ≫ S.f + S.g ≫ h.s
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>(cs.rightInvSeq ω).getD j 1 * (cs.rightInvSeq ω).getD j 1 = 1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>j : ℕ<GOAL>(cs.wordProd (drop (j + 1) ω))⁻¹ * ((Option.map cs.simple (ω.get? j)).getD 1 * (cs.wordProd (drop (j + 1) ω) * ((cs.wordProd (drop (j + 1) ω))⁻¹ * ((Option.map cs.simple (ω.get? j)).getD 1 * cs.wordProd (drop (j + 1) ω))))) = 1
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>f : X → Y<VAR>hf : Isometry f<VAR>H : Monotone m ∨ Surjective f<GOAL>(map f) (mkMetric m) = (restrict (range f)) (mkMetric m)
<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>f : R[X]<VAR>x✝ : X ∣ f<VAR>g : R[X]<VAR>hfg : f = X * g<GOAL>f.coeff 0 = 0
<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>f : R[X]<VAR>hf : f.coeff 0 = 0<GOAL>f = X * f.divX
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_6<VAR>inst✝⁷ : Monoid R<VAR>inst✝⁶ : Monoid S<VAR>σ : R → S<VAR>inst✝⁵ : MulAction R M<VAR>inst✝⁴ : MulAction S N<VAR>inst✝³ : MulAction R M₁<VAR>inst✝² : MulAction R M₂<VAR>F : Type u_7<VAR>h : F<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MulActionSemiHomClass F σ M N<VAR>c : R<VAR>s : Set M<VAR>t : Set N<VAR>hc : Function.Surjective fun m => c • m<VAR>hc' : Function.Injective fun n => σ c • n<GOAL>⇑h ⁻¹' (σ c • t) = c • ⇑h ⁻¹' t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_6<VAR>inst✝⁷ : Monoid R<VAR>inst✝⁶ : Monoid S<VAR>σ : R → S<VAR>inst✝⁵ : MulAction R M<VAR>inst✝⁴ : MulAction S N<VAR>inst✝³ : MulAction R M₁<VAR>inst✝² : MulAction R M₂<VAR>F : Type u_7<VAR>h : F<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MulActionSemiHomClass F σ M N<VAR>c : R<VAR>s : Set M<VAR>t : Set N<VAR>hc : Function.Surjective fun m => c • m<VAR>hc' : Function.Injective fun n => σ c • n<GOAL>⇑h ⁻¹' (σ c • t) ≤ c • ⇑h ⁻¹' t