ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : PseudoEMetricSpace β<VAR>inst✝¹ : PseudoEMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>f : α → β<VAR>inst✝ : Subsingleton α<VAR>K : ℝ≥0<VAR>x y : α<GOAL>edist x y ≤ ↑K * edist (f x) (f y)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T : Triangle Cᵒᵖ<GOAL>T ∈ distinguishedTriangles C ↔ ∃ T', ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles), Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>T : Triangle Cᵒᵖ<GOAL>Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles ↔ ∃ T', ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles), Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>h : UniformEquicontinuous F<GOAL>UniformEquicontinuous Subtype.val
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>F : ι → β → α<VAR>h : UniformEquicontinuous F<GOAL>UniformEquicontinuous (F ∘ rangeSplitting F)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : X → Y<VAR>U₁ Z₁ : Set X<VAR>hU₁ : IsOpen U₁<VAR>hZ₁ : IsClosed Z₁<VAR>U₂ Z₂ : Set X<VAR>hU₂ : IsOpen U₂<VAR>hZ₂ : IsClosed Z₂<GOAL>IsLocallyClosed (U₁ ∩ Z₁ ∩ (U₂ ∩ Z₂))
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝ : MeasurableSpace E<VAR>x✝ : MeasurableSpace Ω<VAR>X : Ω → E<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>hX : AEMeasurable X ℙ<GOAL>HasPDF X ℙ μ ↔ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝ : MeasurableSpace E<VAR>x✝ : MeasurableSpace Ω<VAR>X : Ω → E<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>hX : AEMeasurable X ℙ<GOAL>AEMeasurable X ℙ ∧ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ ↔ (map X ℙ).HaveLebesgueDecomposition μ ∧ map X ℙ ≪ μ
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>hms : MeasurableSet s<VAR>hmt : MeasurableSet t<VAR>hcs : μ s ≠ ⊤<VAR>u : Set Ω<VAR>a✝ : MeasurableSet u<GOAL>μ[|s][|t] u = μ[|s ∩ t] u
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>hms : MeasurableSet s<VAR>hmt : MeasurableSet t<VAR>hcs : μ s ≠ ⊤<VAR>u : Set Ω<VAR>a✝ : MeasurableSet u<GOAL>((μ s)⁻¹ * μ (s ∩ t))⁻¹ * ((μ s)⁻¹ * μ (s ∩ (t ∩ u))) = (μ (s ∩ t))⁻¹ * μ (s ∩ t ∩ u)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>hms : MeasurableSet s<VAR>hmt : MeasurableSet t<VAR>hcs : μ s ≠ ⊤<VAR>u : Set Ω<VAR>a✝ : MeasurableSet u<VAR>hst : μ (s ∩ t) = 0<GOAL>((μ s)⁻¹ * μ (s ∩ t))⁻¹ * ((μ s)⁻¹ * μ (s ∩ (t ∩ u))) = (μ (s ∩ t))⁻¹ * μ (s ∩ t ∩ u)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>hms : MeasurableSet s<VAR>hmt : MeasurableSet t<VAR>hcs : μ s ≠ ⊤<VAR>u : Set Ω<VAR>a✝ : MeasurableSet u<VAR>hst : μ (s ∩ t) ≠ 0<GOAL>((μ s)⁻¹ * μ (s ∩ t))⁻¹ * ((μ s)⁻¹ * μ (s ∩ (t ∩ u))) = (μ (s ∩ t))⁻¹ * μ (s ∩ t ∩ u)
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>p : B × F<GOAL>p ∈ (Z.localTrivAsPartialEquiv i).target ↔ p.1 ∈ Z.baseSet i
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>p : B × F<GOAL>p.1 ∈ Z.baseSet i ∧ p.2 ∈ univ ↔ p.1 ∈ Z.baseSet i
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<GOAL>IsEmpty (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<GOAL>¬IsEmpty (Algebra ℚ R) ↔ ¬∃ p > 0, MixedCharZero R p
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<GOAL>¬IsEmpty (Algebra ℚ R) ↔ ∀ p > 0, ¬MixedCharZero R p
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharZero R<GOAL>Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>r : ℝ<VAR>hr : r ∈ Ioo 0 f.rOut<GOAL>support ↑(f.updateRIn r hr) = support ↑f
<VAR>ι : Type u_1<VAR>F : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>inst✝⁴ : FunLike F α β<VAR>inst✝³ : Group α<VAR>inst✝² : AddCommSemigroup β<VAR>inst✝¹ : LE β<VAR>inst✝ : MulLEAddHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f a ≤ f b + f (a / b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝² : DecidablePred fun x => x ∈ s<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>g : β → E<VAR>t : Set β<GOAL>∫ (b : β) in t, g b ∂(piecewise hs κ η) a = if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝² : DecidablePred fun x => x ∈ s<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>g : β → E<VAR>t : Set β<GOAL>(∫ (b : β) in t, g b ∂if a ∈ s then κ a else η a) = if a ∈ s then ∫ (b : β) in t, g b ∂κ a else ∫ (b : β) in t, g b ∂η a
<VAR>z : ℂ<GOAL>(z + (starRingEnd ℂ) z).re = (↑(2 * z.re)).re ∧ (z + (starRingEnd ℂ) z).im = (↑(2 * z.re)).im
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h' : ∀ (x : Cofix F α), r x x<VAR>h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest<VAR>x y : (P F).M α<VAR>rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)<VAR>r' : (P F).M α → (P F).M α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)<VAR>hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)<GOAL>Mcongr x y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h' : ∀ (x : Cofix F α), r x x<VAR>h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest<VAR>x y : (P F).M α<VAR>rxy : r (Quot.mk Mcongr x) (Quot.mk Mcongr y)<VAR>r' : (P F).M α → (P F).M α → Prop := fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)<VAR>hr' : r' = fun x y => r (Quot.mk Mcongr x) (Quot.mk Mcongr y)<VAR>this : IsPrecongr r'<GOAL>Mcongr x y
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<GOAL>(idealX K).intValuationDef X = ↑(Multiplicative.ofAdd (-1))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<GOAL>(Polynomial.idealX K).intValuation Polynomial.X = ↑(Multiplicative.ofAdd (-1))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>f : Filter X<VAR>s✝ t s₁ s₂ t₁ t₂ : Set X<VAR>x✝ x : X<VAR>s : Set X<GOAL>𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<VAR>g : ℂ →L[ℝ] E<VAR>f : ℂ → E<VAR>map : ℂ →L[ℂ] E<VAR>nonzero : map ≠ 0<GOAL>IsConformalMap (restrictScalars ℝ map)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<VAR>g : ℂ →L[ℝ] E<VAR>f : ℂ → E<VAR>map : ℂ →L[ℂ] E<VAR>nonzero : map ≠ 0<VAR>minor₁ : ‖map 1‖ ≠ 0<GOAL>IsConformalMap (restrictScalars ℝ map)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ a ∈ s, f a ≠ ⊤<GOAL>(∑ a ∈ s, f a).toReal = ∑ a ∈ s, (f a).toReal
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ≥0∞<VAR>hf : ∀ a ∈ s, f a ≠ ⊤<GOAL>∑ a ∈ s, ↑(f a).toNNReal = ∑ a ∈ s, (f a).toReal
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedAddCommGroup R<VAR>inst✝ : Archimedean R<VAR>f : α → ℕ<VAR>hr : r < 0<VAR>hf : Tendsto f l atTop<GOAL>Tendsto (fun x => f x • r) l atBot
<VAR>α : Type u_1<VAR>x y z : ℝ<VAR>l : Filter α<VAR>f g : α → ℝ<GOAL>(IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => ‖rexp (f x)‖ / ‖rexp (g x)‖) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l (f - g)
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>L : (J ⥤ C) ⥤ C<VAR>adj : const J ⊣ L<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>j : J<GOAL>(fun s => (adj.homEquiv s.pt F) s.π) s ≫ (coneOfAdj adj F).π.app j = s.π.app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>L : (J ⥤ C) ⥤ C<VAR>adj : const J ⊣ L<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>j : J<VAR>eq : ((L ⋙ const J).map s.π ≫ adj.counit.app F).app j = (adj.counit.app ((const J).obj s.pt) ≫ (𝟭 (J ⥤ C)).map s.π).app j<GOAL>(fun s => (adj.homEquiv s.pt F) s.π) s ≫ (coneOfAdj adj F).π.app j = s.π.app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>L : (J ⥤ C) ⥤ C<VAR>adj : const J ⊣ L<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>j : J<VAR>eq : ((L ⋙ const J).map s.π ≫ adj.counit.app F).app j = (adj.counit.app ((const J).obj s.pt) ≫ (𝟭 (J ⥤ C)).map s.π).app j<VAR>eq' : ((const J).map (adj.unit.app s.pt) ≫ adj.counit.app ((const J).obj s.pt)).app j = (𝟙 ((const J).obj s.pt)).app j<GOAL>(fun s => (adj.homEquiv s.pt F) s.π) s ≫ (coneOfAdj adj F).π.app j = s.π.app j
<VAR>J : Type u₁<VAR>inst✝² : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>L : (J ⥤ C) ⥤ C<VAR>adj : const J ⊣ L<VAR>F : J ⥤ C<VAR>s : Cone F<VAR>j : J<VAR>eq : L.map s.π ≫ (adj.counit.app F).app j = (adj.counit.app ((const J).obj s.pt)).app j ≫ s.π.app j<VAR>eq' : adj.unit.app s.pt ≫ (adj.counit.app ((const J).obj s.pt)).app j = 𝟙 s.pt<GOAL>(adj.homEquiv s.pt F) s.π ≫ (adj.counit.app F).app j = s.π.app j
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>J : Type w₁<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : PreservesBiproduct f F<VAR>W : C<VAR>g : (j : J) → f j ⟶ W<VAR>j : J<GOAL>ι (F.obj ∘ f) j ≫ (F.mapBiproduct f).inv ≫ F.map (desc g) = ι (F.obj ∘ f) j ≫ desc fun j => F.map (g j)
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>J : Type w₁<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : PreservesBiproduct f F<VAR>W : C<VAR>g : (j : J) → f j ⟶ W<VAR>j : J<GOAL>ι (fun x => F.obj (f x)) j ≫ (F.mapBiproduct f).inv ≫ F.map (desc g) = ι (fun x => F.obj (f x)) j ≫ desc fun j => F.map (g j)
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>inst✝³ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>J : Type w₁<VAR>f : J → C<VAR>inst✝¹ : HasBiproduct f<VAR>inst✝ : PreservesBiproduct f F<VAR>W : C<VAR>g : (j : J) → f j ⟶ W<VAR>j : J<VAR>this : HasBiproduct fun j => F.obj (f j)<GOAL>ι (fun x => F.obj (f x)) j ≫ (F.mapBiproduct f).inv ≫ F.map (desc g) = ι (fun x => F.obj (f x)) j ≫ desc fun j => F.map (g j)
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>γ : HomologyMapData φ S₁.homologyData S₂.homologyData<GOAL>QuasiIso (opMap φ) ↔ QuasiIso φ
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>γ : HomologyMapData φ S₁.homologyData S₂.homologyData<GOAL>IsIso γ.op.right.φH ↔ IsIso γ.left.φH
<VAR>x y : ℝ<GOAL>sinh x + cosh x = rexp x
<VAR>x y : ℝ≥0∞<VAR>hx : x ≠ ⊤<VAR>hy : y ≠ ⊤<VAR>z : ℝ<GOAL>(x * y) ^ z = x ^ z * y ^ z
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁸ : CommRing P<VAR>inst✝⁷ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝⁶ : CommRing P'<VAR>inst✝⁵ : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P''✝ : Type u_4<VAR>inst✝⁴ : CommRing P''✝<VAR>inst✝³ : Algebra R P''✝<VAR>loc'' : IsLocalization S P''✝<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>P'' : Type u_5<VAR>inst✝² : CommRing P''<VAR>inst✝¹ : Algebra R P''<VAR>inst✝ : IsLocalization S P''<VAR>I : FractionalIdeal S P<VAR>x✝ : P''<GOAL>x✝ ∈ (canonicalEquiv S P' P'') ((canonicalEquiv S P P') I) ↔ x✝ ∈ (canonicalEquiv S P P'') I
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝² : FTCFilter a la la'<VAR>inst✝¹ : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>s t : Set ℝ<VAR>inst✝ : FTCFilter a (𝓝[s] a) (𝓝[t] a)<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝[t] a) volume<VAR>ha : Tendsto f (𝓝[t] a ⊓ ae volume) (𝓝 c)<GOAL>HasDerivWithinAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) s a
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>f : ℝ → E<VAR>c ca cb : E<VAR>l l' la la' lb lb' : Filter ℝ<VAR>lt : Filter ι<VAR>a b z : ℝ<VAR>u v ua ub va vb : ι → ℝ<VAR>inst✝² : FTCFilter a la la'<VAR>inst✝¹ : FTCFilter b lb lb'<VAR>hf : IntervalIntegrable f volume a b<VAR>s t : Set ℝ<VAR>inst✝ : FTCFilter a (𝓝[s] a) (𝓝[t] a)<VAR>hmeas : StronglyMeasurableAtFilter f (𝓝[t] a) volume<VAR>ha : Tendsto f (𝓝[t] a ⊓ ae volume) (𝓝 c)<GOAL>HasDerivWithinAt (fun u => -∫ (x : ℝ) in b..u, f x) (-c) s a
<VAR>n✝ m n : ℕ<GOAL>unitsMap ⋯ = MonoidHom.id (ZMod n)ˣ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>i : ι<GOAL>(fun x => if i = x then 1 else 0) ∈ stdSimplex 𝕜 ι
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.pretrivializationAtlas<GOAL>ContinuousOn (↑e.symm) e.target
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝³ : TopologicalSpace X<VAR>E : B → Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : (x : B) → TopologicalSpace (E x)<VAR>a : FiberPrebundle F E<VAR>e : Pretrivialization F TotalSpace.proj<VAR>he : e ∈ a.pretrivializationAtlas<VAR>z : B × F<VAR>H : z ∈ e.target<VAR>U : Set (TotalSpace F E)<VAR>h : U ∈ 𝓝 (↑e.symm z)<GOAL>coinduced (fun x => ↑e.symm ↑x) inferInstance ≤ a.totalSpaceTopology
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>l : Products I<VAR>o₁ o₂ : Ordinal.{u}<VAR>h : o₁ ≤ o₂<VAR>hl : isGood (π C fun x => ord I x < o₁) l<VAR>hl' : eval (π C fun x => ord I x < o₂) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o₂) '' {m | m < l})<GOAL>eval (π C fun x => ord I x < o₁) l ∈ Submodule.span ℤ (eval (π C fun x => ord I x < o₁) '' {m | m < l})
<VAR>p n : ℕ<VAR>hp : 1 ≤ padicValNat p n<GOAL>p ∣ n
<VAR>p n : ℕ<VAR>hp : 1 ≤ padicValNat p n<VAR>h : ¬p ∣ n<GOAL>False
<VAR>p n : ℕ<VAR>hp : 1 ≤ 0<VAR>h : ¬p ∣ n<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<GOAL>1 < s.card ↔ s.Nontrivial
<VAR>R : CommRingCat<GOAL>identityToΓSpec.app (Spec.toLocallyRingedSpace.obj (op R)) ≫ Spec.toLocallyRingedSpace.map (SpecΓIdentity.inv.app R).op = 𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))
<VAR>R : CommRingCat<GOAL>((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).toΓSpec.val.base ≫ (Spec.locallyRingedSpaceMap (SpecΓIdentity.inv.app R).op.unop).val.base = (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).val.base
<VAR>R : CommRingCat<GOAL>∀ (r : ↑(unop (op ((𝟭 CommRingCat).obj R)))), (SpecΓIdentity.inv.app R).op.unop ≫ ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R))).presheaf.map (homOfLE ⋯).op = toOpen (↑(unop (op ((𝟭 CommRingCat).obj R)))) (basicOpen r) ≫ (𝟙 ((𝟭 LocallyRingedSpace).obj (Spec.toLocallyRingedSpace.obj (op R)))).val.c.app (op (basicOpen r))
<VAR>R✝ : Type u_1<VAR>inst✝² : Semiring R✝<VAR>f : R✝[X]<VAR>R : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : NoZeroDivisors R<VAR>p q : R[X]<GOAL>(p * q).trailingCoeff = p.trailingCoeff * q.trailingCoeff
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → ℂ<VAR>a : E<VAR>c : ℂ<VAR>R : ℝ<GOAL>(∮ (z : ℂ) in C(c, R), f z • a) = (∮ (z : ℂ) in C(c, R), f z) • a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CommMonoidWithZero α<VAR>s✝ : Multiset α<VAR>inst✝¹ : NoZeroDivisors α<VAR>inst✝ : Nontrivial α<VAR>s : Multiset α<VAR>l : List α<GOAL>prod ⟦l⟧ = 0 ↔ 0 ∈ ⟦l⟧
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : CommMonoidWithZero α<VAR>s✝ : Multiset α<VAR>inst✝¹ : NoZeroDivisors α<VAR>inst✝ : Nontrivial α<VAR>s : Multiset α<VAR>l : List α<GOAL>l.prod = 0 ↔ 0 ∈ ↑l
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>f p : R[X]<VAR>x : R<GOAL>(aeval (root f)) (C x) = (mk f) (C x)
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>f p : R[X]<VAR>x : R<GOAL>(algebraMap R (AdjoinRoot f)) x = (mk f) (C x)
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>f p✝ p q : R[X]<VAR>ihp : (aeval (root f)) p = (mk f) p<VAR>ihq : (aeval (root f)) q = (mk f) q<GOAL>(aeval (root f)) (p + q) = (mk f) (p + q)
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>f p : R[X]<VAR>n : ℕ<VAR>x : R<VAR>x✝ : (aeval (root f)) (C x * X ^ n) = (mk f) (C x * X ^ n)<GOAL>(aeval (root f)) (C x * X ^ (n + 1)) = (mk f) (C x * X ^ (n + 1))
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>f p : R[X]<VAR>n : ℕ<VAR>x : R<VAR>x✝ : (aeval (root f)) (C x * X ^ n) = (mk f) (C x * X ^ n)<GOAL>(algebraMap R (AdjoinRoot f)) x * root f ^ (n + 1) = (of f) x * root f ^ (n + 1)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>n : ℕ<GOAL>bernoulli' n = 1 - ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsNoetherianRing R<GOAL>IsNilpotent (nilradical R)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsNoetherianRing R<VAR>n : ℕ<VAR>hn : ⊥.radical ^ n ≤ ⊥<GOAL>IsNilpotent (nilradical R)
<VAR>β : Type w<VAR>α : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>f : β → C<VAR>inst✝¹ : HasProduct f<VAR>inst✝ : HasProduct fun b => G.obj (f b)<VAR>P : C<VAR>g : (j : β) → P ⟶ f j<VAR>j : β<GOAL>(G.map (Pi.lift g) ≫ piComparison G f) ≫ Pi.π (fun b => G.obj (f b)) j = (Pi.lift fun j => G.map (g j)) ≫ Pi.π (fun b => G.obj (f b)) j
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>s : Multiset α<VAR>hs : 0 ∉ s<GOAL>normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>s : Multiset α<VAR>hs : 0 ∉ s<VAR>h✝ : Subsingleton α<GOAL>normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizationMonoid α<VAR>inst✝ : UniqueFactorizationMonoid α<VAR>s : Multiset α<VAR>hs : 0 ∉ s<VAR>h✝ : Nontrivial α<GOAL>normalizedFactors s.prod = (Multiset.map normalizedFactors s).sum
<VAR>n : ℕ<VAR>c : Composition n<GOAL>(↑c.blocks).sum = n
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (kerTotal R A) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1) = Submodule.restrictScalars A (kerTotal S B)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹⁵ : CommRing R<VAR>inst✝¹⁴ : CommRing S<VAR>inst✝¹³ : Algebra R S<VAR>M : Type u_1<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module S M<VAR>inst✝⁹ : IsScalarTower R S M<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁸ : CommRing A<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Algebra S B<VAR>inst✝² : IsScalarTower R A B<VAR>inst✝¹ : IsScalarTower R S B<VAR>inst✝ : SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.span A (⇑(Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) '' (((Set.range fun x => Finsupp.single x.1 1 + Finsupp.single x.2 1 - Finsupp.single (x.1 + x.2) 1) ∪ Set.range fun x => Finsupp.single x.2 x.1 + Finsupp.single x.1 x.2 - Finsupp.single (x.1 * x.2) 1) ∪ Set.range fun x => Finsupp.single ((algebraMap R A) x) 1)) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1) = Submodule.span A (((Set.range fun x => Finsupp.single x.1 1 + Finsupp.single x.2 1 - Finsupp.single (x.1 + x.2) 1) ∪ Set.range fun x => Finsupp.single x.2 x.1 + Finsupp.single x.1 x.2 - Finsupp.single (x.1 * x.2) 1) ∪ Set.range fun x => Finsupp.single ((algebraMap S B) x) 1)