ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝³ : EMetricSpace X<VAR>inst✝² : EMetricSpace Y<VAR>inst✝¹ : MeasurableSpace X<VAR>inst✝ : BorelSpace X<VAR>s : Set X<GOAL>dimH s = ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>s : Set X<VAR>inst✝ : BorelSpace X<VAR>this✝ : MeasurableSpace X := borel X<GOAL>dimH s = ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d
<VAR>m n k : ℕ<GOAL>m.Coprime (n + k * m) ↔ m.Coprime n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Div α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma / mb ∈ a / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Div α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>∃ a_1 ∈ a, ∃ a ∈ b, a_1 / a = ma / mb
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>n : ℤ<GOAL>preNormEDS b c d (-n) = -preNormEDS b c d n
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : InfinitePlace K → ℝ≥0<VAR>w₀ : { w // w.IsComplex }<GOAL>Convex ℝ (convexBodyLT' K f w₀)
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>f : InfinitePlace K → ℝ≥0<VAR>w₀ x✝¹ : { w // w.IsComplex }<VAR>x✝ : x✝¹ ∈ Set.univ<GOAL>Convex ℝ (if x✝¹ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑x✝¹) ^ 2} else ball 0 ↑(f ↑x✝¹))
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Injective f<GOAL>(map f) (OuterMeasure.ofFunction m m_empty) = OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>s : Set β<GOAL>(OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty) s ≤ ((map f) (OuterMeasure.ofFunction m m_empty)) s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>s : Set β<GOAL>∀ (i : ℕ → Set α), f ⁻¹' s ⊆ iUnion i → ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n) ≤ ∑' (n : ℕ), m (i n)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>s : Set β<VAR>t : ℕ → Set α<VAR>ht : f ⁻¹' s ⊆ iUnion t<GOAL>⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), m (f ⁻¹' t n) ≤ ∑' (n : ℕ), m (t n)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>s : Set β<VAR>t : ℕ → Set α<VAR>ht : f ⁻¹' s ⊆ iUnion t<GOAL>s ⊆ ⋃ n, (range f)ᶜ ∪ f '' t n
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>m_empty : m ∅ = 0<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Injective f<VAR>s : Set β<VAR>t : ℕ → Set α<VAR>ht : f ⁻¹' s ⊆ iUnion t<GOAL>∑' (n : ℕ), m (f ⁻¹' (fun n => (range f)ᶜ ∪ f '' t n) n) ≤ ∑' (n : ℕ), m (t n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝ : MulOneClass M<VAR>s t : Set α<VAR>f✝ g✝ : α → M<VAR>a : α<VAR>f g : α → M<VAR>h : Disjoint (mulSupport f) (mulSupport g)<GOAL>(mulSupport f).mulIndicator (f * g) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝ : MulOneClass M<VAR>s t : Set α<VAR>f✝ g✝ : α → M<VAR>a : α<VAR>f g : α → M<VAR>h : Disjoint (mulSupport f) (mulSupport g)<VAR>x : α<VAR>hx : x ∈ mulSupport f<GOAL>(f * g) x = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝ : MulOneClass M<VAR>s t : Set α<VAR>f✝ g✝ : α → M<VAR>a : α<VAR>f g : α → M<VAR>h : Disjoint (mulSupport f) (mulSupport g)<VAR>x : α<VAR>hx : x ∈ mulSupport f<VAR>this : g x = 1<GOAL>(f * g) x = f x
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Semiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module Rᵐᵒᵖ M<VAR>m₁ m₂ : M<GOAL>0 •> m₂ + m₁ <• 0 = 0
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>s : ↥S<GOAL>mk' f 0 s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrderedCommRing β<VAR>f : α → β<VAR>inst✝ : DecidablePred fun x => f x ≤ 0<VAR>s : Finset α<VAR>h0 : Even (filter (fun x => f x ≤ 0) s).card<VAR>x : α<VAR>x✝ : x ∈ s<VAR>hx : ¬f x ≤ 0<GOAL>0 ≤ 1 * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrderedCommRing β<VAR>f : α → β<VAR>inst✝ : DecidablePred fun x => f x ≤ 0<VAR>s : Finset α<VAR>h0 : Even (filter (fun x => f x ≤ 0) s).card<VAR>x : α<VAR>x✝ : x ∈ s<VAR>hx : 0 < f x<GOAL>0 ≤ f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrderedCommRing β<VAR>f : α → β<VAR>inst✝ : DecidablePred fun x => f x ≤ 0<VAR>s : Finset α<VAR>h0 : Even (filter (fun x => f x ≤ 0) s).card<GOAL>∏ x ∈ s, (if f x ≤ 0 then -1 else 1) * f x = ∏ x ∈ s, f x
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>n : ℕ<VAR>H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n<GOAL>Module.rank R M ≤ ↑n
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>n : ℕ<VAR>H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n<GOAL>⨆ ι, #↑↑ι ≤ ↑n
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>n : ℕ<VAR>H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n<GOAL>∀ (i : { s // LinearIndependent (ι := { x // x ∈ s }) R Subtype.val }), #↑↑i ≤ ↑n
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M₁<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₁<VAR>n : ℕ<VAR>H : ∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set M<VAR>li : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>#↑↑⟨s, li⟩ ≤ ↑n
<VAR>E : Type u_1<VAR>ι✝ : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι✝<VAR>F : ι✝ → ℂ → E<VAR>f✝ g✝ : ℂ → E<VAR>ι : Type u_3<VAR>p : Filter ι<VAR>f : ι → ℂ → ℂ<VAR>g : ℂ → ℂ<VAR>s : Set ℂ<VAR>hs : IsOpen s<VAR>x : ↑s<VAR>hF : TendstoLocallyUniformlyOn f g p s<VAR>hf : ∀ᶠ (n : ι) in p, DifferentiableOn ℂ (f n) s<VAR>hg : g ↑x ≠ 0<GOAL>Tendsto (fun n => (deriv (f n) / f n) ↑x) p (𝓝 ((deriv g / g) ↑x))
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>f : ℕ → β<GOAL>∏ k ∈ range 1, f k = f 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<GOAL>UniformContinuousOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hs : IsCompact s<VAR>hf : ContinuousOn f s<GOAL>UniformContinuous (s.restrict f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hs : CompactSpace ↑s<VAR>hf : ContinuousOn f s<GOAL>UniformContinuous (s.restrict f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>s : Set α<VAR>f : α → β<VAR>hs : CompactSpace ↑s<VAR>hf : Continuous (s.restrict f)<GOAL>UniformContinuous (s.restrict f)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>ι : Type v₁<VAR>ι' : Type w₁<VAR>b : Basis ι R S<VAR>c : Basis ι' S A<VAR>i : ι<VAR>j : ι'<GOAL>(b.smulTower c) (i, j) = b (i, j).1 • c (i, j).2
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>ι : Type v₁<VAR>ι' : Type w₁<VAR>b : Basis ι R S<VAR>c : Basis ι' S A<VAR>i : ι<VAR>j : ι'<GOAL>(b.smulTower c).repr (b (i, j).1 • c (i, j).2) = single (i, j) 1
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>ι : Type v₁<VAR>ι' : Type w₁<VAR>b : Basis ι R S<VAR>c : Basis ι' S A<VAR>i : ι<VAR>j : ι'<VAR>i' : ι<VAR>j' : ι'<GOAL>((b.smulTower c).repr (b (i, j).1 • c (i, j).2)) (i', j') = (single (i, j) 1) (i', j')
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : Semiring S<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S A<VAR>inst✝¹ : Module R A<VAR>inst✝ : IsScalarTower R S A<VAR>ι : Type v₁<VAR>ι' : Type w₁<VAR>b : Basis ι R S<VAR>c : Basis ι' S A<VAR>i : ι<VAR>j : ι'<VAR>i' : ι<VAR>j' : ι'<GOAL>(b.repr (b (i, j).1 • if (i, j).2 = (i', j').2 then 1 else 0)) (i', j').1 = (single (i, j) 1) (i', j')
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Semiring R✝<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>h : I.radical.FG<GOAL>∃ n, I.radical ^ n ≤ I
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Semiring R✝<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>h : I.radical.FG<VAR>this : I.radical ≤ I.radical<GOAL>∃ n, I.radical ^ n ≤ I
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Semiring R✝<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>h : I.radical.FG<GOAL>I.radical ≤ I.radical → ∃ n, I.radical ^ n ≤ I
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Semiring R✝<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>h : I.radical.FG<GOAL>∀ (x : R), (fun J => J ≤ I.radical → ∃ n, J ^ n ≤ I) (Submodule.span R {x})
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Semiring R✝<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>I : Ideal R<VAR>h : I.radical.FG<GOAL>∀ (M₁ M₂ : Submodule R R), (fun J => J ≤ I.radical → ∃ n, J ^ n ≤ I) M₁ → (fun J => J ≤ I.radical → ∃ n, J ^ n ≤ I) M₂ → (fun J => J ≤ I.radical → ∃ n, J ^ n ≤ I) (M₁ ⊔ M₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a : α<VAR>m : M<GOAL>(single (Option.some a) m).some = single a m
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>U : Set (Quotient α_mod_G)<VAR>meas_U : MeasurableSet U<GOAL>(Measure.map (Quotient.mk α_mod_G) (μ.restrict s)) U = μ (Quotient.mk α_mod_G ⁻¹' U ∩ s)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁵ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>E : Type u_9<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : Module R E<VAR>F : Type u_10<VAR>inst✝ : AddCommMonoid F<VAR>t : ⨂[R] (i : ι), s i<VAR>x✝¹ : R<VAR>x✝ : (i : ι) → s i<GOAL>(tprod R) x✝ ∈ Set.range ⇑(tprod R)
<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>m.Coprime (n - m) ↔ m.Coprime n
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<VAR>N : L.Substructure M<GOAL>N.FG ↔ ∃ n s, (closure L).toFun (range s) = N
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<VAR>N : L.Substructure M<GOAL>(∃ S, S.Finite ∧ (closure L).toFun S = N) ↔ ∃ n s, (closure L).toFun (range s) = N
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>hz : 0 < z<GOAL>x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>dblU (map W' f) (⇑f ∘ P) = f (W'.dblU P)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{?u.2943, u_1} C<VAR>inst✝¹ : Category.{?u.2947, u_2} D<VAR>inst✝ : Category.{?u.2951, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E : L.LeftExtension F<VAR>Y : D<VAR>g₁ g₂ : CostructuredArrow L Y<VAR>φ : g₁ ⟶ g₂<GOAL>F.map φ.left ≫ E.hom.app g₂.left ≫ E.right.map g₂.hom = (E.hom.app g₁.left ≫ E.right.map g₁.hom) ≫ 𝟙 (E.right.obj Y)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Category.{?u.2943, u_1} C<VAR>inst✝¹ : Category.{?u.2947, u_2} D<VAR>inst✝ : Category.{?u.2951, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E : L.LeftExtension F<VAR>Y : D<VAR>g₁ g₂ : CostructuredArrow L Y<VAR>φ : g₁ ⟶ g₂<GOAL>F.map φ.left ≫ E.hom.app g₂.left ≫ E.right.map g₂.hom = (E.hom.app g₁.left ≫ E.right.map (L.map φ.left ≫ g₂.hom)) ≫ 𝟙 (E.right.obj Y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : ConditionallyCompleteLattice β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>s : Set α<VAR>hs : s.Nonempty<VAR>B : α<VAR>hB : B ∈ lowerBounds s<VAR>f' : αᵒᵈ → βᵒᵈ := f<GOAL>f B ≤ sInf (f '' s)
<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>inst✝ : IsNilpotent R L M<VAR>m : M<GOAL>m ∈ weightSpace M 0 ↔ m ∈ ⊤
<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>inst✝ : IsNilpotent R L M<VAR>m : M<GOAL>∀ (a : L), ∃ k, ((toEnd R L M) a ^ k) m = 0
<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>inst✝ : IsNilpotent R L M<VAR>m : M<VAR>x : L<GOAL>∃ k, ((toEnd R L M) x ^ k) m = 0
<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>inst✝ : IsNilpotent R L M<VAR>m : M<VAR>x : L<VAR>k : ℕ<VAR>hk : ∀ (x : L), (toEnd R L M) x ^ k = 0<GOAL>∃ k, ((toEnd R L M) x ^ k) m = 0
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁵ : EMetricSpace X<VAR>inst✝⁴ : EMetricSpace Y<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MeasurableSpace Y<VAR>inst✝ : BorelSpace Y<VAR>e : X ≃ᵢ Y<VAR>d : ℝ<VAR>s : Set Y<GOAL>μH[d] (⇑e ⁻¹' s) = μH[d] s
<GOAL>@Batteries.BinomialHeap.Imp.HeapNode.rankTR = @rank
<VAR>α : Type u_1<VAR>s : HeapNode α<GOAL>Batteries.BinomialHeap.Imp.HeapNode.rankTR s = s.rank
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝³ : SeminormedGroup E<VAR>inst✝² : SeminormedGroup F<VAR>inst✝¹ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>inst✝ : FunLike 𝓕 E F<VAR>x : E<GOAL>Tendsto (fun a => ‖a / x‖) (𝓝 x) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>a : α<VAR>s : Set α<GOAL>𝓝[insert a s] a = pure a ⊔ 𝓝[s] a
<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 y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>o.oangle x ((o.rotation θ) y) = o.oangle x y + θ
<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 y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>↑(↑θ.expMapCircle * (o.kahler x) y).arg = ↑((o.kahler x) y).arg + θ
<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 y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>θ + ↑((o.kahler x) y).arg = ↑((o.kahler x) y).arg + θ
<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 y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>↑θ.expMapCircle ≠ 0
<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 y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>(o.kahler x) y ≠ 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ∆ a = ⊥
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : OrderedCommGroup α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalGroup α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>i : ι<VAR>h : f ≤ g<VAR>hi : f i < g i<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<GOAL>a₁ < a₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : OrderedCommGroup α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalGroup α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>i : ι<VAR>h : f ≤ g<VAR>hi : f i < g i<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<VAR>this : update f i 1 ≤ update g i 1<GOAL>a₁ < a₂
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : OrderedCommGroup α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalGroup α<VAR>inst✝ : OrderClosedTopology α<VAR>f g : ι → α<VAR>a₁ a₂ : α<VAR>i : ι<VAR>h : f ≤ g<VAR>hi : f i < g i<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<VAR>this✝ : update f i 1 ≤ update g i 1<VAR>this : 1 / f i * a₁ ≤ 1 / g i * a₂<GOAL>a₁ < a₂
<VAR>α : Type u_1<VAR>inst✝² : Lattice α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ a b c : α<VAR>this : DistribLattice α := CommGroup.toDistribLattice α<GOAL>mabs ((a ⊔ c) / (b ⊔ c)) * mabs ((a ⊓ c) / (b ⊓ c)) = mabs (a / b)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁶ : CommSemiring k<VAR>inst✝⁵ : Monoid G<VAR>inst✝⁴ : Monoid H<VAR>A : Type u₃<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra k A<VAR>B : Type u_3<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra k B<VAR>F : G →* A<VAR>a : G<VAR>b : k<GOAL>((lift k G A) F) (single a b) = b • F a
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<GOAL>adjoin R ⊥ = ⊥
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<GOAL>GaloisConnection (adjoin R) ?u
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<GOAL>NonUnitalSubalgebra R A → Set A
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<GOAL>count p (nth p 0) = 0
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<GOAL>∀ ⦃x : ℕ⦄, x ∈ range (sInf (setOf p)) → ¬p x
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G✝ : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>G : SimpleGraph V<GOAL>Pairwise fun c c' => Disjoint c.supp c'.supp
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G✝ : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>G : SimpleGraph V<GOAL>Pairwise fun c c' => ∀ ⦃a : V⦄, a ∈ c.supp → a ∉ c'.supp
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G✝ : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>G : SimpleGraph V<VAR>i✝ j✝ : G.ConnectedComponent<VAR>h : i✝ ≠ j✝<VAR>a : V<VAR>hsx : a ∈ i✝.supp<VAR>hsy : a ∈ j✝.supp<GOAL>False
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G✝ : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>G : SimpleGraph V<VAR>i✝ j✝ : G.ConnectedComponent<VAR>h : i✝ ≠ j✝<VAR>a : V<VAR>hsx : G.connectedComponentMk a = i✝<VAR>hsy : G.connectedComponentMk a = j✝<GOAL>False
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<GOAL>(ihom.ev M).app N = (TensorProduct.uncurry R (↑M) (↑M →ₗ[R] ↑N) ↑N) LinearMap.id.flip
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>M N : ModuleCat R<GOAL>∀ (x : ↑M) (y : ↑((ihom M).obj N)), ((ihom.ev M).app N) (x ⊗ₜ[R] y) = ((TensorProduct.uncurry R (↑M) (↑M →ₗ[R] ↑N) ↑N) LinearMap.id.flip) (x ⊗ₜ[R] y)
<VAR>R : Type u_1<VAR>inst✝ : Monoid R<VAR>a b : R<VAR>h : b * a = 1<GOAL>IsLeftRegular 1
<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 y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>o.oangle ((o.rotation θ) x) y = o.oangle x y - θ