ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n✝ : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>n : ℕ∞<VAR>m : ℕ<VAR>h : ContDiffOn 𝕜 n f s<VAR>hmn : ↑m ≤ n<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContinuousOn (iteratedDerivWithin m f s) s
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x<VAR>h : LiftPropWithinAt P g s x<VAR>hts : t ⊆ s<GOAL>LiftPropWithinAt P g t x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>mono : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, t ⊆ s → P f s x → P f t x<VAR>h : LiftPropWithinAt P g s x<VAR>hts : t ⊆ s<VAR>y : H<VAR>hy : y ∈ ↑(chartAt H x).symm ⁻¹' t<GOAL>y ∈ ↑(chartAt H x).symm ⁻¹' s
<VAR>a b : ℝ<VAR>n : ℕ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
<VAR>R : Type u_1<VAR>A : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : TopologicalSpace A<VAR>inst✝ : ContinuousSMul R A<GOAL>Continuous ⇑(algebraMap R A)
<VAR>R : Type u_1<VAR>A : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : TopologicalSpace A<VAR>inst✝ : ContinuousSMul R A<GOAL>Continuous fun r => r • 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<VAR>i : α<VAR>inst✝ : DecidableEq α<GOAL>(f.update a 0).support = f.support.erase a
<VAR>l : Filter ℂ<VAR>hl : IsExpCmpFilter l<VAR>a : ℂ<VAR>b : ℝ<VAR>hb : b < 0<GOAL>(fun z => cexp (↑b * z)) =o[l] fun z => z ^ a
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>G₂ : Type u_2<VAR>inst✝² : Group G₂<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ : Subgroup G<VAR>H₂ : Subgroup G₂<VAR>inst✝¹ : Finite ↥H₁<VAR>inst✝ : Finite ↥H₂<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<GOAL>(Nat.card ↥H₁).Coprime (Nat.card ↥H₂)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>G₂ : Type u_2<VAR>inst✝² : Group G₂<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ : Subgroup G<VAR>H₂ : Subgroup G₂<VAR>inst✝¹ : Finite ↥H₁<VAR>inst✝ : Finite ↥H₂<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<VAR>n₁ : ℕ<VAR>heq₁ : Nat.card ↥H₁ = p₁ ^ n₁<GOAL>(Nat.card ↥H₁).Coprime (Nat.card ↥H₂)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>G₂ : Type u_2<VAR>inst✝² : Group G₂<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ : Subgroup G<VAR>H₂ : Subgroup G₂<VAR>inst✝¹ : Finite ↥H₁<VAR>inst✝ : Finite ↥H₂<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<VAR>n₁ : ℕ<GOAL>(p₁ ^ n₁).Coprime (Nat.card ↥H₂)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>G₂ : Type u_2<VAR>inst✝² : Group G₂<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ : Subgroup G<VAR>H₂ : Subgroup G₂<VAR>inst✝¹ : Finite ↥H₁<VAR>inst✝ : Finite ↥H₂<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<VAR>n₁ n₂ : ℕ<VAR>heq₂ : Nat.card ↥H₂ = p₂ ^ n₂<GOAL>(p₁ ^ n₁).Coprime (Nat.card ↥H₂)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>G₂ : Type u_2<VAR>inst✝² : Group G₂<VAR>p₁ p₂ : ℕ<VAR>hp₁ : Fact (Nat.Prime p₁)<VAR>hp₂ : Fact (Nat.Prime p₂)<VAR>hne : p₁ ≠ p₂<VAR>H₁ : Subgroup G<VAR>H₂ : Subgroup G₂<VAR>inst✝¹ : Finite ↥H₁<VAR>inst✝ : Finite ↥H₂<VAR>hH₁ : IsPGroup p₁ ↥H₁<VAR>hH₂ : IsPGroup p₂ ↥H₂<VAR>n₁ n₂ : ℕ<GOAL>(p₁ ^ n₁).Coprime (p₂ ^ n₂)
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>a b x y z x' y' : α<VAR>h : IsCompl x y<VAR>h' : IsCompl x' y'<GOAL>(x ⊔ x') ⊓ (y ⊓ y') = ⊥
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>a b x y z x' y' : α<VAR>h : IsCompl x y<VAR>h' : IsCompl x' y'<GOAL>x ⊔ x' ⊔ y ⊓ y' = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<GOAL>s \ t =ᶠ[ae μ] s ↔ μ (s ∩ t) = 0
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>a : α<VAR>ha : a ∉ s<GOAL>s ⋖ cons a s ha
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : AddCommGroup G<VAR>inst✝⁶ : μ.IsAddLeftInvariant<VAR>inst✝⁵ : μ.IsNegInvariant<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalAddGroup G<VAR>inst✝² : BorelSpace G<VAR>inst✝¹ : FirstCountableTopology G<VAR>inst✝ : SecondCountableTopologyEither G E<VAR>hbf : BddAbove (range fun x => ‖f x‖)<VAR>hf : Continuous f<VAR>hg : Integrable g μ<GOAL>Continuous (f ⋆[L, μ] g)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : NormedAddCommGroup E'<VAR>inst✝¹⁶ : NormedAddCommGroup E''<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>inst✝¹² : NormedSpace 𝕜 E'<VAR>inst✝¹¹ : NormedSpace 𝕜 E''<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁹ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : AddCommGroup G<VAR>inst✝⁶ : μ.IsAddLeftInvariant<VAR>inst✝⁵ : μ.IsNegInvariant<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : TopologicalAddGroup G<VAR>inst✝² : BorelSpace G<VAR>inst✝¹ : FirstCountableTopology G<VAR>inst✝ : SecondCountableTopologyEither G E<VAR>hbf : BddAbove (range fun x => ‖f x‖)<VAR>hf : Continuous f<VAR>hg : Integrable g μ<GOAL>Continuous (g ⋆[L.flip, μ] f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α ≃ₜ β<GOAL>(map (⇑f) μ).Regular ↔ μ.Regular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α ≃ₜ β<VAR>h : (map (⇑f) μ).Regular<GOAL>μ.Regular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α ≃ₜ β<VAR>h : (map (⇑f) μ).Regular<GOAL>μ = map (⇑f.symm) (map (⇑f) μ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : BorelSpace β<VAR>f : α ≃ₜ β<VAR>h : (map (⇑f) μ).Regular<GOAL>μ = map (⇑f.symm ∘ ⇑f) μ
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X : C<VAR>f : J → C<VAR>j : J<GOAL>(leftDistributor X f).inv ≫ X ◁ biproduct.π f j = biproduct.π (fun j => X ⊗ f j) j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : Countable ι<VAR>t : ι → TopologicalSpace α<VAR>ht₀ : ∃ t₀, T2Space α ∧ ∀ (i : ι), t i ≤ t₀<VAR>u : ι → UniformSpace α<VAR>hcomp : ∀ (i : ι), CompleteSpace α<VAR>hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated<VAR>hut : ∀ (i : ι), UniformSpace.toTopologicalSpace = t i<GOAL>∃ u, CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ UniformSpace.toTopologicalSpace = ⨅ i, t i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : Countable ι<VAR>u : ι → UniformSpace α<VAR>hcomp : ∀ (i : ι), CompleteSpace α<VAR>hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated<VAR>ht₀ : ∃ t₀, T2Space α ∧ ∀ (i : ι), (fun i => UniformSpace.toTopologicalSpace) i ≤ t₀<VAR>hut : ∀ (i : ι), UniformSpace.toTopologicalSpace = (fun i => UniformSpace.toTopologicalSpace) i<GOAL>∃ u_1, CompleteSpace α ∧ (𝓤 α).IsCountablyGenerated ∧ UniformSpace.toTopologicalSpace = ⨅ i, (fun i => UniformSpace.toTopologicalSpace) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : Countable ι<VAR>u : ι → UniformSpace α<VAR>hcomp : ∀ (i : ι), CompleteSpace α<VAR>hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated<VAR>ht₀ : ∃ t₀, T2Space α ∧ ∀ (i : ι), (fun i => UniformSpace.toTopologicalSpace) i ≤ t₀<VAR>hut : ∀ (i : ι), UniformSpace.toTopologicalSpace = (fun i => UniformSpace.toTopologicalSpace) i<GOAL>(𝓤 α).IsCountablyGenerated
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : Countable ι<VAR>u : ι → UniformSpace α<VAR>hcomp : ∀ (i : ι), CompleteSpace α<VAR>hcount : ∀ (i : ι), (𝓤 α).IsCountablyGenerated<VAR>ht₀ : ∃ t₀, T2Space α ∧ ∀ (i : ι), (fun i => UniformSpace.toTopologicalSpace) i ≤ t₀<VAR>hut : ∀ (i : ι), UniformSpace.toTopologicalSpace = (fun i => UniformSpace.toTopologicalSpace) i<GOAL>(⨅ i, 𝓤 α).IsCountablyGenerated
<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>X₁ X₂ X₃ X₄ : GradedObject I C<VAR>inst✝²² : X₁.HasTensor X₂<VAR>inst✝²¹ : X₂.HasTensor X₃<VAR>inst✝²⁰ : X₃.HasTensor X₄<VAR>inst✝¹⁹ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝¹⁸ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>inst✝¹⁷ : (tensorObj X₂ X₃).HasTensor X₄<VAR>inst✝¹⁶ : X₂.HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹⁵ : (tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄<VAR>inst✝¹⁴ : (tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄<VAR>inst✝¹³ : X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)<VAR>inst✝¹² : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))<VAR>inst✝¹¹ : (tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹⁰ : X₁.HasGoodTensor₁₂Tensor X₂ X₃<VAR>inst✝⁹ : X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>inst✝⁸ : X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄<VAR>inst✝⁷ : X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄<VAR>inst✝⁶ : X₂.HasGoodTensor₁₂Tensor X₃ X₄<VAR>inst✝⁵ : X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>inst✝⁴ : (tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄<VAR>inst✝³ : (tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄<VAR>inst✝² : X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)<VAR>inst✝¹ : X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)<VAR>inst✝ : X₁.HasTensor₄ObjExt X₂ X₃ X₄<VAR>j i₁ i₂ i₃ i₄ : I<VAR>h : i₁ + i₂ + i₃ + i₄ = j<GOAL>ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ tensorHom (𝟙 X₁) (associator X₂ X₃ X₄).inv j ≫ (associator X₁ (tensorObj X₂ X₃) X₄).inv j ≫ tensorHom (associator X₁ X₂ X₃).inv (𝟙 X₄) j = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ (associator X₁ X₂ (tensorObj X₃ X₄)).inv j ≫ (associator (tensorObj X₁ X₂) X₃ X₄).inv j
<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>X₁ X₂ X₃ X₄ : GradedObject I C<VAR>inst✝²² : X₁.HasTensor X₂<VAR>inst✝²¹ : X₂.HasTensor X₃<VAR>inst✝²⁰ : X₃.HasTensor X₄<VAR>inst✝¹⁹ : (tensorObj X₁ X₂).HasTensor X₃<VAR>inst✝¹⁸ : X₁.HasTensor (tensorObj X₂ X₃)<VAR>inst✝¹⁷ : (tensorObj X₂ X₃).HasTensor X₄<VAR>inst✝¹⁶ : X₂.HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹⁵ : (tensorObj (tensorObj X₁ X₂) X₃).HasTensor X₄<VAR>inst✝¹⁴ : (tensorObj X₁ (tensorObj X₂ X₃)).HasTensor X₄<VAR>inst✝¹³ : X₁.HasTensor (tensorObj (tensorObj X₂ X₃) X₄)<VAR>inst✝¹² : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))<VAR>inst✝¹¹ : (tensorObj X₁ X₂).HasTensor (tensorObj X₃ X₄)<VAR>inst✝¹⁰ : X₁.HasGoodTensor₁₂Tensor X₂ X₃<VAR>inst✝⁹ : X₁.HasGoodTensorTensor₂₃ X₂ X₃<VAR>inst✝⁸ : X₁.HasGoodTensor₁₂Tensor (tensorObj X₂ X₃) X₄<VAR>inst✝⁷ : X₁.HasGoodTensorTensor₂₃ (tensorObj X₂ X₃) X₄<VAR>inst✝⁶ : X₂.HasGoodTensor₁₂Tensor X₃ X₄<VAR>inst✝⁵ : X₂.HasGoodTensorTensor₂₃ X₃ X₄<VAR>inst✝⁴ : (tensorObj X₁ X₂).HasGoodTensor₁₂Tensor X₃ X₄<VAR>inst✝³ : (tensorObj X₁ X₂).HasGoodTensorTensor₂₃ X₃ X₄<VAR>inst✝² : X₁.HasGoodTensor₁₂Tensor X₂ (tensorObj X₃ X₄)<VAR>inst✝¹ : X₁.HasGoodTensorTensor₂₃ X₂ (tensorObj X₃ X₄)<VAR>inst✝ : X₁.HasTensor₄ObjExt X₂ X₃ X₄<VAR>j i₁ i₂ i₃ i₄ : I<VAR>h : i₁ + i₂ + i₃ + i₄ = j<GOAL>(α_ (X₁ i₁) (X₂ i₂) (X₃ i₃ ⊗ X₄ i₄)).inv ≫ (α_ (X₁ i₁ ⊗ X₂ i₂) (X₃ i₃) (X₄ i₄)).inv ≫ ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ (i₁ + i₂ + i₃) ⋯ ▷ X₄ i₄ ≫ ιTensorObj (tensorObj (tensorObj X₁ X₂) X₃) X₄ (i₁ + i₂ + i₃) i₄ j ⋯ = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ (associator X₁ X₂ (tensorObj X₃ X₄)).inv j ≫ (associator (tensorObj X₁ X₂) X₃ X₄).inv j
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝³ : MonoidWithZero R<VAR>inst✝² : MonoidWithZero S<VAR>r : R<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : MonoidWithZeroHomClass F R S<VAR>f : F<VAR>hf : Injective ⇑f<VAR>x✝ : IsNilpotent (f r)<VAR>k : ℕ<VAR>hk : f r ^ k = 0<GOAL>f (r ^ k) = 0
<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>s : (i : ι) → κ i → Set α<GOAL>(⋂ i, ⋂ j, s i j)ᶜ = ⋃ i, ⋃ j, (s i j)ᶜ
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>(eqToHom ⋯).app X ≫ (shiftFunctorAdd C 0 a).hom.app X = 𝟙 (((shiftMonoidalFunctor C A).obj { as := a }).obj X) ≫ ((shiftMonoidalFunctor C A).obj { as := a }).map ((shiftMonoidalFunctor C A).ε.app X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : HasShift C A<VAR>a : A<VAR>X : C<GOAL>eqToHom ⋯ ≫ (shiftFunctorAdd C 0 a).hom.app X = eqToHom ⋯ ≫ ((shiftMonoidalFunctor C A).μIso (𝟙_ (Discrete A)) { as := a }).inv.app X
<VAR>f✝ f : Ordinal.{u} → Ordinal.{u}<GOAL>(fun a => sup fun n => f^[n] a) = nfp f
<VAR>f✝ f : Ordinal.{u} → Ordinal.{u}<VAR>a : Ordinal.{u}<GOAL>(sup fun n => f^[n] a) ≤ nfp f a
<VAR>f✝ f : Ordinal.{u} → Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>l : List Unit<GOAL>List.foldr (fun x => f) a l ≤ sup fun n => f^[n] a
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b✝ : WithBot α<VAR>b : α<VAR>hb : b ≠ 0<GOAL>⊥ * ↑b = Option.bind ⊥ fun a => Option.some (a * b)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b✝ : WithBot α<VAR>b : α<VAR>hb : b ≠ 0<GOAL>⊥ = Option.bind ⊥ fun a => Option.some (a * b)
<VAR>q a b c : ℚ<VAR>x : ℤ<VAR>hx : x ≠ 0<VAR>n d : ℤ<VAR>hd : ¬d = 0<GOAL>n /. x * (x /. d) = n /. d
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a✝ : α<VAR>b✝ : β<VAR>h₀ : ∀ (b : β), Antitone (swap f b)<VAR>h₁ : ∀ (a : α), Monotone (f a)<VAR>a : α<VAR>ha : a ∈ lowerBounds s<VAR>b : β<VAR>hb : b ∈ upperBounds t<GOAL>BddAbove (image2 f s t)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.79019, u_1} C<VAR>X : PresheafedSpace C<GOAL>X.presheaf = (Presheaf.pushforward C (X.ofRestrict ⋯).base).obj (X.restrict ⋯).presheaf
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.79019, u_1} C<VAR>X : PresheafedSpace C<GOAL>X.presheaf = (Presheaf.pushforward C ((Opens.inclusionTopIso ↑X).inv ≫ (X.ofRestrict ⋯).base)).obj X.presheaf
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.79019, u_1} C<VAR>X : PresheafedSpace C<GOAL>X.presheaf = (Presheaf.pushforward C (𝟙 ↑X)).obj X.presheaf
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.79019, u_1} C<VAR>X : PresheafedSpace C<GOAL>X.presheaf = (𝟭 (Presheaf C ↑X)).obj X.presheaf
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X : PresheafedSpace C<VAR>U✝ : Opens ↑↑X<GOAL>X.presheaf.map (⋯.adjunction.counit.app U✝).op = (eqToHom ⋯).app (op U✝)
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>X : PresheafedSpace C<VAR>U✝ : Opens ↑↑X<GOAL>op U✝ = op (⋯.functor.obj ((Opens.map ⊤.inclusion).obj U✝))
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ✝ γ₁ γ₂ : Cochain K L n✝<VAR>n' a : ℤ<VAR>γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<VAR>p q : ℤ<VAR>hpq : p + n = q<VAR>p' : ℤ<VAR>hp' : p + n' = p'<GOAL>q = p' + a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n✝ : ℤ<VAR>γ✝ γ₁ γ₂ : Cochain K L n✝<VAR>n' a : ℤ<VAR>γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'<VAR>n : ℤ<VAR>hn : n' + a = n<VAR>p q : ℤ<VAR>hpq : p + n = q<GOAL>(mk fun p q hpq => γ.v p (p + n') ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') q ⋯).hom).v p q hpq = γ.v p (p + n') ⋯ ≫ (L.shiftFunctorObjXIso a (p + n') q ⋯).hom
<VAR>x y z : PartENat<VAR>hz : z ≠ ⊤<GOAL>z + x < z + y ↔ x < y
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<GOAL>Tendsto (fun n => ↑(numDerangements n) / ↑n.factorial) atTop (𝓝 (Real.exp (-1)))
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<GOAL>∀ (n : ℕ), ↑(numDerangements n) / ↑n.factorial = s (n + 1)
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<VAR>n : ℕ<GOAL>↑(numDerangements n) / ↑n.factorial = s (n + 1)
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<VAR>n : ℕ<GOAL>↑(∑ k ∈ Finset.range (n + 1), (-1) ^ k * ↑((k + 1).ascFactorial (n - k))) / ↑n.factorial = s (n + 1)
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<VAR>n : ℕ<GOAL>(∑ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n - x))) / ↑n.factorial = s (n + 1)
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<VAR>n : ℕ<GOAL>∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑((i + 1).ascFactorial (n - i)) / ↑n.factorial = s (n + 1)
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<VAR>n : ℕ<GOAL>∀ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n - x)) / ↑n.factorial = (-1) ^ x / ↑x.factorial
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<VAR>n k : ℕ<VAR>hk : k ∈ Finset.range (n + 1)<GOAL>(-1) ^ k * ↑((k + 1).ascFactorial (n - k)) / ↑n.factorial = (-1) ^ k / ↑k.factorial
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<VAR>n k : ℕ<VAR>hk : k ∈ Finset.range (n + 1)<VAR>h_le : k ≤ n<GOAL>(-1) ^ k * ↑((k + 1).ascFactorial (n - k)) / ↑n.factorial = (-1) ^ k / ↑k.factorial
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<VAR>n k : ℕ<VAR>hk : k ∈ Finset.range (n + 1)<VAR>h_le : k ≤ n<GOAL>(-1) ^ k * ↑(n.factorial / k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<VAR>n k : ℕ<VAR>hk : k ∈ Finset.range (n + 1)<VAR>h_le : k ≤ n<GOAL>(-1) ^ k * (↑n.factorial / ↑k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial
<VAR>s : ℕ → ℝ := fun n => ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial<VAR>n k : ℕ<VAR>hk : k ∈ Finset.range (n + 1)<VAR>h_le : k ≤ n<GOAL>(-1) ^ k * ↑n.factorial * ↑k.factorial = (-1) ^ k * (↑k.factorial * ↑n.factorial)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type ?u.10594<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<GOAL>IsSeparatedMap f ↔ ClosedEmbedding (toPullbackDiag f)
<VAR>X : Type u_1<VAR>Y : Sort u_2<VAR>A : Type ?u.10594<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<GOAL>IsClosed (Set.range (toPullbackDiag f)) ↔ ClosedEmbedding (toPullbackDiag f)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : Zero R<VAR>inst✝² : LinearOrder Γ<VAR>inst✝¹ : LocallyFiniteOrder Γ<VAR>inst✝ : Nonempty Γ<GOAL>BddBelow (Function.support 0)
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>p n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>f : R[X]<VAR>inst✝ : PerfectRing R p<GOAL>Multiset.map (⇑(frobenius R p)) ((expand R p) f).roots = p • f.roots
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : DecidableEq α<VAR>g₁ g₂ : α →₀ M<VAR>h : Disjoint g₁.support g₂.support<VAR>a : α<VAR>ha✝ : a ∈ g₁.support ∪ g₂.support<VAR>ha : a ∈ g₁.support<GOAL>a ∈ (g₁ + g₂).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : DecidableEq α<VAR>g₁ g₂ : α →₀ M<VAR>h : Disjoint g₁.support g₂.support<VAR>a : α<VAR>ha✝ : a ∈ g₁.support ∪ g₂.support<VAR>ha : a ∈ g₁.support<VAR>this : a ∉ g₂.support<GOAL>a ∈ (g₁ + g₂).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : DecidableEq α<VAR>g₁ g₂ : α →₀ M<VAR>h : Disjoint g₁.support g₂.support<VAR>a : α<VAR>ha✝ : a ∈ g₁.support ∪ g₂.support<VAR>ha : g₁ a ≠ 0<VAR>this : g₂ a = 0<GOAL>(g₁ + g₂) a ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : DecidableEq α<VAR>g₁ g₂ : α →₀ M<VAR>h : Disjoint g₁.support g₂.support<VAR>a : α<VAR>ha✝ : a ∈ g₁.support ∪ g₂.support<VAR>ha : a ∈ g₂.support<GOAL>a ∈ (g₁ + g₂).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : DecidableEq α<VAR>g₁ g₂ : α →₀ M<VAR>h : Disjoint g₁.support g₂.support<VAR>a : α<VAR>ha✝ : a ∈ g₁.support ∪ g₂.support<VAR>ha : a ∈ g₂.support<VAR>this : a ∉ g₁.support<GOAL>a ∈ (g₁ + g₂).support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : AddZeroClass M<VAR>inst✝ : DecidableEq α<VAR>g₁ g₂ : α →₀ M<VAR>h : Disjoint g₁.support g₂.support<VAR>a : α<VAR>ha✝ : a ∈ g₁.support ∪ g₂.support<VAR>ha : g₂ a ≠ 0<VAR>this : g₁ a = 0<GOAL>(g₁ + g₂) a ≠ 0