ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝ : IsNoetherian R M<VAR>χ : L → R<VAR>x : L<VAR>m : M<VAR>hm : m ∈ ((toEnd R L M) x).maxGenEigenspace (χ x)<GOAL>m ∈ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ ((toEnd R L M) x).maxGenEigenspaceIndex (χ x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>b ∈ Ico a b ↔ False
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝ : TopologicalSpace H<VAR>c : ChartedSpaceCore H M<VAR>e : PartialEquiv M H<VAR>he : e ∈ c.atlas<GOAL>e.source ∈ ⋃ e ∈ c.atlas, ⋃ s, ⋃ (_ : IsOpen s), {↑e ⁻¹' s ∩ e.source}
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝ : TopologicalSpace H<VAR>c : ChartedSpaceCore H M<VAR>e : PartialEquiv M H<VAR>he : e ∈ c.atlas<GOAL>∃ i ∈ c.atlas, ∃ i_1, IsOpen i_1 ∧ e.source = ↑i ⁻¹' i_1 ∩ i.source
<VAR>H : Type u<VAR>H' : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝ : TopologicalSpace H<VAR>c : ChartedSpaceCore H M<VAR>e : PartialEquiv M H<VAR>he : e ∈ c.atlas<GOAL>e.source = ↑e ⁻¹' univ ∩ e.source
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : Memℒp X 2 μ<GOAL>centralMoment X 2 μ = variance X μ
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hX : Memℒp X 2 μ<GOAL>centralMoment X 2 μ = ∫ (x : Ω), ((X - fun x => ∫ (x : Ω), X x ∂μ) ^ 2) x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : OuterMeasure α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>m m' : OuterMeasure α<VAR>hm : m ≤ m'<VAR>u : Set α<GOAL>((restrict s) m) u ≤ ((restrict t) m') u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m✝ : OuterMeasure α<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>m m' : OuterMeasure α<VAR>hm : m ≤ m'<VAR>u : Set α<GOAL>m (u ∩ s) ≤ m' (u ∩ t)
<VAR>F : Type u<VAR>inst✝² : Field F<VAR>K : Type v<VAR>inst✝¹ : Field K<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>f : ι → F<GOAL>(∀ x ∈ univ, ∀ y ∈ univ, f x = f y → x = y) ↔ Function.Injective f
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>A : Matrix m n α<VAR>B : Matrix n n α<VAR>inst✝ : Invertible B<GOAL>A * ⅟B * B = A
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<GOAL>TendstoUniformlyOn F f p {x} ↔ Tendsto (fun n => F n x) p (𝓝 (f x))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<GOAL>(∀ s ∈ 𝓤 β, (fun q => (f q.2, F q.1 q.2)) ⁻¹' s ∈ p ×ˢ 𝓟 {x}) ↔ ∀ s ∈ 𝓤 β, (fun x_1 => (f x, F x_1 x)) ⁻¹' s ∈ p
<VAR>b n : ℕ<VAR>hn : 2 ≤ n<VAR>h : n ≤ b<GOAL>clog b n = 1
<VAR>b n : ℕ<VAR>hn : 2 ≤ n<VAR>h : n ≤ b<GOAL>(n + b - 1) / b ≤ 1
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s : Set α<VAR>f : α → Set X<VAR>hs : s.Finite<VAR>h : ∀ i ∈ s, IsClosed (f i)<GOAL>IsClosed (⋃ i ∈ s, f i)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s : Set α<VAR>f : α → Set X<VAR>hs : s.Finite<VAR>h : ∀ i ∈ s, IsOpen (f i)ᶜ<GOAL>IsOpen (⋂ i ∈ s, (f i)ᶜ)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝ : ∀ (X : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections<VAR>i j : J<VAR>f : i ⟶ j<VAR>X : Cᵒᵖ<GOAL>Hom.app (limitConeπApp F i ≫ F.map f) X = Hom.app (limitConeπApp F j) X
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Ring α<GOAL>NoZeroDivisors α ↔ IsDomain α ∨ Subsingleton α
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : PartialOrder α<VAR>a b c d : α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : PosMulStrictMono α<VAR>H : 0 < a<GOAL>0 < a ^ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁴ : Semiring α<VAR>inst✝³ : PartialOrder α<VAR>a b c d : α<VAR>inst✝² : ZeroLEOneClass α<VAR>inst✝¹ : PosMulStrictMono α<VAR>H : 0 < a<VAR>inst✝ : Nontrivial α<GOAL>0 < a ^ 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁴ : Semiring α<VAR>inst✝³ : PartialOrder α<VAR>a b c d : α<VAR>inst✝² : ZeroLEOneClass α<VAR>inst✝¹ : PosMulStrictMono α<VAR>H : 0 < a<VAR>inst✝ : Nontrivial α<GOAL>0 < 1
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : PartialOrder α<VAR>a b c d : α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : PosMulStrictMono α<VAR>H : 0 < a<VAR>n : ℕ<GOAL>0 < a ^ (n + 1)
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝³ : Semiring α<VAR>inst✝² : PartialOrder α<VAR>a b c d : α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : PosMulStrictMono α<VAR>H : 0 < a<VAR>n : ℕ<GOAL>0 < a ^ n * a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : SMulZeroClass α β<VAR>inst✝² : DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>inst✝¹ : Zero α<VAR>inst✝ : NoZeroSMulDivisors α β<VAR>ha : a ≠ 0<GOAL>0 ∈ a • t ↔ 0 ∈ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t u : Multiset α<VAR>a b : α<VAR>h : s ≤ t<GOAL>s ∪ t = t
<VAR>α : Sort u_1<VAR>b c : α<VAR>h : b = c<VAR>a : α<GOAL>a = b ↔ a = c
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>N = ⊥ ↔ ∀ m ∈ N, m = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>N ≤ ⊥ ↔ ∀ m ∈ N, m = 0
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>j₁ j₂ : J<VAR>t : Cotrident f<GOAL>f j₁ ≫ t.π = f j₂ ≫ t.π
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.12624, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.ShortExact<VAR>h₂ : S₂.ShortExact<VAR>inst✝¹ : IsIso φ.τ₁<VAR>inst✝ : IsIso φ.τ₃<GOAL>IsIso φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.12624, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.ShortExact<VAR>h₂ : S₂.ShortExact<VAR>inst✝¹ : IsIso φ.τ₁<VAR>inst✝ : IsIso φ.τ₃<VAR>this : Mono S₁.f<GOAL>IsIso φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.12624, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.ShortExact<VAR>h₂ : S₂.ShortExact<VAR>inst✝¹ : IsIso φ.τ₁<VAR>inst✝ : IsIso φ.τ₃<VAR>this✝ : Mono S₁.f<VAR>this : Mono S₂.f<GOAL>IsIso φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.12624, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.ShortExact<VAR>h₂ : S₂.ShortExact<VAR>inst✝¹ : IsIso φ.τ₁<VAR>inst✝ : IsIso φ.τ₃<VAR>this✝¹ : Mono S₁.f<VAR>this✝ : Mono S₂.f<VAR>this : Epi S₁.g<GOAL>IsIso φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.12624, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.ShortExact<VAR>h₂ : S₂.ShortExact<VAR>inst✝¹ : IsIso φ.τ₁<VAR>inst✝ : IsIso φ.τ₃<VAR>this✝² : Mono S₁.f<VAR>this✝¹ : Mono S₂.f<VAR>this✝ : Epi S₁.g<VAR>this : Epi S₂.g<GOAL>IsIso φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.12624, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.ShortExact<VAR>h₂ : S₂.ShortExact<VAR>inst✝¹ : IsIso φ.τ₁<VAR>inst✝ : IsIso φ.τ₃<VAR>this✝³ : Mono S₁.f<VAR>this✝² : Mono S₂.f<VAR>this✝¹ : Epi S₁.g<VAR>this✝ : Epi S₂.g<VAR>this : Mono φ.τ₂<GOAL>IsIso φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_1} C<VAR>inst✝⁴ : Category.{?u.12624, u_2} D<VAR>inst✝³ : Preadditive C<VAR>inst✝² : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.ShortExact<VAR>h₂ : S₂.ShortExact<VAR>inst✝¹ : IsIso φ.τ₁<VAR>inst✝ : IsIso φ.τ₃<VAR>this✝⁴ : Mono S₁.f<VAR>this✝³ : Mono S₂.f<VAR>this✝² : Epi S₁.g<VAR>this✝¹ : Epi S₂.g<VAR>this✝ : Mono φ.τ₂<VAR>this : Epi φ.τ₂<GOAL>IsIso φ.τ₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>P : Type u_3<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>f : M →ₗ[R] P<VAR>sb : Submodule R M<VAR>sc : Submodule R P<VAR>hsb : sb.FG<VAR>hsc : sc.FG<VAR>tb : Set M<VAR>htb : tb.Finite ∧ span R tb = sb<VAR>tc : Set P<VAR>htc : tc.Finite ∧ span R tc = sc<GOAL>span R (⇑(LinearMap.inl R M P) '' tb ∪ ⇑(LinearMap.inr R M P) '' tc) = sb.prod sc
<VAR>d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2<GOAL>∃ c, ∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ c
<VAR>d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2<GOAL>∀ (n : ℕ), Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d
<VAR>d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2<VAR>log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))<VAR>n : ℕ<GOAL>Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d
<VAR>d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2<VAR>log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))<VAR>n : ℕ<VAR>h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)<GOAL>Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d
<VAR>d : ℝ := ∑' (k : ℕ), 1 / ↑(k + 1) ^ 2<VAR>log_stirlingSeq' : ℕ → ℝ := fun k => Real.log (stirlingSeq (k + 1))<VAR>n : ℕ<VAR>h₁ : ∀ (k : ℕ), log_stirlingSeq' k - log_stirlingSeq' (k + 1) ≤ 1 / 4 * (1 / ↑(k + 1) ^ 2)<VAR>h₂ : ∑ k ∈ range n, 1 / ↑(k + 1) ^ 2 ≤ d<GOAL>Real.log (stirlingSeq 1) - Real.log (stirlingSeq (n + 1)) ≤ 1 / 4 * d
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>p : Fin 3 → P<VAR>hpi : Function.Injective p<VAR>t : Triangle ℝ P<VAR>hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)<VAR>hto : t.orthocenter ∉ Set.range t.points<VAR>hst : s = insert t.orthocenter (Set.range t.points)<GOAL>AffineIndependent ℝ p
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Set P<VAR>p : Fin 3 → P<VAR>hpi : Function.Injective p<VAR>t : Triangle ℝ P<VAR>hps : Set.range p ⊆ insert t.orthocenter (Set.range t.points)<VAR>hto : t.orthocenter ∉ Set.range t.points<VAR>hst : s = insert t.orthocenter (Set.range t.points)<VAR>c : P<VAR>left✝ : c ∈ affineSpan ℝ (Set.range t.points)<VAR>hc : ∀ p₁ ∈ Set.range p, dist p₁ c = Simplex.circumradius t<GOAL>AffineIndependent ℝ p
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x y : V<GOAL>↑e (x - y) = ↑e (x + -y)
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module 𝕜 V<VAR>e : ENorm 𝕜 V<VAR>x y : V<GOAL>↑e x + ↑e (-y) = ↑e x + ↑e y
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>S : Type v<VAR>inst✝ : CommSemiring S<VAR>r : R<GOAL>(C r).Separable ↔ IsUnit r
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hc : IsColimit c<VAR>f' : Fan Z<GOAL>(opProductIsoCoproduct' hf hc).inv ≫ (hf.lift f').op = hc.desc f'.op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hc : IsColimit c<VAR>f' : Fan Z<VAR>x✝ : Discrete α<VAR>j : α<GOAL>((hf.lift f').op.unop ≫ f.π.app { as := j }).op = (((opProductIsoCoproduct' hf hc).hom ≫ hc.desc f'.op).unop ≫ f.π.app { as := j }).op
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hc : IsColimit c<VAR>f' : Fan Z<VAR>x✝ : Discrete α<VAR>j : α<GOAL>(f'.π.app { as := j }).op = (f.π.app { as := j }).op ≫ (opProductIsoCoproduct' hf hc).hom ≫ hc.desc (Cofan.mk (op f'.pt) fun a => (f'.proj a).op)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : Type u₂<VAR>inst✝ : Category.{v₂, u₂} J<VAR>X : Type v₂<VAR>α : Type u_1<VAR>Z : α → C<VAR>f : Fan Z<VAR>c : Cofan fun x => op (Z x)<VAR>hf : IsLimit f<VAR>hc : IsColimit c<VAR>f' : Fan Z<VAR>x✝ : Discrete α<VAR>j : α<GOAL>(f'.π.app { as := j }).op = (Cofan.mk (op f'.pt) fun a => (f'.proj a).op).ι.app { as := j }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>D : Set β<GOAL>(M.map f hf).Dep D ↔ ∃ D₀, M.Dep D₀ ∧ D = f '' D₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>D : Set β<GOAL>((∀ (x : Set α), M.Indep x → ¬D = f '' x) ∧ ∃ u ⊆ M.E, f '' u = D) ↔ ∃ D₀, (¬M.Indep D₀ ∧ D₀ ⊆ M.E) ∧ D = f '' D₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>D₀ : Set α<VAR>hD₀ : ¬M.Indep D₀<VAR>hD₀E : D₀ ⊆ M.E<VAR>I : Set α<VAR>hI : M.Indep I<VAR>h_eq : f '' D₀ = f '' I<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E I✝ s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>hf : InjOn f M.E<VAR>D₀ : Set α<VAR>hD₀ : ¬M.Indep D₀<VAR>hD₀E : D₀ ⊆ M.E<VAR>I : Set α<VAR>hI : M.Indep I<VAR>h_eq : D₀ = I<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<GOAL>card (s.disjSum t) = card s + card t
<VAR>n n✝ : ℕ<VAR>hi : n✝ + 1 < n + 1<VAR>h0 : ⟨n✝ + 1, hi⟩ ≠ 0<GOAL>⟨n✝ + 1, hi⟩.cycleRange.IsCycle
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>⌊1⌋₊ = 1
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : C ⥤ Type w<VAR>c d : (j : C) × F.obj j<VAR>h : EqvGen (Quot.Rel F) c d<GOAL>Zigzag c.fst d.fst
<VAR>R : Type u<VAR>inst✝¹ : CommSemiring R<VAR>x y z : R<VAR>inst✝ : Nontrivial R<VAR>h : IsCoprime (0 0) (0 1)<GOAL>False
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>f : M₁ →ₗ[R] S<VAR>x : M<VAR>inst✝ : NoZeroSMulDivisors S M<GOAL>f.smulRight x = 0 ↔ f = 0 ∨ x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>f : M₁ →ₗ[R] S<VAR>inst✝ : NoZeroSMulDivisors S M<GOAL>f.smulRight 0 = 0 ↔ f = 0 ∨ 0 = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>f : M₁ →ₗ[R] S<VAR>x : M<VAR>inst✝ : NoZeroSMulDivisors S M<VAR>hx : x ≠ 0<GOAL>f.smulRight x = 0 ↔ f = 0 ∨ x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>f : M₁ →ₗ[R] S<VAR>x : M<VAR>inst✝ : NoZeroSMulDivisors S M<VAR>hx : x ≠ 0<VAR>h : f.smulRight x = 0<GOAL>f = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>f : M₁ →ₗ[R] S<VAR>x : M<VAR>inst✝ : NoZeroSMulDivisors S M<VAR>hx : x ≠ 0<VAR>h : f.smulRight x = 0<VAR>v : M₁<GOAL>f v = 0 v
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>f : M₁ →ₗ[R] S<VAR>x : M<VAR>inst✝ : NoZeroSMulDivisors S M<VAR>hx : x ≠ 0<VAR>v : M₁<VAR>h : f v • x = 0<GOAL>f v = 0 v
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : AddCommMonoid M₁<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R M₁<VAR>inst✝⁴ : Semiring S<VAR>inst✝³ : Module R S<VAR>inst✝² : Module S M<VAR>inst✝¹ : IsScalarTower R S M<VAR>f : M₁ →ₗ[R] S<VAR>x : M<VAR>inst✝ : NoZeroSMulDivisors S M<VAR>hx : x ≠ 0<VAR>v : M₁<VAR>h : f v = 0 ∨ x = 0<GOAL>f v = 0 v
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hg : IsOpenMap g<VAR>hf : IsOpenMap f<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>IsOpen (g ∘ f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hg : IsOpenMap g<VAR>hf : IsOpenMap f<VAR>s : Set X<VAR>hs : IsOpen s<GOAL>IsOpen (g '' (f '' s))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{u_7, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>inst✝⁵ : Category.{?u.50949, u_3} E<VAR>inst✝⁴ : Category.{?u.50953, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>e : F ≅ G<VAR>n : A<GOAL>e.hom.hom n ≫ e.inv.hom n = 𝟙 (F.functor n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : ℕ → Submodule R M<VAR>h : ∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1)))<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → OrderDual.toDual f (m + 1) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : ℕ → Submodule R M<VAR>h : ∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1)))<VAR>n : ℕ<VAR>w : ∀ (m : ℕ), n ≤ m → (partialSups (⇑OrderDual.toDual ∘ f)) n = (partialSups (⇑OrderDual.toDual ∘ f)) m<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → OrderDual.toDual f (m + 1) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : ℕ → Submodule R M<VAR>h : ∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1)))<VAR>n : ℕ<VAR>w : ∀ (m : ℕ), n ≤ m → (partialSups (⇑OrderDual.toDual ∘ f)) n = (partialSups (⇑OrderDual.toDual ∘ f)) m<VAR>m : ℕ<VAR>p : n ≤ m<GOAL>OrderDual.toDual f (m + 1) = ⊤
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b✝ c✝ a b c : α<GOAL>max (a / c) (b / c) = max a b / c
<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>K x : ℝ<GOAL>gronwallBound 0 K 0 x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>b₁ b₂ : α<VAR>a d : β<VAR>hab : b₁ < b₂<VAR>hcd : a < d<GOAL>b₁ • d + b₂ • a < b₁ • a + b₂ • d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>b₁ : α<VAR>a d : β<VAR>hcd : a < d<VAR>b₂ : α<VAR>hab : b₁ < b₁ + b₂<GOAL>b₁ • d + (b₁ + b₂) • a < b₁ • a + (b₁ + b₂) • d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>b₁ : α<VAR>a : β<VAR>b₂ : α<VAR>hab : b₁ < b₁ + b₂<VAR>d : β<VAR>hcd : a < a + d<GOAL>b₁ • (a + d) + (b₁ + b₂) • a < b₁ • a + (b₁ + b₂) • (a + d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>b₁ : α<VAR>a : β<VAR>b₂ : α<VAR>hab : b₁ < b₁ + b₂<VAR>d : β<VAR>hcd : a < a + d<GOAL>b₁ • a + (b₁ + b₂) • a + b₁ • d < b₁ • a + (b₁ + b₂) • a + (b₁ • d + b₂ • d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : OrderedRing α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>b₁ : α<VAR>a : β<VAR>b₂ : α<VAR>hab : 0 < b₂<VAR>d : β<VAR>hcd : 0 < d<GOAL>b₁ • a + (b₁ + b₂) • a + b₁ • d < b₁ • a + (b₁ + b₂) • a + (b₁ • d + b₂ • d)
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(p * C a).degree = p.degree
<VAR>Ω : Type u_1<VAR>mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f g : Ω → ℝ≥0∞<VAR>X Y : Ω → ℝ<VAR>h_meas_f : AEMeasurable f μ<VAR>h_meas_g : AEMeasurable g μ<VAR>h_indep_fun : IndepFun f g μ<GOAL>∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ