ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{u_3, u_1} C<VAR>inst✝⁶ : Category.{u_4, u_2} D<VAR>inst✝⁵ : HasZeroMorphisms C<VAR>inst✝⁴ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝³ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝² : F.PreservesZeroMorphisms<VAR>inst✝¹ : S.HasRightHomology<VAR>inst✝ : F.PreservesRightHomologyOf S<GOAL>rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.rightHomologyData.map F) = rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F) ≫ F.map (rightHomologyMap' (𝟙 S) hr S.rightHomologyData)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a✝ : α<VAR>b : β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(a • s)⁻¹ = op a⁻¹ • s⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidableEq α<VAR>s : Finset α<GOAL>(0 • s)⁻¹ = op 0⁻¹ • s⁻¹
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a✝ : α<VAR>b : β<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>ha : a ≠ 0<GOAL>(a • s)⁻¹ = op a⁻¹ • s⁻¹
<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>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<VAR>a : Ordinal.{max u_4 u_5}<VAR>H : ∀ b < a, ∃ i, ∃ (hi : i < o), f i hi = b<GOAL>a ≤ o.bmex f
<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>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<VAR>a : Ordinal.{max u_4 u_5}<VAR>H : ∀ b < a, ∃ i, ∃ (hi : i < o), f i hi = b<VAR>h : o.bmex f < a<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this : FiniteDimensional 𝕜 E<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝ : FiniteDimensional 𝕜 E<VAR>this : FiniteDimensional 𝕜 F<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝¹ : FiniteDimensional 𝕜 E<VAR>this✝ : FiniteDimensional 𝕜 F<VAR>this : ProperSpace E<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝² : FiniteDimensional 𝕜 E<VAR>this✝¹ : FiniteDimensional 𝕜 F<VAR>this✝ : ProperSpace E<VAR>this : ProperSpace F<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝² : FiniteDimensional 𝕜 E<VAR>this✝¹ : FiniteDimensional 𝕜 F<VAR>this✝ : ProperSpace E<VAR>this : ProperSpace F<VAR>M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝² : FiniteDimensional 𝕜 E<VAR>this✝¹ : FiniteDimensional 𝕜 F<VAR>this✝ : ProperSpace E<VAR>this : ProperSpace F<VAR>M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L<VAR>M_cont : Continuous ⇑M<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝² : FiniteDimensional 𝕜 E<VAR>this✝¹ : FiniteDimensional 𝕜 F<VAR>this✝ : ProperSpace E<VAR>this : ProperSpace F<VAR>M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L<VAR>M_cont : Continuous ⇑M<VAR>hM : Function.Surjective ⇑M<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝² : FiniteDimensional 𝕜 E<VAR>this✝¹ : FiniteDimensional 𝕜 F<VAR>this✝ : ProperSpace E<VAR>this : ProperSpace F<VAR>M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L<VAR>M_cont : Continuous ⇑M<VAR>hM : Function.Surjective ⇑M<VAR>A : ∀ (x : F × E), M x ∈ s ↔ x ∈ ⇑M ⁻¹' s<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝² : FiniteDimensional 𝕜 E<VAR>this✝¹ : FiniteDimensional 𝕜 F<VAR>this✝ : ProperSpace E<VAR>this : ProperSpace F<VAR>M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L<VAR>M_cont : Continuous ⇑M<VAR>hM : Function.Surjective ⇑M<VAR>A : ∀ (x : F × E), M x ∈ s ↔ x ∈ ⇑M ⁻¹' s<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (x : F × E) ∂ν.prod μ, x ∈ ⇑M ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝² : FiniteDimensional 𝕜 E<VAR>this✝¹ : FiniteDimensional 𝕜 F<VAR>this✝ : ProperSpace E<VAR>this : ProperSpace F<VAR>M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L<VAR>M_cont : Continuous ⇑M<VAR>hM : Function.Surjective ⇑M<VAR>A : ∀ (x : F × E), M x ∈ s ↔ x ∈ ⇑M ⁻¹' s<GOAL>(∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (x : F) ∂ν, ∀ᵐ (y : E) ∂μ, (x, y) ∈ ⇑M ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>inst✝¹² : CompleteSpace 𝕜<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : MeasurableSpace E<VAR>inst✝⁹ : BorelSpace E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>L : E →ₗ[𝕜] F<VAR>μ : Measure E<VAR>ν : Measure F<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>inst✝² : ν.IsAddHaarMeasure<VAR>inst✝¹ : LocallyCompactSpace E<VAR>inst✝ : LocallyCompactSpace F<VAR>s : Set F<VAR>hs : MeasurableSet s<VAR>this✝² : FiniteDimensional 𝕜 E<VAR>this✝¹ : FiniteDimensional 𝕜 F<VAR>this✝ : ProperSpace E<VAR>this : ProperSpace F<VAR>M : F × E →ₗ[𝕜] F := LinearMap.id.coprod L<VAR>M_cont : Continuous ⇑M<VAR>hM : Function.Surjective ⇑M<VAR>A : ∀ (x : F × E), M x ∈ s ↔ x ∈ ⇑M ⁻¹' s<GOAL>MeasurableSet (⇑M ⁻¹' s)
<VAR>p✝ q : ℚ<VAR>p : ℚ≥0<VAR>hq : 0 ≤ q<GOAL>q.toNNRat < p ↔ q < ↑p
<VAR>C : Type u₁<VAR>inst✝² : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>A : CostructuredArrow S T<VAR>P : (CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ op A<VAR>inst✝ : Mono f.unop.left.op<GOAL>f.unop.left ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop = (Subobject.mk f.unop.left.op).arrow.unop
<VAR>C : Type u₁<VAR>inst✝² : Category.{v, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v, u₂} D<VAR>S : C ⥤ D<VAR>T : D<VAR>A : CostructuredArrow S T<VAR>P : (CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ op A<VAR>inst✝ : Mono f.unop.left.op<GOAL>f.unop.left.op.unop ≫ (Subobject.underlyingIso f.unop.left.op).hom.unop = (Subobject.mk f.unop.left.op).arrow.unop
<VAR>n : ℕ<GOAL>eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
<GOAL>eulerMascheroniSeq' (0 + 1) < eulerMascheroniSeq' 0
<VAR>n : ℕ<VAR>hn : n > 0<GOAL>eulerMascheroniSeq' (n + 1) < eulerMascheroniSeq' n
<VAR>n : ℕ<VAR>hn : n > 0<GOAL>↑(harmonic (n + 1)) - log ↑(n + 1) < ↑(harmonic n) - log ↑n
<VAR>n : ℕ<VAR>hn : n > 0<GOAL>log (↑(n + 1) / ↑n)⁻¹ < -↑(↑(n + 1))⁻¹
<VAR>n : ℕ<VAR>hn : n > 0<GOAL>0 < (↑(n + 1) / ↑n)⁻¹
<VAR>n : ℕ<VAR>hn : n > 0<GOAL>(↑(n + 1) / ↑n)⁻¹ ≠ 1
<VAR>n : ℕ<VAR>hn : n > 0<GOAL>(↑(n + 1) / ↑n)⁻¹ - 1 = -↑(↑(n + 1))⁻¹
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a✝ b✝ : α<VAR>n a b : ℕ<GOAL>multinomial univ ![a, b] = (a + b)! / (a ! * b !)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>ga : α → α → α<VAR>gb : β → β → β<VAR>inst✝ : Std.Associative gb<VAR>h : Semiconj₂ f ga gb<VAR>h_inj : Injective f<VAR>x₁ x₂ x₃ : α<GOAL>f (ga (ga x₁ x₂) x₃) = f (ga x₁ (ga x₂ x₃))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N N₁ N₂ P P₁ P₂ : Submodule R M<VAR>I : Ideal R<GOAL>colon I ⊤ = I
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N N₁ N₂ P P₁ P₂ : Submodule R M<VAR>I : Ideal R<GOAL>∀ (x : R), (∀ p ∈ ⊤, x * p ∈ I) ↔ x ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β → δ<VAR>s₁ : Stream' α<VAR>s₂ : Stream' β<GOAL>zip f s₁ s₂ = f s₁.head s₂.head :: zip f s₁.tail s₂.tail
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>f : α → β → δ<VAR>s₁ : Stream' α<VAR>s₂ : Stream' β<GOAL>(zip f s₁ s₂).head :: (zip f s₁ s₂).tail = f s₁.head s₂.head :: zip f s₁.tail s₂.tail
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<VAR>n : ℕ+<GOAL>↑↑n = ↑↑n
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<VAR>n : ℕ+<GOAL>↑⋯.unit = ↑↑n
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>m : ℕ<VAR>inst✝ : CharP R m<VAR>n✝ : ℕ<VAR>h : m ∣ n✝ + 1 + 1<GOAL>↑(1 % (n✝ + 1 + 1)) = 1
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>m : ℕ<VAR>inst✝ : CharP R m<VAR>n✝ : ℕ<VAR>h : m ∣ n✝ + 1 + 1<GOAL>↑1 = 1
<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>m : ℕ<VAR>inst✝ : CharP R m<VAR>n✝ : ℕ<VAR>h : m ∣ n✝ + 1 + 1<GOAL>1 < n✝ + 1 + 1
<VAR>α : Type u<VAR>β : Type v<VAR>a✝ b : α<VAR>inst✝ : CommSemiring α<VAR>I : Ideal α<VAR>a : α<VAR>h2 : IsUnit a<VAR>x : α<GOAL>span {x * a} = span {x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<GOAL>Measurable fun μ => map f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => (map f b) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : α → β<VAR>hf : Measurable f<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Measurable fun b => b (f ⁻¹' s)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>r : A<VAR>hr : r ∈ I<GOAL>r ∈ (homogeneousHull 𝒜 I).toIdeal
<VAR>x : ℝ≥0∞<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>x ^ y < ⊤ ↔ x < ⊤
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>p q p' q' : K[X]<VAR>hq : q ≠ 0<VAR>hq' : q' ≠ 0<GOAL>RatFunc.mk p q = RatFunc.mk p' q' ↔ p * q' = p' * q
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>y : ℤ<GOAL>round (x - ↑y) = round x - y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>y : ℤ<GOAL>round (x + -↑y) = round x - y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>y : ℤ<GOAL>round (x + ↑(-y)) = round x - y
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : TopologicalSpace L<VAR>inst✝² : TopologicalSpace X<VAR>ι : Type u_3<VAR>inst✝¹ : SemilatticeSup L<VAR>inst✝ : ContinuousSup L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>x : X<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, ContinuousAt (f i) x<GOAL>ContinuousAt (s.sup' hne f) x
<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>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f✝ f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>f : γ → β → δ<VAR>g : α → γ<GOAL>image2 f (g '' ↑s) ↑t = image2 (fun a b => f (g a) b) ↑s ↑t
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ xs : List α<GOAL>List.filter p l₁ <+: List.filter p (l₁ ++ xs)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l₁ xs : List α<GOAL>List.filter p l₁ <+: List.filter p l₁ ++ List.filter p xs
<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>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>s : Set α<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>x : E<GOAL>setToL1S T (indicatorConst 1 hs ⋯ x) = (T s) 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>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>s : Set α<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>x : E<VAR>h_empty : T ∅ = 0<GOAL>setToL1S T (indicatorConst 1 hs ⋯ x) = (T s) 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>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>s : Set α<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>x : E<VAR>h_empty : T ∅ = 0<GOAL>SimpleFunc.setToSimpleFunc T (toSimpleFunc (indicatorConst 1 hs ⋯ x)) = (T s) 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>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>s : Set α<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>x : E<VAR>h_empty : T ∅ = 0<GOAL>SimpleFunc.setToSimpleFunc T (toSimpleFunc (indicatorConst 1 hs ⋯ x)) = SimpleFunc.setToSimpleFunc T (SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 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>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>T : Set α → E →L[ℝ] F<VAR>s : Set α<VAR>h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0<VAR>h_add : FinMeasAdditive μ T<VAR>hs : MeasurableSet s<VAR>hμs : μ s < ⊤<VAR>x : E<VAR>h_empty : T ∅ = 0<GOAL>↑(toSimpleFunc (indicatorConst 1 hs ⋯ x)) =ᶠ[ae μ] ↑(SimpleFunc.piecewise s hs (SimpleFunc.const α x) (SimpleFunc.const α 0))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0_lt : 0 < p<VAR>f : α → ℝ≥0∞<VAR>hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<GOAL>∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0_lt : 0 < p<VAR>f : α → ℝ≥0∞<VAR>hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<GOAL>∫⁻ (c : α), f c ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ∂μ = 1
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p : ℝ<VAR>hp0_lt : 0 < p<VAR>f : α → ℝ≥0∞<VAR>hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0<VAR>hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤<GOAL>(∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ≠ ⊤
<VAR>f : ℝ → ℝ<VAR>f' : ℝ<VAR>s : Set ℝ<VAR>a b : ℝ<VAR>h : IsLocalMin f a<VAR>hf : HasDerivAt f f' a<GOAL>f' = 0
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>hb : b ≠ 0<VAR>h : b = a⁻¹ * c<GOAL>a * b = c
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b c d : G₀<VAR>m n : ℕ<VAR>hb : b ≠ 0<VAR>h : b = a⁻¹ * c<GOAL>a ≠ 0
<VAR>𝕜 : Type u_1<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁰ : NormedAddCommGroup D<VAR>inst✝⁹ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃L[𝕜] F<VAR>a✝ : Nontrivial E<VAR>O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun f => f.comp ↑e.symm<VAR>O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f<GOAL>ContDiffAt 𝕜 n inverse ↑e