ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure γ<VAR>μ' : Measure δ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure μ'<VAR>X : γ → α<VAR>X' : δ → α<VAR>Y : γ → β<VAR>Y' : δ → β<VAR>h_indep : IndepFun X Y μ<VAR>h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'<GOAL>AEMeasurable X μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure γ<VAR>μ' : Measure δ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure μ'<VAR>X : γ → α<VAR>X' : δ → α<VAR>Y : γ → β<VAR>Y' : δ → β<VAR>h_indep : IndepFun X Y μ<VAR>h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'<GOAL>AEMeasurable Y μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure γ<VAR>μ' : Measure δ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure μ'<VAR>X : γ → α<VAR>X' : δ → α<VAR>Y : γ → β<VAR>Y' : δ → β<VAR>h_indep : IndepFun X Y μ<VAR>h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'<GOAL>AEMeasurable X' μ'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace γ<VAR>inst✝² : MeasurableSpace δ<VAR>μ : Measure γ<VAR>μ' : Measure δ<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>inst✝ : IsFiniteMeasure μ'<VAR>X : γ → α<VAR>X' : δ → α<VAR>Y : γ → β<VAR>Y' : δ → β<VAR>h_indep : IndepFun X Y μ<VAR>h_ident : IdentDistrib (fun ω => (X ω, Y ω)) (fun ω => (X' ω, Y' ω)) μ μ'<GOAL>AEMeasurable Y' μ'
<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>ι : Type u_5<VAR>inst✝² : Fintype ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<GOAL>∃ M, 0 < M ∧ ∀ (x : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G), ‖x.1.prod x.2‖ ≤ M * ‖x‖
<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>ι : Type u_5<VAR>inst✝² : Fintype ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G<GOAL>‖p.1.prod p.2‖ ≤ 1 * ‖p‖
<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>ι : Type u_5<VAR>inst✝² : Fintype ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G<GOAL>‖p.1.prod p.2‖ ≤ ‖p‖
<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>ι : Type u_5<VAR>inst✝² : Fintype ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G<GOAL>∀ (m : (i : ι) → E i), ‖(p.1.prod p.2) m‖ ≤ ‖p‖ * ∏ i : ι, ‖m i‖
<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>ι : Type u_5<VAR>inst✝² : Fintype ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<GOAL>‖(p.1.prod p.2) m‖ ≤ ‖p‖ * ∏ i : ι, ‖m i‖
<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>ι : Type u_5<VAR>inst✝² : Fintype ι<VAR>E : ι → Type u_6<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (E i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>p : ContinuousMultilinearMap 𝕜 E F × ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<GOAL>‖(p.1 m, p.2 m).1‖ ≤ ‖p‖ * ∏ i : ι, ‖m i‖ ∧ ‖(p.1 m, p.2 m).2‖ ≤ ‖p‖ * ∏ i : ι, ‖m i‖
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>s : Set (Set α)<VAR>hs : s.Countable<VAR>h : ∀ t ∈ s, NullMeasurableSet t μ<GOAL>NullMeasurableSet (⋃₀ s) μ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s✝ t : Set α<VAR>s : Set (Set α)<VAR>hs : s.Countable<VAR>h : ∀ t ∈ s, NullMeasurableSet t μ<GOAL>NullMeasurableSet (⋃ i ∈ s, i) μ
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f g : R<GOAL>((toBasicOpen R f).comp (algebraMap R (Localization.Away f))) g = (toOpen R (PrimeSpectrum.basicOpen f)) g
<VAR>𝓕 : Type u_1<VAR>α : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹ : SeminormedGroup E<VAR>inst✝ : SeminormedGroup F<VAR>s : Set E<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>a b c : E<GOAL>dist a (b / c) = dist (a * c) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>inst✝ : DenselyOrdered α<GOAL>Ioo a b = ∅ ↔ ¬a < b
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>v : Vector α n<VAR>x : α<GOAL>scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v
<VAR>n : ℕ<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>b : β<VAR>v : Vector α n<VAR>x : α<GOAL>⟨b :: List.scanl f (f b x) ↑v, ⋯⟩ = b ::ᵥ ⟨List.scanl f (f b x) v.toList, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : PseudoMetricSpace α<VAR>π : β → Type u_3<VAR>inst✝¹ : Fintype β<VAR>inst✝ : (b : β) → PseudoMetricSpace (π b)<VAR>f g : (b : β) → π b<VAR>r : ℝ≥0<GOAL>nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<GOAL>(fun z => resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x => 1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>h : (fun z => resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x => 1<GOAL>resolvent a =ᶠ[cobounded 𝕜] fun z => z⁻¹ • resolvent (z⁻¹ • a) 1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>h : (fun z => resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x => 1<VAR>z : 𝕜<VAR>hz : z ∈ {0}ᶜ<GOAL>resolvent a z = z⁻¹ • resolvent (z⁻¹ • a) 1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>h : (fun z => resolvent (z⁻¹ • a) 1) =O[cobounded 𝕜] fun x => 1<VAR>z : 𝕜ˣ<VAR>hz : ↑z ∈ {0}ᶜ<GOAL>resolvent a ↑z = (↑z)⁻¹ • resolvent ((↑z)⁻¹ • a) 1
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Monoid G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>ρ : Representation k G V<VAR>M : Type u_4<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module (MonoidAlgebra k G) M<VAR>g : G<VAR>x : RestrictScalars k (MonoidAlgebra k G) ρ.asModule<GOAL>((ofModule ρ.asModule) g) x = (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm (ρ.asModuleEquiv.symm ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x))))
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Monoid G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>ρ : Representation k G V<VAR>M : Type u_4<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module (MonoidAlgebra k G) M<VAR>g : G<VAR>x : RestrictScalars k (MonoidAlgebra k G) ρ.asModule<GOAL>(RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) (((ofModule ρ.asModule) g) x) = (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm (ρ.asModuleEquiv.symm ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x)))))
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Monoid G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>ρ : Representation k G V<VAR>M : Type u_4<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module (MonoidAlgebra k G) M<VAR>g : G<VAR>x : RestrictScalars k (MonoidAlgebra k G) ρ.asModule<GOAL>(RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm (MonoidAlgebra.single g 1 • (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x)) = (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm (ρ.asModuleEquiv.symm ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x)))))
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.9321, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.9373, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>X : C<VAR>T : ↑(K.sieves (G.obj X))<GOAL>Sieve.functorPushforward G (Sieve.functorPullback G ↑T) ∈ K.sieves (G.obj X)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.9321, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.9373, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>X : C<VAR>T : ↑(K.sieves (G.obj X))<VAR>Y : D<VAR>iYX : Y ⟶ G.obj X<VAR>hiYX : (↑T).arrows iYX<GOAL>Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)) ∈ K.sieves Y
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.9321, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.9373, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>X : C<VAR>T : ↑(K.sieves (G.obj X))<VAR>Y : D<VAR>iYX : Y ⟶ G.obj X<VAR>hiYX : (↑T).arrows iYX<GOAL>∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ Y⦄, (Sieve.coverByImage G Y).arrows f → Sieve.pullback f (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K.sieves Y_1
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.9321, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.9373, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>X : C<VAR>T : ↑(K.sieves (G.obj X))<VAR>Y : D<VAR>iYX : Y ⟶ G.obj X<VAR>hiYX : (↑T).arrows iYX<VAR>W : D<VAR>Z : C<VAR>iWZ : W ⟶ G.obj Z<VAR>iZY : G.obj Z ⟶ Y<GOAL>Sieve.pullback (iWZ ≫ iZY) (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K.sieves W
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.9321, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.9373, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>X : C<VAR>T : ↑(K.sieves (G.obj X))<VAR>Y : D<VAR>iYX : Y ⟶ G.obj X<VAR>hiYX : (↑T).arrows iYX<VAR>W : D<VAR>Z : C<VAR>iWZ : W ⟶ G.obj Z<VAR>iZY : G.obj Z ⟶ Y<GOAL>Sieve.pullback iWZ (Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))) ∈ K.sieves W
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.9321, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.9373, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>X : C<VAR>T : ↑(K.sieves (G.obj X))<VAR>Y : D<VAR>iYX : Y ⟶ G.obj X<VAR>hiYX : (↑T).arrows iYX<VAR>W : D<VAR>Z : C<VAR>iWZ : W ⟶ G.obj Z<VAR>iZY : G.obj Z ⟶ Y<GOAL>Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K.sieves (G.obj Z)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.9321, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.9373, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>X : C<VAR>T : ↑(K.sieves (G.obj X))<VAR>Y : D<VAR>iYX : Y ⟶ G.obj X<VAR>hiYX : (↑T).arrows iYX<VAR>Z : C<VAR>iZY : G.obj Z ⟶ Y<GOAL>Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K.sieves (G.obj Z)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.9321, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.9373, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>X : C<VAR>T : ↑(K.sieves (G.obj X))<VAR>Y : D<VAR>iYX : Y ⟶ G.obj X<VAR>hiYX : (↑T).arrows iYX<VAR>Z : C<VAR>iZY : G.obj Z ⟶ Y<GOAL>Sieve.functorPushforward G (G.imageSieve (iZY ≫ iYX)) ≤ Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_6, u_2} D<VAR>E : Type u_3<VAR>inst✝³ : Category.{?u.9321, u_3} E<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>L : GrothendieckTopology E<VAR>A : Type u_4<VAR>inst✝² : Category.{?u.9373, u_4} A<VAR>G : C ⥤ D<VAR>inst✝¹ : G.IsCoverDense K<VAR>inst✝ : G.IsLocallyFull K<VAR>X : C<VAR>T : ↑(K.sieves (G.obj X))<VAR>Y : D<VAR>iYX : Y ⟶ G.obj X<VAR>hiYX : (↑T).arrows iYX<VAR>Z : C<VAR>iZY : G.obj Z ⟶ Y<VAR>W : D<VAR>V : C<VAR>iVZ : V ⟶ Z<VAR>iWV : W ⟶ G.obj V<VAR>iVX : V ⟶ X<VAR>e : G.map iVX = G.map iVZ ≫ iZY ≫ iYX<GOAL>(Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))).arrows (iWV ≫ G.map iVZ)
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>p : α → Prop<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>h₀ : abs ⟨a, f⟩ = x<VAR>h₁ : ∀ (i : (P F).B a), p (f i)<GOAL>Liftp p x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>p : α → Prop<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>h₀ : abs ⟨a, f⟩ = x<VAR>h₁ : ∀ (i : (P F).B a), p (f i)<GOAL>Subtype.val <$> abs ⟨a, fun i => ⟨f i, ⋯⟩⟩ = x
<VAR>F : Type u → Type u<VAR>q : QPF F<VAR>α : Type u<VAR>p : α → Prop<VAR>x : F α<VAR>a : (P F).A<VAR>f : (P F).B a → α<VAR>h₀ : abs ⟨a, f⟩ = x<VAR>h₁ : ∀ (i : (P F).B a), p (f i)<GOAL>abs ((P F).map Subtype.val ⟨a, fun i => ⟨f i, ⋯⟩⟩) = abs ⟨a, f⟩
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C<VAR>hza : a ≤ z.re<VAR>hzb : z.re ≤ b<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C<VAR>hza : a ≤ z.re<VAR>hzb : z.re ≤ b<GOAL>‖f (z * I * -I)‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C<VAR>hza : a ≤ z.re<VAR>hzb : z.re ≤ b<VAR>H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)<GOAL>‖f (z * I * -I)‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C<VAR>hza : a ≤ z.re<VAR>hzb : z.re ≤ b<VAR>H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)<GOAL>∃ c < π / (b - a), ∃ B, (fun z => f (z * -I)) =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.re|))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z✝ : ℂ<VAR>hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C<VAR>hza : a ≤ z✝.re<VAR>hzb : z✝.re ≤ b<VAR>H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)<VAR>z : ℂ<VAR>hz : z.im = a<GOAL>(z * -I).re = a
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z✝ : ℂ<VAR>hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C<VAR>hza : a ≤ z✝.re<VAR>hzb : z✝.re ≤ b<VAR>H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)<VAR>z : ℂ<VAR>hz : z.im = b<GOAL>(z * -I).re = b
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C<VAR>hza : a ≤ z.re<VAR>hzb : z.re ≤ b<VAR>H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)<GOAL>a ≤ (z * I).im
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hfd : DiffContOnCl ℂ f (re ⁻¹' Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.im|))<VAR>hle_a : ∀ (z : ℂ), z.re = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.re = b → ‖f z‖ ≤ C<VAR>hza : a ≤ z.re<VAR>hzb : z.re ≤ b<VAR>H : MapsTo (fun x => x * -I) (im ⁻¹' Ioo a b) (re ⁻¹' Ioo a b)<GOAL>(z * I).im ≤ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>R' : Type u_4<VAR>S : Type u_5<VAR>S' : Type u_6<VAR>T : Type u_7<VAR>T' : Type u_8<VAR>inst✝² : NonUnitalNonAssocSemiring R<VAR>inst✝¹ : NonUnitalNonAssocSemiring S<VAR>inst✝ : NonUnitalNonAssocSemiring T<VAR>f✝ : R →ₙ+* S<VAR>g : R →ₙ+* T<VAR>f : R →ₙ+* S × T<VAR>x : R<GOAL>(((fst S T).comp f).prod ((snd S T).comp f)) x = f x
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>K L : HomologicalComplex₂ C (up ℤ) (up ℤ)<VAR>f : K ⟶ L<VAR>x y : ℤ<VAR>inst✝¹ : K.HasTotal (up ℤ)<VAR>inst✝ : L.HasTotal (up ℤ)<VAR>n i₁ i₂ : ℤ<VAR>h : i₁ + i₂ = n<GOAL>((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (total.map ((shiftFunctor₂ C y).map f) (up ℤ)).f n ≫ (L.totalShift₂Iso y).hom.f n = ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₂Iso y).hom.f n ≫ (total.map f (up ℤ)).f (n + y)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>K L : HomologicalComplex₂ C (up ℤ) (up ℤ)<VAR>f : K ⟶ L<VAR>x y : ℤ<VAR>inst✝¹ : K.HasTotal (up ℤ)<VAR>inst✝ : L.HasTotal (up ℤ)<VAR>n i₁ i₂ : ℤ<VAR>h : i₁ + i₂ = n<GOAL>(((shiftFunctor₂ C y).map f).f i₁).f i₂ ≫ ((i₁ * y).negOnePow • (L.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) y n (n + y) ⋯).inv) = ((i₁ * y).negOnePow • (K.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv) ≫ (total.map f (up ℤ)).f (n + y)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>K L : HomologicalComplex₂ C (up ℤ) (up ℤ)<VAR>f : K ⟶ L<VAR>x y : ℤ<VAR>inst✝¹ : K.HasTotal (up ℤ)<VAR>inst✝ : L.HasTotal (up ℤ)<VAR>n i₁ i₂ : ℤ<VAR>h : i₁ + i₂ = n<GOAL>(f.f i₁).f (i₂ + y) ≫ ((i₁ * y).negOnePow • 𝟙 ((L.X i₁).X (i₂ + y)) ≫ L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((L.total (up ℤ)).X (n + y))) = ((i₁ * y).negOnePow • 𝟙 ((K.X i₁).X (i₂ + y)) ≫ K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫ 𝟙 ((K.total (up ℤ)).X (n + y))) ≫ (total.map f (up ℤ)).f (n + y)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β✝ : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β✝ i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β✝ ↑i<VAR>i✝ : ι<VAR>f✝ : Π₀ (i : ι), β✝ i<VAR>b✝ : β✝ i✝<VAR>j✝ : ι<VAR>β : ι → Type u_1<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<VAR>j : ι<GOAL>(update i f b) j = (single i b + erase i f) j
<VAR>ι : Type u<VAR>γ : Type w<VAR>β✝ : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β✝ i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β✝ ↑i<VAR>i✝ : ι<VAR>f✝ : Π₀ (i : ι), β✝ i<VAR>b✝ : β✝ i✝<VAR>j : ι<VAR>β : ι → Type u_1<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<GOAL>(update i f b) i = (single i b + erase i f) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β✝ : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β✝ i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β✝ ↑i<VAR>i✝ : ι<VAR>f✝ : Π₀ (i : ι), β✝ i<VAR>b✝ : β✝ i✝<VAR>j✝ : ι<VAR>β : ι → Type u_1<VAR>inst✝ : (i : ι) → AddZeroClass (β i)<VAR>f : Π₀ (i : ι), β i<VAR>i : ι<VAR>b : β i<VAR>j : ι<VAR>h : i ≠ j<GOAL>(update i f b) j = (single i b + erase i f) j