ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>N : Subgroup G<VAR>n : N.Normal<VAR>s : Set G<VAR>s_op : IsOpen s<GOAL>IsOpen (mk ⁻¹' (mk '' s))
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>N : Subgroup G<VAR>n : N.Normal<VAR>s : Set G<VAR>s_op : IsOpen s<GOAL>IsOpen (⋃ x, (fun x_1 => x_1 * ↑x) ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s : Finset β<VAR>h : (mulSupport f).Finite<GOAL>Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s : Finset β<VAR>h : (mulSupport f).Finite<GOAL>∀ b ∉ h.toFinset, f b = 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option α<VAR>l : List α<VAR>acc : Array α<GOAL>go f l acc = acc.toListAppend (lookmap f l)
<VAR>n m : ℕ<VAR>hmn : m ≤ n<VAR>a b : Fin m<GOAL>castLE hmn a = castLE hmn b ↔ a = b
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<VAR>δ : ℝ<VAR>δ0 : 0 < δ<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>δ' : ℝ := δ / (↑π₀.boxes.card + 1)<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>δ' : ℝ := δ / (↑π₀.boxes.card + 1)<VAR>H0 : 0 < ↑π₀.boxes.card + 1<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>δ' : ℝ := δ / (↑π₀.boxes.card + 1)<VAR>H0 : 0 < ↑π₀.boxes.card + 1<VAR>δ'0 : 0 < δ'<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>δ' : ℝ := δ / (↑π₀.boxes.card + 1)<VAR>H0 : 0 < ↑π₀.boxes.card + 1<VAR>δ'0 : 0 < δ'<VAR>C : ℝ≥0 := max π₀.distortion π₀.compl.distortion<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>δ' : ℝ := δ / (↑π₀.boxes.card + 1)<VAR>H0 : 0 < ↑π₀.boxes.card + 1<VAR>δ'0 : 0 < δ'<VAR>C : ℝ≥0 := max π₀.distortion π₀.compl.distortion<VAR>this : ∀ J ∈ π₀, ∃ πi, πi.IsPartition ∧ dist (integralSum f vol πi) (integral J l f vol) ≤ δ' ∧ l.MemBaseSet J C (h.convergenceR δ' C) πi<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>δ' : ℝ := δ / (↑π₀.boxes.card + 1)<VAR>H0 : 0 < ↑π₀.boxes.card + 1<VAR>δ'0 : 0 < δ'<VAR>C : ℝ≥0 := max π₀.distortion π₀.compl.distortion<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>hπip : ∀ J ∈ π₀, (πi J).IsPartition<VAR>hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'<VAR>hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>δ' : ℝ := δ / (↑π₀.boxes.card + 1)<VAR>H0 : 0 < ↑π₀.boxes.card + 1<VAR>δ'0 : 0 < δ'<VAR>C : ℝ≥0 := max π₀.distortion π₀.compl.distortion<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>hπip : ∀ J ∈ π₀, (πi J).IsPartition<VAR>hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'<VAR>hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)<VAR>this : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>δ' : ℝ := δ / (↑π₀.boxes.card + 1)<VAR>H0 : 0 < ↑π₀.boxes.card + 1<VAR>δ'0 : 0 < δ'<VAR>C : ℝ≥0 := max π₀.distortion π₀.compl.distortion<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>hπip : ∀ J ∈ π₀, (πi J).IsPartition<VAR>hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'<VAR>hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)<VAR>this : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)<VAR>hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>δ' : ℝ := δ / (↑π₀.boxes.card + 1)<VAR>H0 : 0 < ↑π₀.boxes.card + 1<VAR>δ'0 : 0 < δ'<VAR>C : ℝ≥0 := max π₀.distortion π₀.compl.distortion<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>hπip : ∀ J ∈ π₀, (πi J).IsPartition<VAR>hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'<VAR>hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)<VAR>this✝ : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)<VAR>hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion<VAR>this : dist (integralSum f vol π) (integralSum f vol (π₀.biUnionTagged πi)) ≤ ε + δ'<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝¹ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c c₁ c₂ : ℝ≥0<VAR>ε ε₁ ε₂ : ℝ<VAR>π₁ π₂ : TaggedPrepartition I<VAR>inst✝ : CompleteSpace F<VAR>h : Integrable I l f vol<VAR>h0 : 0 < ε<VAR>hπ : l.MemBaseSet I c (h.convergenceR ε c) π<VAR>π₀ : Prepartition I<VAR>hU : π.iUnion = π₀.iUnion<VAR>δ : ℝ<VAR>δ0 : 0 < δ<VAR>δ' : ℝ := δ / (↑π₀.boxes.card + 1)<VAR>H0 : 0 < ↑π₀.boxes.card + 1<VAR>δ'0 : 0 < δ'<VAR>C : ℝ≥0 := max π₀.distortion π₀.compl.distortion<VAR>πi : (J : Box ι) → TaggedPrepartition J<VAR>hπip : ∀ J ∈ π₀, (πi J).IsPartition<VAR>hπiδ' : ∀ J ∈ π₀, dist (integralSum f vol (πi J)) (integral J l f vol) ≤ δ'<VAR>hπiC : ∀ J ∈ π₀, l.MemBaseSet J C (h.convergenceR δ' C) (πi J)<VAR>this✝ : l.MemBaseSet I C (h.convergenceR δ' C) (π₀.biUnionTagged πi)<VAR>hU' : π.iUnion = (π₀.biUnionTagged πi).iUnion<VAR>this : dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integralSum f vol (πi J)) ≤ ε + δ'<GOAL>dist (integralSum f vol π) (∑ J ∈ π₀.boxes, integral J l f vol) ≤ ε + δ
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝¹ : TopologicalSpace X<VAR>ι' : Sort u_6<VAR>inst✝ : Mul M<VAR>ts : ι' → TopologicalSpace M<VAR>h' : ∀ (i : ι'), ContinuousMul M<GOAL>ContinuousMul M
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>n : γ → δ<VAR>m' : α' → β' → δ<VAR>n₁ : α → α'<VAR>n₂ : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)<GOAL>map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝³ : Group G<VAR>inst✝² : PseudoMetricSpace G<VAR>inst✝¹ : IsometricSMul G G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b c : G<GOAL>dist (a / b) (a / c) = dist b c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>h : ω ≤ o<GOAL>1 + o = o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Lattice α<VAR>a b c a₁ a₂ b₁ b₂ : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>Icc a b ∩ Icc b c = {b}
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.61855, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<VAR>φ : S₁ ⟶ S₂<VAR>hg₁ : S₁.g = 0<VAR>c₁ : CokernelCofork S₁.f<VAR>hc₁ : IsColimit c₁<VAR>hg₂ : S₂.g = 0<VAR>c₂ : CokernelCofork S₂.f<VAR>hc₂ : IsColimit c₂<VAR>f : c₁.pt ⟶ c₂.pt<VAR>comm : φ.τ₂ ≫ Cofork.π c₂ = Cofork.π c₁ ≫ f<GOAL>(LeftHomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁).f' ≫ φ.τ₂ = φ.τ₁ ≫ (LeftHomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂).f'
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Ring α<VAR>inst✝¹ : AddCommGroup β<VAR>inst✝ : Module α β<VAR>a : α<VAR>s : Set α<VAR>t : Set β<GOAL>-a • t = -(a • t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : ι → Set α<VAR>hs : IndexedPartition s<VAR>x : α<GOAL>x ∈ ⋃ i, s i ↔ x ∈ univ
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>a : α<VAR>ha : IsAtom a<VAR>haS : a ≤ sSup S<GOAL>a ∈ S
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T : Set α<VAR>hT : T ⊆ S<VAR>ha : IsAtom (sSup T)<VAR>haS : sSup T ≤ sSup S<GOAL>sSup T ∈ S
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>hT : ∅ ⊆ S<VAR>ha : IsAtom (sSup ∅)<VAR>haS : sSup ∅ ≤ sSup S<GOAL>sSup ∅ ∈ S
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T : Set α<VAR>hT : T ⊆ S<VAR>ha : IsAtom (sSup T)<VAR>haS : sSup T ≤ sSup S<VAR>a : α<VAR>haT : a ∈ T<GOAL>sSup T ∈ S
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T : Set α<VAR>hT : T ⊆ S<VAR>ha : IsAtom (sSup T)<VAR>haS : sSup T ≤ sSup S<VAR>a : α<VAR>haT : a ∈ T<GOAL>sSup T = a
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T : Set α<VAR>hT : T ⊆ S<VAR>ha : IsAtom (sSup T)<VAR>haS : sSup T ≤ sSup S<VAR>a : α<VAR>haT : a ∈ T<VAR>this : a ≤ sSup T<GOAL>sSup T = a
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>S : Set α<VAR>hS : BooleanGenerators S<VAR>T : Set α<VAR>hT : T ⊆ S<VAR>ha : IsAtom (sSup T)<VAR>haS : sSup T ≤ sSup S<VAR>a : α<VAR>haT : a ∈ T<VAR>this : a ≤ sSup T<GOAL>a ≠ ⊥
<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<VAR>inst✝³ : T2Space M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>G : Type u_1<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>g : M → G<VAR>hg : SmoothOn I 𝓘(ℝ, G) g (chartAt H c).source<GOAL>Smooth I 𝓘(ℝ, G) fun x => ↑f x • g x
<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x✝ : M<VAR>inst✝³ : T2Space M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>G : Type u_1<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>g : M → G<VAR>hg : SmoothOn I 𝓘(ℝ, G) g (chartAt H c).source<VAR>x : M<VAR>hx : x ∈ tsupport fun x => ↑f x • g x<GOAL>ContMDiffAt I 𝓘(ℝ, G) ⊤ (fun x => ↑f x • g x) x
<VAR>E : Type uE<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝⁷ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝⁶ : TopologicalSpace M<VAR>inst✝⁵ : ChartedSpace H M<VAR>inst✝⁴ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x✝ : M<VAR>inst✝³ : T2Space M<VAR>inst✝² : SmoothManifoldWithCorners I M<VAR>G : Type u_1<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>g : M → G<VAR>hg : SmoothOn I 𝓘(ℝ, G) g (chartAt H c).source<VAR>x : M<VAR>hx : x ∈ tsupport fun x => ↑f x • g x<VAR>this : x ∈ (chartAt H c).source<GOAL>ContMDiffAt I 𝓘(ℝ, G) ⊤ (fun x => ↑f x • g x) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hY : AEMeasurable Y μ<VAR>hf : AEStronglyMeasurable f (Measure.map (fun a => (X a, Y a)) μ)<GOAL>(∀ᵐ (a : β) ∂Measure.map X μ, Integrable (fun ω => f (a, ω)) ((condDistrib Y X μ) a)) ∧ Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂(condDistrib Y X μ) a) (Measure.map X μ) ↔ Integrable f (Measure.map (fun a => (X a, Y a)) μ)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.4689, u_1} C<VAR>inst✝ : Category.{?u.4693, u_2} D<VAR>F : C ⥤ Cat<VAR>X : Grothendieck F<GOAL>(F.map (𝟙 X.base)).obj X.fiber = X.fiber
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>a : α<VAR>ha : 0 < a<VAR>b c : α<GOAL>∃! m, b - m • a ∈ Ico c (c + a)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>K₁ K₂ : Cofork I.fstSigmaMap I.sndSigmaMap<VAR>f : K₁ ⟶ K₂<VAR>a✝ : I.L<GOAL>(Multicofork.ofSigmaCofork I K₁).ι.app (WalkingMultispan.left a✝) ≫ f.hom = (Multicofork.ofSigmaCofork I K₂).ι.app (WalkingMultispan.left a✝)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>inst✝¹ : HasCoproduct I.left<VAR>inst✝ : HasCoproduct I.right<VAR>K₁ K₂ : Cofork I.fstSigmaMap I.sndSigmaMap<VAR>f : K₁ ⟶ K₂<VAR>a✝ : I.R<GOAL>(Multicofork.ofSigmaCofork I K₁).ι.app (WalkingMultispan.right a✝) ≫ f.hom = (Multicofork.ofSigmaCofork I K₂).ι.app (WalkingMultispan.right a✝)
<VAR>c : Char<VAR>cs : List Char<VAR>i : Pos<GOAL>{ data := c :: cs }.get (i + c) = { data := cs }.get i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Monoid α<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : DistribMulAction α β<VAR>a : α<VAR>s : Set α<VAR>t : Set β<GOAL>a • -t = -(a • t)
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : ℙ K V<GOAL>finrank K ↥v.submodule = 1
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>v : ℙ K V<GOAL>finrank K ↥(Submodule.span K {v.rep}) = 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>h : HasLineDerivAt 𝕜 f (c • f') x (c • v)<GOAL>HasLineDerivAt 𝕜 f f' x v
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Zero α<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Lattice α<VAR>f g : ι →₀ α<VAR>x✝ : ι<GOAL>x✝ ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support))ᶜ ↔ x✝ ∈ (↑(f.support ∪ g.support))ᶜ
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>s t : Submodule K V<VAR>inst✝¹ : FiniteDimensional K ↥s<VAR>inst✝ : FiniteDimensional K ↥t<GOAL>finrank K ↥(s ⊔ t) ≤ finrank K ↥s + finrank K ↥t
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module K V<VAR>s t : Submodule K V<VAR>inst✝¹ : FiniteDimensional K ↥s<VAR>inst✝ : FiniteDimensional K ↥t<GOAL>finrank K ↥(s ⊔ t) ≤ finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m✝ : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>m : α → β<VAR>hm : Surjective m<GOAL>comap m f = ⊥ ↔ f = ⊥
<VAR>m✝ n m n✝ : ℕ<VAR>a✝ : (m + n✝).bodd = bxor m.bodd n✝.bodd<GOAL>(m + (n✝ + 1)).bodd = bxor m.bodd (n✝ + 1).bodd
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>g' : Z ⟶ W<VAR>inst✝² : HasPushout f g<VAR>inst✝¹ : HasPushout (pushout.inr f g) g'<VAR>inst✝ : HasPushout f (g ≫ g')<GOAL>pushout.inr f g ≫ pushout.inl (pushout.inr f g) g' ≫ (pushoutLeftPushoutInrIso f g g').hom = g' ≫ pushout.inr f (g ≫ g')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : BooleanRing α<VAR>a b : α<GOAL>a + a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : BooleanRing α<VAR>a b : α<VAR>this : a + a = a + a + (a + a)<GOAL>a + a = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>f : (i : ι) → α i → β i<GOAL>(range fun g i => f i (g i)) = univ.pi fun i => range (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>f : (i : ι) → α i → β i<GOAL>(range fun g i => f i (g i)) ⊆ univ.pi fun i => range (f i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i : ι<VAR>f : (i : ι) → α i → β i<VAR>x : (i : ι) → β i<VAR>hx : x ∈ univ.pi fun i => range (f i)<GOAL>x ∈ range fun g i => f i (g i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝² : DecidablePred p<VAR>inst✝¹ : DecidablePred q<VAR>s✝ t : Finset α<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<VAR>x✝ : α<GOAL>x✝ ∈ filter (fun a => p a ∧ q a) s ↔ x✝ ∈ filter p s ∩ filter q s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : NonUnitalNonAssocRing α<VAR>a b c : α<GOAL>a * (b - c) = a * b - a * c
<VAR>α β : SemilatSupCat<VAR>e : α.X ≃o β.X<VAR>x✝ : (forget SemilatSupCat).obj α<GOAL>({ toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 α) x✝
<VAR>α β : SemilatSupCat<VAR>e : α.X ≃o β.X<VAR>x✝ : (forget SemilatSupCat).obj β<GOAL>({ toFun := ⇑e.symm, map_sup' := ⋯, map_bot' := ⋯ } ≫ { toFun := ⇑e, map_sup' := ⋯, map_bot' := ⋯ }) x✝ = (𝟙 β) x✝