ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')<VAR>this : LinearMap.ker F = W ⊓ W'<VAR>x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')<GOAL>∃ y ∈ dualAnnihilator W, ∃ z ∈ dualAnnihilator W', y + z = F.dualMap x
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')<VAR>this : LinearMap.ker F = W ⊓ W'<VAR>a : Dual K (V₁ ⧸ W)<VAR>b : Dual K (V₁ ⧸ W')<GOAL>∃ y ∈ dualAnnihilator W, ∃ z ∈ dualAnnihilator W', y + z = F.dualMap ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) (a, b))
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')<VAR>this : LinearMap.ker F = W ⊓ W'<VAR>b : Dual K (V₁ ⧸ W')<VAR>a' : ↥(dualAnnihilator W)<GOAL>∃ y ∈ dualAnnihilator W, ∃ z ∈ dualAnnihilator W', y + z = F.dualMap ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) ((dualQuotEquivDualAnnihilator W).symm a', b))
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')<VAR>this : LinearMap.ker F = W ⊓ W'<VAR>a' : ↥(dualAnnihilator W)<VAR>b' : ↥(dualAnnihilator W')<GOAL>∃ y ∈ dualAnnihilator W, ∃ z ∈ dualAnnihilator W', y + z = F.dualMap ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) ((dualQuotEquivDualAnnihilator W).symm a', (dualQuotEquivDualAnnihilator W').symm b'))
<VAR>K : Type uK<VAR>inst✝⁴ : Field K<VAR>V₁ : Type uV₁<VAR>V₂ : Type uV₂<VAR>inst✝³ : AddCommGroup V₁<VAR>inst✝² : Module K V₁<VAR>inst✝¹ : AddCommGroup V₂<VAR>inst✝ : Module K V₂<VAR>W W' : Subspace K V₁<VAR>F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')<VAR>this : LinearMap.ker F = W ⊓ W'<VAR>a' : ↥(dualAnnihilator W)<VAR>b' : ↥(dualAnnihilator W')<GOAL>↑a' + ↑b' = F.dualMap ((dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) ((dualQuotEquivDualAnnihilator W).symm a', (dualQuotEquivDualAnnihilator W').symm b'))
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>β : Type u_5<VAR>inst✝ : CommMonoid β<VAR>a u : β<VAR>hu : IsUnit u<GOAL>u * a ~ᵤ a
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>β : Type u_5<VAR>inst✝ : CommMonoid β<VAR>a u : β<VAR>hu : IsUnit u<GOAL>a * u ~ᵤ a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<GOAL>Pointed 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b : α<GOAL>_root_.Disjoint (s ∪ t) u ↔ _root_.Disjoint s u ∧ _root_.Disjoint t u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁✝ s₂✝ t t₁ t₂ u v : Finset α<VAR>a b : α<VAR>s₁ s₂ : Finset α<VAR>x✝ : α<GOAL>x✝ ∈ s₁ ∩ s₂ ↔ x✝ ∈ s₂ ∩ s₁
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀ : Type u_4<VAR>inst✝¹ : CommMonoidWithZero M₀<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>f : ι → M₀<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<VAR>h : f i = 0<GOAL>∏ j ∈ s, f j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>ι : Sort u_3<VAR>inst✝ : CompleteLattice β<VAR>f : ι → α →o β<GOAL>⇑(⨆ i, f i) = ⨆ i, ⇑(f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>ι : Sort u_3<VAR>inst✝ : CompleteLattice β<VAR>f : ι → α →o β<VAR>x : α<GOAL>(⨆ i, f i) x = (⨆ i, ⇑(f i)) x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁵ : OrderedCommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : StarOrderedRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalSemiring R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type ?u.771514) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>r : R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, x ≤ r<VAR>ha : autoParam (p a) _auto✝<GOAL>a ≤ (algebraMap R A) r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁵ : OrderedCommSemiring R<VAR>inst✝¹⁴ : StarRing R<VAR>inst✝¹³ : StarOrderedRing R<VAR>inst✝¹² : MetricSpace R<VAR>inst✝¹¹ : TopologicalSemiring R<VAR>inst✝¹⁰ : ContinuousStar R<VAR>inst✝⁹ : ∀ (α : Type ?u.771514) [inst : TopologicalSpace α], StarOrderedRing C(α, R)<VAR>inst✝⁸ : TopologicalSpace A<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : PartialOrder A<VAR>inst✝⁴ : StarOrderedRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>r : R<VAR>a : A<VAR>h : ∀ x ∈ spectrum R a, x ≤ r<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc id a ≤ (algebraMap R A) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>f : α → β → ℝ≥0∞<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>hf : Measurable (Function.uncurry f)<VAR>a : α<GOAL>(κ.withDensity f) a = (κ a).withDensity (f a)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝⁵ : Countable ↥Γ<VAR>inst✝⁴ : MeasurableSpace (G ⧸ Γ)<VAR>inst✝³ : BorelSpace (G ⧸ Γ)<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → E<VAR>hf₁ : Integrable f μ<VAR>hf₂ : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))<GOAL>∫ (x : G), f x ∂μ = ∫ (x : G ⧸ Γ), automorphize f x ∂Measure.map mk (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝⁵ : Countable ↥Γ<VAR>inst✝⁴ : MeasurableSpace (G ⧸ Γ)<VAR>inst✝³ : BorelSpace (G ⧸ Γ)<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → E<VAR>hf₁ : Integrable f μ<VAR>hf₂ : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))<GOAL>∑' (γ : ↥Γ.op), ∫ (x : G) in 𝓕, f (γ • x) ∂μ = ∫ (x : G) in 𝓕, ∑' (γ : ↥Γ.op), f (γ • x) ∂μ
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝⁵ : Countable ↥Γ<VAR>inst✝⁴ : MeasurableSpace (G ⧸ Γ)<VAR>inst✝³ : BorelSpace (G ⧸ Γ)<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → E<VAR>hf₁ : Integrable f μ<VAR>hf₂ : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))<GOAL>∀ (i : ↥Γ.op), AEStronglyMeasurable (fun x => f (i • x)) (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝⁵ : Countable ↥Γ<VAR>inst✝⁴ : MeasurableSpace (G ⧸ Γ)<VAR>inst✝³ : BorelSpace (G ⧸ Γ)<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → E<VAR>hf₁ : Integrable f μ<VAR>hf₂ : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))<GOAL>∑' (i : ↥Γ.op), ∫⁻ (a : G) in 𝓕, ↑‖f (i • a)‖₊ ∂μ ≠ ⊤
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>inst✝ : DecidableEq V<VAR>v : V<VAR>x✝ : ↑(G.neighborSet v)<VAR>w : V<VAR>hw : w ∈ G.neighborSet v<GOAL>(fun e => ⟨G.otherVertexOfIncident ⋯, ⋯⟩) ((fun w => ⟨s(v, ↑w), ⋯⟩) ⟨w, hw⟩) = ⟨w, hw⟩
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>inst✝ : DecidableEq V<VAR>v : V<VAR>x✝ : ↑(G.neighborSet v)<VAR>w : V<VAR>hw : w ∈ G.neighborSet v<GOAL>G.otherVertexOfIncident ⋯ = w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<GOAL>s.attach = ∅ ↔ s = ∅
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>f ▷ 𝟙_ C = (ρ_ X).hom ≫ f ≫ (ρ_ Y).inv
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>f ▷ 𝟙_ C = (f ▷ 𝟙_ C ≫ (ρ_ Y).hom) ≫ (ρ_ Y).inv
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.cos (angle x (x + y)) = ‖x‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>‖x‖ ≤ ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<VAR>δ : ℝ<VAR>E : Set α<VAR>h : y ∈ E<VAR>h' : dist x y ≤ δ<GOAL>x ∈ cthickening δ E
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<VAR>δ : ℝ<VAR>E : Set α<VAR>h : y ∈ E<VAR>h' : dist x y ≤ δ<GOAL>edist x y ≤ ENNReal.ofReal δ
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<VAR>δ : ℝ<VAR>E : Set α<VAR>h : y ∈ E<VAR>h' : dist x y ≤ δ<GOAL>ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : Filter α<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>g₁ : Set α₁ → Filter β₁<VAR>g₂ : Set α₂ → Filter β₂<VAR>hg₁ : Monotone g₁<VAR>hg₂ : Monotone g₂<GOAL>f₁.lift g₁ ×ˢ f₂.lift g₂ = f₁.lift fun s => f₂.lift fun t => g₁ s ×ˢ g₂ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : Filter α<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>g₁ : Set α₁ → Filter β₁<VAR>g₂ : Set α₂ → Filter β₂<VAR>hg₁ : Monotone g₁<VAR>hg₂ : Monotone g₂<GOAL>(f₁.lift fun s => (g₁ s).lift fun s => (f₂.lift g₂).lift' fun t => s ×ˢ t) = f₁.lift fun s => f₂.lift fun t => (g₁ s).lift fun s => (g₂ t).lift' fun t => s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : Filter α<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>g₁ : Set α₁ → Filter β₁<VAR>g₂ : Set α₂ → Filter β₂<VAR>hg₁ : Monotone g₁<VAR>hg₂ : Monotone g₂<GOAL>(fun s => (g₁ s).lift fun s => (f₂.lift g₂).lift' fun t => s ×ˢ t) = fun s => f₂.lift fun t => (g₁ s).lift fun s => (g₂ t).lift' fun t => s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : Filter α<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>g₁ : Set α₁ → Filter β₁<VAR>g₂ : Set α₂ → Filter β₂<VAR>hg₁ : Monotone g₁<VAR>hg₂ : Monotone g₂<VAR>x : Set α₁<GOAL>((g₁ x).lift fun s => (f₂.lift g₂).lift' fun t => s ×ˢ t) = f₂.lift fun t => (g₁ x).lift fun s => (g₂ t).lift' fun t => s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : Filter α<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>g₁ : Set α₁ → Filter β₁<VAR>g₂ : Set α₂ → Filter β₂<VAR>hg₁ : Monotone g₁<VAR>hg₂ : Monotone g₂<VAR>x : Set α₁<GOAL>((g₁ x).lift fun s => (f₂.lift g₂).lift' fun t => s ×ˢ t) = (g₁ x).lift fun t => f₂.lift fun s => (g₂ s).lift' fun t_1 => t ×ˢ t_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : Filter α<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>g₁ : Set α₁ → Filter β₁<VAR>g₂ : Set α₂ → Filter β₂<VAR>hg₁ : Monotone g₁<VAR>hg₂ : Monotone g₂<VAR>x : Set α₁<GOAL>(fun s => (f₂.lift g₂).lift' fun t => s ×ˢ t) = fun t => f₂.lift fun s => (g₂ s).lift' fun t_1 => t ×ˢ t_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f : Filter α<VAR>α₁ : Type u_5<VAR>α₂ : Type u_6<VAR>β₁ : Type u_7<VAR>β₂ : Type u_8<VAR>f₁ : Filter α₁<VAR>f₂ : Filter α₂<VAR>g₁ : Set α₁ → Filter β₁<VAR>g₂ : Set α₂ → Filter β₂<VAR>hg₁ : Monotone g₁<VAR>hg₂ : Monotone g₂<VAR>x : Set α₁<VAR>y : Set β₁<GOAL>((f₂.lift g₂).lift' fun t => y ×ˢ t) = f₂.lift fun s => (g₂ s).lift' fun t => y ×ˢ t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>σ : Type u_4<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>S : Subsemigroup M<VAR>s : Subsemigroup N<VAR>x : M × N<GOAL>x ∈ ⊤.prod s ↔ x ∈ comap (MulHom.snd M N) s
<VAR>α : Type u<VAR>l l' : List α<VAR>β : Type u_1<VAR>l₁ : List α<VAR>f : α → β<VAR>n : ℕ<GOAL>List.map f l₁ ~r List.map f (l₁.rotate n)
<VAR>α : Type u<VAR>l l' : List α<VAR>β : Type u_1<VAR>l₁ : List α<VAR>f : α → β<VAR>n : ℕ<GOAL>List.map f l₁ ~r (List.map f l₁).rotate n
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoDiv hp a b • p - b = -toIcoMod hp a b
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<GOAL>⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>S : Set ι<VAR>hS : #↑S < c<VAR>s t : (i : ι) → i ∈ S → Set α<VAR>h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi<GOAL>⋂ x, s ↑x ⋯ ≤ᶠ[l] ⋂ x, t ↑x ⋯
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝¹ a✝ : α<VAR>z a : ℤ<GOAL>a ≤ ⌊a✝ + ↑z⌋ ↔ a ≤ ⌊a✝⌋ + z
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : AddMonoid B<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>ψ✝ ψ : AddChar A M<VAR>hψ : Surjective ⇑ψ<VAR>f g : M →* N<VAR>h : (fun f => f.compAddChar ψ) f = (fun f => f.compAddChar ψ) g<GOAL>f = g
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : AddMonoid B<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>ψ✝ ψ : AddChar A M<VAR>hψ : Surjective ⇑ψ<VAR>f g : M →* N<VAR>h : ⇑((fun f => f.compAddChar ψ) f) = ⇑((fun f => f.compAddChar ψ) g)<GOAL>⇑f = ⇑g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a✝ a₁ a₂ b b₁ b₂ c d x a : α<GOAL>Injective (Ι a)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁹ : CommRing R₁<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>R₄ : Type u_7<VAR>M₄ : Type u_8<VAR>inst✝³ : CommRing R₄<VAR>inst✝² : IsDomain R₄<VAR>inst✝¹ : AddCommGroup M₄<VAR>inst✝ : Module R₄ M₄<VAR>G : BilinForm R₄ M₄<VAR>n : Type w<VAR>B : BilinForm K V<VAR>v : n → V<VAR>hv₁ : B.iIsOrtho v<VAR>hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)<GOAL>LinearIndependent K v
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>1 ≤ b⁻¹ * a ↔ b ≤ a
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : G → E<VAR>x : G<VAR>f' : G →L[𝕜] E<GOAL>HasFDerivAt (⇑iso ∘ f) ((↑iso).comp f') x ↔ HasFDerivAt f f' x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a✝ b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u : Set α<VAR>a : α<VAR>s : Set α<GOAL>insert a (s \ {a}) = insert a s
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R L<VAR>b' : Basis ι' R L<GOAL>φ.nilRankAux b ≤ φ.nilRankAux b'
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R L<VAR>b' : Basis ι' R L<GOAL>(φ.polyCharpoly b).coeff (φ.nilRankAux b') ≠ 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b✝ : Basis ι R L<VAR>inst✝ : Nontrivial R<VAR>b : Basis ι R L<VAR>b' : Basis ι' R L<GOAL>¬(φ.polyCharpoly b').coeff (φ.nilRankAux b') = 0
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>x : X<VAR>hx : x ∈ e.source<VAR>x' : X<VAR>hx' : ↑e.symm (↑e x') = x'<VAR>h : ↑e x' = ↑e x<GOAL>x' ∈ {x}
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>X Y : D<VAR>f f' : X ⟶ e.functor.obj (e.inverse.obj Y)<GOAL>f ≫ e.counit.app Y = f' ≫ e.counit.app Y ↔ f = f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∉ s<GOAL>_root_.Disjoint (insert a s) (t.erase a) ↔ _root_.Disjoint s t
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>h : l.length = 1<GOAL>l = [l.nthLe 0 ⋯]
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>h : l.length = 1<VAR>n : ℕ<VAR>h₁ : n < l.length<VAR>h₂ : n < [l.nthLe 0 ⋯].length<GOAL>l.get ⟨n, h₁⟩ = [l.nthLe 0 ⋯].get ⟨n, h₂⟩
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ l : List α<VAR>h : l.length = 1<VAR>n : ℕ<VAR>h₁ : n < l.length<VAR>h₂ : n < [l.nthLe 0 ⋯].length<GOAL>l.get ⟨n, h₁⟩ = l.nthLe 0 ⋯
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (φ i) μ<VAR>hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (φ i) μ<VAR>hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I<VAR>hfm : AEStronglyMeasurable f μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (φ i) μ<VAR>hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I<VAR>hfm : AEStronglyMeasurable f μ<GOAL>∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (φ i) μ<VAR>hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ENNReal.ofReal ‖f a‖ ∂μ).toReal ≤ I<VAR>hfm : AEStronglyMeasurable f μ<GOAL>∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (φ i) μ<VAR>hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ).toReal ≤ I<VAR>hfm : AEStronglyMeasurable f μ<GOAL>∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (φ i) μ<VAR>hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ).toReal ≤ I<VAR>hfm : AEStronglyMeasurable f μ<VAR>i : ι<VAR>hi : (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ).toReal ≤ I<GOAL>∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : l.NeBot<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), IntegrableOn f (φ i) μ<VAR>hbounded : ∀ᶠ (i : ι) in l, (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ).toReal ≤ I<VAR>hfm : AEStronglyMeasurable f μ<VAR>i : ι<VAR>hi : (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ).toReal ≤ I<GOAL>ENNReal.ofReal (∫⁻ (a : α) in φ i, ↑‖f a‖₊ ∂μ).toReal ≤ ENNReal.ofReal I
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>hr : 0 < r<GOAL>Tendsto (fun x => f x / r) l atBot ↔ Tendsto f l atBot