ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : lift.{v, u} #ι < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord<VAR>a : Ordinal.{max u v}<GOAL>a < c.ord → derivFamily f a < c.ord
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>ι : Type u<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>c : Cardinal.{max u v}<VAR>hc : c.IsRegular<VAR>hι : lift.{v, u} #ι < c<VAR>hc' : c ≠ ℵ₀<VAR>hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord<VAR>a : Ordinal.{max u v}<VAR>hω : ℵ₀ < c.ord.cof<GOAL>a < c.ord → derivFamily f a < c.ord
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>l : List (Perm α)<VAR>h0 : l.prod = σ<VAR>h1 : ∀ σ ∈ l, σ.IsCycle<VAR>h2 : List.Pairwise Disjoint l<GOAL>σ.cycleType = ↑(List.map (Finset.card ∘ support) l)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>l : List (Perm α)<VAR>h0 : l.prod = σ<VAR>h1 : ∀ σ ∈ l, σ.IsCycle<VAR>h2 : List.Pairwise Disjoint l<VAR>hl : l.Nodup<GOAL>σ.cycleType = ↑(List.map (Finset.card ∘ support) l)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>l : List (Perm α)<VAR>h0 : l.prod = σ<VAR>h1 : ∀ σ ∈ l, σ.IsCycle<VAR>h2 : List.Pairwise Disjoint l<VAR>hl : l.Nodup<GOAL>Multiset.map (Finset.card ∘ support) l.toFinset.val = ↑(List.map (Finset.card ∘ support) l)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>l : List (Perm α)<VAR>h0 : l.prod = σ<VAR>h1 : ∀ σ ∈ l, σ.IsCycle<VAR>h2 : List.Pairwise Disjoint l<VAR>hl : l.Nodup<GOAL>∀ f ∈ l.toFinset, f.IsCycle
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>l : List (Perm α)<VAR>h0 : l.prod = σ<VAR>h1 : ∀ σ ∈ l, σ.IsCycle<VAR>h2 : List.Pairwise Disjoint l<VAR>hl : l.Nodup<GOAL>(↑l.toFinset).Pairwise Disjoint
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>l : List (Perm α)<VAR>h0 : l.prod = σ<VAR>h1 : ∀ σ ∈ l, σ.IsCycle<VAR>h2 : List.Pairwise Disjoint l<VAR>hl : l.Nodup<GOAL>l.toFinset.noncommProd id ⋯ = σ
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i✝ : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>i : Fin (n + 1)<GOAL>HasIntegral I GP (fun x => (f' x) (Pi.single i 1)) BoxAdditiveMap.volume (integral (I.face i) GP (fun x => f (i.insertNth (I.upper i) x)) BoxAdditiveMap.volume - integral (I.face i) GP (fun x => f (i.insertNth (I.lower i) x)) BoxAdditiveMap.volume)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i✝ : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>i : Fin (n + 1)<VAR>Hc : ContinuousOn f (Box.Icc I)<GOAL>HasIntegral I GP (fun x => (f' x) (Pi.single i 1)) BoxAdditiveMap.volume (integral (I.face i) GP (fun x => f (i.insertNth (I.upper i) x)) BoxAdditiveMap.volume - integral (I.face i) GP (fun x => f (i.insertNth (I.lower i) x)) BoxAdditiveMap.volume)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i✝ : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>i : Fin (n + 1)<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (i.insertNth y x)) BoxAdditiveMap.volume<GOAL>HasIntegral I GP (fun x => (f' x) (Pi.single i 1)) BoxAdditiveMap.volume (integral (I.face i) GP (fun x => f (i.insertNth (I.upper i) x)) BoxAdditiveMap.volume - integral (I.face i) GP (fun x => f (i.insertNth (I.lower i) x)) BoxAdditiveMap.volume)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i✝ : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>i : Fin (n + 1)<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (i.insertNth y x)) BoxAdditiveMap.volume<VAR>fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x => ⋯.toBoxAdditive<GOAL>HasIntegral I GP (fun x => (f' x) (Pi.single i 1)) BoxAdditiveMap.volume (integral (I.face i) GP (fun x => f (i.insertNth (I.upper i) x)) BoxAdditiveMap.volume - integral (I.face i) GP (fun x => f (i.insertNth (I.lower i) x)) BoxAdditiveMap.volume)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i✝ : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>i : Fin (n + 1)<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (i.insertNth y x)) BoxAdditiveMap.volume<VAR>fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x => ⋯.toBoxAdditive<VAR>F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯<GOAL>HasIntegral I GP (fun x => (f' x) (Pi.single i 1)) BoxAdditiveMap.volume (F I)
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i✝ : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>i : Fin (n + 1)<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (i.insertNth y x)) BoxAdditiveMap.volume<VAR>fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x => ⋯.toBoxAdditive<VAR>F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯<GOAL>Fin (n + 1) →ᵇᵃ[↑I] ℝ
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i✝ : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>i : Fin (n + 1)<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (i.insertNth y x)) BoxAdditiveMap.volume<VAR>fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x => ⋯.toBoxAdditive<VAR>F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯<GOAL>∀ (J : Box (Fin (n + 1))), 0 ≤ ?refine_1 J
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i✝ : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>i : Fin (n + 1)<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (i.insertNth y x)) BoxAdditiveMap.volume<VAR>fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x => ⋯.toBoxAdditive<VAR>F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯<GOAL>∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I ∩ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ closedBall x δ → x ∈ Box.Icc J → (GP.bDistortion = true → J.distortion ≤ c) → dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤ ε
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>n : ℕ<VAR>inst✝ : CompleteSpace E<VAR>I : Box (Fin (n + 1))<VAR>i✝ : Fin (n + 1)<VAR>f : (Fin (n + 1) → ℝ) → E<VAR>f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E<VAR>s : Set (Fin (n + 1) → ℝ)<VAR>hs : s.Countable<VAR>Hs : ∀ x ∈ s, ContinuousWithinAt f (Box.Icc I) x<VAR>Hd : ∀ x ∈ Box.Icc I \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x<VAR>i : Fin (n + 1)<VAR>Hc : ContinuousOn f (Box.Icc I)<VAR>fI : ℝ → Box (Fin n) → E := fun y J => integral J GP (fun x => f (i.insertNth y x)) BoxAdditiveMap.volume<VAR>fb : ↑(Set.Icc (I.lower i) (I.upper i)) → Fin n →ᵇᵃ[↑(I.face i)] E := fun x => ⋯.toBoxAdditive<VAR>F : Fin (n + 1) →ᵇᵃ[↑I] E := BoxAdditiveMap.upperSubLower I i fI fb ⋯<GOAL>∀ (c : ℝ≥0), ∀ x ∈ Box.Icc I \ s, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ closedBall x δ → x ∈ Box.Icc J → (GP.bDistortion = true → J.distortion ≤ c) → dist ((BoxAdditiveMap.volume J) ((f' x) (Pi.single i 1))) (F J) ≤ ε * ?refine_1 J
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : OrderedSemiring 𝕜<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : AddCommMonoid F<VAR>inst✝² : OrderedCancelAddCommMonoid β<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : DistribMulAction 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hg : StrictConvexOn 𝕜 s g<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : InfiniteDimensionalOrder α<VAR>m : WithBot (WithTop ℕ)<VAR>hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m<VAR>hm : ∀ (i : LTSeries α), ↑i.length ≤ ⊥<VAR>this : Inhabited α<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : InfiniteDimensionalOrder α<VAR>m✝ : WithBot (WithTop ℕ)<VAR>hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝<VAR>m : ℕ<VAR>hm : ∀ (i : LTSeries α), ↑i.length ≤ some (some m)<GOAL>⊤ ≤ some (some m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : InfiniteDimensionalOrder α<VAR>m✝ : WithBot (WithTop ℕ)<VAR>hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝<VAR>m : ℕ<VAR>hm : ∀ (i : LTSeries α), ↑i.length ≤ some (some m)<GOAL>some (some m) < ↑(LTSeries.withLength α (m + 1)).length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : InfiniteDimensionalOrder α<VAR>m✝ : WithBot (WithTop ℕ)<VAR>hm✝ : ∀ (i : LTSeries α), ↑i.length ≤ m✝<VAR>m : ℕ<VAR>hm : ∀ (i : LTSeries α), ↑i.length ≤ some (some m)<GOAL>m < ↑(LTSeries.withLength α (m + 1)).length
<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<VAR>i0 : ι<GOAL>vectorSpan k (range p) = Submodule.span k (range fun i => p i0 -ᵥ p i)
<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<VAR>i0 : ι<GOAL>Submodule.span k (range ((fun x => p i0 -ᵥ x) ∘ p)) = Submodule.span k (range fun i => p i0 -ᵥ p i)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>h : IsEllSequence W<VAR>x : R<VAR>m n r : ℤ<GOAL>(x • W) (m + n) * (x • W) (m - n) * (x • W) r ^ 2 = (x • W) (m + r) * (x • W) (m - r) * (x • W) n ^ 2 - (x • W) (n + r) * (x • W) (n - r) * (x • W) m ^ 2
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ✝ : F<VAR>s✝ t : Set α<VAR>I : Set ι<VAR>μ : F<VAR>hI : I.Countable<VAR>s : ι → Set α<VAR>this : Countable ↑I<GOAL>μ (⋃ i ∈ I, s i) ≤ ∑' (i : ↑I), μ (s ↑i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ✝ : F<VAR>s✝ t : Set α<VAR>I : Set ι<VAR>μ : F<VAR>hI : I.Countable<VAR>s : ι → Set α<VAR>this : Countable ↑I<GOAL>μ (⋃ x, s ↑x) ≤ ∑' (i : ↑I), μ (s ↑i)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : Archimedean α<VAR>a : α<GOAL>⋃ n, Ico (a + ↑n) (a + ↑n + 1) = univ
<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<VAR>s : Set M<VAR>m : M<VAR>hm : m ∈ s<GOAL>m ∈ ↑(lieSpan R L s)
<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<VAR>s : Set M<VAR>m : M<VAR>hm : m ∈ s<GOAL>∀ (N : LieSubmodule R L M), s ⊆ ↑N → m ∈ N
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>s : Set EReal<GOAL>(∃ i, True ∧ Iio ↑i ⊆ s) ↔ ∃ y, Iio ↑y ⊆ s
<VAR>α✝ : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>α : Type u<VAR>u : Core α<VAR>x : α<GOAL>𝓝 x = comap (Prod.mk x) u.uniformity
<VAR>α✝ : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>α : Type u<VAR>u : Core α<VAR>x : α<GOAL>∀ (a : α), ∀ i ∈ u.uniformity, a ∈ Prod.mk a ⁻¹' id i
<VAR>α✝ : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>α : Type u<VAR>u : Core α<VAR>x : α<GOAL>∀ (a : α), ∀ i ∈ u.uniformity, ∀ᶠ (x : α) in comap (Prod.mk a) u.uniformity, Prod.mk a ⁻¹' id i ∈ comap (Prod.mk x) u.uniformity
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a✝ b✝ x : α<VAR>ht : IsAntichain r t<VAR>h : maximals r s ⊆ t<VAR>hs : ∀ ⦃a : α⦄, a ∈ t → ∃ b ∈ maximals r s, r b a<VAR>a : α<VAR>ha : a ∈ t<VAR>b : α<VAR>hb : b ∈ maximals r s<VAR>hr : r b a<GOAL>a ∈ maximals r s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝¹ t✝ u : Multiset α<VAR>a✝ b : α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>IH : ∀ (t : Multiset α), s ∩ t ≤ t<VAR>t : Multiset α<VAR>h : a ∈ t<GOAL>(a ::ₘ s) ∩ t ≤ t
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasInjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : InjectiveResolution X<GOAL>(NatTrans.rightDerivedToHomotopyCategory α).app X = (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex) ≫ (P.isoRightDerivedToHomotopyCategoryObj G).inv
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasInjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : InjectiveResolution X<GOAL>(NatTrans.rightDerivedToHomotopyCategory α).app X ≫ (P.isoRightDerivedToHomotopyCategoryObj G).hom = (P.isoRightDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasInjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : InjectiveResolution X<GOAL>(HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as) ≫ (G.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫ 𝟙 ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex)) = ((F.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫ 𝟙 ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex))) ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasInjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : InjectiveResolution X<GOAL>(HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as) ≫ (G.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫ 𝟙 ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj ((G.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex)) = (F.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫ 𝟙 ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex)) ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasInjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : InjectiveResolution X<GOAL>(HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as) ≫ (G.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom = (F.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasInjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : InjectiveResolution X<VAR>β : (injectiveResolution X).cocomplex ⟶ P.cocomplex<VAR>hβ : (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map β = P.iso.hom<GOAL>(HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as) ≫ (G.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom = (F.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasInjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : InjectiveResolution X<VAR>β : (injectiveResolution X).cocomplex ⟶ P.cocomplex<VAR>hβ : (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map β = P.iso.hom<GOAL>(HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as) ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((G.mapHomologicalComplex (ComplexShape.up ℕ)).map β) = (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map β) ≫ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasInjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : InjectiveResolution X<VAR>β : (injectiveResolution X).cocomplex ⟶ P.cocomplex<VAR>hβ : (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map β = P.iso.hom<GOAL>(HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as ≫ (G.mapHomologicalComplex (ComplexShape.up ℕ)).map β) = (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app (injectiveResolution X).cocomplex ≫ (G.mapHomologicalComplex (ComplexShape.up ℕ)).map β)
<VAR>α : Type u_1<VAR>ι✝ : Type u_2<VAR>F : Type u_3<VAR>inst✝² : FunLike F (Set α) ℝ≥0∞<VAR>inst✝¹ : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t : Set α<VAR>ι : Sort u_4<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<GOAL>μ (⋃ i, s i) = 0 ↔ ∀ (i : ι), μ (s i) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>f : Filter α<VAR>g : Filter β<VAR>α₁ : Type u<VAR>α₂ : Type v<VAR>β₁ : Type w<VAR>β₂ : Type x<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>m₁ : α₁ → β₁<VAR>m₂ : α₂ → β₂<VAR>s : Set (β₁ × β₂)<GOAL>s ∈ (map m₁ f₁).coprod (map m₂ f₂) → s ∈ map (Prod.map m₁ m₂) (f₁.coprod f₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>f : Filter α<VAR>g : Filter β<VAR>α₁ : Type u<VAR>α₂ : Type v<VAR>β₁ : Type w<VAR>β₂ : Type x<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>m₁ : α₁ → β₁<VAR>m₂ : α₂ → β₂<VAR>s : Set (β₁ × β₂)<GOAL>((∃ t₁, m₁ ⁻¹' t₁ ∈ f₁ ∧ Prod.fst ⁻¹' t₁ ⊆ s) ∧ ∃ t₂, m₂ ⁻¹' t₂ ∈ f₂ ∧ Prod.snd ⁻¹' t₂ ⊆ s) → (∃ t₁ ∈ f₁, Prod.fst ⁻¹' t₁ ⊆ Prod.map m₁ m₂ ⁻¹' s) ∧ ∃ t₂ ∈ f₂, Prod.snd ⁻¹' t₂ ⊆ Prod.map m₁ m₂ ⁻¹' s
<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>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<GOAL>S₁.rightHomologyIso.hom ≫ homologyMap φ = rightHomologyMap φ ≫ S₂.rightHomologyIso.hom
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>d₁ d₂ d₃ : ManyOneDegree<GOAL>d₁ + d₂ ≤ d₃ ↔ d₁ ≤ d₃ ∧ d₂ ≤ d₃
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>d₂ d₃ : ManyOneDegree<VAR>p✝ : Set ℕ<GOAL>of p✝ + d₂ ≤ d₃ ↔ of p✝ ≤ d₃ ∧ d₂ ≤ d₃
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>d₃ : ManyOneDegree<VAR>p✝¹ p✝ : Set ℕ<GOAL>of p✝¹ + of p✝ ≤ d₃ ↔ of p✝¹ ≤ d₃ ∧ of p✝ ≤ d₃
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>p✝² p✝¹ p✝ : Set ℕ<GOAL>of p✝² + of p✝¹ ≤ of p✝ ↔ of p✝² ≤ of p✝ ∧ of p✝¹ ≤ of p✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>s t : Set α<VAR>a b : α<VAR>inst✝ : Nonempty ι<VAR>f : ι → α<VAR>h₁ : ∀ (i : ι), b ≤ f i<VAR>h₂ : ∀ (w : α), b < w → ∃ i, f i < w<GOAL>⨅ i, f i = b