ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Inhabited F.M<VAR>bisim : IsBisimulation R<VAR>ps : List F.Idx<VAR>ps_ih : ∀ (a : F.A) (f f' : F.B a → F.M), R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) → (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧ ∃ a_1 f_1 f'_1, isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)<VAR>a : F.A<VAR>f f' : F.B a → F.M<VAR>h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)<VAR>i : F.B a<VAR>hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)<VAR>h₁ : R (f i) (f' i)<VAR>a₀ : F.A<VAR>f₀ : F.B a₀ → F.M<VAR>h : f i = M.mk ⟨a₀, f₀⟩<VAR>a₁ : F.A<VAR>f₁ : F.B a₁ → F.M<VAR>h' : f' i = M.mk ⟨a₁, f₁⟩<GOAL>(isubtree ps (M.mk ⟨a₀, f₀⟩)).head = (isubtree ps (M.mk ⟨a₁, f₁⟩)).head ∧ ∃ a f f', isubtree ps (M.mk ⟨a₀, f₀⟩) = M.mk ⟨a, f⟩ ∧ isubtree ps (M.mk ⟨a₁, f₁⟩) = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Inhabited F.M<VAR>bisim : IsBisimulation R<VAR>ps : List F.Idx<VAR>ps_ih : ∀ (a : F.A) (f f' : F.B a → F.M), R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) → (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧ ∃ a_1 f_1 f'_1, isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)<VAR>a : F.A<VAR>f f' : F.B a → F.M<VAR>h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)<VAR>i : F.B a<VAR>hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)<VAR>a₀ : F.A<VAR>f₀ : F.B a₀ → F.M<VAR>h : f i = M.mk ⟨a₀, f₀⟩<VAR>a₁ : F.A<VAR>f₁ : F.B a₁ → F.M<VAR>h₁ : R (M.mk ⟨a₀, f₀⟩) (M.mk ⟨a₁, f₁⟩)<VAR>h' : f' i = M.mk ⟨a₁, f₁⟩<GOAL>(isubtree ps (M.mk ⟨a₀, f₀⟩)).head = (isubtree ps (M.mk ⟨a₁, f₁⟩)).head ∧ ∃ a f f', isubtree ps (M.mk ⟨a₀, f₀⟩) = M.mk ⟨a, f⟩ ∧ isubtree ps (M.mk ⟨a₁, f₁⟩) = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Inhabited F.M<VAR>bisim : IsBisimulation R<VAR>ps : List F.Idx<VAR>ps_ih : ∀ (a : F.A) (f f' : F.B a → F.M), R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) → (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧ ∃ a_1 f_1 f'_1, isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)<VAR>a : F.A<VAR>f f' : F.B a → F.M<VAR>h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)<VAR>i : F.B a<VAR>hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)<VAR>a₀ : F.A<VAR>f₀ : F.B a₀ → F.M<VAR>h : f i = M.mk ⟨a₀, f₀⟩<VAR>f₁ : F.B a₀ → F.M<VAR>h₁ : R (M.mk ⟨a₀, f₀⟩) (M.mk ⟨a₀, f₁⟩)<VAR>h' : f' i = M.mk ⟨a₀, f₁⟩<GOAL>(isubtree ps (M.mk ⟨a₀, f₀⟩)).head = (isubtree ps (M.mk ⟨a₀, f₁⟩)).head ∧ ∃ a f f', isubtree ps (M.mk ⟨a₀, f₀⟩) = M.mk ⟨a, f⟩ ∧ isubtree ps (M.mk ⟨a₀, f₁⟩) = M.mk ⟨a, f'⟩ ∧ ∀ (i : F.B a), R (f i) (f' i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>R : F.M → F.M → Prop<VAR>inst✝ : Inhabited F.M<VAR>bisim : IsBisimulation R<VAR>ps : List F.Idx<VAR>ps_ih : ∀ (a : F.A) (f f' : F.B a → F.M), R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) → IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) → (isubtree ps (M.mk ⟨a, f⟩)).head = (isubtree ps (M.mk ⟨a, f'⟩)).head ∧ ∃ a_1 f_1 f'_1, isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧ isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)<VAR>a : F.A<VAR>f f' : F.B a → F.M<VAR>h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)<VAR>i : F.B a<VAR>hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)<VAR>a₀ : F.A<VAR>f₀ : F.B a₀ → F.M<VAR>h : f i = M.mk ⟨a₀, f₀⟩<VAR>f₁ : F.B a₀ → F.M<VAR>h₁ : R (M.mk ⟨a₀, f₀⟩) (M.mk ⟨a₀, f₁⟩)<VAR>h' : f' i = M.mk ⟨a₀, f₁⟩<GOAL>IsPath ps (f i) ∨ IsPath ps (f' i)
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<GOAL>J.toSheafify (P ⋙ F) ≫ (J.sheafifyCompIso F P).inv = whiskerRight (J.toSheafify P) F
<VAR>C : Type u<VAR>inst✝⁸ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w₁<VAR>inst✝⁷ : Category.{max v u, w₁} D<VAR>E : Type w₂<VAR>inst✝⁶ : Category.{max v u, w₂} E<VAR>F : D ⥤ E<VAR>inst✝⁵ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D<VAR>inst✝⁴ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E<VAR>inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E<VAR>inst✝¹ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ F<VAR>inst✝ : (X : C) → (W : J.Cover X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (W.index P).multicospan F<VAR>P : Cᵒᵖ ⥤ D<GOAL>J.toSheafify (P ⋙ F) = whiskerRight (J.toSheafify P) F ≫ (J.sheafifyCompIso F P).hom
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<GOAL>GrowsPolynomially fun x => ‖deriv (fun z => z ^ p * (1 + ε z)) x‖
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : V<VAR>nz : v ≠ 0<VAR>h : finrank K V = 1<GOAL>span K {v} = ⊤
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : V<VAR>nz : v ≠ 0<VAR>s : span K {v} = ⊤<GOAL>⊤ ≤ span K (Set.range fun x => ↑x)
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : V<VAR>nz : v ≠ 0<VAR>s : span K {v} = ⊤<GOAL>(Set.range fun x => ↑x) = {v}
<VAR>x✝ y : ℝ<VAR>x : ℝ≥0<GOAL>↑(NNReal.sqrt x) = √↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝³ : SFinite μ<VAR>inst✝² : IsSFiniteKernel κ<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α × β → E<VAR>hf : Integrable f (μ ⊗ₘ κ)<GOAL>∫ (x : α × β), f x ∂μ ⊗ₘ κ = ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝³ : SFinite μ<VAR>inst✝² : IsSFiniteKernel κ<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α × β → E<VAR>hf : Integrable f (μ ⊗ₘ κ)<GOAL>∫ (x : α), ∫ (y : β), f (x, y) ∂(Kernel.prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () = ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t : Set α<VAR>f g : α → β<VAR>s : Set α<VAR>h : ∀ a ∈ s, f a = g a<VAR>x : β<GOAL>x ∈ f '' s ↔ x ∈ g '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ✝ : Measure α<VAR>p✝ : ℝ≥0∞<VAR>p : ℝ<VAR>f : α →ₛ F<VAR>μ : Measure α<VAR>h_map : (fun a => ↑‖↑f a‖₊ ^ p) = ↑(map (fun a => ↑‖a‖₊ ^ p) f)<GOAL>eLpNorm' (↑f) p μ = (∑ y ∈ f.range, ↑‖y‖₊ ^ p * μ (↑f ⁻¹' {y})) ^ (1 / p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>i : σ<GOAL>constantCoeff (X i) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<VAR>hgf : UniformInducing (g ∘ f)<GOAL>UniformInducing f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<VAR>hgf : UniformInducing (g ∘ f)<GOAL>comap (fun x => (f x.1, f x.2)) (𝓤 β) ≤ 𝓤 α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : α → β<VAR>g : β → γ<VAR>hf : UniformContinuous f<VAR>hg : UniformContinuous g<VAR>hgf : UniformInducing (g ∘ f)<GOAL>comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>hs : IsIntegral R s<VAR>p : R[X]<VAR>hp0 : p ≠ 0<VAR>hp : (Polynomial.aeval s) p = 0<GOAL>(minpoly R s).degree ≤ p.degree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>hs : IsIntegral R s<VAR>p : R[X]<VAR>hp0 : p ≠ 0<VAR>hp : (Polynomial.aeval s) p = 0<GOAL>↑(minpoly R s).natDegree ≤ ↑p.natDegree
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>s : S<VAR>hs : IsIntegral R s<VAR>p : R[X]<VAR>hp0 : p ≠ 0<VAR>hp : (Polynomial.aeval s) p = 0<GOAL>(minpoly R s).natDegree ≤ p.natDegree
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U : X.Opens<VAR>x : ↥U<GOAL>Function.Injective ⇑(X.presheaf.germ x)
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U : X.Opens<VAR>x : ↥U<GOAL>∀ (a : ↑(X.presheaf.obj (op U))), (X.presheaf.germ x) a = 0 → a = 0
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U : X.Opens<VAR>x : ↥U<VAR>y : ↑(X.presheaf.obj (op U))<VAR>hy : (X.presheaf.germ x) y = 0<GOAL>y = 0
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U : X.Opens<VAR>x : ↥U<VAR>y : ↑(X.presheaf.obj (op U))<VAR>hy : (X.presheaf.germ x) y = (X.presheaf.germ x) 0<GOAL>y = 0
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U : X.Opens<VAR>x : ↥U<VAR>y : ↑(X.presheaf.obj (op U))<VAR>hy : (X.presheaf.germ x) y = (X.presheaf.germ x) 0<VAR>W : Opens ↑↑X.toPresheafedSpace<VAR>hW : ↑x ∈ W<VAR>iU iV : W ⟶ U<VAR>e : (X.presheaf.map iU.op) y = (X.presheaf.map iV.op) 0<GOAL>y = 0
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U : X.Opens<VAR>x : ↥U<VAR>y : ↑(X.presheaf.obj (op U))<VAR>hy : (X.presheaf.germ x) y = (X.presheaf.germ x) 0<VAR>W : Opens ↑↑X.toPresheafedSpace<VAR>hW : ↑x ∈ W<VAR>iU : W ⟶ U<VAR>e : (X.presheaf.map iU.op) y = (X.presheaf.map iU.op) 0<GOAL>y = 0
<VAR>X : Scheme<VAR>inst✝ : IsIntegral X<VAR>U : X.Opens<VAR>x : ↥U<VAR>y : ↑(X.presheaf.obj (op U))<VAR>hy : (X.presheaf.germ x) y = (X.presheaf.germ x) 0<VAR>W : Opens ↑↑X.toPresheafedSpace<VAR>hW : ↑x ∈ W<VAR>iU : W ⟶ U<VAR>e : (X.presheaf.map iU.op) y = (X.presheaf.map iU.op) 0<VAR>this : Nonempty ↑↑(↑W).toPresheafedSpace<GOAL>y = 0
<GOAL>sin (↑π / 2) = ↑(Real.sin (π / 2))
<GOAL>sin (↑π / 2) = sin ↑(π / 2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>Ω✝ : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : CountablyGenerated γ<VAR>inst✝⁵ : MeasurableSpace Ω✝<VAR>inst✝⁴ : StandardBorelSpace Ω✝<VAR>inst✝³ : Nonempty Ω✝<VAR>Ω : Type u_5<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : StandardBorelSpace Ω<VAR>η : Kernel α ℝ<VAR>a : α<GOAL>(borelMarkovFromReal Ω η) a = if (η a) (range (embeddingReal Ω))ᶜ = 0 then Measure.comap (embeddingReal Ω) (η a) else Measure.comap (embeddingReal Ω) (Measure.dirac (Exists.choose ⋯))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{?u.21810, u_1} C<VAR>inst✝⁹ : Category.{?u.21814, u_2} D<VAR>inst✝⁸ : Category.{?u.21818, u_3} E<VAR>inst✝⁷ : HasShift C ℤ<VAR>inst✝⁶ : HasShift D ℤ<VAR>inst✝⁵ : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝⁴ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝³ : G.CommShift ℤ<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>inst✝ : F.Additive<VAR>n : ℤ<VAR>T : Triangle C<GOAL>(F.map (n.negOnePow • (shiftFunctor C n).map T.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app T.obj₁) ≫ (F.commShiftIso 1).hom.app ((shiftFunctor C n).obj T.obj₁)) ≫ (shiftFunctor D 1).map ((F.commShiftIso n).hom.app T.obj₁) = (F.commShiftIso n).hom.app T.obj₃ ≫ (n.negOnePow • (shiftFunctor D n).map (F.map T.mor₃ ≫ (F.commShiftIso 1).hom.app T.obj₁) ≫ (shiftFunctorComm D 1 n).hom.app (F.obj T.obj₁))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{?u.21810, u_1} C<VAR>inst✝⁹ : Category.{?u.21814, u_2} D<VAR>inst✝⁸ : Category.{?u.21818, u_3} E<VAR>inst✝⁷ : HasShift C ℤ<VAR>inst✝⁶ : HasShift D ℤ<VAR>inst✝⁵ : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝⁴ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝³ : G.CommShift ℤ<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>inst✝ : F.Additive<VAR>n : ℤ<VAR>T : Triangle C<GOAL>n.negOnePow • F.map ((shiftFunctor C n).map T.mor₃) ≫ F.map ((shiftFunctorComm C 1 n).hom.app T.obj₁) ≫ (F.commShiftIso 1).hom.app ((shiftFunctor C n).obj T.obj₁) ≫ (shiftFunctor D 1).map ((F.commShiftIso n).hom.app T.obj₁) = n.negOnePow • F.map ((shiftFunctor C n).map T.mor₃) ≫ (F.commShiftIso n).hom.app ((shiftFunctor C 1).obj T.obj₁) ≫ (shiftFunctor D n).map ((F.commShiftIso 1).hom.app T.obj₁) ≫ (shiftFunctorComm D 1 n).hom.app (F.obj T.obj₁)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>inst✝¹⁰ : Category.{?u.21810, u_1} C<VAR>inst✝⁹ : Category.{?u.21814, u_2} D<VAR>inst✝⁸ : Category.{?u.21818, u_3} E<VAR>inst✝⁷ : HasShift C ℤ<VAR>inst✝⁶ : HasShift D ℤ<VAR>inst✝⁵ : HasShift E ℤ<VAR>F : C ⥤ D<VAR>inst✝⁴ : F.CommShift ℤ<VAR>G : D ⥤ E<VAR>inst✝³ : G.CommShift ℤ<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>inst✝ : F.Additive<VAR>n : ℤ<VAR>T : Triangle C<GOAL>n.negOnePow • F.map ((shiftFunctor C n).map T.mor₃) ≫ ((F.commShiftIso n).hom.app ((shiftFunctor C 1).obj T.obj₁) ≫ (shiftFunctor D n).map ((F.commShiftIso 1).hom.app T.obj₁) ≫ (shiftFunctorComm D 1 n).hom.app (F.obj T.obj₁) ≫ (shiftFunctor D 1).map ((F.commShiftIso n).inv.app T.obj₁) ≫ (F.commShiftIso 1).inv.app ((shiftFunctor C n).obj T.obj₁)) ≫ (F.commShiftIso 1).hom.app ((shiftFunctor C n).obj T.obj₁) ≫ (shiftFunctor D 1).map ((F.commShiftIso n).hom.app T.obj₁) = n.negOnePow • F.map ((shiftFunctor C n).map T.mor₃) ≫ (F.commShiftIso n).hom.app ((shiftFunctor C 1).obj T.obj₁) ≫ (shiftFunctor D n).map ((F.commShiftIso 1).hom.app T.obj₁) ≫ (shiftFunctorComm D 1 n).hom.app (F.obj T.obj₁)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionSemiring α<VAR>q r : ℚ≥0<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<VAR>hp_pair : Integrable (↑(f.pair g)) μ<GOAL>setToSimpleFunc T (f + g) = ∑ x ∈ (f.pair g).range, (T (↑(f.pair g) ⁻¹' {x})) (x.1 + x.2)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<VAR>hp_pair : Integrable (↑(f.pair g)) μ<GOAL>0.1 + 0.2 = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<VAR>hp_pair : Integrable (↑(f.pair g)) μ<GOAL>∑ x ∈ (f.pair g).range, ((T (↑(f.pair g) ⁻¹' {x})) x.1 + (T (↑(f.pair g) ⁻¹' {x})) x.2) = ∑ x ∈ (f.pair g).range, (T (↑(f.pair g) ⁻¹' {x})) x.1 + ∑ x ∈ (f.pair g).range, (T (↑(f.pair g) ⁻¹' {x})) x.2
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T : Set α → E →L[ℝ] F<VAR>h_add : FinMeasAdditive μ T<VAR>f g : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>hg : Integrable (↑g) μ<VAR>hp_pair : Integrable (↑(f.pair g)) μ<GOAL>∑ x ∈ (f.pair g).range, (T (↑(f.pair g) ⁻¹' {x})) x.1 + ∑ x ∈ (f.pair g).range, (T (↑(f.pair g) ⁻¹' {x})) x.2 = setToSimpleFunc T (map Prod.fst (f.pair g)) + setToSimpleFunc T (map Prod.snd (f.pair g))
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<GOAL>{i | x₀ ∈ tsupport ⇑(ρ i)}.Finite
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>t : Set X<VAR>t_in : t ∈ 𝓝 x₀<VAR>ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite<GOAL>{i | x₀ ∈ tsupport ⇑(ρ i)}.Finite
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>t : Set X<VAR>t_in : t ∈ 𝓝 x₀<VAR>ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite<GOAL>{i | x₀ ∈ tsupport ⇑(ρ i)} ⊆ {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>t : Set X<VAR>t_in : t ∈ 𝓝 x₀<VAR>ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite<VAR>i : ι<VAR>hi : i ∈ {i | x₀ ∈ tsupport ⇑(ρ i)}<GOAL>i ∈ {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀ : X<VAR>t : Set X<VAR>t_in : t ∈ 𝓝 x₀<VAR>ht : {i | ((fun i => support ⇑(ρ i)) i ∩ t).Nonempty}.Finite<VAR>i : ι<VAR>hi : i ∈ {i | x₀ ∈ tsupport ⇑(ρ i)}<GOAL>i ∈ {i | (t ∩ support ⇑(ρ i)).Nonempty}
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DistribLattice α<VAR>x y z : α<VAR>h₁ : x ⊓ z ≤ y ⊓ z<VAR>h₂ : x ⊔ z ≤ y ⊔ z<GOAL>y ⊓ z ⊔ x = (y ⊔ x) ⊓ (x ⊔ z)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : DistribLattice α<VAR>x y z : α<VAR>h₁ : x ⊓ z ≤ y ⊓ z<VAR>h₂ : x ⊔ z ≤ y ⊔ z<GOAL>(y ⊔ x) ⊓ (y ⊔ z) = y ⊔ x ⊓ z
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>n : Type w<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : Fintype n<VAR>P A : Matrix n n R<VAR>h : Invertible P<GOAL>(P.lieConj h) A = P * A * P⁻¹
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u<VAR>S : Type v<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>s : Set σ<GOAL>supported R s = (rename Subtype.val).range
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u<VAR>S : Type v<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>s : Set σ<GOAL>(aeval fun x => X ↑x).range = (aeval (X ∘ Subtype.val)).range
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>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>N₂ : LieSubmodule R L M₂<VAR>x : ↥I<VAR>m : ↥N<GOAL>⁅↑x, ↑m⁆ ∈ ⁅I, N⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>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>N₂ : LieSubmodule R L M₂<VAR>x : ↥I<VAR>m : ↥N<GOAL>⁅↑x, ↑m⁆ ∈ lieSpan R L {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>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>N₂ : LieSubmodule R L M₂<VAR>x : ↥I<VAR>m : ↥N<GOAL>⁅↑x, ↑m⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K1 K2 : Compacts X<GOAL>rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K1 K2 : Compacts X<GOAL>∀ (ε : ℝ≥0), 0 < ε → rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K1 K2 : Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<GOAL>rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K1 K2 : Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>f1 : X →ᵇ ℝ≥0<VAR>f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2<GOAL>rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>Λ : (X →ᵇ ℝ≥0) →ₗ[ℝ≥0] ℝ≥0<VAR>K1 K2 : Compacts X<VAR>ε : ℝ≥0<VAR>εpos : 0 < ε<VAR>f1 : X →ᵇ ℝ≥0<VAR>f_test_function_K1 : (∀ x ∈ K1, 1 ≤ f1 x) ∧ Λ f1 < rieszContentAux Λ K1 + ε / 2<VAR>f2 : X →ᵇ ℝ≥0<VAR>f_test_function_K2 : (∀ x ∈ K2, 1 ≤ f2 x) ∧ Λ f2 < rieszContentAux Λ K2 + ε / 2<GOAL>rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2 + ε