ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidablePred fun x => x ∈ t<VAR>f : γ → α<GOAL>(fun a => (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : IsLocalization M S<VAR>I : Ideal S<VAR>inst✝ : I.IsPrime<VAR>J : Ideal R<VAR>H : J ≤ Ideal.comap (algebraMap R S) I<VAR>hI : (Ideal.comap (algebraMap R S) I).IsMaximal<VAR>s : S ⧸ I<GOAL>∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = s
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : IsLocalization M S<VAR>I : Ideal S<VAR>inst✝ : I.IsPrime<VAR>J : Ideal R<VAR>H : J ≤ Ideal.comap (algebraMap R S) I<VAR>hI : (Ideal.comap (algebraMap R S) I).IsMaximal<VAR>s : S<GOAL>∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) s
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : IsLocalization M S<VAR>I : Ideal S<VAR>inst✝ : I.IsPrime<VAR>J : Ideal R<VAR>H : J ≤ Ideal.comap (algebraMap R S) I<VAR>hI : (Ideal.comap (algebraMap R S) I).IsMaximal<VAR>r m : R<VAR>hm : m ∈ M<GOAL>∃ a, (Ideal.quotientMap I (algebraMap R S) H) a = (Ideal.Quotient.mk I) (mk' S r ⟨m, hm⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>f : α → β<VAR>l : Filter β<GOAL>Tendsto f (𝓝[s] a) l ↔ Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>s : Set α<VAR>a : α<VAR>h : a ∈ s<VAR>f : α → β<VAR>l : Filter β<GOAL>Tendsto (f ∘ Subtype.val) (𝓝 ⟨a, h⟩) l ↔ Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι : Type u_3<VAR>κ✝ : Type u_4<VAR>α : Type u_5<VAR>κ : Type u_6<VAR>η : Type u_7<VAR>inst✝² : Finite α<VAR>inst✝¹ : Finite κ<VAR>inst✝ : Finite η<GOAL>∃ n, ∀ (C : (Fin n → α) → κ), ∃ l, IsMono C l
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>α : Type u_5<VAR>κ : Type u_6<VAR>η : Type u_7<VAR>inst✝² : Finite α<VAR>inst✝¹ : Finite κ<VAR>inst✝ : Finite η<VAR>ι : Type<VAR>ιfin : Fintype ι<VAR>hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l<GOAL>∃ n, ∀ (C : (Fin n → α) → κ), ∃ l, IsMono C l
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>α : Type u_5<VAR>κ : Type u_6<VAR>η : Type u_7<VAR>inst✝² : Finite α<VAR>inst✝¹ : Finite κ<VAR>inst✝ : Finite η<VAR>ι : Type<VAR>ιfin : Fintype ι<VAR>hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l<VAR>C : (Fin (Fintype.card ι) → α) → κ<VAR>l : Subspace η α ι<VAR>c : κ<VAR>cl : ∀ (x : η → α), (fun v => C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c<VAR>e : η<GOAL>∃ i, (l.idxFun ∘ ⇑(Fintype.equivFin ι).symm) i = Sum.inr e
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>α : Type u_5<VAR>κ : Type u_6<VAR>η : Type u_7<VAR>inst✝² : Finite α<VAR>inst✝¹ : Finite κ<VAR>inst✝ : Finite η<VAR>ι : Type<VAR>ιfin : Fintype ι<VAR>hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l<VAR>C : (Fin (Fintype.card ι) → α) → κ<VAR>l : Subspace η α ι<VAR>c : κ<VAR>cl : ∀ (x : η → α), (fun v => C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c<VAR>e : η<VAR>i : ι<VAR>hi : l.idxFun i = Sum.inr e<GOAL>∃ i, (l.idxFun ∘ ⇑(Fintype.equivFin ι).symm) i = Sum.inr e
<VAR>η✝ : Type u_1<VAR>α✝ : Type u_2<VAR>ι✝ : Type u_3<VAR>κ✝ : Type u_4<VAR>α : Type u_5<VAR>κ : Type u_6<VAR>η : Type u_7<VAR>inst✝² : Finite α<VAR>inst✝¹ : Finite κ<VAR>inst✝ : Finite η<VAR>ι : Type<VAR>ιfin : Fintype ι<VAR>hι : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l<VAR>C : (Fin (Fintype.card ι) → α) → κ<VAR>l : Subspace η α ι<VAR>c : κ<VAR>cl : ∀ (x : η → α), (fun v => C (v ∘ ⇑(Fintype.equivFin ι).symm)) (↑l x) = c<VAR>e : η<VAR>i : ι<VAR>hi : l.idxFun i = Sum.inr e<GOAL>(l.idxFun ∘ ⇑(Fintype.equivFin ι).symm) ((Fintype.equivFin ι) i) = Sum.inr e
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>κ : ι → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>l : α → β<VAR>u : β → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>s : Set β<GOAL>l (sInf (u '' s)) = sInf s
<VAR>α✝ : Type u<VAR>β : Type v<VAR>a b : α✝<VAR>inst✝² : CommSemiring α✝<VAR>I : Ideal α✝<VAR>α : Type u<VAR>inst✝¹ : CommRing α<VAR>inst✝ : IsDomain α<VAR>x y : α<GOAL>span {x} = span {y} ↔ Associated x y
<VAR>α✝ : Type u<VAR>β : Type v<VAR>a b : α✝<VAR>inst✝² : CommSemiring α✝<VAR>I : Ideal α✝<VAR>α : Type u<VAR>inst✝¹ : CommRing α<VAR>inst✝ : IsDomain α<VAR>x y : α<GOAL>span {y} ≤ span {x} ∧ span {x} ≤ span {y} ↔ x ∣ y ∧ y ∣ x
<GOAL>volume (⋃ p, ⋃ (_ : 2 < p), {x | LiouvilleWith p x}) = 0
<GOAL>volume {x | ∃ i, 2 < i ∧ LiouvilleWith i x} = 0
<GOAL>volume (⋃ m, (fun x => x + ↑m) ⁻¹' ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) = 0
<GOAL>∀ (i : ℤ), volume ((fun x => x + ↑i) ⁻¹' ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) = 0
<VAR>m : ℤ<GOAL>volume ((fun x => x + ↑m) ⁻¹' ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) = 0
<VAR>m : ℤ<GOAL>volume (⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) = 0
<GOAL>volume (⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) = 0
<VAR>n : ℕ<VAR>hn : 1 ≤ n<GOAL>volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)} = 0
<VAR>n : ℕ<VAR>hn : 1 ≤ n<VAR>r : ℝ<VAR>hr : 2 + 1 / ↑n = r<GOAL>volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0
<VAR>n : ℕ<VAR>hn : 1 ≤ n<VAR>r : ℝ<VAR>hr : 2 < r<GOAL>volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0
<VAR>r : ℝ<VAR>hr : 2 < r<GOAL>volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0
<VAR>r : ℝ<VAR>hr : 2 < r<GOAL>∑' (i : ℕ), volume {x | ∃ a ∈ Finset.Icc 0 ↑i, |x - ↑a / ↑i| < 1 / ↑i ^ r} ≠ ⊤
<VAR>r : ℝ<VAR>hr : 2 < r<GOAL>∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
<VAR>r : ℝ<VAR>hr : 2 < r<VAR>B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)<GOAL>∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
<VAR>r : ℝ<VAR>hr : 2 < r<VAR>B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)<VAR>hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)<GOAL>∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
<VAR>r : ℝ<VAR>hr : 2 < r<VAR>B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)<VAR>hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)<VAR>this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))<GOAL>∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
<VAR>r : ℝ<VAR>hr : 2 < r<VAR>B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)<VAR>hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)<VAR>this : ∀ (b : ℕ), volume (⋃ a ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))<GOAL>Summable fun a => 2 * (↑a ^ (1 - r) + ↑a ^ (-r))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Ring R<VAR>p q r : R[X]<VAR>n : ℕ<GOAL>(p * (X - ↑n)).comp q = p.comp q * (q - ↑n)
<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>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, f' x < 0<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>deriv f x < 0
<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>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, f' x < 0<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>f' x < 0
<VAR>s : ℂ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>IntegrableOn (fun x => ↑x ^ s) (Ioi t) volume ↔ s.re < -1
<VAR>s : ℂ<VAR>t : ℝ<VAR>ht : 0 < t<VAR>h : IntegrableOn (fun x => ↑x ^ s) (Ioi t) volume<GOAL>s.re < -1
<VAR>s : ℂ<VAR>t : ℝ<VAR>ht : 0 < t<VAR>h : IntegrableOn (fun x => ↑x ^ s) (Ioi t) volume<VAR>B : IntegrableOn (fun a => a ^ s.re) (Ioi t) volume<GOAL>s.re < -1
<VAR>R : Type u<VAR>S✝ : Type v<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : LocalRing R<VAR>S : Type v<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : LocalRing S<VAR>f : R →+* S<GOAL>IsLocalRingHom f ↔ (PrimeSpectrum.comap f) (closedPoint S) = closedPoint R
<VAR>R : Type u<VAR>S✝ : Type v<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : LocalRing R<VAR>S : Type v<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : LocalRing S<VAR>f : R →+* S<VAR>this : IsLocalRingHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R<GOAL>IsLocalRingHom f ↔ (PrimeSpectrum.comap f) (closedPoint S) = closedPoint R
<VAR>R : Type u<VAR>S✝ : Type v<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : LocalRing R<VAR>S : Type v<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : LocalRing S<VAR>f : R →+* S<VAR>this : IsLocalRingHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R<GOAL>Ideal.comap f (maximalIdeal S) = maximalIdeal R ↔ ((PrimeSpectrum.comap f) (closedPoint S)).asIdeal = (closedPoint R).asIdeal
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝ : p.IsHomLift f φ<GOAL>p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hb : b ≠ 0<GOAL>a * b = b ↔ a = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Topology.IsUpperSet α<VAR>inst✝ : IsUpper β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Topology.IsUpperSet α<VAR>inst✝ : IsUpper β<VAR>f : α → β<VAR>hf : Monotone f<GOAL>∀ (s : Set β), IsOpen s → IsUpperSet (f ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Topology.IsUpperSet α<VAR>inst✝ : IsUpper β<VAR>f : α → β<VAR>hf : Monotone f<VAR>s : Set β<VAR>hs : IsOpen s<GOAL>IsUpperSet (f ⁻¹' s)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>K.toCycles i j ≫ (K.cyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).toCycles
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>ofInt' ↑(n + 1) = -ofInt' -[n+1]
<VAR>α : Type u_1<GOAL>(Num.ofNat' 0).toZNum = -(Num.ofNat' 0).toZNum
<VAR>α : Type u_1<GOAL>Num.toZNum 0 = -Num.toZNum 0
<VAR>α : Type u_1<VAR>n : ℕ<GOAL>(Num.ofNat' (n + 1)).toZNumNeg = -(Num.ofNat' (n + 1)).toZNum
<VAR>V : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Matrix V V α<VAR>inst✝¹ : MulZeroOneClass α<VAR>inst✝ : Nontrivial α<VAR>h : A.IsAdjMatrix<VAR>i j : V<GOAL>¬A i j = 0 ↔ A i j = 1
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<GOAL>M.Basis' I X ↔ M.Basis I (X ∩ M.E)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<GOAL>I ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ X} ↔ I ∈ maximals (fun x x_1 => x ⊆ x_1) {A | M.Indep A ∧ A ⊆ X ∩ M.E}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<GOAL>{A | M.Indep A ∧ A ⊆ X ∩ M.E} = {A | M.Indep A ∧ A ⊆ X}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I✝ J X Y : Set α<VAR>e : α<VAR>I : Set α<GOAL>I ∈ {A | M.Indep A ∧ A ⊆ X ∩ M.E} ↔ I ∈ {A | M.Indep A ∧ A ⊆ X}
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I✝ J X Y : Set α<VAR>e : α<VAR>I : Set α<GOAL>M.Indep I → I ⊆ X → I ⊆ M.E
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>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>N₂ : LieSubmodule R L M₂<GOAL>⁅I, J⁆ ≤ I ⊓ J
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>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>N₂ : LieSubmodule R L M₂<GOAL>⁅I, J⁆ ≤ I ∧ ⁅I, J⁆ ≤ J
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a b c : α<VAR>f : α → β<VAR>h : a < b<GOAL>ContinuousWithinAt f (Ioc a b) b ↔ ContinuousWithinAt f (Iic b) b
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<GOAL>IsCoseparator G ↔ (preadditiveYonedaObj G).Faithful
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<GOAL>(preadditiveYonedaObj G ⋙ forget₂ (ModuleCat (End G)) AddCommGrp).Faithful ↔ (preadditiveYonedaObj G).Faithful
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>∑ c : Composition n, p.compAlongComposition (id 𝕜 E) c = p n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>p.compAlongComposition (id 𝕜 E) (Composition.ones n) = p n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>∀ b ∈ Finset.univ, b ≠ Composition.ones n → p.compAlongComposition (id 𝕜 E) b = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<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>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>Composition.ones n ∉ Finset.univ → p.compAlongComposition (id 𝕜 E) (Composition.ones n) = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α✝ i)<VAR>m✝ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>α : Fin 2 → Type u<VAR>m : (i : Fin 2) → MeasurableSpace (α i)<VAR>μ : (i : Fin 2) → Measure (α i)<VAR>inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)<GOAL>MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ) ((μ 0).prod (μ 1))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α✝ i)<VAR>m✝ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>α : Fin 2 → Type u<VAR>m : (i : Fin 2) → MeasurableSpace (α i)<VAR>μ : (i : Fin 2) → Measure (α i)<VAR>inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)<VAR>s : Set (α 0)<VAR>t : Set (α 1)<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : MeasurableSet t<GOAL>(Measure.map (⇑(MeasurableEquiv.piFinTwo α)) (Measure.pi μ)) (s ×ˢ t) = (μ 0) s * (μ 1) t
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α✝ : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝¹ : (i : ι) → OuterMeasure (α✝ i)<VAR>m✝ : (i : ι) → MeasurableSpace (α✝ i)<VAR>μ✝ : (i : ι) → Measure (α✝ i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ✝ i)<VAR>inst✝¹ : Fintype ι'<VAR>α : Fin 2 → Type u<VAR>m : (i : Fin 2) → MeasurableSpace (α i)<VAR>μ : (i : Fin 2) → Measure (α i)<VAR>inst✝ : ∀ (i : Fin 2), SigmaFinite (μ i)<VAR>s : Set (α 0)<VAR>t : Set (α 1)<VAR>x✝¹ : MeasurableSet s<VAR>x✝ : MeasurableSet t<GOAL>(μ 0) (Fin.cons s (Fin.cons t finZeroElim) 0) * (μ 1) (Fin.cons s (Fin.cons t finZeroElim) 1) = (μ 0) s * (μ 1) t
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>p : R[X]<VAR>hsep : p.Separable<VAR>x : R<VAR>hp : ¬p = 0<GOAL>rootMultiplicity x p ≤ 1
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>p : R[X]<VAR>hsep : p.Separable<VAR>x : R<VAR>hp : ¬p = 0<GOAL>multiplicity (X - C x) p ≤ 1
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>q : Seminorm 𝕜 E<VAR>hq : Continuous ⇑q<GOAL>∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>q : Seminorm 𝕜 E<VAR>hq : Continuous ⇑q<VAR>V : Set E<VAR>hV : V ∈ p.basisSets<VAR>hε : id V ⊆ q.ball 0 1<GOAL>∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>q : Seminorm 𝕜 E<VAR>hq : Continuous ⇑q<VAR>s : Finset ι<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hV : (s.sup p).ball 0 ε ∈ p.basisSets<VAR>hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1<GOAL>∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>q : Seminorm 𝕜 E<VAR>s : Finset ι<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hV : (s.sup p).ball 0 ε ∈ p.basisSets<VAR>hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1<VAR>x✝ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup<GOAL>∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>q : Seminorm 𝕜 E<VAR>s : Finset ι<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hV : (s.sup p).ball 0 ε ∈ p.basisSets<VAR>hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1<VAR>x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup<VAR>x✝ : NormedSpace 𝕜 E := NormedSpace.mk ⋯<GOAL>∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>q : Seminorm 𝕜 E<VAR>s : Finset ι<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hV : (s.sup p).ball 0 ε ∈ p.basisSets<VAR>hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1<VAR>x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup<VAR>x✝ : NormedSpace 𝕜 E := NormedSpace.mk ⋯<VAR>this : Continuous ⇑q<GOAL>∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : Nonempty ι<VAR>q : Seminorm 𝕜 E<VAR>s : Finset ι<VAR>ε : ℝ<VAR>ε_pos : 0 < ε<VAR>hV : (s.sup p).ball 0 ε ∈ p.basisSets<VAR>hε : id ((s.sup p).ball 0 ε) ⊆ q.ball 0 1<VAR>x✝¹ : SeminormedAddCommGroup E := (s.sup p).toSeminormedAddCommGroup<VAR>x✝ : NormedSpace 𝕜 E := NormedSpace.mk ⋯<VAR>this : Continuous ⇑q<VAR>C : ℝ<VAR>C_pos : 0 < C<VAR>hC : ∀ (x : E), q x ≤ C * ‖x‖<GOAL>∃ s C, C ≠ 0 ∧ q ≤ C • s.sup p
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.28, u_1} C<VAR>inst✝ : Preadditive C<VAR>Y : C<VAR>X : SimplicialObject C<VAR>n b q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnbq : n + 1 = b + q<GOAL>b < n + 1 + 1
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>Y : C<VAR>X : SimplicialObject C<VAR>n b q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnbq : n + 1 = b + q<VAR>j : Fin (n + 1 + 1)<VAR>hj : n + 1 + 1 ≤ ↑j + q<GOAL>(φ ≫ X.σ ⟨b, ⋯⟩) ≫ X.δ j.succ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>Y : C<VAR>X : SimplicialObject C<VAR>n b q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnbq : n + 1 = b + q<VAR>j : Fin (n + 1 + 1)<VAR>hj : n + 1 + 1 ≤ ↑j + q<GOAL>⟨b, ⋯⟩.succ < j.succ
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>Y : C<VAR>X : SimplicialObject C<VAR>n b q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnbq : n + 1 = b + q<VAR>j : Fin (n + 1 + 1)<VAR>hj : n + 1 + 1 ≤ ↑j + q<GOAL>j ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>f✝ : Filter α<VAR>b : α<VAR>v : Filter ι<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>inst✝¹ : Countable (Subtype p)<VAR>inst✝ : Nonempty (Subtype p)<VAR>hv : v.HasBasis p s<VAR>f : ι → α<VAR>H : ¬∃ j, s ↑j = ∅<GOAL>liminf f v = if ∃ j, s ↑j = ∅ then sSup univ else if ∀ (j : Subtype p), ¬BddBelow (range fun i => f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i