ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>inst✝ : SeminormedCommGroup A<VAR>a : A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hn : 0 < n<VAR>han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n<VAR>f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b => ⟨a * ↑b, ⋯⟩<VAR>hf : Surjective f<GOAL>⋃ i, ⋃ (_ : orderOf i = n), ball (a * i) δ = ⋃ x, ⋃ (_ : orderOf x = n), ball x δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝¹³ : TopologicalSpace α<VAR>inst✝¹² : MeasurableSpace α<VAR>inst✝¹¹ : OpensMeasurableSpace α<VAR>inst✝¹⁰ : TopologicalSpace β<VAR>inst✝⁹ : MeasurableSpace β<VAR>inst✝⁸ : OpensMeasurableSpace β<VAR>inst✝⁷ : TopologicalSpace γ<VAR>inst✝⁶ : MeasurableSpace γ<VAR>inst✝⁵ : BorelSpace γ<VAR>inst✝⁴ : TopologicalSpace γ₂<VAR>inst✝³ : MeasurableSpace γ₂<VAR>inst✝² : BorelSpace γ₂<VAR>inst✝¹ : MeasurableSpace δ<VAR>inst✝ : R1Space γ<VAR>K : Set γ<VAR>hK : IsCompact K<VAR>μ : Measure γ<GOAL>μ (closure K) = μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝¹³ : TopologicalSpace α<VAR>inst✝¹² : MeasurableSpace α<VAR>inst✝¹¹ : OpensMeasurableSpace α<VAR>inst✝¹⁰ : TopologicalSpace β<VAR>inst✝⁹ : MeasurableSpace β<VAR>inst✝⁸ : OpensMeasurableSpace β<VAR>inst✝⁷ : TopologicalSpace γ<VAR>inst✝⁶ : MeasurableSpace γ<VAR>inst✝⁵ : BorelSpace γ<VAR>inst✝⁴ : TopologicalSpace γ₂<VAR>inst✝³ : MeasurableSpace γ₂<VAR>inst✝² : BorelSpace γ₂<VAR>inst✝¹ : MeasurableSpace δ<VAR>inst✝ : R1Space γ<VAR>K : Set γ<VAR>hK : IsCompact K<VAR>μ : Measure γ<GOAL>μ (closure K) ≤ μ K
<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 α<VAR>inst✝ : DecidableEq M<GOAL>(f.update a b).support ⊆ insert a f.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✝² : Zero M<VAR>f : α →₀ M<VAR>a : α<VAR>b : M<VAR>i : α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq M<GOAL>(if b = 0 then f.support.erase a else insert a f.support) ⊆ insert a f.support
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>IsLocalization.Away f ↑Γ(X, X.basicOpen f)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>IsLocalization (Submonoid.powers f) ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>e_1✝ : ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring<GOAL>(asIso (hU.basicOpenSectionsToAffine f)).commRingCatIsoToRingEquiv.toRingHom.comp (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) = StructureSheaf.toOpen (↑Γ(X, U)) (unop (op (PrimeSpectrum.basicOpen f)))
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>e_1✝ : ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring<GOAL>CommRingCat.ofHom (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ≫ CommRingCat.ofHom (hU.basicOpenSectionsToAffine f) = StructureSheaf.toOpen (↑Γ(X, U)) (unop (op (PrimeSpectrum.basicOpen f)))
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>e_1✝ : ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring<GOAL>X.presheaf.map (homOfLE ⋯).op ≫ hU.basicOpenSectionsToAffine f = StructureSheaf.toOpen (↑Γ(X, U)) (PrimeSpectrum.basicOpen f)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>e_1✝ : ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring<GOAL>X.presheaf.map (homOfLE ⋯).op ≫ hU.fromSpec.val.c.app (op (X.basicOpen f)) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op = StructureSheaf.toOpen (↑Γ(X, U)) (PrimeSpectrum.basicOpen f)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>e_1✝ : ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring<GOAL>((Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op) ≫ (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.val.base).map (homOfLE ⋯).op.unop).op ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op = StructureSheaf.toOpen (↑Γ(X, U)) (PrimeSpectrum.basicOpen f)
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>e_1✝ : ↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) = ↑((structureSheaf ↑Γ(X, U)).val.obj (op (PrimeSpectrum.basicOpen f)))<VAR>he✝ : CommRing.toCommSemiring = CommRing.toCommSemiring<GOAL>(Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯ ≫ (Opens.map hU.fromSpec.val.base).map (homOfLE ⋯).op.unop ≫ eqToHom ⋯).op = StructureSheaf.toOpen (↑Γ(X, U)) (PrimeSpectrum.basicOpen f)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>g : F ≃ₗᵢ[𝕜] G<VAR>f : E → F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<GOAL>‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>g : F ≃ₗᵢ[𝕜] G<VAR>f : E → F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<VAR>this : iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑{ toLinearEquiv := g.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)<GOAL>‖iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>g : F ≃ₗᵢ[𝕜] G<VAR>f : E → F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>i : ℕ<VAR>this : iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑{ toLinearEquiv := g.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)<GOAL>‖(↑{ toLinearEquiv := g.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖
<VAR>b : Bool<VAR>n : ℕ<VAR>h : n = 0 → b = true<VAR>ih : n.bits.length = n.size<GOAL>(bit b n).bits.length = (bit b n).size
<VAR>b : Bool<VAR>n : ℕ<VAR>h : n = 0 → b = true<VAR>ih : n.bits.length = n.size<GOAL>(b :: n.bits).length = n.size.succ
<VAR>b : Bool<VAR>n : ℕ<VAR>h : n = 0 → b = true<VAR>ih : n.bits.length = n.size<GOAL>bit b n ≠ 0
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>a : G<GOAL>of' k G a /ᵒᶠ a = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y z : F<GOAL>⟪x, y + z⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y z : F<GOAL>(starRingEnd 𝕜) ⟪y, x⟫_𝕜 + (starRingEnd 𝕜) ⟪z, x⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>sublistsLen (n + 1) (a :: l) <+ (a :: l).sublists'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>sublistsLen (n + 1) l ++ map (cons a) (sublistsLen n l) <+ l.sublists' ++ map (cons a) l.sublists'
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedCommGroup α<VAR>m n : ℤ<VAR>a✝ b✝ : α<VAR>hn : 0 ≤ n<VAR>a b : α<VAR>hab : a ≤ b<GOAL>(fun x => x ^ n) a ≤ (fun x => x ^ n) b
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : OrderedCommGroup α<VAR>m n : ℤ<VAR>a✝ b✝ : α<VAR>hn : 0 ≤ n<VAR>a b : α<VAR>hab : a ≤ b<GOAL>1 ≤ (b / a) ^ n
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : EnoughInjectives C<VAR>Z : C<VAR>n : ℕ<GOAL>HomologicalComplex.ExactAt (ofCocomplex Z) (n + 1)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : EnoughInjectives C<VAR>Z : C<VAR>n : ℕ<GOAL>(HomologicalComplex.sc' (ofCocomplex Z) n (n + 1) (n + 1 + 1)).Exact
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : EnoughInjectives C<VAR>Z : C<VAR>n : ℕ<GOAL>(ShortComplex.mk ((CochainComplex.of (fun n => (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).X₁) (fun n => (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).f) ⋯).d n (n + 1)) ((CochainComplex.of (fun n => (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).X₁) (fun n => (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).f) ⋯).d (n + 1) (n + 1 + 1)) ⋯).Exact
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>inst✝ : EnoughInjectives C<VAR>Z : C<VAR>n : ℕ<GOAL>(ShortComplex.mk (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) n).f (CochainComplex.mkAux (under Z) (syzygies (Injective.ι Z)) (syzygies (d (Injective.ι Z))) (d (Injective.ι Z)) (d (d (Injective.ι Z))) ⋯ (fun S => ⟨syzygies S.g, ⟨d S.g, ⋯⟩⟩) (n + 1)).f ⋯).Exact
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ✝ : Type u_6<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : DecidableEq ι<VAR>κ : ι → Type u_7<VAR>s : Finset ι<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<GOAL>(s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ✝ : Type u_6<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : DecidableEq ι<VAR>κ : ι → Type u_7<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<GOAL>(∅.inf fun i => (t i).sup (f i)) = (∅.pi t).sup fun g => ∅.attach.inf fun i => f (↑i) (g ↑i ⋯)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ✝ : Type u_6<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : DecidableEq ι<VAR>κ : ι → Type u_7<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)<GOAL>((insert i s).inf fun i => (t i).sup (f i)) = ((insert i s).pi t).sup fun g => (insert i s).attach.inf fun i_1 => f (↑i_1) (g ↑i_1 ⋯)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ✝ : Type u_6<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : DecidableEq ι<VAR>κ : ι → Type u_7<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)<GOAL>((t i ×ˢ s.pi t).sup fun i_1 => f i i_1.1 ⊓ s.attach.inf fun i_2 => f (↑i_2) (i_1.2 ↑i_2 ⋯)) = ((insert i s).pi t).sup fun g => (insert ⟨i, ⋯⟩ (image (fun x => ⟨↑x, ⋯⟩) s.attach)).inf fun i_1 => f (↑i_1) (g ↑i_1 ⋯)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ✝ : Type u_6<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : DecidableEq ι<VAR>κ : ι → Type u_7<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)<VAR>c : α<GOAL>((t i ×ˢ s.pi t).sup fun i_1 => f i i_1.1 ⊓ s.attach.inf fun i_2 => f (↑i_2) (i_1.2 ↑i_2 ⋯)) ≤ c ↔ (((insert i s).pi t).sup fun g => (insert ⟨i, ⋯⟩ (image (fun x => ⟨↑x, ⋯⟩) s.attach)).inf fun i_1 => f (↑i_1) (g ↑i_1 ⋯)) ≤ c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ✝ : Type u_6<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : DecidableEq ι<VAR>κ : ι → Type u_7<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)<VAR>c : α<GOAL>(∀ (a : κ i) (b : (a : ι) → a ∈ s → κ a), a ∈ t i → (∀ (a : ι) (h : a ∈ s), b a h ∈ t a) → (f i a ⊓ s.attach.inf fun i => f (↑i) (b ↑i ⋯)) ≤ c) ↔ ∀ (b : (a : ι) → a ∈ insert i s → κ a), (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) → f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 => f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x => ⟨↑x, ⋯⟩) ≤ c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ✝ : Type u_6<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : DecidableEq ι<VAR>κ : ι → Type u_7<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)<VAR>c : α<VAR>h : ∀ (b : (a : ι) → a ∈ insert i s → κ a), (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) → f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 => f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x => ⟨↑x, ⋯⟩) ≤ c<VAR>a : κ i<VAR>g : (a : ι) → a ∈ s → κ a<VAR>ha : a ∈ t i<VAR>hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a<GOAL>(f i a ⊓ s.attach.inf fun i => f (↑i) (g ↑i ⋯)) ≤ c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ✝ : Type u_6<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : DecidableEq ι<VAR>κ : ι → Type u_7<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)<VAR>c : α<VAR>h : ∀ (b : (a : ι) → a ∈ insert i s → κ a), (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) → f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 => f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x => ⟨↑x, ⋯⟩) ≤ c<VAR>a : κ i<VAR>g : (a : ι) → a ∈ s → κ a<VAR>ha : a ∈ t i<VAR>hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a<VAR>aux : ∀ (j : { x // x ∈ s }), ↑j ≠ i<GOAL>(f i a ⊓ s.attach.inf fun i => f (↑i) (g ↑i ⋯)) ≤ c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ✝ : Type u_6<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : DecidableEq ι<VAR>κ : ι → Type u_7<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)<VAR>c : α<VAR>h : ∀ (b : (a : ι) → a ∈ insert i s → κ a), (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) → f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 => f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x => ⟨↑x, ⋯⟩) ≤ c<VAR>a : κ i<VAR>g : (a : ι) → a ∈ s → κ a<VAR>ha : a ∈ t i<VAR>hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a<VAR>aux : ∀ (j : { x // x ∈ s }), ↑j ≠ i<VAR>this : f i ((fun j hj => if hji : j = i then cast ⋯ a else g j ⋯) i ⋯) ⊓ s.attach.inf ((fun i_1 => f (↑i_1) ((fun j hj => if hji : j = i then cast ⋯ a else g j ⋯) ↑i_1 ⋯)) ∘ fun x => ⟨↑x, ⋯⟩) ≤ c<GOAL>(f i a ⊓ s.attach.inf fun i => f (↑i) (g ↑i ⋯)) ≤ c
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ✝ : Type u_6<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : DecidableEq ι<VAR>κ : ι → Type u_7<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)<VAR>c : α<VAR>h : ∀ (b : (a : ι) → a ∈ insert i s → κ a), (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) → f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 => f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x => ⟨↑x, ⋯⟩) ≤ c<VAR>a : κ i<VAR>g : (a : ι) → a ∈ s → κ a<VAR>ha : a ∈ t i<VAR>hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a<VAR>aux : ∀ (j : { x // x ∈ s }), ↑j ≠ i<VAR>j : ι<VAR>hj : j ∈ insert i s<GOAL>(fun j hj => if hji : j = i then cast ⋯ a else g j ⋯) j hj ∈ t j
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ✝ : Type u_6<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : BoundedOrder α<VAR>inst✝ : DecidableEq ι<VAR>κ : ι → Type u_7<VAR>t : (i : ι) → Finset (κ i)<VAR>f : (i : ι) → κ i → α<VAR>i : ι<VAR>s : Finset ι<VAR>hi : i ∉ s<VAR>ih : (s.inf fun i => (t i).sup (f i)) = (s.pi t).sup fun g => s.attach.inf fun i => f (↑i) (g ↑i ⋯)<VAR>c : α<VAR>h : ∀ (b : (a : ι) → a ∈ insert i s → κ a), (∀ (a : ι) (h : a ∈ insert i s), b a h ∈ t a) → f i (b i ⋯) ⊓ s.attach.inf ((fun i_1 => f (↑i_1) (b ↑i_1 ⋯)) ∘ fun x => ⟨↑x, ⋯⟩) ≤ c<VAR>a : κ i<VAR>g : (a : ι) → a ∈ s → κ a<VAR>ha : a ∈ t i<VAR>hg : ∀ (a : ι) (h : a ∈ s), g a h ∈ t a<VAR>aux : ∀ (j : { x // x ∈ s }), ↑j ≠ i<VAR>j : ι<VAR>hj✝ : j ∈ insert i s<VAR>hj : j = i ∨ j ∈ s<GOAL>(fun j hj => if hji : j = i then cast ⋯ a else g j ⋯) j hj✝ ∈ t j
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>ε : ℝ<GOAL>volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>ε : ℝ<VAR>hT' : |T| = T<GOAL>volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>ε : ℝ<VAR>hT' : |T| = T<VAR>I : Set ℝ := Ioc (-(T / 2)) (T / 2)<GOAL>volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>ε : ℝ<VAR>hT' : |T| = T<VAR>I : Set ℝ := Ioc (-(T / 2)) (T / 2)<VAR>h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε<GOAL>volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>ε : ℝ<VAR>hT' : |T| = T<VAR>I : Set ℝ := Ioc (-(T / 2)) (T / 2)<VAR>h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε<VAR>h₂ : QuotientAddGroup.mk ⁻¹' Metric.closedBall 0 ε ∩ I = if ε < T / 2 then Metric.closedBall 0 ε else I<GOAL>volume (Metric.closedBall x ε) = ENNReal.ofReal (min T (2 * ε))
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>x : AddCircle T<VAR>ε : ℝ<VAR>hT' : |T| = T<VAR>I : Set ℝ := Ioc (-(T / 2)) (T / 2)<VAR>h₁ : ε < T / 2 → Metric.closedBall 0 ε ∩ I = Metric.closedBall 0 ε<VAR>h₂ : QuotientAddGroup.mk ⁻¹' Metric.closedBall 0 ε ∩ I = if ε < T / 2 then Metric.closedBall 0 ε else I<GOAL>volume (if ε < T / 2 then Metric.closedBall 0 ε else I) = ENNReal.ofReal (min T (2 * ε))
<VAR>θ : Angle<GOAL>-θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ ↑π
<VAR>z τ : ℂ<GOAL>(Summable fun x => jacobiTheta₂_term x z τ) ↔ 0 < τ.im
<VAR>z τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>Summable fun x => jacobiTheta₂_term x z τ
<VAR>z τ : ℂ<VAR>h : Summable fun x => jacobiTheta₂_term x z τ<GOAL>0 < τ.im
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>inst✝ : DecidableRel R<VAR>l : List α<GOAL>pwFilter R l = l ↔ Pairwise R l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>inst✝ : DecidableRel R<VAR>l : List α<VAR>p : Pairwise R l<GOAL>pwFilter R l = l
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G₁ : A ⥤ C<VAR>G₂ : C ⥤ E<VAR>H₁ : B ⥤ D<VAR>H₂ : D ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : E ⥤ F<VAR>R₃ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁<VAR>β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂<VAR>b : B<GOAL>({ toFun := fun α => whiskerLeft (R₁ ⋙ G₁ ⋙ G₂) adj₃.unit ≫ whiskerRight (whiskerLeft R₁ α) R₃ ≫ whiskerRight adj₁.counit ((H₁ ⋙ H₂) ⋙ R₃), invFun := fun β => whiskerRight adj₁.unit ((G₁ ⋙ G₂) ⋙ L₃) ≫ whiskerRight (whiskerLeft L₁ β) L₃ ≫ whiskerLeft (L₁ ⋙ H₁ ⋙ H₂) adj₃.counit, left_inv := ⋯, right_inv := ⋯ } (whiskerLeft G₁ β ≫ whiskerRight α H₂)).app b = (whiskerRight ({ toFun := fun α => whiskerLeft (R₁ ⋙ G₁) adj₂.unit ≫ whiskerRight (whiskerLeft R₁ α) R₂ ≫ whiskerRight adj₁.counit (H₁ ⋙ R₂), invFun := fun β => whiskerRight adj₁.unit (G₁ ⋙ L₂) ≫ whiskerRight (whiskerLeft L₁ β) L₂ ≫ whiskerLeft (L₁ ⋙ H₁) adj₂.counit, left_inv := ⋯, right_inv := ⋯ } α) G₂ ≫ whiskerLeft H₁ ({ toFun := fun α => whiskerLeft (R₂ ⋙ G₂) adj₃.unit ≫ whiskerRight (whiskerLeft R₂ α) R₃ ≫ whiskerRight adj₂.counit (H₂ ⋙ R₃), invFun := fun β => whiskerRight adj₂.unit (G₂ ⋙ L₃) ≫ whiskerRight (whiskerLeft L₂ β) L₃ ≫ whiskerLeft (L₂ ⋙ H₂) adj₃.counit, left_inv := ⋯, right_inv := ⋯ } β)).app b
<VAR>A : Type u₁<VAR>B : Type u₂<VAR>C : Type u₃<VAR>D : Type u₄<VAR>E : Type u₅<VAR>F : Type u₆<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>inst✝³ : Category.{v₃, u₃} C<VAR>inst✝² : Category.{v₄, u₄} D<VAR>inst✝¹ : Category.{v₅, u₅} E<VAR>inst✝ : Category.{v₆, u₆} F<VAR>G₁ : A ⥤ C<VAR>G₂ : C ⥤ E<VAR>H₁ : B ⥤ D<VAR>H₂ : D ⥤ F<VAR>L₁ : A ⥤ B<VAR>R₁ : B ⥤ A<VAR>L₂ : C ⥤ D<VAR>R₂ : D ⥤ C<VAR>L₃ : E ⥤ F<VAR>R₃ : F ⥤ E<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>adj₃ : L₃ ⊣ R₃<VAR>α : G₁ ⋙ L₂ ⟶ L₁ ⋙ H₁<VAR>β : G₂ ⋙ L₃ ⟶ L₂ ⋙ H₂<VAR>b : B<GOAL>adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫ R₃.map (β.app (G₁.obj (R₁.obj b))) ≫ R₃.map (H₂.map (α.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) = G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.app (R₁.obj b))) ≫ G₂.map (R₂.map (H₁.map (adj₁.counit.app b))) ≫ adj₃.unit.app (G₂.obj (R₂.obj (H₁.obj b))) ≫ R₃.map (β.app (R₂.obj (H₁.obj b))) ≫ R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))