ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>(ascPochhammer ℕ (k + 1)).smeval (r + 1) = (k + 1).factorial • multichoose (r + 1) k + (ascPochhammer ℕ (k + 1)).smeval r
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>((X + ↑k) * ascPochhammer ℕ k).smeval (r + 1) = (k + 1).factorial • multichoose (r + 1) k + (X * (ascPochhammer ℕ k).comp (X + 1)).smeval r
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>((r + 1) ^ 1 + (↑k).smeval (r + 1)) * (ascPochhammer ℕ k).smeval (r + 1) = (k + 1).factorial • multichoose (r + 1) k + r ^ 1 * (ascPochhammer ℕ k).smeval (r ^ 1 + smeval 1 r)
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>((r + 1) ^ 1 + (↑k).smeval (r + 1)) * (ascPochhammer ℕ k).smeval (r + 1) = k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r ^ 1 * (ascPochhammer ℕ k).smeval (r ^ 1 + smeval 1 r)
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>(r + 1 + (↑k).smeval (r + 1)) * (ascPochhammer ℕ k).smeval (r + 1) = k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>r * (ascPochhammer ℕ k).smeval (r + 1) + (↑↑k * (ascPochhammer ℕ k).smeval (r + 1) + 1 * (ascPochhammer ℕ k).smeval (r + 1)) = k.succ • (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)
<VAR>R✝ : Type u_1<VAR>inst✝⁶ : AddCommMonoid R✝<VAR>inst✝⁵ : Pow R✝ ℕ<VAR>inst✝⁴ : BinomialRing R✝<VAR>R : Type u_2<VAR>inst✝³ : NonAssocSemiring R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : NatPowAssoc R<VAR>inst✝ : BinomialRing R<VAR>r : R<VAR>k : ℕ<GOAL>↑k • (ascPochhammer ℕ k).smeval (r + 1) + (1 * (ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1)) = k • (ascPochhammer ℕ k).smeval (r + 1) + ((ascPochhammer ℕ k).smeval (r + 1) + r * (ascPochhammer ℕ k).smeval (r + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>m : Set (Measure α)<VAR>h : μ ∈ m<VAR>this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(sInf m) s ≤ μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>m : Set (Measure α)<VAR>h : μ ∈ m<VAR>this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(sInf (toOuterMeasure '' m)) s ≤ μ s
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>f g : M[ι]<GOAL>(f * g).toDirectSum = f.toDirectSum * g.toDirectSum
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>f g : M[ι]<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<GOAL>(f * g).toDirectSum = f.toDirectSum * g.toDirectSum
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<VAR>x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring<GOAL>∀ (f g : M[ι]), to_hom (f * g) = to_hom f * to_hom g
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<VAR>x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring<GOAL>AddMonoidHom.mul.compr₂ to_hom = (AddMonoidHom.mul.comp to_hom).compl₂ to_hom
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<VAR>x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring<VAR>xi : ι<VAR>xv : M<GOAL>((AddMonoidHom.mul.compr₂ to_hom).comp (Finsupp.singleAddHom xi)) xv = (((AddMonoidHom.mul.comp to_hom).compl₂ to_hom).comp (Finsupp.singleAddHom xi)) xv
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<VAR>x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring<VAR>xi : ι<VAR>xv : M<VAR>yi : ι<VAR>yv : M<GOAL>((((AddMonoidHom.mul.compr₂ to_hom).comp (Finsupp.singleAddHom xi)) xv).comp (Finsupp.singleAddHom yi)) yv = (((((AddMonoidHom.mul.comp to_hom).compl₂ to_hom).comp (Finsupp.singleAddHom xi)) xv).comp (Finsupp.singleAddHom yi)) yv
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<VAR>x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring<VAR>xi : ι<VAR>xv : M<VAR>yi : ι<VAR>yv : M<GOAL>((AddMonoidHom.mul.compr₂ to_hom) (Finsupp.single xi xv)) (Finsupp.single yi yv) = (((AddMonoidHom.mul.comp to_hom).compl₂ to_hom) (Finsupp.single xi xv)) (Finsupp.single yi yv)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<VAR>x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring<VAR>xi : ι<VAR>xv : M<VAR>yi : ι<VAR>yv : M<GOAL>((AddMonoidHom.mul.compr₂ to_hom) (Finsupp.single xi xv)) (Finsupp.single yi yv) = ((AddMonoidHom.mul.comp to_hom) (Finsupp.single xi xv)) (to_hom (Finsupp.single yi yv))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<VAR>x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring<VAR>xi : ι<VAR>xv : M<VAR>yi : ι<VAR>yv : M<GOAL>{ toFun := ⇑to_hom ∘ ⇑(AddMonoidHom.mul (Finsupp.single xi xv)), map_zero' := ⋯ } (Finsupp.single yi yv) = ((AddMonoidHom.mul.comp to_hom) (Finsupp.single xi xv)) (to_hom (Finsupp.single yi yv))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<VAR>x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring<VAR>xi : ι<VAR>xv : M<VAR>yi : ι<VAR>yv : M<GOAL>(⇑to_hom ∘ ⇑(AddMonoidHom.mul (Finsupp.single xi xv))) (Finsupp.single yi yv) = ((AddMonoidHom.mul.comp to_hom) (Finsupp.single xi xv)) (to_hom (Finsupp.single yi yv))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<VAR>x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring<VAR>xi : ι<VAR>xv : M<VAR>yi : ι<VAR>yv : M<GOAL>to_hom (Finsupp.single xi xv * Finsupp.single yi yv) = to_hom (Finsupp.single xi xv) * to_hom (Finsupp.single yi yv)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<VAR>x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring<VAR>xi : ι<VAR>xv : M<VAR>yi : ι<VAR>yv : M<GOAL>(DirectSum.of (fun i => M) (xi + yi)) (xv * yv) = toDirectSum (Finsupp.single xi xv) * toDirectSum (Finsupp.single yi yv)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>A : Type u_4<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : Semiring M<VAR>to_hom : M[ι] →+ ⨁ (x : ι), M := { toFun := toDirectSum, map_zero' := ⋯, map_add' := ⋯ }<VAR>x✝ : NonUnitalNonAssocSemiring (ι →₀ M) := nonUnitalNonAssocSemiring<VAR>xi : ι<VAR>xv : M<VAR>yi : ι<VAR>yv : M<GOAL>(DirectSum.of (fun i => M) (xi + yi)) (xv * yv) = (DirectSum.of (fun i => M) xi) xv * (DirectSum.of (fun i => M) yi) yv
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>hv : LinearIndependent R v<VAR>i : ι<VAR>x : ↥(span R (range v))<VAR>hx : ↑x = v i<GOAL>hv.repr x = Finsupp.single i 1
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>hv : LinearIndependent R v<VAR>i : ι<VAR>x : ↥(span R (range v))<VAR>hx : ↑x = v i<GOAL>(Finsupp.total ι M R v) (Finsupp.single i 1) = ↑x
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>φ : L.BoundedFormula α n✝<VAR>tf : α → L.Term β<VAR>v : β → M<VAR>xs : Fin n✝ → M<VAR>n : ℕ<VAR>t : L.Term (α ⊕ Fin n)<VAR>x : Fin n → M<GOAL>realize (Sum.elim v x) (t.subst (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr))) = realize (Sum.elim (fun a => realize v (tf a)) x) t
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>φ : L.BoundedFormula α n✝<VAR>tf : α → L.Term β<VAR>v : β → M<VAR>xs : Fin n✝ → M<VAR>n : ℕ<VAR>t : L.Term (α ⊕ Fin n)<VAR>x : Fin n → M<GOAL>realize (fun a => realize (Sum.elim v x) (Sum.elim (Term.relabel Sum.inl ∘ tf) (var ∘ Sum.inr) a)) t = realize (Sum.elim (fun a => realize v (tf a)) x) t
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : AddCommGroup N<VAR>inst✝¹⁰ : AddCommGroup P<VAR>inst✝⁹ : AddCommGroup Q<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : Module R Q<VAR>inst✝⁴ : Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Free R N<VAR>inst✝¹ : Module.Finite R N<VAR>inst✝ : Nontrivial R<VAR>x : (M →ₗ[R] P) ⊗[R] Q<GOAL>(rTensorHomEquivHomRTensor R M P Q) x = (rTensorHomToHomRTensor R M P Q) x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : HasExt C<VAR>X Y Z✝ T : C<VAR>n : ℕ<VAR>α : Ext X Y n<VAR>Z : C<VAR>m p : ℕ<VAR>h : n + m = p<VAR>this : HasDerivedCategory C := HasDerivedCategory.standard C<GOAL>(α.comp 0 h).hom = hom 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : MulOneClass M<VAR>inst✝ : ContinuousMul M<VAR>U : Set M<VAR>hU : U ∈ 𝓝 1<GOAL>∃ V, IsOpen V ∧ 1 ∈ V ∧ V * V ⊆ U
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁷ : DecidableEq n✝<VAR>inst✝⁶ : Fintype n✝<VAR>inst✝⁵ : DecidableEq m<VAR>inst✝⁴ : Fintype m<VAR>R : Type v<VAR>inst✝³ : CommRing R<VAR>n : Type u_3<VAR>inst✝² : Unique n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>A : Matrix n n R<GOAL>A.det = A default default
<VAR>α β : Type u<VAR>n : ℕ<VAR>a : Cardinal.{u}<GOAL>↑n = lift.{v, u} a ↔ ↑n = a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<VAR>n : ℕ<GOAL>f.reverse.coeff n = f.coeff ((revAt f.natDegree) n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : LocallyFiniteOrderBot α<VAR>b : α<GOAL>Iic b = cons b (Iio b) ⋯
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<GOAL>p ∈ lifts f ↔ ∃ q, map f q = p
<VAR>T : Type u₁<VAR>inst✝ : Category.{v₁, u₁} T<VAR>X✝ X : T<VAR>U V : Over X<VAR>f g : U ⟶ V<VAR>left✝¹ : U.left ⟶ V.left<VAR>b : U.right ⟶ V.right<VAR>w✝¹ : (𝟭 T).map left✝¹ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map b<VAR>left✝ : U.left ⟶ V.left<VAR>e : U.right ⟶ V.right<VAR>w✝ : (𝟭 T).map left✝ ≫ V.hom = U.hom ≫ (Functor.fromPUnit X).map e<VAR>h : { left := left✝¹, right := b, w := w✝¹ }.left = { left := left✝, right := e, w := w✝ }.left<GOAL>b = e
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Monoid M<VAR>inst✝¹ : NonUnitalNonAssocRing R<VAR>inst✝ : DistribMulAction M R<VAR>k : M<VAR>h : ∀ (x : R), k • x = 0 → x = 0<VAR>a b : R<VAR>h' : k • a = k • b<GOAL>a = b
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Monoid M<VAR>inst✝¹ : NonUnitalNonAssocRing R<VAR>inst✝ : DistribMulAction M R<VAR>k : M<VAR>h : ∀ (x : R), k • x = 0 → x = 0<VAR>a b : R<VAR>h' : k • a = k • b<GOAL>a - b = 0
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>inst✝² : Monoid M<VAR>inst✝¹ : NonUnitalNonAssocRing R<VAR>inst✝ : DistribMulAction M R<VAR>k : M<VAR>h : ∀ (x : R), k • x = 0 → x = 0<VAR>a b : R<VAR>h' : k • a = k • b<GOAL>k • (a - b) = 0
<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>A : Matrix n n R[X]<VAR>M : Matrix n n R<GOAL>eval 0 (A + X • M.map ⇑C).det = eval 0 A.det
<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>A : Matrix n n R[X]<VAR>M : Matrix n n R<GOAL>(eval 0 (matPolyEquiv A) + eval 0 (matPolyEquiv ((algebraMap R[X] (Matrix n n R[X])) X) * matPolyEquiv (M.map ⇑C))).det = (eval 0 (matPolyEquiv A)).det
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝⁴ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝³ : TopologicalSpace 𝕜<VAR>inst✝² : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝¹ : Archimedean 𝕜<VAR>x✝ : AddCircle p<VAR>hx✝ : x✝ ≠ ↑a<VAR>inst✝ : DiscreteTopology ↥(zmultiples p)<VAR>x : 𝕜<VAR>hx : x ∈ Ioo a (a + p)<VAR>hx' : ↑x ∈ {↑a}<GOAL>False
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝⁴ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝³ : TopologicalSpace 𝕜<VAR>inst✝² : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝¹ : Archimedean 𝕜<VAR>x✝ : AddCircle p<VAR>hx✝ : x✝ ≠ ↑a<VAR>inst✝ : DiscreteTopology ↥(zmultiples p)<VAR>x : AddCircle p<VAR>hx : x ∈ {↑a}ᶜ<GOAL>(fun x => ↑((equivIco p a) x)) x ∈ Ioo a (a + p)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>inst✝⁴ : LinearOrderedAddCommGroup 𝕜<VAR>inst✝³ : TopologicalSpace 𝕜<VAR>inst✝² : OrderTopology 𝕜<VAR>p : 𝕜<VAR>hp : Fact (0 < p)<VAR>a : 𝕜<VAR>inst✝¹ : Archimedean 𝕜<VAR>x : AddCircle p<VAR>hx : x ≠ ↑a<VAR>inst✝ : DiscreteTopology ↥(zmultiples p)<GOAL>ContinuousOn { toFun := QuotientAddGroup.mk, invFun := fun x => ↑((equivIco p a) x), source := Ioo a (a + p), target := {↑a}ᶜ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.invFun { toFun := QuotientAddGroup.mk, invFun := fun x => ↑((equivIco p a) x), source := Ioo a (a + p), target := {↑a}ᶜ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }.target
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α✝<VAR>μ✝ μ₁ μ₂ : Measure α✝<VAR>s s₁ s₂ t : Set α✝<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) (Accumulate f)<GOAL>μ (⋃ i, f i) = ⨆ i, μ (Accumulate f i)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α✝<VAR>μ✝ μ₁ μ₂ : Measure α✝<VAR>s s₁ s₂ t : Set α✝<VAR>α : Type u_8<VAR>ι : Type u_9<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : Countable ι<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>f : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) (Accumulate f)<GOAL>μ (⋃ x, Accumulate f x) = ⨆ i, μ (Accumulate f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a✝ b✝ c : α<VAR>inst✝ : DecidableEq α<VAR>a b : α<GOAL>(Icc a b).erase b = Ico a b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>hn : 0 < n<GOAL>1 ∈ nthRootsFinset n R
<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>i : Set α<VAR>s t : (a : α) → Set (π a)<GOAL>i.pi s \ i.pi t ⊆ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a)
<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>i : Set α<VAR>s t : (a : α) → Set (π a)<VAR>x : (i : α) → π i<VAR>hx : x ∈ i.pi s \ ⋃ a ∈ i, eval a ⁻¹' (s a \ t a)<VAR>a : α<VAR>ha : a ∈ i<GOAL>x a ∈ t a
<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>i : Set α<VAR>s t : (a : α) → Set (π a)<VAR>x : (i : α) → π i<VAR>a : α<VAR>ha : a ∈ i<VAR>hx : (∀ i_1 ∈ i, x i_1 ∈ s i_1) ∧ ∀ x_1 ∈ i, eval x_1 x ∈ s x_1 → eval x_1 x ∈ t x_1<GOAL>x a ∈ t a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ✝ ν✝ ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>inst✝ : SigmaFinite ν<GOAL>(sum fun n => μ.restrict (disjointed (spanningSets ν) n)) = μ
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : Preadditive C<VAR>D : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} D<VAR>inst✝² : Preadditive D<VAR>inst✝¹ : HasFiniteBiproducts D<VAR>F : Mat_ C ⥤ D<VAR>inst✝ : F.Additive<VAR>M N : Mat_ C<VAR>f : M ⟶ N<GOAL>(additiveObjIsoBiproduct F M).inv ≫ F.map f = (biproduct.matrix fun i j => F.map ((embedding C).map (f i j))) ≫ (additiveObjIsoBiproduct F N).inv
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>α : Type u_1<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<GOAL>comap (Prod.map f f) (𝓤 β) = 𝓟 idRel
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>α : Type u_1<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<GOAL>comap (Prod.map f f) (𝓤 β) ≤ 𝓟 idRel
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>α : Type u_1<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<GOAL>Prod.map f f ⁻¹' s ⊆ idRel
<VAR>α✝ : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>α : Type u_1<VAR>f : α → β<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>hf : Pairwise fun x y => (f x, f y) ∉ s<VAR>x y : α<GOAL>(x, y) ∈ Prod.map f f ⁻¹' s → (x, y) ∈ idRel
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>p : ℕ<VAR>φ : MvPolynomial σ R<GOAL>(rename f) ((expand p) φ) = (expand p) ((rename f) φ)
<VAR>a b c d✝ m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n d : ℕ<VAR>h : n / d * d = n<GOAL>d ∣ n / d * d
<VAR>a b n : ℕ<VAR>hn : n ≠ 0<GOAL>a ∣ b ^ n ↔ n.ceilRoot a ∣ b
<VAR>b n : ℕ<VAR>hn : n ≠ 0<GOAL>0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b
<VAR>a b n : ℕ<VAR>hn : n ≠ 0<VAR>ha : a ≠ 0<GOAL>a ∣ b ^ n ↔ n.ceilRoot a ∣ b
<VAR>a n : ℕ<VAR>hn : n ≠ 0<VAR>ha : a ≠ 0<GOAL>a ∣ 0 ^ n ↔ n.ceilRoot a ∣ 0
<VAR>a b n : ℕ<VAR>hn : n ≠ 0<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>a ∣ b ^ n ↔ n.ceilRoot a ∣ b
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>arccos x = arctan (√(1 - x ^ 2) / x)
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>arctan (√(1 - x ^ 2) / x) = π / 2 - arcsin x
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>tan (π / 2 - arcsin x) = √(1 - x ^ 2) / x
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>-(π / 2) < π / 2 - arcsin x
<VAR>x : ℝ<VAR>h : 0 < x<GOAL>π / 2 - arcsin x < π / 2
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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<GOAL>engel R 0 = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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<GOAL>⊤ ≤ engel R 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>x : L<GOAL>x ∈ engel R 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>x : L<GOAL>∃ n, (0 ^ n) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>x : L<GOAL>(0 ^ 1) x = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>hg : S.g = 0<VAR>c : CokernelCofork S.f<VAR>hc : IsColimit c<GOAL>(ofIsColimitCokernelCofork S hg c hc).g' = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f g : α → β<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<GOAL>∫⁻ (a : α), edist (f a) (0 a) ∂μ < ⊤ ∧ ∫⁻ (a : α), edist (g a) (0 a) ∂μ < ⊤