ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝⁵ : AddGroup G<VAR>inst✝⁴ : MeasurableAdd₂ G<VAR>inst✝³ : MeasurableNeg G<VAR>inst✝² : SFinite μ<VAR>inst✝¹ : μ.IsAddRightInvariant<VAR>inst✝ : SFinite ν<VAR>hf : Integrable f ν<VAR>hg : Integrable g μ<VAR>h_meas : AEStronglyMeasurable (fun p => (L (f p.2)) (g (p.1 - p.2))) (μ.prod ν)<VAR>h2_meas : AEStronglyMeasurable (fun y => ∫ (x : G), ‖(L (f y)) (g (x - y))‖ ∂μ) ν<VAR>t : G<GOAL>‖∫ (x : G), ‖(L (f t)) (g (x - t))‖ ∂μ‖ ≤ ‖L‖ * ‖f t‖ * ∫ (x : G), ‖g (x - t)‖ ∂μ
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LT α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c : α<GOAL>b < a * 1 ↔ b < a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>h₁.homologyIso.inv ≫ homologyMap φ = rightHomologyMap' φ h₁ h₂ ≫ h₂.homologyIso.inv
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>P : C<GOAL>Projective P ↔ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>P : C<GOAL>(coyoneda.obj (op P)).PreservesEpimorphisms ↔ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>W'.addY P (W'.neg P) = -W'.dblZ P ^ 3
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>hP : W'.Equation P<GOAL>-![W'.dblZ P ^ 2, W'.dblZ P ^ 3, addZ P (W'.neg P)] y = -W'.dblZ P ^ 3
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>f : α → α<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : PreErgodic f μ<VAR>hs : MeasurableSet s<VAR>hs' : f ⁻¹' s = s<GOAL>μ s = 0 ∨ μ sᶜ = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>N : Submonoid R<VAR>h₁ : M ≤ N<VAR>h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)<VAR>x y : R<GOAL>(algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>N : Submonoid R<VAR>h₁ : M ≤ N<VAR>h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)<VAR>x y : R<GOAL>(∃ c, ↑c * x = ↑c * y) → ∃ c, ↑c * x = ↑c * y
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>N : Submonoid R<VAR>h₁ : M ≤ N<VAR>h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)<VAR>x y : R<VAR>c : ↥M<VAR>hc : ↑c * x = ↑c * y<GOAL>∃ c, ↑c * x = ↑c * 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>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>‖1‖ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<GOAL>{ ofColex := s } < { ofColex := t } ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<GOAL>(∃ x, ¬(x ∈ t → x ∉ s → ∃ b ∈ s, b ∉ t ∧ x ≤ b)) ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>f : R[X]<GOAL>toLaurent (Polynomial.C r * f) = C r * toLaurent f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : CommSemiring R<VAR>n k : ℕ<VAR>c : R<GOAL>(⇑derivative)^[k] ((X + C c) ^ n) = n.descFactorial k • (X + C c) ^ (n - k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<VAR>x y : α<VAR>hxy : mapNatBool α x = mapNatBool α y<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : CountablyGenerated α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<VAR>x y : α<VAR>hxy : mapNatBool α x = mapNatBool α y<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : CountablyGenerated α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<VAR>x y : α<VAR>hxy : mapNatBool α x = mapNatBool α y<GOAL>∀ s ∈ range (natGeneratingSequence α), x ∈ s ↔ y ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : CountablyGenerated α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<VAR>x y : α<VAR>hxy : mapNatBool α x = mapNatBool α y<VAR>n : ℕ<GOAL>x ∈ natGeneratingSequence α n ↔ y ∈ natGeneratingSequence α n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : CountablyGenerated α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<VAR>x y : α<VAR>hxy : mapNatBool α x = mapNatBool α y<VAR>n : ℕ<GOAL>decide (x ∈ natGeneratingSequence α n) = decide (y ∈ natGeneratingSequence α n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : CountablyGenerated α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<VAR>x y : α<VAR>hxy : mapNatBool α x = mapNatBool α y<VAR>n : ℕ<GOAL>Decidable (x ∈ natGeneratingSequence α n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : CountablyGenerated α<VAR>inst✝¹ : CountablyGenerated α<VAR>inst✝ : SeparatesPoints α<VAR>x y : α<VAR>hxy : mapNatBool α x = mapNatBool α y<VAR>n : ℕ<GOAL>Decidable (y ∈ natGeneratingSequence α n)
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : Field S<VAR>inst✝⁸ : NonUnitalRing A<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : Module S A<VAR>inst✝⁴ : IsScalarTower S A A<VAR>inst✝³ : SMulCommClass S A A<VAR>inst✝² : IsScalarTower R S A<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSpace S<VAR>a : A<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<VAR>h_cpct : CompactSpace ↑(σₙ S a)<GOAL>CompactSpace ↑(σₙ R a)
<VAR>𝕜 : Type u_1<VAR>A✝ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝¹⁰ : Semifield R<VAR>inst✝⁹ : Field S<VAR>inst✝⁸ : NonUnitalRing A<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : Module R A<VAR>inst✝⁵ : Module S A<VAR>inst✝⁴ : IsScalarTower S A A<VAR>inst✝³ : SMulCommClass S A A<VAR>inst✝² : IsScalarTower R S A<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSpace S<VAR>a : A<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<VAR>h_cpct : IsCompact (σₙ S a)<GOAL>IsCompact (σₙ R a)
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>inst✝⁶ : HasZeroMorphisms C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝³ : G.PreservesZeroMorphisms<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>h : Z ⟶ X<VAR>w : h ≫ f = 0<VAR>inst✝² : HasKernel f<VAR>inst✝¹ : HasKernel (G.map f)<VAR>inst✝ : PreservesLimit (parallelPair f 0) G<GOAL>(iso G f).hom = kernelComparison f G
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>inst✝⁶ : HasZeroMorphisms C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms D<VAR>G : C ⥤ D<VAR>inst✝³ : G.PreservesZeroMorphisms<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>h : Z ⟶ X<VAR>w : h ≫ f = 0<VAR>inst✝² : HasKernel f<VAR>inst✝¹ : HasKernel (G.map f)<VAR>inst✝ : PreservesLimit (parallelPair f 0) G<GOAL>(iso G f).hom ≫ kernel.ι (G.map f) = kernelComparison f G ≫ kernel.ι (G.map f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq β<GOAL>(image f s).card ≤ s.card
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>c : Con M<VAR>x y : M<VAR>f✝ : M →* P<VAR>f g : c.Quotient →* P<VAR>h : ∀ (a : M), f ↑a = g ↑a<GOAL>f = g
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>c : Con M<VAR>x y : M<VAR>f✝ : M →* P<VAR>f g : c.Quotient →* P<VAR>h : ∀ (a : M), f ↑a = g ↑a<GOAL>c.lift (f.comp c.mk') ⋯ = c.lift (g.comp c.mk') ⋯
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : MulOneClass M<VAR>inst✝¹ : MulOneClass N<VAR>inst✝ : MulOneClass P<VAR>c : Con M<VAR>x y : M<VAR>f✝ : M →* P<VAR>f g : c.Quotient →* P<VAR>h : ∀ (a : M), f ↑a = g ↑a<GOAL>f.comp c.mk' = g.comp c.mk'
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>y p q : R[X]<GOAL>(p • 1 + q • (mk W) Y) * (mk W) (C y) = (p * y) • 1 + (q * y) • (mk W) Y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>y p q : R[X]<GOAL>((mk W) (C p) * 1 + (mk W) (C q) * (mk W) Y) * (mk W) (C y) = (mk W) (C p) * (mk W) (C y) * 1 + (mk W) (C q) * (mk W) (C y) * (mk W) Y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : BorelSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>g : α → E<VAR>l : Filter ι<VAR>x₀ : α<VAR>s t✝ : Set α<VAR>φ : ι → α → ℝ<VAR>a : E<VAR>inst✝ : CompleteSpace E<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>h'ts : t ∈ 𝓝 x₀<VAR>h't : μ t ≠ ⊤<VAR>hnφ : ∀ᶠ (i : ι) in l, ∀ (x : α), 0 ≤ φ i x<VAR>hlφ : ∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l uᶜ<VAR>hiφ : Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)<VAR>h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) μ<VAR>hmg : Integrable g μ<VAR>hcg : Tendsto g (𝓝 x₀) (𝓝 a)<GOAL>Tendsto (fun i => ∫ (x : α) in univ, φ i x • g x ∂μ) l (𝓝 a)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<GOAL>φ ≫ (Hσ q).f (n + 1) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<VAR>hnaq_shift : ∀ (d : ℕ), n + d = a + d + q<GOAL>φ ≫ (Hσ q).f (n + 1) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<VAR>hnaq_shift : ∀ (d : ℕ), n + d = a + d + q<GOAL>φ ≫ ((AlternatingFaceMapComplex.obj X).d (n + 1) n ≫ ((-1) ^ a • X.σ ⟨a, ⋯⟩) ≫ eqToHom ⋯ + (((-1) ^ (a + 1) • X.σ ⟨a + 1, ⋯⟩) ≫ eqToHom ⋯) ≫ (AlternatingFaceMapComplex.obj X).d (n + 2) (n + 1)) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<VAR>hnaq_shift : ∀ (d : ℕ), n + d = a + d + q<GOAL>∑ j : Fin (n + 2), φ ≫ ((-1) ^ ↑j • X.δ j) ≫ ((-1) ^ a • X.σ ⟨a, ⋯⟩) + ∑ j : Fin (n + 1 + 2), φ ≫ ((-1) ^ (a + 1) • X.σ ⟨a + 1, ⋯⟩) ≫ ((-1) ^ ↑j • X.δ j) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<VAR>hnaq_shift : ∀ (d : ℕ), n + d = a + d + q<GOAL>∑ x : Fin (n + 2), ((-1) ^ a * (-1) ^ ↑x) • (φ ≫ X.δ x) ≫ X.σ ⟨a, ⋯⟩ + ∑ x : Fin (n + 1 + 2), ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ x = -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<VAR>hnaq_shift : ∀ (d : ℕ), n + d = a + d + q<GOAL>∑ i : Fin (a + 2), ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castLE ⋯ i))) • (φ ≫ X.δ (Fin.cast ⋯ (Fin.castLE ⋯ i))) ≫ X.σ ⟨a, ⋯⟩ + ∑ x : Fin (n + 1 + 2), ((-1) ^ ↑x * (-1) ^ (a + 1)) • (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ x = -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<VAR>hnaq_shift : ∀ (d : ℕ), n + d = a + d + q<GOAL>∀ (j : Fin q), ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 2) j))) • (φ ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 2) j))) ≫ X.σ ⟨a, ⋯⟩ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<VAR>hnaq_shift : ∀ (d : ℕ), n + d = a + d + q<GOAL>∑ i : Fin (a + 2), ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castLE ⋯ i))) • (φ ≫ X.δ (Fin.cast ⋯ (Fin.castLE ⋯ i))) ≫ X.σ ⟨a, ⋯⟩ + ∑ i : Fin (a + 3), ((-1) ^ ↑(Fin.cast ⋯ (Fin.castLE ⋯ i)) * (-1) ^ (a + 1)) • (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ (Fin.cast ⋯ (Fin.castLE ⋯ i)) = -(φ ≫ X.δ ⟨a + 1, ⋯⟩) ≫ X.σ ⟨a, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<VAR>hnaq_shift : ∀ (d : ℕ), n + d = a + d + q<GOAL>∀ (j : Fin q), ((-1) ^ ↑(Fin.cast ⋯ (Fin.natAdd (a + 3) j)) * (-1) ^ (a + 1)) • (φ ≫ X.σ ⟨a + 1, ⋯⟩) ≫ X.δ (Fin.cast ⋯ (Fin.natAdd (a + 3) j)) = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<VAR>hnaq_shift : ∀ (d : ℕ), n + d = a + d + q<GOAL>∑ x : Fin (a + 2), ((-1) ^ a * (-1) ^ ↑(Fin.cast ⋯ (Fin.castLE ⋯ x))) • φ ≫ X.δ (Fin.cast ⋯ (Fin.castLE ⋯ x)) ≫ X.σ ⟨a, ⋯⟩ + ∑ x : Fin (a + 3), ((-1) ^ ↑(Fin.cast ⋯ (Fin.castLE ⋯ x)) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ (Fin.cast ⋯ (Fin.castLE ⋯ x)) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<VAR>hnaq_shift : ∀ (d : ℕ), n + d = a + d + q<GOAL>∑ i : Fin (a + 1), ((-1) ^ a * (-1) ^ ↑i) • φ ≫ X.δ ⟨↑i, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ + ((-1) ^ a * (-1) ^ (a + 1)) • φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ + (∑ i : Fin (a + 1), ((-1) ^ ↑i * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨↑i, ⋯⟩ + ((-1) ^ (a + 1) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 1, ⋯⟩ + ((-1) ^ (a + 2) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 2, ⋯⟩) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>Y : C<VAR>n a q : ℕ<VAR>φ : Y ⟶ X _[n + 1]<VAR>v : HigherFacesVanish q φ<VAR>hnaq : n = a + q<VAR>hnaq_shift : ∀ (d : ℕ), n + d = a + d + q<VAR>simplif : ∀ (a b c d e f : Y ⟶ X _[n + 1]), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f<GOAL>∑ i : Fin (a + 1), ((-1) ^ a * (-1) ^ ↑i) • φ ≫ X.δ ⟨↑i, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ + ((-1) ^ a * (-1) ^ (a + 1)) • φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩ + (∑ i : Fin (a + 1), ((-1) ^ ↑i * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨↑i, ⋯⟩ + ((-1) ^ (a + 1) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 1, ⋯⟩ + ((-1) ^ (a + 2) * (-1) ^ (a + 1)) • φ ≫ X.σ ⟨a + 1, ⋯⟩ ≫ X.δ ⟨a + 2, ⋯⟩) = -φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ ⟨a, ⋯⟩
<VAR>x✝ y x : ℝ<GOAL>tan (arcsin x) = x / √(1 - x ^ 2)
<VAR>x✝ y x : ℝ<GOAL>sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)
<VAR>x✝ y x : ℝ<VAR>hx₁ : -1 ≤ x<VAR>hx₂ : x ≤ 1<GOAL>sin (arcsin x) / √(1 - x ^ 2) = x / √(1 - x ^ 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<VAR>g g₁ g₂ : Perm α<VAR>s t : Set α<VAR>h : SurjOn (⇑g) s t<VAR>b : α<VAR>hb : b ∈ s<VAR>ha : g b ∈ t<GOAL>(Subtype.val ∘ ⇑f) (g b) ∈ ⇑(g.extendDomain f) '' (Subtype.val ∘ ⇑f '' s)
<VAR>z : ℂ<GOAL>abs z ^ 2 - z.re ^ 2 = z.im ^ 2
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : DecidableEq m<VAR>d : m × o → α<VAR>k : o<VAR>i j : m<GOAL>(diagonal d).blockDiag k i j = diagonal (fun i => d (i, k)) i j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : DecidableEq m<VAR>d : m × o → α<VAR>k : o<VAR>i : m<GOAL>(diagonal d).blockDiag k i i = diagonal (fun i => d (i, k)) i i
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : Zero α<VAR>inst✝² : Zero β<VAR>inst✝¹ : DecidableEq o<VAR>inst✝ : DecidableEq m<VAR>d : m × o → α<VAR>k : o<VAR>i j : m<VAR>hij : i ≠ j<GOAL>(diagonal d).blockDiag k i j = diagonal (fun i => d (i, k)) i j
<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 μ<VAR>x : α<VAR>n : ℕ<GOAL>spanningSetsIndex μ x = n ↔ x ∈ disjointed (spanningSets μ) n
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v : V<VAR>w y : W<GOAL>(fderiv ℝ (fun w => ↑(𝐞 (-(L v) w))) w) y = -2 * ↑π * I * ↑((L v) y) * ↑(𝐞 (-(L v) w))
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>v : V<VAR>w y : W<GOAL>2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L v) y) = 2 * ↑π * I * ↑((L v) y) * ↑(𝐞 (-(L v) w))
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A R S : ValuationSubring K<VAR>hR : A ≤ R<VAR>hS : A ≤ S<VAR>h : R ≤ S<VAR>x : ↥A<VAR>hx : x ∈ A.idealOfLE S hS<GOAL>R.valuation ↑((A.inclusion R hR) x) < 1
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A R S : ValuationSubring K<VAR>hR : A ≤ R<VAR>hS : A ≤ S<VAR>h : R ≤ S<VAR>x : ↥A<VAR>hx : x ∈ A.idealOfLE S hS<VAR>c : ¬R.valuation ↑((A.inclusion R hR) x) < 1<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A R S : ValuationSubring K<VAR>hR : A ≤ R<VAR>hS : A ≤ S<VAR>h : R ≤ S<VAR>x : ↥A<VAR>hx : x ∈ A.idealOfLE S hS<VAR>c : 1 ≤ R.valuation ↑((A.inclusion R hR) x)<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A R S : ValuationSubring K<VAR>hR : A ≤ R<VAR>hS : A ≤ S<VAR>h : R ≤ S<VAR>x : ↥A<VAR>hx : x ∈ A.idealOfLE S hS<VAR>c : (R.mapOfLE S h) 1 ≤ (R.mapOfLE S h) (R.valuation ↑((A.inclusion R hR) x))<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>A R S : ValuationSubring K<VAR>hR : A ≤ R<VAR>hS : A ≤ S<VAR>h : R ≤ S<VAR>x : ↥A<VAR>hx : x ∈ A.idealOfLE S hS<VAR>c : 1 ≤ S.valuation ↑((A.inclusion R hR) x)<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y✝ : E<VAR>s✝ t : Set E<VAR>f : E →ᵃ[𝕜] F<VAR>s : Set F<VAR>hs : StarConvex 𝕜 (f x) s<VAR>y : E<VAR>hy : y ∈ ⇑f ⁻¹' s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ ⇑f ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y✝ : E<VAR>s✝ t : Set E<VAR>f : E →ᵃ[𝕜] F<VAR>s : Set F<VAR>hs : StarConvex 𝕜 (f x) s<VAR>y : E<VAR>hy : y ∈ ⇑f ⁻¹' s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y ∈ s
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : C<VAR>f : Y ≅ Z<GOAL>X ◁ f.hom ≫ X ◁ f.inv = 𝟙 (X ⊗ Y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A ⊗[R] R[X]<GOAL>invFun R A ((toFunAlgHom R A) x) = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A ⊗[R] R[X]<GOAL>invFun R A ((toFunAlgHom R A) 0) = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A ⊗[R] R[X]<GOAL>∀ (x : A) (y : R[X]), invFun R A ((toFunAlgHom R A) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : A ⊗[R] R[X]<GOAL>∀ (x y : A ⊗[R] R[X]), invFun R A ((toFunAlgHom R A) x) = x → invFun R A ((toFunAlgHom R A) y) = y → invFun R A ((toFunAlgHom R A) (x + y)) = x + y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommSemigroup G<VAR>a b c : G<GOAL>a * b * c = b * c * 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>α : Type u_12<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>f : ι → Set α<VAR>t : Set α<GOAL>⋂ i ∈ s, t ∩ f i = t ∩ ⋂ i ∈ s, f i
<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>α : Type u_12<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>f : ι → Set α<VAR>t : Set α<GOAL>⋂ i ∈ s, t ∩ f i = ⋂ i ∈ s, f i ∩ t
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>i : E ≃L[𝕜] F<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>p.rightInv i n = -(↑i.symm).compContinuousMultilinearMap (∑ c ∈ {c | 1 < c.length}.toFinset, p.compAlongComposition (p.rightInv i) c)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r : ℝ≥0∞<GOAL>IsOpen {x | AnalyticAt 𝕜 f x}