ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<VAR>v : M₁ →SL[σ₁₂] M₂<VAR>hv : v ∈ {f | IsCompactOperator ⇑f}<VAR>huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}<VAR>T : Set M₂<VAR>hT : T.Finite<VAR>hTv : closure (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V<VAR>x : M₁<VAR>hx : x ∈ closedBall 0 1<VAR>t : M₂<VAR>ht : t ∈ T<VAR>htx : x ∈ ⇑v ⁻¹' (t +ᵥ V)<GOAL>x ∈ ⇑u ⁻¹' (t +ᵥ U)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<VAR>v : M₁ →SL[σ₁₂] M₂<VAR>hv : v ∈ {f | IsCompactOperator ⇑f}<VAR>huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}<VAR>T : Set M₂<VAR>hT : T.Finite<VAR>hTv : closure (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V<VAR>x : M₁<VAR>hx : x ∈ closedBall 0 1<VAR>t : M₂<VAR>ht : t ∈ T<VAR>htx : v x - t ∈ V<GOAL>u x - t ∈ U
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<VAR>v : M₁ →SL[σ₁₂] M₂<VAR>hv : v ∈ {f | IsCompactOperator ⇑f}<VAR>huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}<VAR>T : Set M₂<VAR>hT : T.Finite<VAR>hTv : closure (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V<VAR>x : M₁<VAR>hx : x ∈ closedBall 0 1<VAR>t : M₂<VAR>ht : t ∈ T<VAR>htx : v x - t ∈ V<GOAL>u x - t = v x - t + -(v - u) x
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₁<VAR>inst✝⁹ : NormedField 𝕜₂<VAR>σ₁₂ : 𝕜₁ →+* 𝕜₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝⁸ : SeminormedAddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : NormedSpace 𝕜₁ M₁<VAR>inst✝⁵ : Module 𝕜₂ M₂<VAR>inst✝⁴ : UniformSpace M₂<VAR>inst✝³ : UniformAddGroup M₂<VAR>inst✝² : ContinuousConstSMul 𝕜₂ M₂<VAR>inst✝¹ : T2Space M₂<VAR>inst✝ : CompleteSpace M₂<VAR>u : M₁ →SL[σ₁₂] M₂<VAR>hu : ∀ U ∈ 𝓝 0, ∃ y ∈ {f | IsCompactOperator ⇑f}, y - u ∈ U<VAR>U : Set M₂<VAR>hU : U ∈ 𝓝 0<VAR>V : Set M₂<VAR>hV : V ∈ 𝓝 0<VAR>hVU : ∀ v ∈ V, ∀ w ∈ V, v + w ∈ U<VAR>SV : Set M₁ × Set M₂ := (closedBall 0 1, -V)<VAR>v : M₁ →SL[σ₁₂] M₂<VAR>hv : v ∈ {f | IsCompactOperator ⇑f}<VAR>huv : v - u ∈ {f | ∀ x ∈ SV.1, f x ∈ SV.2}<VAR>T : Set M₂<VAR>hT : T.Finite<VAR>hTv : closure (⇑↑v '' closedBall 0 1) ⊆ ⋃ y ∈ T, y +ᵥ V<VAR>x : M₁<VAR>hx : x ∈ closedBall 0 1<VAR>t : M₂<VAR>ht : t ∈ T<VAR>htx : v x - t ∈ V<GOAL>u x - t = v x - t + -(v x - u x)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>h : μ ≪ ν<VAR>s : Set α<GOAL>μ.restrict s ≪ ν.restrict s
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>h : μ ≪ ν<VAR>s t : Set α<VAR>ht : MeasurableSet t<VAR>htν : (ν.restrict s) t = 0<GOAL>(μ.restrict s) t = 0
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>h : μ ≪ ν<VAR>s t : Set α<VAR>ht : MeasurableSet t<VAR>htν : ν (t ∩ s) = 0<GOAL>μ (t ∩ s) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Finset α<GOAL>¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s✝ s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ : ℕ∞<VAR>f : M → M'<VAR>inst✝ : One M'<VAR>x : M<VAR>hx : x ∉ mulTSupport f<VAR>n : ℕ∞<VAR>s : Set M<GOAL>ContMDiffWithinAt I I' n f s x
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hS : S ∈ leftTransversals ↑H<VAR>g : G<GOAL>((↑(toFun hS g))⁻¹ * g)⁻¹ = g⁻¹ * ↑(toFun hS g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : DecidableEq α<VAR>f : α × β →₀ M<GOAL>f.curry.support ⊆ image Prod.fst f.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : DecidableEq α<VAR>f : α × β →₀ M<GOAL>f.curry.support ⊆ f.support.biUnion fun a => {a.1}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : DecidableEq α<VAR>f : α × β →₀ M<GOAL>(f.support.biUnion fun a => (single a.1 (single a.2 (f a))).support) ⊆ f.support.biUnion fun a => {a.1}
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>A F G : Cᵒᵖ ⥤ Type v<VAR>η : F ⟶ A<VAR>μ : G ⟶ A<VAR>ε : F ⟶ G<VAR>hε : ε ≫ μ = η<VAR>X : C<VAR>s : yoneda.obj X ⟶ A<VAR>u : F.obj (op X)<VAR>h : MakesOverArrow η s u<GOAL>μ.app (op X) (ε.app (op X) u) = yonedaEquiv s
<VAR>α : Type u_1<VAR>l l₁ l₂ : List α<VAR>p : α → Prop<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>l₁ ∩ l₂ = [] ↔ l₁.Disjoint l₂
<VAR>α : Type u_1<VAR>l l₁ l₂ : List α<VAR>p : α → Prop<VAR>a : α<VAR>inst✝ : DecidableEq α<GOAL>(∀ (a : α), a ∈ l₁ → ¬a ∈ l₂) ↔ l₁.Disjoint l₂
<VAR>α : Type u_1<VAR>n : ℕ<VAR>val : α<GOAL>replicate (n + 1) val = (replicate n val).snoc val
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : R →+* S<VAR>x y : 𝕎 R<VAR>n : ℤ<GOAL>mapFun (⇑f) n.castDef = ↑n
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : NonUnitalSemiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : Fintype m<VAR>v : m → α<VAR>M : Matrix m n α<VAR>N : Matrix n o α<VAR>x✝ : o<GOAL>(v ᵥ* M ᵥ* N) x✝ = (v ᵥ* (M * N)) x✝
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a)<VAR>h : (↑x).1 = (↑y).1<GOAL>a = (↑x).1 • (↑x).2
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>s : Set G<VAR>t : Set P<VAR>a : P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsCancelSMul G P<VAR>x y : ↑(s.smulAntidiagonal t a)<VAR>h : (↑x).2 = (↑y).2<GOAL>a = (↑x).1 • (↑x).2
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>x ∈ ball y ε ↔ y ∈ ball x ε
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>P : Type u_7<VAR>inst✝¹ : Mul M<VAR>inst✝ : Monoid N<VAR>a₁ a₂ : M<GOAL>(a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>s : Set α<VAR>t : Set β<GOAL>MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>s : Set α<VAR>t : Set β<VAR>h : s ×ˢ t = ∅<GOAL>MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>s : Set α<VAR>t : Set β<VAR>h : (s ×ˢ t).Nonempty<GOAL>MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>μ✝ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction G α<VAR>inst✝¹ : MeasurableSMul G α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>f : α → E<VAR>g : G<GOAL>∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>μ✝ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MulAction G α<VAR>inst✝¹ : MeasurableSMul G α<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure G α μ<VAR>f : α → E<VAR>g : G<VAR>h : MeasurableEmbedding fun x => g • x<GOAL>∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.88317, u_1} C<VAR>inst✝³ : Category.{?u.88321, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<GOAL>S.RightHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.88317, u_1} C<VAR>inst✝³ : Category.{?u.88321, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<VAR>hp : IsColimit (CokernelCofork.ofπ S.g ⋯)<GOAL>S.RightHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.88317, u_1} C<VAR>inst✝³ : Category.{?u.88321, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<VAR>hp : IsColimit (CokernelCofork.ofπ S.g ⋯)<VAR>g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)<GOAL>S.RightHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.88317, u_1} C<VAR>inst✝³ : Category.{?u.88321, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<VAR>hp : IsColimit (CokernelCofork.ofπ S.g ⋯)<VAR>g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)<VAR>hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt<GOAL>S.RightHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.88317, u_1} C<VAR>inst✝³ : Category.{?u.88321, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<VAR>hp : IsColimit (CokernelCofork.ofπ S.g ⋯)<VAR>g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)<VAR>hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt<VAR>wι : 0 ≫ g' = 0<GOAL>S.RightHomologyData
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.88317, u_1} C<VAR>inst✝³ : Category.{?u.88321, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝ : HasZeroObject C<VAR>s : S.Splitting<VAR>hp : IsColimit (CokernelCofork.ofπ S.g ⋯)<VAR>g' : (CokernelCofork.ofπ S.g ⋯).pt ⟶ (CokernelCofork.ofπ S.g ⋯).pt := hp.desc (CokernelCofork.ofπ S.g ⋯)<VAR>hg' : g' = 𝟙 (CokernelCofork.ofπ S.g ⋯).pt<VAR>wι : 0 ≫ g' = 0<VAR>hι : IsLimit (KernelFork.ofι 0 wι)<GOAL>S.RightHomologyData
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Module R (Additive ℤˣ)<VAR>u : ℤˣ<VAR>z : ℤ<GOAL>Additive.toMul (↑z • Additive.ofMul u) = u ^ z
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>f g : ↥(Lp E p μ)<VAR>s : Set X<GOAL>↑↑(Memℒp.toLp ↑↑(f + g) ⋯) =ᶠ[ae (μ.restrict s)] ↑↑(Memℒp.toLp ↑↑f ⋯ + Memℒp.toLp ↑↑g ⋯)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>f g : ↥(Lp E p μ)<VAR>s : Set X<GOAL>∀ᵐ (x : X) ∂μ.restrict s, ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(Memℒp.toLp ↑↑(f + g) ⋯) x = ↑↑(Memℒp.toLp ↑↑f ⋯ + Memℒp.toLp ↑↑g ⋯) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>f g : ↥(Lp E p μ)<VAR>s : Set X<GOAL>∀ᵐ (x : X) ∂μ.restrict s, ↑↑(Memℒp.toLp ↑↑f ⋯ + Memℒp.toLp ↑↑g ⋯) x = (↑↑(Memℒp.toLp ↑↑f ⋯) + ↑↑(Memℒp.toLp ↑↑g ⋯)) x → ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(Memℒp.toLp ↑↑(f + g) ⋯) x = ↑↑(Memℒp.toLp ↑↑f ⋯ + Memℒp.toLp ↑↑g ⋯) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>f g : ↥(Lp E p μ)<VAR>s : Set X<GOAL>∀ᵐ (x : X) ∂μ.restrict s, ↑↑(Memℒp.toLp ↑↑f ⋯) x = ↑↑f x → ↑↑(Memℒp.toLp ↑↑f ⋯ + Memℒp.toLp ↑↑g ⋯) x = (↑↑(Memℒp.toLp ↑↑f ⋯) + ↑↑(Memℒp.toLp ↑↑g ⋯)) x → ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(Memℒp.toLp ↑↑(f + g) ⋯) x = ↑↑(Memℒp.toLp ↑↑f ⋯ + Memℒp.toLp ↑↑g ⋯) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>f g : ↥(Lp E p μ)<VAR>s : Set X<GOAL>∀ᵐ (x : X) ∂μ.restrict s, ↑↑(Memℒp.toLp ↑↑g ⋯) x = ↑↑g x → ↑↑(Memℒp.toLp ↑↑f ⋯) x = ↑↑f x → ↑↑(Memℒp.toLp ↑↑f ⋯ + Memℒp.toLp ↑↑g ⋯) x = (↑↑(Memℒp.toLp ↑↑f ⋯) + ↑↑(Memℒp.toLp ↑↑g ⋯)) x → ↑↑(f + g) x = (↑↑f + ↑↑g) x → ↑↑(Memℒp.toLp ↑↑(f + g) ⋯) x = ↑↑(Memℒp.toLp ↑↑f ⋯ + Memℒp.toLp ↑↑g ⋯) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace X<VAR>inst✝³ : NormedAddCommGroup E<VAR>𝕜 : Type u_5<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>μ : Measure X<VAR>f g : ↥(Lp E p μ)<VAR>s : Set X<VAR>x : X<VAR>hx1 : ↑↑(Memℒp.toLp ↑↑(f + g) ⋯) x = ↑↑(f + g) x<VAR>hx2 : ↑↑(Memℒp.toLp ↑↑g ⋯) x = ↑↑g x<VAR>hx3 : ↑↑(Memℒp.toLp ↑↑f ⋯) x = ↑↑f x<VAR>hx4 : ↑↑(Memℒp.toLp ↑↑f ⋯ + Memℒp.toLp ↑↑g ⋯) x = (↑↑(Memℒp.toLp ↑↑f ⋯) + ↑↑(Memℒp.toLp ↑↑g ⋯)) x<VAR>hx5 : ↑↑(f + g) x = (↑↑f + ↑↑g) x<GOAL>↑↑(Memℒp.toLp ↑↑(f + g) ⋯) x = ↑↑(Memℒp.toLp ↑↑f ⋯ + Memℒp.toLp ↑↑g ⋯) x
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LinearOrder G<VAR>inst✝² : LinearOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<GOAL>⋯.min ⋯ = hs.min hsn • ht.min htn
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LinearOrder G<VAR>inst✝² : LinearOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<GOAL>hs.min hsn • ht.min htn ≤ ⋯.min ⋯
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LinearOrder G<VAR>inst✝² : LinearOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<GOAL>∀ b ∈ s • t, hs.min hsn • ht.min htn ≤ b
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : LinearOrder G<VAR>inst✝² : LinearOrder P<VAR>inst✝¹ : SMul G P<VAR>inst✝ : IsOrderedCancelSMul G P<VAR>s : Set G<VAR>t : Set P<VAR>hs : s.IsWF<VAR>ht : t.IsWF<VAR>hsn : s.Nonempty<VAR>htn : t.Nonempty<VAR>x : G<VAR>hx : x ∈ s<VAR>y : P<VAR>hy : y ∈ t<GOAL>hs.min hsn • ht.min htn ≤ (fun x x_1 => x • x_1) x y
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>V : Type u_3<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : ι → ℙ K V<GOAL>Independent f ↔ ¬Dependent f
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x y : E<GOAL>(o.areaForm (φ x)) (φ y) = (o.areaForm x) y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x y : E<GOAL>o = (map (Fin 2) φ.toLinearEquiv) o
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x y : E<GOAL>x = φ.symm (φ x)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>φ : E ≃ₗᵢ[ℝ] E<VAR>hφ : 0 < LinearMap.det ↑φ.toLinearEquiv<VAR>x y : E<GOAL>y = φ.symm (φ y)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f : α → ι →₀ A<VAR>i✝ : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Fintype α<VAR>i : α<VAR>m : M<GOAL>∑ j : α, (single i m) j = m
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f : α → ι →₀ A<VAR>i✝ : ι<VAR>g : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Fintype α<VAR>i : α<VAR>m : M<GOAL>(if i ∈ univ then m else 0) = m
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g✝ : P →ₐ[R] P'<VAR>I : FractionalIdeal S P'<VAR>g : P ≃ₐ[R] P'<GOAL>map (↑g) (map (↑g.symm) I) = I
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : LE α<VAR>inst✝² : LE β<VAR>inst✝¹ : EquivLike F α β<VAR>inst✝ : OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>a ≤ EquivLike.inv f b ↔ f a ≤ b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : LE α<VAR>inst✝² : LE β<VAR>inst✝¹ : EquivLike F α β<VAR>inst✝ : OrderIsoClass F α β<VAR>f : F<VAR>a : α<VAR>b : β<GOAL>b = f (EquivLike.inv f b)
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n d : ℕ<VAR>inst✝ : NeZero n<VAR>hd : d ∣ n<VAR>χ₂ : DirichletCharacter R d<GOAL>∃! χ', (changeLevel hd) χ₂ = (changeLevel ⋯) χ'
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t s : Set α<VAR>hs : IsSeparable s<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t s : Set α<VAR>hs : IsSeparable s<VAR>this : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<GOAL>IsUnit ((X.presheaf.map (homOfLE ⋯).op) f)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<GOAL>∀ (x : ↥(X.basicOpen f)), IsUnit ((X.presheaf.germ x) ((X.presheaf.map (homOfLE ⋯).op) f))
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>hx : IsUnit ((X.presheaf.germ x) f)<GOAL>(X.presheaf.germ ⟨↑x, ⋯⟩) ((X.presheaf.map (homOfLE ⋯).op) f) = (X.presheaf.germ x) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MulOneClass α<VAR>inst✝¹ : LE α<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>h : a ≤ a * b<GOAL>a * 1 ≤ a * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a : α<VAR>h : a ∈ s<GOAL>(insert a s).ncard = s.ncard
<VAR>x✝ y z x : ℝ<GOAL>|sinh x| = sinh |x|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Nat<VAR>h : 0 < n<GOAL>(mk n h).size = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Nat<VAR>h : 0 < n<GOAL>Nat.sum (List.map (fun x => x.toList.length) (List.replicate n AssocList.nil)) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Nat<GOAL>Nat.sum (List.map (fun x => x.toList.length) (List.replicate n AssocList.nil)) = 0