ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a✝ b✝ : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in b..a, f x ∂μ = -∫ (x : ℝ) in a..b, f x ∂μ
<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 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'<VAR>n : ℤ<VAR>hn : n + a = n'<GOAL>(leftShiftAddEquiv K L n a n' hn).symm (-γ) = -γ.leftUnshift n hn
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y : V<GOAL>affineSegment R x y = segment R x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>emb : Fintype (α ↪ β)<GOAL>‖α ↪ β‖ = ‖β‖.descFactorial ‖α‖
<VAR>β : Type u_2<VAR>inst✝ : Fintype β<VAR>α₁ α₂ : Type u_1<VAR>h₂ : Fintype α₂<VAR>e : α₁ ≃ α₂<VAR>ih : (fun t [Fintype t] => ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) α₁<GOAL>‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖
<VAR>β : Type u_2<VAR>inst✝ : Fintype β<GOAL>‖PEmpty.{u_1 + 1} ↪ β‖ = ‖β‖.descFactorial ‖PEmpty.{u_1 + 1}‖
<VAR>β : Type u_2<VAR>inst✝ : Fintype β<VAR>γ : Type u_1<VAR>h : Fintype γ<VAR>ih : (fun t [Fintype t] => ‖t ↪ β‖ = ‖β‖.descFactorial ‖t‖) γ<GOAL>‖Option γ ↪ β‖ = ‖β‖.descFactorial ‖Option γ‖
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : NoMaxOrder α<GOAL>Bounded (fun x x_1 => x ≤ x_1) s ↔ Bounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : NoMaxOrder α<VAR>h : Bounded (fun x x_1 => x ≤ x_1) s<GOAL>Bounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<VAR>ha : ∀ b ∈ s, (fun x x_1 => x ≤ x_1) b a<GOAL>Bounded (fun x x_1 => x < x_1) s
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s t : Set α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<VAR>ha : ∀ b ∈ s, (fun x x_1 => x ≤ x_1) b a<VAR>b : α<VAR>hb : a < b<GOAL>Bounded (fun x x_1 => x < x_1) s
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<GOAL>∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w✝ : K<VAR>h_mem : w✝ ∈ ↑1<VAR>h_nz : w✝ ≠ 0<VAR>h_nm : ↑|(Algebra.norm ℚ) w✝| ≤ ↑(FractionalIdeal.absNorm ↑1) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|<GOAL>∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>a : 𝓞 K<VAR>h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1<VAR>h_nz : (algebraMap (𝓞 K) K) a ≠ 0<VAR>h_nm : ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤ ↑(FractionalIdeal.absNorm ↑1) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|<GOAL>∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>a : 𝓞 K<VAR>h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1<VAR>h_nz : (algebraMap (𝓞 K) K) a ≠ 0<VAR>h_nm : ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤ ↑(FractionalIdeal.absNorm ↑1) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|<GOAL>↑|(Algebra.norm ℚ) ↑a| ≤ (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>a : 𝓞 K<VAR>h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1<VAR>h_nz : (algebraMap (𝓞 K) K) a ≠ 0<VAR>h_nm : ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤ (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|<GOAL>↑|(Algebra.norm ℚ) ↑a| ≤ (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>v : α<VAR>t : RBNode α<GOAL>(match t.isRed with | red => (ins cmp v t).setBlack | black => ins cmp v t).setBlack = (ins cmp v t).setBlack
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y x : V<VAR>hx : x ≠ 0<GOAL>arccos (⟪x, x⟫_ℝ / (‖x‖ * ‖x‖)) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s : Set α<VAR>h : s.Finite<VAR>val✝ : Fintype ↑s<GOAL>∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<GOAL>↑(⨆ i, p i) = ⨆ i, ↑(p i)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<GOAL>sSup {x | ∃ s ∈ range fun i => p i, ↑s = x} = ⨆ i, ↑(p i)
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>p : ι → LieSubmodule R L M<VAR>x✝ : M<GOAL>x✝ ∈ sSup {x | ∃ s ∈ range fun i => p i, ↑s = x} ↔ x✝ ∈ ⨆ i, ↑(p i)
<VAR>n m : ℕ<VAR>p i : Fin n<VAR>h : p ≤ i<GOAL>p.predAbove i.succ = i
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<GOAL>(f z - f x) / (z - x) < (f z - f y) / (z - y)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>s : Set 𝕜<VAR>f : 𝕜 → 𝕜<VAR>hf : StrictConvexOn 𝕜 s f<VAR>x y z : 𝕜<VAR>hx : x ∈ s<VAR>hz : z ∈ s<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hyz' : 0 < z - y<VAR>hxz' : 0 < z - x<GOAL>(f z - f x) * (z - y) < (f z - f y) * (z - x)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.13014, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.HomologyData<GOAL>S.Exact ↔ h.left.i ≫ h.right.p = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.13014, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.HomologyData<VAR>this : S.HasHomology<GOAL>S.Exact ↔ h.left.i ≫ h.right.p = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.13014, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S S₁ S₂ : ShortComplex C<VAR>h : S.HomologyData<VAR>this : S.HasHomology<GOAL>IsZero h.left.H ↔ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0
<VAR>a x z✝ z : ℂ<GOAL>|z.arg| < π / 2 ↔ 0 < z.re ∨ z = 0
<VAR>a x z✝ z : ℂ<GOAL>0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
<VAR>a x z✝ z : ℂ<VAR>hz : z = 0<GOAL>0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
<VAR>a x z✝ z : ℂ<VAR>hz : z ≠ 0<GOAL>0 < z.re ∨ 0 ≤ z.im ∧ (z.im < 0 ∨ z = 0) ↔ 0 < z.re ∨ z = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>0 ≤ᶠ[ae (μ.restrict t)] f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x✝ : μ (s ∩ t) < ⊤<GOAL>0 ≤ ∫ (x : α) in s ∩ t, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f✝ f : α → ℝ<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>x✝ : μ (s ∩ t) < ⊤<GOAL>μ (s ∩ t) < ⊤
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>E : Type u₄<VAR>inst✝⁵ : Category.{v₁, u₁} C₁<VAR>inst✝⁴ : Category.{v₂, u₂} C₂<VAR>inst✝³ : Category.{v₃, u₃} C₃<VAR>inst✝² : Category.{v₄, u₄} E<VAR>L₁ : C₁ ⥤ C₂<VAR>L₂ : C₂ ⥤ C₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>inst✝ : L₂.IsLocalization W₂<VAR>W₃ : MorphismProperty C₁<VAR>hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)<VAR>hW₁₃ : W₁ ≤ W₃<VAR>hW₂₃ : W₂ ≤ W₃.map L₁<VAR>E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁<VAR>W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor<GOAL>(L₁ ⋙ L₂).IsLocalization W₃
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>E : Type u₄<VAR>inst✝⁵ : Category.{v₁, u₁} C₁<VAR>inst✝⁴ : Category.{v₂, u₂} C₂<VAR>inst✝³ : Category.{v₃, u₃} C₃<VAR>inst✝² : Category.{v₄, u₄} E<VAR>L₁ : C₁ ⥤ C₂<VAR>L₂ : C₂ ⥤ C₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>inst✝ : L₂.IsLocalization W₂<VAR>W₃ : MorphismProperty C₁<VAR>hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)<VAR>hW₁₃ : W₁ ≤ W₃<VAR>hW₂₃ : W₂ ≤ W₃.map L₁<VAR>E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁<VAR>W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor<VAR>Φ : LocalizerMorphism W₂ W₂' := { functor := E₂.functor, map := ⋯ }<GOAL>(L₁ ⋙ L₂).IsLocalization W₃
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>E : Type u₄<VAR>inst✝⁵ : Category.{v₁, u₁} C₁<VAR>inst✝⁴ : Category.{v₂, u₂} C₂<VAR>inst✝³ : Category.{v₃, u₃} C₃<VAR>inst✝² : Category.{v₄, u₄} E<VAR>L₁ : C₁ ⥤ C₂<VAR>L₂ : C₂ ⥤ C₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>inst✝ : L₂.IsLocalization W₂<VAR>W₃ : MorphismProperty C₁<VAR>hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)<VAR>hW₁₃ : W₁ ≤ W₃<VAR>hW₂₃ : W₂ ≤ W₃.map L₁<VAR>E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁<VAR>W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor<VAR>Φ : LocalizerMorphism W₂ W₂' := { functor := E₂.functor, map := ⋯ }<VAR>this : Φ.IsLocalizedEquivalence<GOAL>(L₁ ⋙ L₂).IsLocalization W₃
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>E : Type u₄<VAR>inst✝⁵ : Category.{v₁, u₁} C₁<VAR>inst✝⁴ : Category.{v₂, u₂} C₂<VAR>inst✝³ : Category.{v₃, u₃} C₃<VAR>inst✝² : Category.{v₄, u₄} E<VAR>L₁ : C₁ ⥤ C₂<VAR>L₂ : C₂ ⥤ C₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>inst✝ : L₂.IsLocalization W₂<VAR>W₃ : MorphismProperty C₁<VAR>hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)<VAR>hW₁₃ : W₁ ≤ W₃<VAR>hW₂₃ : W₂ ≤ W₃.map L₁<VAR>E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁<VAR>W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor<VAR>Φ : LocalizerMorphism W₂ W₂' := { functor := E₂.functor, map := ⋯ }<VAR>this : Φ.IsLocalizedEquivalence<VAR>E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence<VAR>iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ := Trans.trans (Trans.trans (W₁.Q.associator W₂'.Q E₃.inverse ≪≫ isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm (W₂'.Q ⋙ E₃.inverse) ≪≫ L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse)) (isoWhiskerLeft L₁ ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫ isoWhiskerRight (CatCommSq.iso Φ.functor L₂ W₂'.Q (Φ.localizedFunctor L₂ W₂'.Q)) E₃.inverse ≪≫ L₂.associator (Φ.localizedFunctor L₂ W₂'.Q) E₃.inverse))) (isoWhiskerLeft L₁ (isoWhiskerLeft L₂ E₃.unitIso.symm ≪≫ L₂.rightUnitor))<GOAL>(L₁ ⋙ L₂).IsLocalization W₃
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>E : Type u₄<VAR>inst✝⁵ : Category.{v₁, u₁} C₁<VAR>inst✝⁴ : Category.{v₂, u₂} C₂<VAR>inst✝³ : Category.{v₃, u₃} C₃<VAR>inst✝² : Category.{v₄, u₄} E<VAR>L₁ : C₁ ⥤ C₂<VAR>L₂ : C₂ ⥤ C₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>inst✝ : L₂.IsLocalization W₂<VAR>W₃ : MorphismProperty C₁<VAR>hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)<VAR>hW₁₃ : W₁ ≤ W₃<VAR>hW₂₃ : W₂ ≤ W₃.map L₁<VAR>E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁<VAR>W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor<VAR>Φ : LocalizerMorphism W₂ W₂' := { functor := E₂.functor, map := ⋯ }<VAR>this : Φ.IsLocalizedEquivalence<VAR>E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence<VAR>iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ := Trans.trans (Trans.trans (W₁.Q.associator W₂'.Q E₃.inverse ≪≫ isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm (W₂'.Q ⋙ E₃.inverse) ≪≫ L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse)) (isoWhiskerLeft L₁ ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫ isoWhiskerRight (CatCommSq.iso Φ.functor L₂ W₂'.Q (Φ.localizedFunctor L₂ W₂'.Q)) E₃.inverse ≪≫ L₂.associator (Φ.localizedFunctor L₂ W₂'.Q) E₃.inverse))) (isoWhiskerLeft L₁ (isoWhiskerLeft L₂ E₃.unitIso.symm ≪≫ L₂.rightUnitor))<VAR>hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)<GOAL>(L₁ ⋙ L₂).IsLocalization W₃
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>E : Type u₄<VAR>inst✝⁵ : Category.{v₁, u₁} C₁<VAR>inst✝⁴ : Category.{v₂, u₂} C₂<VAR>inst✝³ : Category.{v₃, u₃} C₃<VAR>inst✝² : Category.{v₄, u₄} E<VAR>L₁ : C₁ ⥤ C₂<VAR>L₂ : C₂ ⥤ C₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>inst✝ : L₂.IsLocalization W₂<VAR>W₃ : MorphismProperty C₁<VAR>hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)<VAR>hW₁₃ : W₁ ≤ W₃<VAR>hW₂₃ : W₂ ≤ W₃.map L₁<VAR>E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁<VAR>W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor<VAR>Φ : LocalizerMorphism W₂ W₂' := { functor := E₂.functor, map := ⋯ }<VAR>this : Φ.IsLocalizedEquivalence<VAR>E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence<VAR>iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ := Trans.trans (Trans.trans (W₁.Q.associator W₂'.Q E₃.inverse ≪≫ isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm (W₂'.Q ⋙ E₃.inverse) ≪≫ L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse)) (isoWhiskerLeft L₁ ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫ isoWhiskerRight (CatCommSq.iso Φ.functor L₂ W₂'.Q (Φ.localizedFunctor L₂ W₂'.Q)) E₃.inverse ≪≫ L₂.associator (Φ.localizedFunctor L₂ W₂'.Q) E₃.inverse))) (isoWhiskerLeft L₁ (isoWhiskerLeft L₂ E₃.unitIso.symm ≪≫ L₂.rightUnitor))<VAR>hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)<VAR>hW₂₃' : W₂' ≤ W₃.map W₁.Q<GOAL>(L₁ ⋙ L₂).IsLocalization W₃
<VAR>C₁ : Type u₁<VAR>C₂ : Type u₂<VAR>C₃ : Type u₃<VAR>E : Type u₄<VAR>inst✝⁵ : Category.{v₁, u₁} C₁<VAR>inst✝⁴ : Category.{v₂, u₂} C₂<VAR>inst✝³ : Category.{v₃, u₃} C₃<VAR>inst✝² : Category.{v₄, u₄} E<VAR>L₁ : C₁ ⥤ C₂<VAR>L₂ : C₂ ⥤ C₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>inst✝¹ : L₁.IsLocalization W₁<VAR>inst✝ : L₂.IsLocalization W₂<VAR>W₃ : MorphismProperty C₁<VAR>hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)<VAR>hW₁₃ : W₁ ≤ W₃<VAR>hW₂₃ : W₂ ≤ W₃.map L₁<VAR>E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁<VAR>W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor<VAR>Φ : LocalizerMorphism W₂ W₂' := { functor := E₂.functor, map := ⋯ }<VAR>this✝ : Φ.IsLocalizedEquivalence<VAR>E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor L₂ W₂'.Q).asEquivalence<VAR>iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ := Trans.trans (Trans.trans (W₁.Q.associator W₂'.Q E₃.inverse ≪≫ isoWhiskerRight (compUniqFunctor L₁ W₁.Q W₁).symm (W₂'.Q ⋙ E₃.inverse) ≪≫ L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse)) (isoWhiskerLeft L₁ ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫ isoWhiskerRight (CatCommSq.iso Φ.functor L₂ W₂'.Q (Φ.localizedFunctor L₂ W₂'.Q)) E₃.inverse ≪≫ L₂.associator (Φ.localizedFunctor L₂ W₂'.Q) E₃.inverse))) (isoWhiskerLeft L₁ (isoWhiskerLeft L₂ E₃.unitIso.symm ≪≫ L₂.rightUnitor))<VAR>hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)<VAR>hW₂₃' : W₂' ≤ W₃.map W₁.Q<VAR>this : (W₁.Q ⋙ W₂'.Q).IsLocalization W₃<GOAL>(L₁ ⋙ L₂).IsLocalization W₃
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ 𝟙_ C ◁ (ρ_ X).hom = 𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>𝟙_ C ◁ (β_ (𝟙_ C) X).hom ≫ (α_ (𝟙_ C) X (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).hom ▷ 𝟙_ C ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom = (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>((((α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv) ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C) ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom) ≫ 𝟙_ C ◁ (ρ_ X).hom = (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ (α_ X (𝟙_ C) (𝟙_ C)).inv ≫ (β_ (𝟙_ C) X).inv ▷ 𝟙_ C ≫ (α_ (𝟙_ C) X (𝟙_ C)).hom ≫ 𝟙_ C ◁ (ρ_ X).hom = (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ X ◁ (ρ_ (𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (β_ (𝟙_ C ⊗ 𝟙_ C) X).hom ≫ X ◁ (ρ_ (𝟙_ C)).hom ≫ (β_ (𝟙_ C) X).inv = (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ (𝟙_ C) (𝟙_ C) X).inv ≫ ((ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom) ≫ (β_ (𝟙_ C) X).inv = (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X ≫ (β_ (𝟙_ C) X).hom ≫ (β_ (𝟙_ C) X).inv = (α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(α_ (𝟙_ C) (𝟙_ C) X).inv ≫ (ρ_ (𝟙_ C)).hom ▷ X = 𝟙_ C ◁ (λ_ X).hom
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<VAR>hst : Disjoint s t<GOAL>SeparatedNhds s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space X<VAR>s t : Set X<VAR>hs : IsCompact s<VAR>ht : IsCompact t<VAR>hst : s ×ˢ t ⊆ (diagonal X)ᶜ<GOAL>∃ U V, IsOpen U ∧ IsOpen V ∧ s ⊆ U ∧ t ⊆ V ∧ U ×ˢ V ⊆ (diagonal X)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α β<VAR>f : β → ℝ≥0∞<VAR>g : α → β<VAR>a : α<VAR>hg : Measurable g<VAR>inst✝ : MeasurableSingletonClass β<GOAL>∫⁻ (x : β), f x ∂(deterministic g hg) a = f (g a)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>x : CofiniteTopology X<VAR>s : Set (CofiniteTopology X)<GOAL>s ∈ 𝓝 x ↔ x ∈ s ∧ sᶜ.Finite
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k m n : ℕ<VAR>u v w : R<VAR>hkm : k < m<VAR>hmn : m < n<VAR>a✝ : Nontrivial R<GOAL>(trinomial k m n u v 1).Monic
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j k : ι<VAR>hij : c.Rel i j<VAR>hjk : c.Rel j k<GOAL>d φ i j ≫ fstX φ j k hjk = -fstX φ i j hij ≫ F.d j k
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>F G K : HomologicalComplex C c<VAR>φ : F ⟶ G<VAR>inst✝¹ : HasHomotopyCofiber φ<VAR>inst✝ : DecidableRel c.Rel<VAR>i j : ι<VAR>hij : c.Rel i j<VAR>hjk : c.Rel j (c.next j)<GOAL>d φ i j ≫ fstX φ j (c.next j) hjk = -fstX φ i j hij ≫ F.d j (c.next j)
<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>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hg : DifferentiableOn 𝕜 f s<GOAL>DifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 g s
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>injectiveSeminorm x = ⨆ p, ↑p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>n : ℕ<VAR>ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i<VAR>q : α<GOAL>q ∣ p ^ (n + 1) ↔ ∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>n : ℕ<VAR>ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i<VAR>q : α<VAR>h : q ∣ p ^ (n + 1)<GOAL>∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>n : ℕ<VAR>ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i<VAR>q : α<VAR>h : q ∣ p * p ^ n<GOAL>∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>n : ℕ<VAR>ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i<VAR>q : α<VAR>h : p * q ∣ p * p ^ n<GOAL>∃ i, i ≤ n + 1 ∧ p * q ~ᵤ p ^ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>n : ℕ<VAR>ih : ∀ {q : α}, q ∣ p ^ n ↔ ∃ i, i ≤ n ∧ q ~ᵤ p ^ i<VAR>q : α<VAR>h : q ∣ p * p ^ n<VAR>hno : q ∣ p ^ n<GOAL>∃ i, i ≤ n + 1 ∧ q ~ᵤ p ^ i