ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>xl xr : Type u<VAR>x y : PGame<VAR>h₁ : y ⧏ x<VAR>h₂ : y ≤ x<GOAL>x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
<VAR>xl xr : Type u<VAR>x y : PGame<VAR>h₁ : y ⧏ x<VAR>h₂ : x ⧏ y<GOAL>x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ : ↥H → R<VAR>x : L<VAR>m : M<VAR>hx : x ∈ rootSpace H χ₁<VAR>hm : m ∈ weightSpace M χ₂<VAR>n : ℕ<GOAL>((toEnd R L M) x ^ n) m ∈ weightSpace M (n • χ₁ + χ₂)
<VAR>m n✝ n : ℕ<VAR>a b : ZMod n<VAR>h : a.val + b.val < n<VAR>this : NeZero n<GOAL>(a + b).val = a.val + b.val
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n : ℕ<GOAL>(ascPochhammer ℕ (n + 0 + 1)).smeval (-↑n) = 0
<VAR>R : Type u_1<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Pow R ℕ<VAR>inst✝ : BinomialRing R<VAR>n k : ℕ<GOAL>(ascPochhammer ℕ (n + (k + 1) + 1)).smeval (-↑n) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>hl' : l'.HasBasis p s<VAR>t : Set α<GOAL>t ∈ l ↔ t ∈ l'
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<GOAL>∃ s, x ∈ ⨆ i ∈ s, f i
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<VAR>this : F⟮x⟯ ≤ ⨆ i, f i → ∃ s, F⟮x⟯ ≤ ⨆ i ∈ s, f i<GOAL>∃ s, x ∈ ⨆ i ∈ s, f i
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>ι : Type u_3<VAR>f : ι → IntermediateField F E<VAR>x : E<VAR>hx : x ∈ ⨆ i, f i<VAR>this : x ∈ ⨆ i, f i → ∃ s, x ∈ ⨆ i ∈ s, f i<GOAL>∃ s, x ∈ ⨆ i ∈ s, f i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : ι →₀ M<VAR>g : κ →₀ N<VAR>i : ι<VAR>k : κ<GOAL>((finsuppTensorFinsupp R S M N ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : ι →₀ M<VAR>g : κ →₀ N<VAR>i : ι<VAR>k : κ<GOAL>((finsuppTensorFinsupp R S M N ι κ) (0 ⊗ₜ[R] g)) (i, k) = 0 i ⊗ₜ[R] g k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : ι →₀ M<VAR>g : κ →₀ N<VAR>i : ι<VAR>k : κ<GOAL>∀ (f g_1 : ι →₀ M), ((finsuppTensorFinsupp R S M N ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k → ((finsuppTensorFinsupp R S M N ι κ) (g_1 ⊗ₜ[R] g)) (i, k) = g_1 i ⊗ₜ[R] g k → ((finsuppTensorFinsupp R S M N ι κ) ((f + g_1) ⊗ₜ[R] g)) (i, k) = (f + g_1) i ⊗ₜ[R] g k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : ι →₀ M<VAR>g : κ →₀ N<VAR>i : ι<VAR>k : κ<GOAL>∀ (a : ι) (b : M), ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single a b ⊗ₜ[R] g)) (i, k) = (Finsupp.single a b) i ⊗ₜ[R] g k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : ι →₀ M<VAR>g : κ →₀ N<VAR>i : ι<VAR>k : κ<VAR>i' : ι<VAR>m : M<GOAL>((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] g k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : ι →₀ M<VAR>g : κ →₀ N<VAR>i : ι<VAR>k : κ<VAR>i' : ι<VAR>m : M<GOAL>((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] 0)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] 0 k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : ι →₀ M<VAR>g : κ →₀ N<VAR>i : ι<VAR>k : κ<VAR>i' : ι<VAR>m : M<GOAL>∀ (f g : κ →₀ N), ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] f)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] f k → ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] g k → ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] (f + g))) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] (f + g) k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : ι →₀ M<VAR>g : κ →₀ N<VAR>i : ι<VAR>k : κ<VAR>i' : ι<VAR>m : M<GOAL>∀ (a : κ) (b : N), ((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single a b)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single a b) k
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Semiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>f : ι →₀ M<VAR>g : κ →₀ N<VAR>i : ι<VAR>k : κ<VAR>i' : ι<VAR>m : M<VAR>k' : κ<VAR>n : N<GOAL>((finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n)) (i, k) = (Finsupp.single i' m) i ⊗ₜ[R] (Finsupp.single k' n) k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<VAR>h : a ≤ b<VAR>x val✝ : α<VAR>property✝ : val✝ ∈ Icc a b<GOAL>projIcc a b h ↑⟨val✝, property✝⟩ = ⟨val✝, property✝⟩
<VAR>n m : ℕ<VAR>a b : Fin m<GOAL>castAdd n a = castAdd n b ↔ a = b
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝⁴ : Fintype ι<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → DecidableEq (α i)<VAR>inst✝¹ : (i : ι) → PartialOrder (α i)<VAR>inst✝ : (i : ι) → LocallyFiniteOrder (α i)<VAR>a b : (i : ι) → α i<GOAL>(Ioc a b).card = ∏ i : ι, (Icc (a i) (b i)).card - 1
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>E : Type u_3<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F K<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra K E<VAR>inst✝³ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝² : Field E'<VAR>inst✝¹ : Algebra F E'<VAR>f : E →ₐ[F] E'<VAR>inst✝ : Algebra.IsSeparable F E'<VAR>this : Algebra E E' := f.toAlgebra<GOAL>Algebra.IsSeparable F E
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>E : Type u_3<VAR>inst✝⁹ : Field F<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field E<VAR>inst✝⁶ : Algebra F K<VAR>inst✝⁵ : Algebra F E<VAR>inst✝⁴ : Algebra K E<VAR>inst✝³ : IsScalarTower F K E<VAR>E' : Type u_4<VAR>inst✝² : Field E'<VAR>inst✝¹ : Algebra F E'<VAR>f : E →ₐ[F] E'<VAR>inst✝ : Algebra.IsSeparable F E'<VAR>this✝ : Algebra E E' := f.toAlgebra<VAR>this : IsScalarTower F E E'<GOAL>Algebra.IsSeparable F E
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>(a ⇨ b) ⊓ (b ⇨ c) ≤ a ⇨ c
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>(a ⇨ b) ⊓ a ≤ (b ⇨ c) ⇨ c
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>comm : a ≫ f₁ = b ≫ f₁<VAR>big_k : IsKernelPair (f₁ ≫ f₂) a b<VAR>s : PullbackCone f₁ f₁<VAR>s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯<GOAL>{ l // l ≫ (PullbackCone.mk a b ⋯).fst = s.fst ∧ l ≫ (PullbackCone.mk a b ⋯).snd = s.snd ∧ ∀ {m : s.pt ⟶ (PullbackCone.mk a b ⋯).pt}, m ≫ (PullbackCone.mk a b ⋯).fst = s.fst → m ≫ (PullbackCone.mk a b ⋯).snd = s.snd → m = l }
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>comm : a ≫ f₁ = b ≫ f₁<VAR>big_k : IsKernelPair (f₁ ≫ f₂) a b<VAR>s : PullbackCone f₁ f₁<VAR>s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯<VAR>m✝ : s.pt ⟶ (PullbackCone.mk a b ⋯).pt<VAR>m₁ : m✝ ≫ (PullbackCone.mk a b ⋯).fst = s.fst<VAR>m₂ : m✝ ≫ (PullbackCone.mk a b ⋯).snd = s.snd<GOAL>m✝ = (IsPullback.isLimit big_k).lift s'
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>comm : a ≫ f₁ = b ≫ f₁<VAR>big_k : IsKernelPair (f₁ ≫ f₂) a b<VAR>s : PullbackCone f₁ f₁<VAR>s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯<VAR>m✝ : s.pt ⟶ (PullbackCone.mk a b ⋯).pt<VAR>m₁ : m✝ ≫ (PullbackCone.mk a b ⋯).fst = s.fst<VAR>m₂ : m✝ ≫ (PullbackCone.mk a b ⋯).snd = s.snd<GOAL>∀ (j : WalkingCospan), m✝ ≫ (IsPullback.cone big_k).π.app j = (IsPullback.isLimit big_k).lift s' ≫ (IsPullback.cone big_k).π.app j
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>comm : a ≫ f₁ = b ≫ f₁<VAR>big_k : IsKernelPair (f₁ ≫ f₂) a b<VAR>s : PullbackCone f₁ f₁<VAR>s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯<VAR>m✝ : s.pt ⟶ (PullbackCone.mk a b ⋯).pt<VAR>m₁ : m✝ ≫ (PullbackCone.mk a b ⋯).fst = s.fst<VAR>m₂ : m✝ ≫ (PullbackCone.mk a b ⋯).snd = s.snd<GOAL>a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>comm : a ≫ f₁ = b ≫ f₁<VAR>big_k : IsKernelPair (f₁ ≫ f₂) a b<VAR>s : PullbackCone f₁ f₁<VAR>s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯<VAR>m✝ : s.pt ⟶ (PullbackCone.mk a b ⋯).pt<VAR>m₁ : m✝ ≫ (PullbackCone.mk a b ⋯).fst = s.fst<VAR>m₂ : m✝ ≫ (PullbackCone.mk a b ⋯).snd = s.snd<GOAL>m✝ ≫ (PullbackCone.mk a b ?refine_1).fst = (IsPullback.isLimit big_k).lift s' ≫ (PullbackCone.mk a b ?refine_1).fst
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>R X Y Z : C<VAR>f : X ⟶ Y<VAR>a b : R ⟶ X<VAR>f₁ : X ⟶ Y<VAR>f₂ : Y ⟶ Z<VAR>comm : a ≫ f₁ = b ≫ f₁<VAR>big_k : IsKernelPair (f₁ ≫ f₂) a b<VAR>s : PullbackCone f₁ f₁<VAR>s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯<VAR>m✝ : s.pt ⟶ (PullbackCone.mk a b ⋯).pt<VAR>m₁ : m✝ ≫ (PullbackCone.mk a b ⋯).fst = s.fst<VAR>m₂ : m✝ ≫ (PullbackCone.mk a b ⋯).snd = s.snd<GOAL>m✝ ≫ (PullbackCone.mk a b ?refine_1).snd = (IsPullback.isLimit big_k).lift s' ≫ (PullbackCone.mk a b ?refine_1).snd
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hM : IsNilpotent M<GOAL>IsNilpotent M.trace
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hM : IsNilpotent M<VAR>h✝ : IsEmpty n<GOAL>IsNilpotent M.trace
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hM : IsNilpotent M<VAR>h✝ : Nonempty n<GOAL>IsNilpotent M.trace
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>n G : Type v<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α β : Type v<VAR>inst✝¹ : DecidableEq α<VAR>M : Matrix n n R<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>hM : IsNilpotent M<VAR>h✝ : Nonempty n<GOAL>IsNilpotent (M.charpolyRev.coeff 1)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<GOAL>∀ (f : α × β → ℝ≥0∞), Measurable f → ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>m : ∀ {α : Type ?u.194755} {β : Type ?u.194754} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)<GOAL>∀ (f : α × β → ℝ≥0∞), Measurable f → ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>m : ∀ {α : Type ?u.194755} {β : Type ?u.194754} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)<GOAL>∀ (c : ℝ≥0∞) ⦃s : Set (α × β)⦄, MeasurableSet s → (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (s.indicator fun x => c)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>m : ∀ {α : Type ?u.194755} {β : Type ?u.194754} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)<GOAL>∀ ⦃f g : α × β → ℝ≥0∞⦄, Disjoint (support f) (support g) → Measurable f → Measurable g → (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) f → (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) g → (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f + g)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SFinite ν<VAR>m : ∀ {α : Type ?u.194755} {β : Type ?u.194754} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)<GOAL>∀ ⦃f : ℕ → α × β → ℝ≥0∞⦄, (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) (f n)) → (fun f => ∫⁻ (z : α × β), f z ∂μ.prod ν = ∫⁻ (x : α), ∫⁻ (y : β), f (x, y) ∂ν ∂μ) fun x => ⨆ n, f n x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>φ ψ : MvPolynomial σ R<VAR>m n : M<VAR>w : σ → M<VAR>hφ : φ ≠ 0<VAR>hm : IsWeightedHomogeneous w φ m<VAR>hn : IsWeightedHomogeneous w φ n<GOAL>m = n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : AddCommMonoid M<VAR>φ ψ : MvPolynomial σ R<VAR>m n : M<VAR>w : σ → M<VAR>hφ : φ ≠ 0<VAR>hm : IsWeightedHomogeneous w φ m<VAR>hn : IsWeightedHomogeneous w φ n<VAR>d : σ →₀ ℕ<VAR>hd : coeff d φ ≠ 0<GOAL>m = n
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>m₁ : M i<VAR>m₂ : M j<VAR>w : Word M<GOAL>⟨i, m₁⟩ ∈ (of m₂ • w).toList ↔ ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨ m₁ ≠ 1 ∧ ∃ (hij : i = j), ⟨i, m₁⟩ ∈ w.toList.tail ∨ (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝³ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝² : Monoid N<VAR>inst✝¹ : (i : ι) → DecidableEq (M i)<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>m₁ : M i<VAR>m₂ : M j<VAR>w : Word M<GOAL>(⟨i, m₁⟩ ∈ w.toList.tail ∨ (i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m₁⟩) ∨ m₁ ≠ 1 ∧ ∃ (h : j = i), m₁ = h ▸ (let __src := (equivPair j) w; { head := m₂ * if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1, tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔ ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨ m₁ ≠ 1 ∧ ∃ (hij : i = j), ⟨i, m₁⟩ ∈ w.toList.tail ∨ (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>f✝ f g : α → ℚ → ℝ<VAR>a : α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>hf : p a → IsRatStieltjesPoint f a<VAR>hg : ¬p a → IsRatStieltjesPoint g a<VAR>h : p a<GOAL>Monotone (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>f✝ f g : α → ℚ → ℝ<VAR>a : α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>hf : p a → IsRatStieltjesPoint f a<VAR>hg : ¬p a → IsRatStieltjesPoint g a<VAR>h : ¬p a<GOAL>Monotone (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>f✝ f g : α → ℚ → ℝ<VAR>a : α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>hf : p a → IsRatStieltjesPoint f a<VAR>hg : ¬p a → IsRatStieltjesPoint g a<VAR>h : p a<GOAL>Tendsto (f a) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>f✝ f g : α → ℚ → ℝ<VAR>a : α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>hf : p a → IsRatStieltjesPoint f a<VAR>hg : ¬p a → IsRatStieltjesPoint g a<VAR>h : ¬p a<GOAL>Tendsto (g a) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>f✝ f g : α → ℚ → ℝ<VAR>a : α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>hf : p a → IsRatStieltjesPoint f a<VAR>hg : ¬p a → IsRatStieltjesPoint g a<VAR>h : p a<GOAL>Tendsto (f a) atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>f✝ f g : α → ℚ → ℝ<VAR>a : α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>hf : p a → IsRatStieltjesPoint f a<VAR>hg : ¬p a → IsRatStieltjesPoint g a<VAR>h : ¬p a<GOAL>Tendsto (g a) atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>f✝ f g : α → ℚ → ℝ<VAR>a : α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>hf : p a → IsRatStieltjesPoint f a<VAR>hg : ¬p a → IsRatStieltjesPoint g a<VAR>h : p a<GOAL>∀ (t : ℚ), ⨅ r, f a ↑r = f a t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : MeasurableSpace α<VAR>f✝ f g : α → ℚ → ℝ<VAR>a : α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>hf : p a → IsRatStieltjesPoint f a<VAR>hg : ¬p a → IsRatStieltjesPoint g a<VAR>h : ¬p a<GOAL>∀ (t : ℚ), ⨅ r, g a ↑r = g a t
<VAR>x y : ℝ<GOAL>↑(sin (x + y)) = ↑(sin x * cos y + cos x * sin y)
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝⁵ : DecidableEq α<VAR>M : α → Type u_3<VAR>P : α → Type u_4<VAR>inst✝⁴ : (a : α) → Zero (N a)<VAR>inst✝³ : (a : α) → Zero (M a)<VAR>inst✝² : (a : α) → Zero (P a)<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → DecidableEq (M a)<VAR>f g : Π₀ (a : α), N a<VAR>F : (a : α) → N a → M a<VAR>F0 : ∀ (a : α), F a 0 = 0<VAR>a : α<GOAL>a ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) → a ∈ f.neLocus g
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<VAR>h : f.lim = 0<GOAL>f.LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<VAR>h : f.lim = 0<VAR>hf : f ≈ const abv f.lim<GOAL>f.LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<VAR>h : f.lim = 0<VAR>hf : f ≈ const abv 0<GOAL>f.LimZero
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<VAR>h : f.LimZero<GOAL>f.lim = 0
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<VAR>h : f.LimZero<VAR>h₁ : f = f - const abv 0<GOAL>f.lim = 0
<VAR>α : Type u_1<VAR>inst✝³ : LinearOrderedField α<VAR>β : Type u_2<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>inst✝ : IsComplete β abv<VAR>f : CauSeq β abv<VAR>h : (f - const abv 0).LimZero<VAR>h₁ : f = f - const abv 0<GOAL>f.lim = 0
<VAR>a b : ℝ<VAR>n : ℕ<VAR>c : ℂ<VAR>hc : c ≠ 0<GOAL>∫ (x : ℝ) in a..b, Complex.exp (c * ↑x) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>c : ℂ<VAR>hc : c ≠ 0<VAR>D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x<GOAL>∫ (x : ℝ) in a..b, Complex.exp (c * ↑x) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>c : ℂ<VAR>hc : c ≠ 0<VAR>D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x<GOAL>Complex.exp (c * ↑b) / c - Complex.exp (c * ↑a) / c = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
<VAR>a b : ℝ<VAR>n : ℕ<VAR>c : ℂ<VAR>hc : c ≠ 0<VAR>D : ∀ (x : ℝ), HasDerivAt (fun y => Complex.exp (c * ↑y) / c) (Complex.exp (c * ↑x)) x<GOAL>ContinuousOn (fun x => Complex.exp (c * ↑x)) [[a, b]]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<GOAL>∫ (x : γ) in u, κ.densityProcess ν n a x s ∂ν a = ((κ a) (u ×ˢ s)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>hν : IsFiniteKernel ν<VAR>n : ℕ<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>u : Set γ<VAR>hu : u ∈ countablePartition γ n<VAR>this : IsFiniteKernel κ<GOAL>∫ (x : γ) in u, κ.densityProcess ν n a x s ∂ν a = ((κ a) (u ×ˢ s)).toReal