ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Ioo b c = Ioo (a - c) (a - b)
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>s : Set ℝ≥0∞<VAR>hf : ∀ r ∈ s, r ≠ ⊤<GOAL>(sSup s).toReal = sSup (ENNReal.toReal '' s)
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{?u.103744}<VAR>h0 : 0 < o<VAR>a : (Quotient.out o).α<GOAL>0 < type fun x x_1 => x < x_1
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>h0 : 0 < o<VAR>a : (Quotient.out o).α<GOAL>enum (fun x x_1 => x < x_1) 0 ⋯ ≤ a
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<VAR>h0 : 0 < o<VAR>a : (Quotient.out o).α<GOAL>¬a < enum (fun x x_1 => x < x_1) 0 ⋯
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<VAR>c : E<GOAL>↑↑↑((condexpL2 𝕜 𝕜 hm) (Memℒp.toLp (fun a => ⟪c, ↑↑f a⟫_𝕜) ⋯)) =ᶠ[ae μ] fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<VAR>c : E<VAR>h_mem_Lp : Memℒp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) 2 μ<GOAL>↑↑↑((condexpL2 𝕜 𝕜 hm) (Memℒp.toLp (fun a => ⟪c, ↑↑f a⟫_𝕜) ⋯)) =ᶠ[ae μ] fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<VAR>c : E<VAR>h_mem_Lp : Memℒp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) 2 μ<VAR>h_eq : ↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) h_mem_Lp) =ᶠ[ae μ] fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜<GOAL>↑↑↑((condexpL2 𝕜 𝕜 hm) (Memℒp.toLp (fun a => ⟪c, ↑↑f a⟫_𝕜) ⋯)) =ᶠ[ae μ] fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<VAR>c : E<VAR>h_mem_Lp : Memℒp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) 2 μ<VAR>h_eq : ↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) h_mem_Lp) =ᶠ[ae μ] fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜<GOAL>↑↑↑((condexpL2 𝕜 𝕜 hm) (Memℒp.toLp (fun a => ⟪c, ↑↑f a⟫_𝕜) ⋯)) =ᶠ[ae μ] ↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) h_mem_Lp)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<VAR>c : E<VAR>h_mem_Lp : Memℒp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) 2 μ<VAR>h_eq : ↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) h_mem_Lp) =ᶠ[ae μ] fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) h_mem_Lp)) s μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<VAR>c : E<VAR>h_mem_Lp : Memℒp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) 2 μ<VAR>h_eq : ↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) h_mem_Lp) =ᶠ[ae μ] fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜<GOAL>∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑((condexpL2 𝕜 𝕜 hm) (Memℒp.toLp (fun a => ⟪c, ↑↑f a⟫_𝕜) ⋯)) x ∂μ = ∫ (x : α) in s, ↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) h_mem_Lp) x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<VAR>c : E<VAR>h_mem_Lp : Memℒp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) 2 μ<VAR>h_eq : ↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) h_mem_Lp) =ᶠ[ae μ] fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜<GOAL>AEStronglyMeasurable' m (↑↑↑((condexpL2 𝕜 𝕜 hm) (Memℒp.toLp (fun a => ⟪c, ↑↑f a⟫_𝕜) ⋯))) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹³ : RCLike 𝕜<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁰ : CompleteSpace E<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : InnerProductSpace 𝕜 E'<VAR>inst✝⁷ : CompleteSpace E'<VAR>inst✝⁶ : NormedSpace ℝ E'<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace ℝ G'<VAR>inst✝ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>hm : m ≤ m0<VAR>f : ↥(Lp E 2 μ)<VAR>c : E<VAR>h_mem_Lp : Memℒp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) 2 μ<VAR>h_eq : ↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) h_mem_Lp) =ᶠ[ae μ] fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜<GOAL>AEStronglyMeasurable' m (↑↑(Memℒp.toLp (fun a => ⟪c, ↑↑↑((condexpL2 E 𝕜 hm) f) a⟫_𝕜) h_mem_Lp)) μ
<VAR>p q✝ : ℚ<VAR>q : ℚ≥0<VAR>hp : 0 ≤ p<GOAL>q ≤ p.toNNRat ↔ ↑q ≤ p
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>f g : Perm α<VAR>hf : f ∈ g.cycleFactorsFinset<GOAL>(g * f⁻¹).cycleType + f.cycleType = g.cycleType - f.cycleType + f.cycleType
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s✝ : Rel β β<VAR>s : RelSeries r<VAR>x : α<VAR>hs : s.length = 0<VAR>i j : Fin (s.length + 1)<GOAL>i = j
<GOAL>(γ - Real.log (4 * π)) / 2 ≠ 0
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>x y : F<GOAL>eval y (basisDivisor x y) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R<GOAL>basicOpen f = ⊥ ↔ IsNilpotent f
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R<GOAL>(zeroLocus {f})ᶜ = ↑⊥ ↔ IsNilpotent f
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R<GOAL>(∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), J.IsPrime → f ∈ J
<VAR>a b c : Ordinal.{u}<VAR>h : c.IsLimit<GOAL>a < b + c ↔ ∃ c' < c, a < b + c'
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>α : Type u_4<VAR>inst✝⁷ : Fintype l<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A : Matrix m m α<VAR>B : Matrix m n α<VAR>C : Matrix n m α<VAR>D : Matrix n n α<VAR>inst✝ : Invertible D<VAR>this : fromBlocks A B C D = (fromBlocks D C B A).submatrix ⇑(Equiv.sumComm m n) ⇑(Equiv.sumComm m n)<GOAL>(fromBlocks A B C D).det = D.det * (A - B * ⅟D * C).det
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<GOAL>p.leadingCoeff ≠ 0 ↔ p ≠ 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : Integrable f μ<GOAL>∃ x, f x ≤ ∫ (a : α), f a ∂μ
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>u : Rˣ<VAR>v : Module.Ray R M<VAR>this : 0 < ↑u * ↑u<GOAL>(u * u) • u⁻¹ • v = u • v
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>A : Matrix m n R<GOAL>(Aᴴ * A).PosSemidef
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>A : Matrix m n R<VAR>x : n → R<GOAL>0 ≤ star x ⬝ᵥ (Aᴴ * A) *ᵥ x
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>R : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : Fintype n<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : PartialOrder R<VAR>inst✝² : StarRing R<VAR>inst✝¹ : StarOrderedRing R<VAR>inst✝ : RCLike 𝕜<VAR>A : Matrix m n R<VAR>x : n → R<GOAL>0 ≤ star (A *ᵥ x) ⬝ᵥ A *ᵥ x
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T✝ T' T : Set α → β<VAR>T_empty : T ∅ = 0<VAR>h_add : FinMeasAdditive μ T<VAR>ι : Type u_8<VAR>S : ι → Set α<VAR>sι : Finset ι<VAR>hS_meas : ∀ (i : ι), MeasurableSet (S i)<GOAL>(∀ i ∈ sι, μ (S i) ≠ ⊤) → (∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T✝ T' T : Set α → β<VAR>T_empty : T ∅ = 0<VAR>h_add : FinMeasAdditive μ T<VAR>ι : Type u_8<VAR>S : ι → Set α<VAR>sι : Finset ι<VAR>hS_meas : ∀ (i : ι), MeasurableSet (S i)<GOAL>(∀ i ∈ ∅, μ (S i) ≠ ⊤) → (∀ i ∈ ∅, ∀ j ∈ ∅, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ ∅, S i) = ∑ i ∈ ∅, T (S i)
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T✝ T' T : Set α → β<VAR>T_empty : T ∅ = 0<VAR>h_add : FinMeasAdditive μ T<VAR>ι : Type u_8<VAR>S : ι → Set α<VAR>sι : Finset ι<VAR>hS_meas : ∀ (i : ι), MeasurableSet (S i)<GOAL>∀ ⦃a : ι⦄ {s : Finset ι}, a ∉ s → ((∀ i ∈ s, μ (S i) ≠ ⊤) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)) → (∀ i ∈ insert a s, μ (S i) ≠ ⊤) → (∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T✝ T' T : Set α → β<VAR>T_empty : T ∅ = 0<VAR>h_add : FinMeasAdditive μ T<VAR>ι : Type u_8<VAR>S : ι → Set α<VAR>sι : Finset ι<VAR>hS_meas : ∀ (i : ι), MeasurableSet (S i)<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>h : (∀ i ∈ s, μ (S i) ≠ ⊤) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)<VAR>hps : ∀ i ∈ insert a s, μ (S i) ≠ ⊤<VAR>h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)<GOAL>T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T✝ T' T : Set α → β<VAR>T_empty : T ∅ = 0<VAR>h_add : FinMeasAdditive μ T<VAR>ι : Type u_8<VAR>S : ι → Set α<VAR>sι : Finset ι<VAR>hS_meas : ∀ (i : ι), MeasurableSet (S i)<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>h : (∀ i ∈ s, μ (S i) ≠ ⊤) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)<VAR>hps : ∀ i ∈ insert a s, μ (S i) ≠ ⊤<VAR>h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)<GOAL>T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T✝ T' T : Set α → β<VAR>T_empty : T ∅ = 0<VAR>h_add : FinMeasAdditive μ T<VAR>ι : Type u_8<VAR>S : ι → Set α<VAR>sι : Finset ι<VAR>hS_meas : ∀ (i : ι), MeasurableSet (S i)<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>h : (∀ i ∈ s, μ (S i) ≠ ⊤) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)<VAR>hps : ∀ i ∈ insert a s, μ (S i) ≠ ⊤<VAR>h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)<GOAL>∀ i ∈ s, μ (S i) ≠ ⊤
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T✝ T' T : Set α → β<VAR>T_empty : T ∅ = 0<VAR>h_add : FinMeasAdditive μ T<VAR>ι : Type u_8<VAR>S : ι → Set α<VAR>sι : Finset ι<VAR>hS_meas : ∀ (i : ι), MeasurableSet (S i)<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>h : (∀ i ∈ s, μ (S i) ≠ ⊤) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)<VAR>hps : ∀ i ∈ insert a s, μ (S i) ≠ ⊤<VAR>h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)<GOAL>∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T✝ T' T : Set α → β<VAR>T_empty : T ∅ = 0<VAR>h_add : FinMeasAdditive μ T<VAR>ι : Type u_8<VAR>S : ι → Set α<VAR>sι : Finset ι<VAR>hS_meas : ∀ (i : ι), MeasurableSet (S i)<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>h : (∀ i ∈ s, μ (S i) ≠ ⊤) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)<VAR>hps : ∀ i ∈ insert a s, μ (S i) ≠ ⊤<VAR>h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)<GOAL>T (⋃ i ∈ insert a s, S i) = T (S a ∪ ⋃ i ∈ s, S i)
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T✝ T' T : Set α → β<VAR>T_empty : T ∅ = 0<VAR>h_add : FinMeasAdditive μ T<VAR>ι : Type u_8<VAR>S : ι → Set α<VAR>sι : Finset ι<VAR>hS_meas : ∀ (i : ι), MeasurableSet (S i)<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>h : (∀ i ∈ s, μ (S i) ≠ ⊤) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)<VAR>hps : ∀ i ∈ insert a s, μ (S i) ≠ ⊤<VAR>h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)<GOAL>μ (⋃ i ∈ s, S i) ≠ ⊤
<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>β : Type u_7<VAR>inst✝ : AddCommMonoid β<VAR>T✝ T' T : Set α → β<VAR>T_empty : T ∅ = 0<VAR>h_add : FinMeasAdditive μ T<VAR>ι : Type u_8<VAR>S : ι → Set α<VAR>sι : Finset ι<VAR>hS_meas : ∀ (i : ι), MeasurableSet (S i)<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>h : (∀ i ∈ s, μ (S i) ≠ ⊤) → (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)<VAR>hps : ∀ i ∈ insert a s, μ (S i) ≠ ⊤<VAR>h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)<GOAL>S a ∩ ⋃ i ∈ s, S i = ∅
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 1 ∨ a ≠ 0<GOAL>DifferentiableAt ℂ (expZeta a) s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 1 ∨ a ≠ 0<GOAL>DifferentiableAt ℂ (cosZeta a) s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : s ≠ 1 ∨ a ≠ 0<GOAL>DifferentiableAt ℂ (fun y => I * sinZeta a y) s
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x<VAR>huv' : IntegrableOn (u * v') (Iic a) volume<VAR>hu'v : IntegrableOn (u' * v) (Iic a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atBot (𝓝 b')<GOAL>∫ (x : ℝ) in Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x<VAR>huv' : IntegrableOn (fun i => u i * v' i) (Iic a) volume<VAR>hu'v : IntegrableOn (fun i => u' i * v i) (Iic a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atBot (𝓝 b')<GOAL>∫ (x : ℝ) in Iic a, u x * v' x = a' - b' - ∫ (x : ℝ) in Iic a, u' x * v x
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x<VAR>huv' : IntegrableOn (fun i => u i * v' i) (Iic a) volume<VAR>hu'v : IntegrableOn (fun i => u' i * v i) (Iic a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atBot (𝓝 b')<GOAL>∫ (a : ℝ) in Iic a, u a * v' a + u' a * v a ∂volume = a' - b'
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝² : (ofArrows X c.inj).hasPullbacks<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>this : HasCoproduct X<VAR>h : (Pi.lift fun i => F.map (c.inj i).op) = F.map (Pi.lift fun i => (c.inj i).op) ≫ piComparison F fun i => op (X i)<GOAL>(piComparison F fun x => op (X x)) = F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Pi.lift fun i => F.map (c.inj i).op