ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>M : Matrix n n 𝕜<VAR>e : n ≃ Fin (Fintype.card n)<GOAL>∃ L L' D, (List.map toMatrix L).prod * M * (List.map toMatrix L').prod = diagonal D
<VAR>n : Type u_1<VAR>p : Type u_2<VAR>R : Type u₂<VAR>𝕜 : Type u_3<VAR>inst✝⁵ : Field 𝕜<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : DecidableEq p<VAR>inst✝² : CommRing R<VAR>r : ℕ<VAR>M✝ : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype p<VAR>M : Matrix n n 𝕜<VAR>e : n ≃ Fin (Fintype.card n)<GOAL>∃ L L' D, (List.map toMatrix L).prod * (reindexAlgEquiv 𝕜 𝕜 e) M * (List.map toMatrix L').prod = diagonal D
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s<GOAL>s.Subsingleton
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s<VAR>x : X<VAR>hx : x ∈ s<VAR>y : X<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<GOAL>False
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s<VAR>x : X<VAR>hx : x ∈ s<VAR>y : X<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<VAR>U : Set X<VAR>hUo : IsOpen U<VAR>hU : Xor' (x ∈ U) (y ∈ U)<GOAL>False
<VAR>X✝ : Type u_1<VAR>inst✝² : TopologicalSpace X✝<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s<VAR>x : X<VAR>hx : x ∈ s<VAR>y : X<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<VAR>U : Set X<VAR>hUo : IsOpen U<VAR>hU : Xor' (x ∈ U) (y ∈ U)<VAR>hxU : x ∈ U<VAR>hyU : y ∉ U<GOAL>False
<VAR>X✝ : Type u_1<VAR>inst✝² : TopologicalSpace X✝<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hmin : ∀ t ⊆ s, t.Nonempty → IsClosed t → t = s<VAR>x : X<VAR>hx : x ∈ s<VAR>y : X<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<VAR>U : Set X<VAR>hUo : IsOpen U<VAR>hU : Xor' (x ∈ U) (y ∈ U)<VAR>hxU : x ∈ U<VAR>hyU : y ∉ U<VAR>this : s \ U = s<GOAL>False
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>D✝ D E : Set C<VAR>h : D ≤ E<GOAL>full D ≤ full E
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>D✝ D E : Set C<VAR>h : D ≤ E<GOAL>∀ {c d : C}, (full D).arrows c d ⊆ (full E).arrows c d
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>D✝ D E : Set C<VAR>h : D ≤ E<VAR>c d : C<VAR>f : c ⟶ d<GOAL>f ∈ (full D).arrows c d → f ∈ (full E).arrows c d
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>D✝ D E : Set C<VAR>h : D ≤ E<VAR>c d : C<VAR>f : c ⟶ d<GOAL>c ∈ D ∧ d ∈ D → c ∈ E ∧ d ∈ E
<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>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>x : L<GOAL>φ.IsNilRegular x ↔ (charpoly (φ x)).natTrailingDegree = φ.nilRank
<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>ιM : Type u_7<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup L<VAR>inst✝¹² : Module R L<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁹ : Fintype ι<VAR>inst✝⁸ : Fintype ι'<VAR>inst✝⁷ : Fintype ιM<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : DecidableEq ι'<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝² : Module.Finite R L<VAR>inst✝¹ : Module.Free R L<VAR>inst✝ : Nontrivial R<VAR>x : L<GOAL>(charpoly (φ x)).coeff φ.nilRank ≠ 0 ↔ (charpoly (φ x)).natTrailingDegree = φ.nilRank
<VAR>α : Type u_1<VAR>l : List α<VAR>x y : α<VAR>h : x ∈+ y :: l<VAR>hx : x ≠ y<GOAL>x ∈+ l
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n✝ : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>hp : p.Monic<VAR>n : ℕ<GOAL>(p ^ n).nextCoeff = n • p.nextCoeff
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<GOAL>∃ ϖ, Irreducible ϖ
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<GOAL>∃ ϖ, maximalIdeal R = span {ϖ}
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>I : LieIdeal R L<VAR>hI : IsSolvable R ↥↑I<VAR>s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}<GOAL>sInf s = 0 ↔ I = ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>I : LieIdeal R L<VAR>hI : IsSolvable R ↥↑I<VAR>s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}<VAR>hne : s ≠ ∅<GOAL>sInf s = 0 ↔ I = ⊥
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>hs : IsIntegral R s<VAR>p : R[X]<VAR>hp : (Polynomial.aeval s) p = 0<VAR>K : Type u_1 := FractionRing R<VAR>L : Type u_2 := FractionRing S<VAR>x✝ : Algebra K L := FractionRing.liftAlgebra R L<VAR>this✝ : IsScalarTower R (FractionRing R) L<VAR>this : minpoly K ((algebraMap S L) s) ∣ map (algebraMap R K) (p %ₘ minpoly R s)<GOAL>minpoly R s ∣ p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>hs : IsIntegral R s<VAR>p : R[X]<VAR>hp : (Polynomial.aeval s) p = 0<VAR>K : Type u_1 := FractionRing R<VAR>L : Type u_2 := FractionRing S<VAR>x✝ : Algebra K L := FractionRing.liftAlgebra R L<VAR>this✝ : IsScalarTower R (FractionRing R) L<VAR>this : minpoly R s ∣ p %ₘ minpoly R s<GOAL>minpoly R s ∣ p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>hs : IsIntegral R s<VAR>p : R[X]<VAR>hp : (Polynomial.aeval s) p = 0<VAR>K : Type u_1 := FractionRing R<VAR>L : Type u_2 := FractionRing S<VAR>x✝ : Algebra K L := FractionRing.liftAlgebra R L<VAR>this✝ : IsScalarTower R (FractionRing R) L<VAR>this : minpoly R s ∣ p %ₘ minpoly R s<GOAL>p %ₘ minpoly R s = 0
<VAR>x y : ℂ<GOAL>sinh x - cosh x = -cexp (-x)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : C<VAR>inst✝ : ExactPairing X Y<GOAL>Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y = ⊗𝟙
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝⁸ : FunLike F α β<VAR>inst✝⁷ : Inf α<VAR>inst✝⁶ : Top α<VAR>inst✝⁵ : Inf β<VAR>inst✝⁴ : Top β<VAR>inst✝³ : Inf γ<VAR>inst✝² : Top γ<VAR>inst✝¹ : Inf δ<VAR>inst✝ : Top δ<VAR>g : InfTopHom β γ<VAR>f₁ f₂ : InfTopHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{?u.4808, u_1} C<VAR>inst✝⁶ : Category.{?u.4812, u_2} D<VAR>inst✝⁵ : Category.{?u.4816, u_3} E<VAR>inst✝⁴ : Category.{?u.4820, 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>n m a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>m + n + a = a''
<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.4816, u_3} E<VAR>inst✝⁴ : Category.{?u.4820, 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>n m a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso (m + n) a a'' ⋯).hom.app X = (shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X) ≫ (shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v w : E<VAR>hw : w ∈ K<GOAL>⟪w, v - ↑((orthogonalProjection K) v)⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>v w : E<VAR>hw : w ∈ K<GOAL>⟪v - ↑((orthogonalProjection K) v), w⟫_𝕜 = 0
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>f : ℝ ≃ᵐ ℝ<VAR>f' : ℝ → ℝ<VAR>h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>(Measure.map (⇑f.symm) (gaussianReal μ v)) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>hv : v ≠ 0<VAR>f : ℝ ≃ᵐ ℝ<VAR>f' : ℝ → ℝ<VAR>h_deriv : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x<VAR>s : Set ℝ<VAR>hs : MeasurableSet s<GOAL>(Measure.map (⇑f.symm) (ℙ.withDensity fun x => ENNReal.ofReal (gaussianPDFReal μ v x))) s = ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * gaussianPDFReal μ v (f x))
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Fintype σ<VAR>s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val<GOAL>∏ i : σ, (Polynomial.X + Polynomial.C (X i)) = ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Fintype σ<VAR>s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val<VAR>this : Fintype.card σ = Multiset.card s<GOAL>∏ i : σ, (Polynomial.X + Polynomial.C (X i)) = ∑ j ∈ range (Fintype.card σ + 1), Polynomial.C (esymm σ R j) * Polynomial.X ^ (Fintype.card σ - j)
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Fintype σ<VAR>s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val<VAR>this : Fintype.card σ = Multiset.card s<GOAL>(Multiset.map (fun i => Polynomial.X + Polynomial.C (X i)) univ.val).prod = ∑ x ∈ range (Multiset.card s + 1), Polynomial.C ((Multiset.map X univ.val).esymm x) * Polynomial.X ^ (Multiset.card s - x)
<VAR>R : Type u_1<VAR>σ : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : Fintype σ<VAR>s : Multiset (MvPolynomial σ R) := Multiset.map (fun i => X i) univ.val<VAR>this : Fintype.card σ = Multiset.card s<GOAL>Multiset.map (fun i => Polynomial.X + Polynomial.C (X i)) univ.val = Multiset.map (fun r => Polynomial.X + Polynomial.C r) s
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>inst✝⁷ : AddMonoid ιA<VAR>inst✝⁶ : VAdd ιA ιB<VAR>inst✝⁵ : (i : ιA) → AddCommMonoid (A i)<VAR>inst✝⁴ : (i : ιB) → AddCommMonoid (M i)<VAR>inst✝³ : DecidableEq ιA<VAR>inst✝² : DecidableEq ιB<VAR>inst✝¹ : GMonoid A<VAR>inst✝ : Gmodule A M<VAR>x : ⨁ (i : ιB), M i<GOAL>1 • x = x
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>inst✝⁷ : AddMonoid ιA<VAR>inst✝⁶ : VAdd ιA ιB<VAR>inst✝⁵ : (i : ιA) → AddCommMonoid (A i)<VAR>inst✝⁴ : (i : ιB) → AddCommMonoid (M i)<VAR>inst✝³ : DecidableEq ιA<VAR>inst✝² : DecidableEq ιB<VAR>inst✝¹ : GMonoid A<VAR>inst✝ : Gmodule A M<VAR>x : ⨁ (i : ιB), M i<GOAL>(smulAddMonoidHom A M) 1 = AddMonoidHom.id (⨁ (i : ιB), M i)
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>inst✝⁷ : AddMonoid ιA<VAR>inst✝⁶ : VAdd ιA ιB<VAR>inst✝⁵ : (i : ιA) → AddCommMonoid (A i)<VAR>inst✝⁴ : (i : ιB) → AddCommMonoid (M i)<VAR>inst✝³ : DecidableEq ιA<VAR>inst✝² : DecidableEq ιB<VAR>inst✝¹ : GMonoid A<VAR>inst✝ : Gmodule A M<VAR>x : ⨁ (i : ιB), M i<GOAL>∀ (i : ιB) (y : M i), ((smulAddMonoidHom A M) 1) ((of M i) y) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) y)
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>inst✝⁷ : AddMonoid ιA<VAR>inst✝⁶ : VAdd ιA ιB<VAR>inst✝⁵ : (i : ιA) → AddCommMonoid (A i)<VAR>inst✝⁴ : (i : ιB) → AddCommMonoid (M i)<VAR>inst✝³ : DecidableEq ιA<VAR>inst✝² : DecidableEq ιB<VAR>inst✝¹ : GMonoid A<VAR>inst✝ : Gmodule A M<VAR>x : ⨁ (i : ιB), M i<VAR>i : ιB<VAR>xi : M i<GOAL>((smulAddMonoidHom A M) ((of A 0) GOne.one)) ((of M i) xi) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) xi)
<VAR>ιA : Type u_1<VAR>ιB : Type u_2<VAR>A : ιA → Type u_3<VAR>M : ιB → Type u_4<VAR>inst✝⁷ : AddMonoid ιA<VAR>inst✝⁶ : VAdd ιA ιB<VAR>inst✝⁵ : (i : ιA) → AddCommMonoid (A i)<VAR>inst✝⁴ : (i : ιB) → AddCommMonoid (M i)<VAR>inst✝³ : DecidableEq ιA<VAR>inst✝² : DecidableEq ιB<VAR>inst✝¹ : GMonoid A<VAR>inst✝ : Gmodule A M<VAR>x : ⨁ (i : ιB), M i<VAR>i : ιB<VAR>xi : M i<GOAL>(of M (0 +ᵥ i)) (GSMul.smul GOne.one xi) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) xi)
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : F[X]<VAR>h : ¬f * g = 0<GOAL>(f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f g : F[X]<VAR>h : ¬f * g = 0<GOAL>((f.aroots (AlgebraicClosure F)).toFinset ∪ (g.aroots (AlgebraicClosure F)).toFinset).card ≤ (f.aroots (AlgebraicClosure F)).toFinset.card + (g.aroots (AlgebraicClosure F)).toFinset.card
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q p : R[X]<GOAL>(p.sum fun n a => C a * X ^ n) = p
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<GOAL>∫⁻ (x : ℝ), gammaPDF a r x = 1
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0<GOAL>∫⁻ (x : ℝ), gammaPDF a r x = 1
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0<VAR>rightSide : ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x = ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))<GOAL>∫⁻ (x : ℝ), gammaPDF a r x = 1
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0<VAR>rightSide : ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x = ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))<GOAL>∫ (a_1 : ℝ) in Ici 0, r ^ a / Gamma a * a_1 ^ (a - 1) * rexp (-(r * a_1)) = 1
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0<VAR>rightSide : ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x = ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))<GOAL>0 ≤ᶠ[ae (ℙ.restrict (Ici 0))] fun x => r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
<VAR>a r : ℝ<VAR>ha : 0 < a<VAR>hr : 0 < r<VAR>leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0<VAR>rightSide : ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x = ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))<GOAL>AEStronglyMeasurable (fun x => r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (ℙ.restrict (Ici 0))
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f₁ : α → β<VAR>f₂ : α → γ<VAR>h₁ : UniformContinuous f₁<VAR>h₂ : UniformContinuous f₂<GOAL>UniformContinuous fun a => (f₁ a, f₂ a)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f₁ : α → β<VAR>f₂ : α → γ<VAR>h₁ : UniformContinuous f₁<VAR>h₂ : UniformContinuous f₂<GOAL>Tendsto (fun x => ((f₁ x.1, f₂ x.1), f₁ x.2, f₂ x.2)) (𝓤 α) (comap (fun p => (p.1.1, p.2.1)) (𝓤 β) ⊓ comap (fun p => (p.1.2, p.2.2)) (𝓤 γ))
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>n : ℕ<VAR>hn : longestPrefix x s < n<GOAL>Disjoint s (cylinder x n)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>n : ℕ<VAR>hn : ¬Disjoint s (cylinder x n)<GOAL>n ≤ longestPrefix x s
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>n : ℕ<VAR>hn : ¬Disjoint s (cylinder x n)<VAR>y : (n : ℕ) → E n<VAR>ys : y ∈ s<VAR>hy : y ∈ cylinder x n<GOAL>n ≤ longestPrefix x s
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>n : ℕ<VAR>hn : ¬Disjoint s (cylinder x n)<VAR>y : (n : ℕ) → E n<VAR>ys : y ∈ s<VAR>hy : y ∈ cylinder x n<GOAL>n ≤ firstDiff x y
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>n : ℕ<VAR>hn : ¬Disjoint s (cylinder x n)<VAR>y : (n : ℕ) → E n<VAR>ys : y ∈ s<VAR>hy : y ∈ cylinder x n<GOAL>x ∈ cylinder y n
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>X : Cᵒᵖ<GOAL>contractibleTriangle X ∈ distinguishedTriangles C
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>X : Cᵒᵖ<GOAL>∃ T', ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles), Nonempty (contractibleTriangle X ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))
<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>R₂ : ?m.76253<VAR>x✝¹ x✝ : M<GOAL>(RingHom.id R) ((B x✝¹) x✝) = (B x✝) x✝¹ ↔ ((flipHom B) x✝¹) x✝ = (B x✝¹) x✝
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>inst✝² : One M<VAR>inst✝¹ : ConditionallyCompleteLattice M<VAR>inst✝ : Nonempty ι<VAR>f : ι → α → M<GOAL>(mulSupport fun x => ⨆ i, f i x) ⊆ ⋃ i, mulSupport (f i)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>inst✝² : One M<VAR>inst✝¹ : ConditionallyCompleteLattice M<VAR>inst✝ : Nonempty ι<VAR>f : ι → α → M<GOAL>∀ (x : α), (∀ (x_1 : ι), f x_1 x = 1) → ⨆ i, f i x = 1
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>inst✝² : One M<VAR>inst✝¹ : ConditionallyCompleteLattice M<VAR>inst✝ : Nonempty ι<VAR>f : ι → α → M<VAR>x : α<VAR>hx : ∀ (x_1 : ι), f x_1 x = 1<GOAL>⨆ i, f i x = 1
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p p₁ p₂ : P<VAR>h : (∡ p₁ p p₂).sign = 0<GOAL>p₁ = p ∨ p₂ = p ∨ ∠ p₁ p p₂ = 0 ∨ ∠ p₁ p p₂ = π
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<GOAL>UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' univ ∩ range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<GOAL>UniqueDiffWithinAt 𝕜 (range ↑I) (↑(extChartAt I x) x)
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>ρ ν : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a<GOAL>ρ s ≤ ν s
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>ρ ν : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>x✝ : ν s < ⊤<GOAL>ρ s ≤ ν s + ↑ε
<VAR>α : Type u_1<VAR>inst✝⁴ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SecondCountableTopology α<VAR>inst✝¹ : BorelSpace α<VAR>ρ ν : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ν<VAR>hρ : ρ ≪ μ<VAR>s : Set α<VAR>hs : ∀ x ∈ s, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ≤ ν a<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>x✝ : ν s < ⊤<VAR>U : Set α<VAR>sU : s ⊆ U<VAR>U_open : IsOpen U<VAR>νU : ν U ≤ ν s + ↑ε<GOAL>ρ s ≤ ν s + ↑ε