ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2<VAR>x : S<VAR>e₁ : (TensorProduct.lmul' R).kerSquareLift (f x) = (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))<GOAL>((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x = (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x ↔ ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2<VAR>x : S<VAR>e₁ : (TensorProduct.lmul' R).kerSquareLift (f x) = (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))<VAR>e₂ : x = (quotientCotangentIdealRingEquiv R S) ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)<GOAL>((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x = (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x ↔ ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x
<VAR>X : Compactum<VAR>x : X.A<GOAL>(β.η.app X.A ≫ X.a) x = x
<VAR>X : Compactum<VAR>x : X.A<GOAL>𝟙 X.A x = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : DistribLattice α<VAR>a b✝ c✝ : α<VAR>h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a<VAR>b c : α<GOAL>b ⊓ c ≤ a → b ≤ a ∨ c ≤ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : DistribLattice α<VAR>a b✝ c✝ : α<VAR>h : ∀ ⦃b c : α⦄, b ⊓ c = a → b = a ∨ c = a<VAR>b c : α<GOAL>(a ⊔ b) ⊓ (a ⊔ c) = a → a ⊔ b = a ∨ a ⊔ c = a
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>β : Type u_2<VAR>inst✝² : Preorder β<VAR>f✝ g : α → β<VAR>x : α<VAR>s t : Set α<VAR>y z : β<VAR>γ : Type u_3<VAR>inst✝¹ : CompleteLinearOrder γ<VAR>inst✝ : DenselyOrdered γ<VAR>f : α → γ<GOAL>LowerSemicontinuousAt f x ↔ f x ≤ liminf f (𝓝 x)
<VAR>a b : ℤ<GOAL>Fintype.card ↑(Set.uIcc a b) = (b - a).natAbs + 1
<VAR>p q b : ℝ<VAR>hp : 1 ≤ p<VAR>hq : -2 < q<VAR>hb : 0 < b<GOAL>∫ (x : ℂ), ‖x‖ ^ q * rexp (-b * ‖x‖ ^ p) = 2 * π / p * b ^ (-(q + 2) / p) * Real.Gamma ((q + 2) / p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>f =O[l] g ↔ ∃ c, IsBigOWith c l f g
<VAR>x y : ℝ<VAR>f g : Cauchy abs<GOAL>{ cauchy := f / g } = { cauchy := f } / { cauchy := g }
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • s + b • interior s ⊆ interior s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>b • interior s + a • s ⊆ interior s
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ x y : MvPolynomial σ R<VAR>h : Coe.coe x = Coe.coe y<VAR>m✝ : σ →₀ ℕ<GOAL>coeff m✝ x = coeff m✝ y
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>φ ψ x y : MvPolynomial σ R<VAR>h : Coe.coe x = Coe.coe y<VAR>m✝ : σ →₀ ℕ<GOAL>(MvPowerSeries.coeff R m✝) ↑x = (MvPowerSeries.coeff R m✝) ↑y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>a : α<GOAL>‖‖a‖‖₊ = ‖a‖₊
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : SeminormedAddCommGroup α<VAR>a : α<GOAL>⟨‖a‖, ⋯⟩ = ‖a‖₊
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>h✝ : IsEmpty ((i : ι) → A i)<GOAL>∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>h✝ : Nonempty ((i : ι) → A i)<GOAL>∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>h✝ : Nonempty ((i : ι) → A i)<VAR>inhabited_h : Inhabited ((i : ι) → A i)<GOAL>∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)
<VAR>ι : Type u_1<VAR>inst✝³ : Fintype ι<VAR>A : ι → Type u_2<VAR>inst✝² : (i : ι) → MeasurableSpace (A i)<VAR>μ : (i : ι) → Measure (A i)<VAR>inst✝¹ : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq ι<VAR>p : ℝ<VAR>hp₀ : 0 ≤ p<VAR>hp : (↑#ι - 1) * p ≤ 1<VAR>f : ((i : ι) → A i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>h✝ : Nonempty ((i : ι) → A i)<VAR>inhabited_h : Inhabited ((i : ι) → A i)<VAR>H : ∅ ≤ Finset.univ<GOAL>∫⁻ (x : (i : ι) → A i), f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤ (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>s : ℕ<GOAL>Valued.v ((ofPowerSeries ℤ K) PowerSeries.X ^ s) = ↑(Multiplicative.ofAdd (-↑s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>c : ℝ≥0∞<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (a : α), f a ∂c • μ = c * ∫⁻ (a : α), f a ∂μ
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>A : Matrix m n α<GOAL>‖Aᵀ‖₊ = ‖A‖₊
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>A : Matrix m n α<GOAL>(∑ y : m, ∑ x : n, ‖Aᵀ x y‖₊ ^ 2) ^ (1 / 2) = (∑ i : m, ∑ j : n, ‖A i j‖₊ ^ 2) ^ (1 / 2)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a < wellOrderSucc b<GOAL>a ≤ b
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : IsWellOrder α fun x x_1 => x < x_1<VAR>a b : α<VAR>h : a < wellOrderSucc b<VAR>this : b < a<GOAL>False
<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>p : ι → Prop<VAR>s : ι → Set X<VAR>h : (𝓝 x).HasBasis p s<GOAL>(∀ (i : ι), p i → (s i ∩ t).Nonempty) ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝² : MulZeroClass α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : PosMulStrictMono α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a * b
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Abelian C<VAR>A : Type u₁<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} A<VAR>inst✝³ : Category.{v₂, u₂} B<VAR>inst✝² : Abelian A<VAR>inst✝¹ : Abelian B<VAR>L : A ⥤ B<VAR>inst✝ : L.PreservesZeroMorphisms<VAR>hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact<VAR>X✝ Y✝ : A<VAR>f : X✝ ⟶ Y✝<VAR>hf : Epi f<GOAL>Epi (L.map f)
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Abelian C<VAR>A : Type u₁<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} A<VAR>inst✝³ : Category.{v₂, u₂} B<VAR>inst✝² : Abelian A<VAR>inst✝¹ : Abelian B<VAR>L : A ⥤ B<VAR>inst✝ : L.PreservesZeroMorphisms<VAR>hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact<VAR>X✝ Y✝ : A<VAR>f : X✝ ⟶ Y✝<VAR>hf : Epi f<GOAL>(ShortComplex.mk (L.map f) 0 ⋯).Exact
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>inst✝⁵ : Abelian C<VAR>A : Type u₁<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} A<VAR>inst✝³ : Category.{v₂, u₂} B<VAR>inst✝² : Abelian A<VAR>inst✝¹ : Abelian B<VAR>L : A ⥤ B<VAR>inst✝ : L.PreservesZeroMorphisms<VAR>hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact<VAR>X✝ Y✝ : A<VAR>f : X✝ ⟶ Y✝<VAR>hf : Epi f<GOAL>(ShortComplex.mk f 0 ⋯).map L ≅ ShortComplex.mk (L.map f) 0 ⋯
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹⁵ : CommSemiring R<VAR>inst✝¹⁴ : AddCommMonoid M<VAR>inst✝¹³ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹² : CommRing R₁<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁹ : Field K<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module K V<VAR>M'✝ : Type u_7<VAR>M'' : Type u_8<VAR>inst✝⁶ : AddCommMonoid M'✝<VAR>inst✝⁵ : AddCommMonoid M''<VAR>inst✝⁴ : Module R M'✝<VAR>inst✝³ : Module R M''<VAR>B : BilinForm R M<VAR>B₁✝ : BilinForm R₁ M₁<VAR>M' : Type u_9<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>inst✝ : FiniteDimensional K V<VAR>B₁ B₂ : BilinForm K V<VAR>b₂ : B₂.Nondegenerate<VAR>v w : V<GOAL>(B₂ ((B₁.symmCompOfNondegenerate B₂ b₂) w)) v = (B₁ w) v
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p a b c d x y k1 : R<VAR>hk1 : a * x + b * y = p * k1<VAR>k2 : R<VAR>hk2 : c * x + d * y = p * k2<GOAL>(a * d - b * c) * x = p * (d * k1 - b * k2)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p a b c d x y k1 : R<VAR>hk1 : a * x + b * y = p * k1<VAR>k2 : R<VAR>hk2 : c * x + d * y = p * k2<GOAL>(p * k1 - b * y) * d - (p * k2 - d * y) * b = p * (d * k1 - b * k2)
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c d : α<VAR>h : b ≤ c<VAR>x : α<VAR>hab : x ∈ Ico a b<VAR>hbc : x ∈ Ico c d<GOAL>False
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ a b c d : α<VAR>h : b ≤ c<VAR>x : α<VAR>hab : a ≤ x ∧ x < b<VAR>hbc : c ≤ x ∧ x < d<GOAL>False
<VAR>m n✝ n p : ℕ<VAR>hp : Nat.Prime p<GOAL>IsUnit ↑p ↔ ¬p ∣ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>ι : Type u_11<VAR>t : Set ι<VAR>s : ι → Set α<VAR>H : Nonempty α<VAR>w : ⋃ i ∈ t, s i = ⊤<GOAL>t.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι✝ → Sort u_7<VAR>κ₁ : ι✝ → Sort u_8<VAR>κ₂ : ι✝ → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>ι : Type u_11<VAR>t : Set ι<VAR>s : ι → Set α<VAR>H : Nonempty α<VAR>w : ⋃ i ∈ t, s i = ⊤<VAR>x : ι<VAR>m : x ∈ t<GOAL>t.Nonempty
<VAR>ι✝ : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x✝ y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>ι : Type u_2<VAR>f : ι → Set α<VAR>I : Set ι<VAR>x : α<GOAL>infEdist x (⋃ i ∈ I, f i) = ⨅ i ∈ I, infEdist x (f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>p✝ q : α → Prop<VAR>inst✝ : Countable ι<VAR>p : ι → α → Prop<VAR>hp : ∀ (i : ι), Measurable (p i)<GOAL>MeasurableSet {a | ∀ (i : ι), p i a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>p✝ q : α → Prop<VAR>inst✝ : Countable ι<VAR>p : ι → α → Prop<VAR>hp : ∀ (i : ι), Measurable (p i)<GOAL>MeasurableSet (⋂ i, {x | p i x})
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v : α → M<VAR>v' : α' → M'<VAR>c : R<VAR>a : α<GOAL>(Finsupp.total α M R v) (single a c) = c • v a
<VAR>s : Finset ℕ<VAR>p n : ℕ<VAR>hp : Prime p<VAR>e : ℕ<VAR>hn : n ∈ factoredNumbers s<GOAL>p ^ e * n ∈ factoredNumbers (insert p s)
<VAR>s : Finset ℕ<VAR>p n : ℕ<VAR>hp : Prime p<VAR>e : ℕ<VAR>hn : n ∈ factoredNumbers s<VAR>hp' : p ^ e ≠ 0<GOAL>p ^ e * n ∈ factoredNumbers (insert p s)
<VAR>s : Finset ℕ<VAR>p n : ℕ<VAR>hp : Prime p<VAR>e : ℕ<VAR>hn : n ∈ factoredNumbers s<VAR>hp' : p ^ e ≠ 0<VAR>q : ℕ<VAR>hq : q ∈ (p ^ e * n).primeFactorsList<GOAL>q ∈ insert p s
<VAR>s : Finset ℕ<VAR>p n : ℕ<VAR>hp : Prime p<VAR>e : ℕ<VAR>hn : n ∈ factoredNumbers s<VAR>hp' : p ^ e ≠ 0<VAR>q : ℕ<VAR>hq : q ∈ (p ^ e * n).primeFactorsList<VAR>H : q ∈ (p ^ e).primeFactorsList<GOAL>q ∈ insert p s
<VAR>s : Finset ℕ<VAR>p n : ℕ<VAR>hp : Prime p<VAR>e : ℕ<VAR>hn : n ∈ factoredNumbers s<VAR>hp' : p ^ e ≠ 0<VAR>q : ℕ<VAR>hq : q ∈ (p ^ e * n).primeFactorsList<VAR>H : q ∈ n.primeFactorsList<GOAL>q ∈ insert p 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>K : LieSubalgebra R L<GOAL>(∃ I, lieIdealSubalgebra R L I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K
<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>K : LieSubalgebra R L<GOAL>(∀ (x m : L), m ∈ K.toSubmodule → ⁅x, m⁆ ∈ K.toSubmodule) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>a b : α<VAR>l : List α<VAR>h : indexOf a (b :: l) < (b :: l).length<GOAL>(b :: l)[indexOf a (b :: l)] = a
<VAR>α : Type u<VAR>l✝ l' l : List α<VAR>hn : l.Nodup<GOAL>l.cyclicPermutations.Nodup
<VAR>α : Type u<VAR>l l' : List α<VAR>hn : [].Nodup<GOAL>[].cyclicPermutations.Nodup
<VAR>α : Type u<VAR>l✝ l' l : List α<VAR>hn : l.Nodup<VAR>hl : l ≠ []<GOAL>l.cyclicPermutations.Nodup
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>w : W<VAR>hw : w ≠ 1<GOAL>∃ i, cs.IsLeftDescent w i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>hw : cs.wordProd ω ≠ 1<VAR>h : ω.length = cs.length (cs.wordProd ω)<GOAL>∃ i, cs.IsLeftDescent (cs.wordProd ω) i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<VAR>hw : cs.wordProd ω ≠ 1<VAR>h : ω.length = cs.length (cs.wordProd ω)<VAR>h₁ : ω ≠ []<GOAL>∃ i, cs.IsLeftDescent (cs.wordProd ω) i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<VAR>ω' : List B<VAR>hw : cs.wordProd (i :: ω') ≠ 1<VAR>h : (i :: ω').length = cs.length (cs.wordProd (i :: ω'))<VAR>h₁ : i :: ω' ≠ []<GOAL>∃ i_1, cs.IsLeftDescent (cs.wordProd (i :: ω')) i_1
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<VAR>ω' : List B<VAR>hw : cs.wordProd (i :: ω') ≠ 1<VAR>h : (i :: ω').length = cs.length (cs.wordProd (i :: ω'))<VAR>h₁ : i :: ω' ≠ []<GOAL>cs.IsLeftDescent (cs.wordProd (i :: ω')) i
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i : B<VAR>ω' : List B<VAR>hw : cs.wordProd (i :: ω') ≠ 1<VAR>h : (i :: ω').length = cs.length (cs.wordProd (i :: ω'))<VAR>h₁ : i :: ω' ≠ []<GOAL>cs.length (cs.wordProd ω') < (i :: ω').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>v : V<GOAL>AffineIndependent k (v +ᵥ p) ↔ AffineIndependent k p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a : Part α<VAR>ha : a.Dom<VAR>b : α<VAR>h : a.get ha = b<GOAL>a = some b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f g : ι → N<VAR>s t : Finset ι<VAR>i j : ι<VAR>hf : ∀ i ∈ s, 1 ≤ f i<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hne : i ≠ j<GOAL>f i * f j = ∏ k ∈ cons i {j} ⋯, f k
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f g : ι → N<VAR>s t : Finset ι<VAR>i j : ι<VAR>hf : ∀ i ∈ s, 1 ≤ f i<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hne : i ≠ j<GOAL>∏ k ∈ cons i {j} ⋯, f k ≤ ∏ k ∈ s, f k
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : OrderedCommMonoid N<VAR>f g : ι → N<VAR>s t : Finset ι<VAR>i j : ι<VAR>hf : ∀ i ∈ s, 1 ≤ f i<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hne : i ≠ j<GOAL>cons i {j} ⋯ ⊆ s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f ⁻¹' s ≤ᶠ[ae μ] s<VAR>h_fin : μ s ≠ ⊤<GOAL>s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f ⁻¹' s ≤ᶠ[ae μ] s<VAR>h_fin : μ s ≠ ⊤<GOAL>f ⁻¹' s =ᶠ[ae μ] s
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : Ergodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f ⁻¹' s ≤ᶠ[ae μ] s<VAR>h_fin : μ s ≠ ⊤<GOAL>MeasurableSet (f ⁻¹' s)
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : OreSet R⁰<VAR>inst✝ : NoZeroDivisors R<GOAL>0⁻¹ = 0
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : OreSet R⁰<VAR>inst✝ : NoZeroDivisors R<GOAL>(if hr : 0 = 0 then 0 else ↑1 /ₒ ⟨0, ⋯⟩) = 0 /ₒ 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f✝ : X → Y<VAR>g✝ : Y → Z<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<VAR>g_inj : Injective g<VAR>ℱ : Filter X<VAR>y : Y<VAR>h : MapClusterPt y ℱ f<GOAL>∃ x, f x = y ∧ ClusterPt x ℱ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace W<VAR>f✝ : X → Y<VAR>g✝ : Y → Z<VAR>f : X → Y<VAR>g : Y → Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<VAR>g_inj : Injective g<VAR>ℱ : Filter X<VAR>y : Y<VAR>h : MapClusterPt y ℱ f<VAR>x : X<VAR>hx1 : (g ∘ f) x = g y<VAR>hx2 : ClusterPt x ℱ<GOAL>∃ x, f x = y ∧ ClusterPt x ℱ
<VAR>I : Type u<VAR>inst✝⁵ : AddMonoid I<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : DecidableEq I<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : (X₁ : C) → PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)<VAR>X X' : GradedObject I C<VAR>φ : X ⟶ X'<GOAL>tensorHom φ (𝟙 tensorUnit) ≫ (rightUnitor X').hom = (rightUnitor X).hom ≫ φ
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Finset β<VAR>hf : BijOn f (f ⁻¹' ↑s) ↑s<GOAL>↑(image f (s.preimage f ⋯)) = ↑s
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ : C<VAR>f✝ : X✝ ⟶ Y✝<VAR>inst✝³ : HasImage f✝<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>inst✝² : HasImage f<VAR>g : Y ⟶ Z<VAR>inst✝¹ : HasImage g<VAR>sq : Arrow.mk f ⟶ Arrow.mk g<VAR>inst✝ : HasImageMap sq<GOAL>(image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv) ≫ (imageSubobject (Arrow.mk g).hom).arrow = ((imageSubobjectIso f).inv ≫ imageSubobjectMap sq) ≫ (imageSubobject (Arrow.mk g).hom).arrow
<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>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>hf : Injective (f a)<GOAL>(image₂ f {a} t).card = t.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace Ω<VAR>inst✝⁵ : StandardBorelSpace Ω<VAR>inst✝⁴ : Nonempty Ω<VAR>inst✝³ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>hX : Measurable X<VAR>hY : AEMeasurable Y μ<VAR>hf : StronglyMeasurable f<VAR>hf_int : Integrable (fun a => f (X a, Y a)) μ<GOAL>Integrable f (Measure.map (fun a => (X a, Y a)) μ)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁶ : MonoidWithZero R<VAR>inst✝⁵ : MonoidWithZero R'<VAR>inst✝⁴ : Zero M<VAR>inst✝³ : MulActionWithZero R M<VAR>inst✝² : Zero M'<VAR>inst✝¹ : SMul R M'<VAR>p : Prop<VAR>inst✝ : Decidable p<VAR>a : R<VAR>b : M<GOAL>(if p then a else 0) • b = if p then a • b else 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>f : α →* β<VAR>a b : α<VAR>c : αˣ<VAR>hc : SemiconjBy (↑c) a b<GOAL>SemiconjBy (↑((Units.map f) c)) (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>s : Set ι<VAR>t : Set ι'<VAR>inst✝ : LinearOrder ι<VAR>f : ι → Set α<VAR>h : ¬s.PairwiseDisjoint f<GOAL>∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j