ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>f : (i : ι) → κ i → α<VAR>x✝ : CompleteLattice α := minAx.toCompleteLattice<VAR>g : ((i : ι) → κ i) → ι<GOAL>⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>f : (i : ι) → κ i → α<VAR>x✝ : CompleteLattice α := minAx.toCompleteLattice<VAR>g : ((i : ι) → κ i) → ι<VAR>a : ι<VAR>ha : ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)<GOAL>⨅ i, f (g i) (i (g i)) ≤ ⨆ i, ⨅ j, f i j
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>f : (i : ι) → κ i → α<VAR>x✝ : CompleteLattice α := minAx.toCompleteLattice<VAR>g : ((i : ι) → κ i) → ι<VAR>a : ι<VAR>ha : ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)<GOAL>⨅ i, f (g i) (i (g i)) ≤ ⨅ j, f a j
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>f : (i : ι) → κ i → α<VAR>x✝ : CompleteLattice α := minAx.toCompleteLattice<VAR>g : ((i : ι) → κ i) → ι<VAR>a : ι<VAR>ha : ∀ (b : κ a), ∃ f, ∃ (h : a = g f), h ▸ b = f (g f)<VAR>b : κ a<GOAL>⨅ i, f (g i) (i (g i)) ≤ f a b
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>minAx : MinimalAxioms α<VAR>f : (i : ι) → κ i → α<VAR>x✝ : CompleteLattice α := minAx.toCompleteLattice<VAR>g : ((i : ι) → κ i) → ι<VAR>h : (i : ι) → κ i<VAR>ha : ∀ (b : κ (g h)), ∃ f, ∃ (h_1 : g h = g f), h_1 ▸ b = f (g f)<GOAL>⨅ i, f (g i) (i (g i)) ≤ f (g h) (h (g h))
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : HasContDiffBump E<VAR>inst✝ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x✝ : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>x : E<GOAL>f.normed μ (c - x) = f.normed μ (c + x)
<VAR>s : Set ℝ<VAR>h : BddAbove s<VAR>h' : s.Nonempty<VAR>a : ℝ<GOAL>a ≤ sSup s ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x
<VAR>s : Set ℝ<VAR>h : BddAbove s<VAR>h' : s.Nonempty<VAR>a : ℝ<GOAL>(∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ : R<VAR>a✝ : μ₁ ∈ {μ | ⨆ k, (f.genEigenspace μ) k ≠ ⊥}<VAR>μ₂ : R<VAR>hμ₂ : μ₂ ∈ {μ | ⨆ k, (f.genEigenspace μ) k ≠ ⊥}<VAR>hμ₁₂ : ⨆ k, (f.genEigenspace μ₁) k = ⨆ k, (f.genEigenspace μ₂) k<GOAL>μ₁ = μ₂
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ : R<VAR>a✝ : μ₁ ∈ {μ | ⨆ k, (f.genEigenspace μ) k ≠ ⊥}<VAR>μ₂ : R<VAR>hμ₂ : μ₂ ∈ {μ | ⨆ k, (f.genEigenspace μ) k ≠ ⊥}<VAR>hμ₁₂ : ⨆ k, (f.genEigenspace μ₁) k = ⨆ k, (f.genEigenspace μ₂) k<VAR>contra : ¬μ₁ = μ₂<GOAL>False
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Field K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : End R M<VAR>μ₁ : R<VAR>a✝ : μ₁ ∈ {μ | ⨆ k, (f.genEigenspace μ) k ≠ ⊥}<VAR>μ₂ : R<VAR>hμ₂ : μ₂ ∈ {μ | ⨆ k, (f.genEigenspace μ) k ≠ ⊥}<VAR>hμ₁₂ : ⨆ k, (f.genEigenspace μ₁) k = ⨆ k, (f.genEigenspace μ₂) k<VAR>contra : ¬μ₁ = μ₂<GOAL>⨆ k, (f.genEigenspace μ₂) k = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>f g : Filter α<VAR>s t : Set α<GOAL>¬f ≤ g ↔ ∃ s ∈ g, s ∉ f
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>h : H.index = 2<VAR>a b : G<VAR>ha : a ∉ H<VAR>hb : b ∉ H<GOAL>a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>h : H.index = 2<VAR>a b : G<VAR>ha : a ∉ H<VAR>hb : b ∉ H<GOAL>a * b ∈ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>h : H.index = 2<VAR>a b : G<VAR>ha : a ∉ H<VAR>hb : b ∉ H<VAR>c : G<VAR>hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)<GOAL>a * b ∈ H
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K L : Subgroup G<VAR>h : H.index = 2<VAR>a b : G<VAR>ha : a ∉ H<VAR>hb : b ∉ H<VAR>c : G<VAR>hc : ∀ (b : G), Xor' (b * c ∈ H) (b ∈ H)<GOAL>a * b * c ∉ H
<VAR>n d : Int<GOAL>-(n /. d) = -n /. d
<VAR>b : Ordinal.{u_1}<VAR>h : 1 < b<VAR>x : Ordinal.{u_1}<GOAL>log b x = (sInf {o | x < b ^ o}).pred
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X✝ Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>X : Set α<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>M.closure X = ⋂₀ {F | M.Flat F ∧ X ⊆ F}
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>x : ℤ<GOAL>x ∈ map castEmbedding (filter (fun x => x ≡ v [MOD r]) (Ico a b)) ↔ x ∈ filter (fun x => x ≡ ↑v [ZMOD ↑r]) (Ico ↑a ↑b)
<VAR>a b r : ℕ<VAR>hr : 0 < r<VAR>v : ℕ<VAR>x : ℤ<GOAL>(∃ a_1, ((a ≤ a_1 ∧ a_1 < b) ∧ a_1 ≡ v [MOD r]) ∧ ↑a_1 = x) ↔ (↑a ≤ x ∧ x < ↑b) ∧ x ≡ ↑v [ZMOD ↑r]
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : S.HasRightHomology<VAR>A : C<VAR>f₁ f₂ : A ⟶ S.rightHomology<VAR>h : f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι<GOAL>f₁ = f₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a✝ b✝ c✝ d a b c : G<GOAL>a * c * (b / c) = a * b
<VAR>α : Type u_1<VAR>a : α<GOAL>∀ {L : Array (Array α)}, a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l
<VAR>α : Type u_1<VAR>a : α<GOAL>∀ {L : Array (Array α)}, (∃ l, (∃ a, a ∈ L.data ∧ a.data = l) ∧ a ∈ l) ↔ ∃ l, l ∈ L.data ∧ a ∈ l.data
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : AEMeasurable f ((κ ⊗ₖ η) a)<GOAL>∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : AEMeasurable f ((κ ⊗ₖ η) a)<VAR>A : ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η) a<GOAL>∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : AEMeasurable f ((κ ⊗ₖ η) a)<VAR>A : ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η) a<VAR>B : ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a = ∫⁻ (x : β), ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂η (a, x) ∂κ a<GOAL>∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>f : β × γ → ℝ≥0∞<VAR>hf : AEMeasurable f ((κ ⊗ₖ η) a)<VAR>A : ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η) a<VAR>B : ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a = ∫⁻ (x : β), ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂η (a, x) ∂κ a<GOAL>Measurable (AEMeasurable.mk f hf)
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → AddGroup (N a)<VAR>f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a<GOAL>(f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂
<VAR>J : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝ : Category.{v₂, u₂} K<VAR>F : J ⥤ K ⥤ TypeMax<VAR>k : K<VAR>t : Cocone F<VAR>h : IsColimit t<VAR>x : t.pt.obj k<VAR>hev : IsColimit (((evaluation K TypeMax).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K TypeMax).obj k) h<GOAL>∃ j y, x = (t.ι.app j).app k y
<VAR>J : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝ : Category.{v₂, u₂} K<VAR>F : J ⥤ K ⥤ TypeMax<VAR>k : K<VAR>t : Cocone F<VAR>h : IsColimit t<VAR>hev : IsColimit (((evaluation K TypeMax).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K TypeMax).obj k) h<VAR>j : J<VAR>y : (F ⋙ (evaluation K TypeMax).obj k).obj j<GOAL>∃ j_1 y_1, (((evaluation K TypeMax).obj k).mapCocone t).ι.app j y = (t.ι.app j_1).app k y_1
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>f : G → G → ℝ≥0∞<VAR>hf : AEMeasurable (uncurry f) (μ.prod ν)<GOAL>∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>f : G → G → ℝ≥0∞<VAR>hf : AEMeasurable (uncurry f) (μ.prod ν)<VAR>h : Measurable fun z => (z.2 * z.1, z.1⁻¹)<GOAL>∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>f : G → G → ℝ≥0∞<VAR>hf : AEMeasurable (uncurry f) (μ.prod ν)<VAR>h : Measurable fun z => (z.2 * z.1, z.1⁻¹)<VAR>h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹) (μ.prod ν)<GOAL>∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>f : G → G → ℝ≥0∞<VAR>hf : AEMeasurable (uncurry f) (μ.prod ν)<VAR>h : Measurable fun z => (z.2 * z.1, z.1⁻¹)<VAR>h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹) (μ.prod ν)<GOAL>∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν = ∫⁻ (z : G × G), f z.1 z.2 ∂μ.prod ν
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>f : G → G → ℝ≥0∞<VAR>hf : AEMeasurable (uncurry f) (μ.prod ν)<VAR>h : Measurable fun z => (z.2 * z.1, z.1⁻¹)<VAR>h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹) (μ.prod ν)<GOAL>∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν = ∫⁻ (z : G × G), f z.1 z.2 ∂map (fun z => (z.2 * z.1, z.1⁻¹)) (μ.prod ν)
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>f : G → G → ℝ≥0∞<VAR>hf : AEMeasurable (uncurry f) (μ.prod ν)<VAR>h : Measurable fun z => (z.2 * z.1, z.1⁻¹)<VAR>h2f : AEMeasurable (uncurry fun x y => f (y * x) x⁻¹) (μ.prod ν)<GOAL>∫⁻ (z : G × G), f z.1 z.2 ∂map (fun z => (z.2 * z.1, z.1⁻¹)) (μ.prod ν) = ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>y : Set β<GOAL>maximals r (⇑f ⁻¹' y) = ⇑f ⁻¹' maximals s (y ∩ range ⇑f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>y : Set β<GOAL>⇑f ⁻¹' y = univ ∩ ⇑f ⁻¹' y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>y : Set β<GOAL>⇑f ⁻¹' maximals s (y ∩ range ⇑f) = univ ∩ ⇑f ⁻¹' maximals s (⇑f '' univ ∩ y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>a a' : α<VAR>v : Vector α n<GOAL>a' ∈ (a ::ᵥ v).toList ↔ a' = a ∨ a' ∈ v.toList
<VAR>a b : ℕ<GOAL>range (a + b) = range a ∪ map (fun x => a + x) (range b)
<VAR>a b : ℕ<GOAL>(range a).Disjoint (map (fun x => a + x) (range b))
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ sinKernel a =O[atTop] fun x => rexp (-p * x)
<VAR>a : ℝ<GOAL>∃ p, 0 < p ∧ sinKernel ↑a =O[atTop] fun x => rexp (-p * x)
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t => rexp (-p * t)<GOAL>∃ p, 0 < p ∧ sinKernel ↑a =O[atTop] fun x => rexp (-p * x)
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t => rexp (-p * t)<GOAL>∀ᶠ (x : ℝ) in atTop, ‖sinKernel (↑a) x‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 x
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t => rexp (-p * t)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>‖sinKernel (↑a) t‖ ≤ 2 * HurwitzKernelBounds.F_nat 1 0 t
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t => rexp (-p * t)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>‖∑' (b : ℕ), 2 * ↑b * Real.sin (2 * π * a * ↑b) * rexp (-π * ↑b ^ 2 * t)‖ ≤ 2 * ∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t => rexp (-p * t)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => 2 * HurwitzKernelBounds.f_nat 1 0 t n) (2 * ∑' (n : ℕ), HurwitzKernelBounds.f_nat 1 0 t n)
<VAR>a p : ℝ<VAR>hp : 0 < p<VAR>hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t => rexp (-p * t)<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>∀ (i : ℕ), ‖2 * ↑i * Real.sin (2 * π * a * ↑i) * rexp (-π * ↑i ^ 2 * t)‖ ≤ 2 * HurwitzKernelBounds.f_nat 1 0 t i
<VAR>P : MorphismProperty Scheme<VAR>hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f<GOAL>IsLocalAtTarget P.universally
<VAR>P : MorphismProperty Scheme<VAR>hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f<GOAL>∀ {X Y : Scheme} (f : X ⟶ Y) (U : Y.Opens), P.universally f → P.universally (f ∣_ U)
<VAR>P : MorphismProperty Scheme<VAR>hP₂ : ∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f<GOAL>∀ {X Y : Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P.universally (f ∣_ U i)) → P.universally f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>r : List α<GOAL>take ((r ++ l₁).length - l₁.length) (r ++ l₁) ++ l₁ = r ++ l₁
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝³ : Ring R₂<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>s : Set M₂<VAR>h₀ : s.Nonempty<VAR>h₁ : s ⊆ ↑(range f)<GOAL>span R (⇑f ⁻¹' s) = comap f (span R₂ s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝³ : Ring R₂<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>s : Set M₂<VAR>h₀ : s.Nonempty<VAR>h₁ : s ⊆ ↑(range f)<GOAL>comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝³ : Ring R₂<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>s : Set M₂<VAR>h₀ : s.Nonempty<VAR>h₁ : s ⊆ ↑(range f)<VAR>hk : ker f ≤ span R (⇑f ⁻¹' s)<GOAL>comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝³ : Ring R₂<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>s : Set M₂<VAR>h₀ : s.Nonempty<VAR>h₁ : s ⊆ ↑(range f)<VAR>hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ ker f<GOAL>comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝³ : Ring R₂<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>s : Set M₂<VAR>h₀ : s.Nonempty<VAR>h₁ : s ⊆ Set.range ⇑f<VAR>hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ ker f<GOAL>comap f (span R₂ s) ≤ span R (⇑f ⁻¹' s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>r : R<VAR>x y : M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>p p' : Submodule R M<VAR>R₂ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝³ : Ring R₂<VAR>inst✝² : AddCommGroup M₂<VAR>inst✝¹ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>q : Submodule R₂ M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>s : Set M₂<VAR>h₀ : s.Nonempty<VAR>h₁ : s ⊆ Set.range ⇑f<VAR>hk : span R (⇑f ⁻¹' s) = span R (⇑f ⁻¹' s) ⊔ ker f<GOAL>range f ⊓ span R₂ s ≤ span R₂ s
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{?u.9011, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝¹ : HasWeakSheafify J D<VAR>inst✝ : J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X'✝ X✝ : Sheaf J E<VAR>Y✝ : Sheaf J D<VAR>f : X'✝ ⟶ X✝<VAR>g : X✝ ⟶ (sheafCompose J F).obj Y✝<GOAL>sheafifyLift J (((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X'✝.val Y✝.val).symm (f.val ≫ g.val)) ⋯ = ((presheafToSheaf J D).map (whiskerRight f.val G)).val ≫ sheafifyLift J (((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X✝.val Y✝.val).symm g.val) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{?u.9011, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝¹ : HasWeakSheafify J D<VAR>inst✝ : J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X'✝ X✝ : Sheaf J E<VAR>Y✝ : Sheaf J D<VAR>f : X'✝ ⟶ X✝<VAR>g : X✝ ⟶ (sheafCompose J F).obj Y✝<GOAL>sheafifyLift J (((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X'✝.val Y✝.val).symm (f.val ≫ g.val)) ⋯ = sheafifyLift J (whiskerRight f.val G ≫ ((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X✝.val Y✝.val).symm g.val) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{?u.9011, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝¹ : HasWeakSheafify J D<VAR>inst✝ : J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X'✝ X✝ : Sheaf J E<VAR>Y✝ : Sheaf J D<VAR>f : X'✝ ⟶ X✝<VAR>g : X✝ ⟶ (sheafCompose J F).obj Y✝<GOAL>sheafifyLift J (((whiskeringRight Cᵒᵖ E D).obj G).map f.val ≫ ((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X✝.val Y✝.val).symm g.val) ⋯ = sheafifyLift J (whiskerRight f.val G ≫ ((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X✝.val Y✝.val).symm g.val) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{?u.9011, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝¹ : HasWeakSheafify J D<VAR>inst✝ : J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X'✝ X✝ : Sheaf J E<VAR>Y✝ : Sheaf J D<VAR>f : X'✝ ⟶ X✝<VAR>g : X✝ ⟶ (sheafCompose J F).obj Y✝<GOAL>sheafifyLift J (whiskerRight f.val G ≫ ((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X✝.val Y✝.val).symm g.val) ⋯ = sheafifyLift J (whiskerRight f.val G ≫ ((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X✝.val Y✝.val).symm g.val) ⋯
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{?u.9011, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝¹ : HasWeakSheafify J D<VAR>inst✝ : J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X✝ : Sheaf J E<VAR>Y✝ Y'✝ : Sheaf J D<VAR>f : (composeAndSheafify J G).obj X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Y'✝<VAR>x✝ : Cᵒᵖ<GOAL>(((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X✝.val Y'✝.val) (toSheafify J (X✝.val ⋙ G) ≫ f.val ≫ g.val)).app x✝ = (((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv X✝.val Y✝.val) (toSheafify J (X✝.val ⋙ G) ≫ f.val)).app x✝ ≫ F.map (g.val.app x✝)
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{?u.9011, u_1} E<VAR>F : D ⥤ E<VAR>G : E ⥤ D<VAR>inst✝¹ : HasWeakSheafify J D<VAR>inst✝ : J.HasSheafCompose F<VAR>adj : G ⊣ F<VAR>X✝ : Sheaf J E<VAR>Y✝ Y'✝ : Sheaf J D<VAR>f : (composeAndSheafify J G).obj X✝ ⟶ Y✝<VAR>g : Y✝ ⟶ Y'✝<VAR>x✝ : Cᵒᵖ<GOAL>((Adjunction.whiskerRight Cᵒᵖ adj).unit.app X✝.val ≫ ((whiskeringRight Cᵒᵖ D E).obj F).map (toSheafify J (X✝.val ⋙ G) ≫ f.val ≫ g.val)).app x✝ = ((Adjunction.whiskerRight Cᵒᵖ adj).unit.app X✝.val ≫ ((whiskeringRight Cᵒᵖ D E).obj F).map (toSheafify J (X✝.val ⋙ G) ≫ f.val)).app x✝ ≫ F.map (g.val.app x✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h : MapsTo f s t<GOAL>Injective (restrict f s t h) ↔ InjOn f s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>f : ↥(lp G 2)<GOAL>Summable fun i => (V i) (↑f i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>f : ↥(lp G 2)<GOAL>Summable fun i => ‖↑f i‖ ^ 2
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>f : ↥(lp G 2)<VAR>x✝ : ι<GOAL>‖↑f x✝‖ ^ 2 = ‖↑f x✝‖ ^ ENNReal.toReal 2
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>f : ↥(lp G 2)<GOAL>0 < ENNReal.toReal 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<GOAL>IsOpen (range ofNNReal)