ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>H : ι → Type := fun _i => FreeGroup Unit<VAR>f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i<VAR>X' : ι → Set α := fun i => X i ∪ Y i<GOAL>Pairwise fun i j => Disjoint (X' i) (X' j)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>H : ι → Type := fun _i => FreeGroup Unit<VAR>f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i<VAR>X' : ι → Set α := fun i => X i ∪ Y i<GOAL>Pairwise fun i j => ∀ (h : H i), h ≠ 1 → (f i) h • X' j ⊆ X' i
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>H : ι → Type := fun _i => FreeGroup Unit<VAR>f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i<VAR>X' : ι → Set α := fun i => X i ∪ Y i<GOAL>3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>H : ι → Type := fun _i => FreeGroup Unit<VAR>f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i<VAR>X' : ι → Set α := fun i => X i ∪ Y i<VAR>inhabited_h : Inhabited ι<GOAL>∃ i, 3 ≤ #(H i)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>H : ι → Type := fun _i => FreeGroup Unit<VAR>f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i<VAR>X' : ι → Set α := fun i => X i ∪ Y i<VAR>inhabited_h : Inhabited ι<GOAL>3 ≤ #(H default)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>H : ι → Type := fun _i => FreeGroup Unit<VAR>f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i<VAR>X' : ι → Set α := fun i => X i ∪ Y i<VAR>inhabited_h : Inhabited ι<GOAL>3 ≤ #(FreeGroup Unit)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>H : ι → Type := fun _i => FreeGroup Unit<VAR>f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i<VAR>X' : ι → Set α := fun i => X i ∪ Y i<VAR>inhabited_h : Inhabited ι<GOAL>3 ≤ ℵ₀
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝⁴ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝³ : Monoid N<VAR>inst✝² : Nontrivial ι<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>a : ι → G<VAR>α : Type u_4<VAR>inst✝ : MulAction G α<VAR>X Y : ι → Set α<VAR>hXnonempty : ∀ (i : ι), (X i).Nonempty<VAR>hXdisj : Pairwise fun i j => Disjoint (X i) (X j)<VAR>hYdisj : Pairwise fun i j => Disjoint (Y i) (Y j)<VAR>hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)<VAR>hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i<VAR>hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i<VAR>H : ι → Type := fun _i => FreeGroup Unit<VAR>f : (i : ι) → H i →* G := fun i => FreeGroup.lift fun x => a i<VAR>X' : ι → Set α := fun i => X i ∪ Y i<VAR>inhabited_h : Inhabited ι<GOAL>3 < ℵ₀
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<GOAL>range (continuousLinearMapOfBilin B) = ⊤
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<VAR>this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))<GOAL>range (continuousLinearMapOfBilin B) = ⊤
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<VAR>this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))<GOAL>(range (continuousLinearMapOfBilin B))ᗮᗮ = ⊤
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>coercive : IsCoercive B<VAR>this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))<GOAL>∀ (x : V), x ∈ (range (continuousLinearMapOfBilin B))ᗮᗮ
<VAR>V : Type u<VAR>inst✝² : NormedAddCommGroup V<VAR>inst✝¹ : InnerProductSpace ℝ V<VAR>inst✝ : CompleteSpace V<VAR>B : V →L[ℝ] V →L[ℝ] ℝ<VAR>this : CompleteSpace ↑↑(range (continuousLinearMapOfBilin B))<VAR>v : V<VAR>C : ℝ<VAR>C_pos : 0 < C<VAR>coercivity : ∀ (u : V), C * ‖u‖ * ‖u‖ ≤ (B u) u<VAR>mem_w_orthogonal : 0 ∈ (range (continuousLinearMapOfBilin B))ᗮ<GOAL>⟪0, v⟫_ℝ = 0
<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_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<GOAL>IsSFiniteKernel (κ.withDensity f)
<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_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<VAR>h_eq_sum : κ.withDensity f = Kernel.sum fun i => (κ.seq i).withDensity f<GOAL>IsSFiniteKernel (κ.withDensity f)
<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_ne_top : ∀ (a : α) (b : β), f a b ≠ ⊤<VAR>h_eq_sum : κ.withDensity f = Kernel.sum fun i => (κ.seq i).withDensity f<GOAL>IsSFiniteKernel (Kernel.sum fun i => (κ.seq i).withDensity f)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>(𝓤 E).HasBasis (fun ε => 0 < ε) fun ε => {p | ‖p.1 / p.2‖ < ε}
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝² : SeminormedGroup E<VAR>inst✝¹ : SeminormedGroup F<VAR>inst✝ : SeminormedGroup G<VAR>s : Set E<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<GOAL>(fun ε => {p | ‖p.1 / p.2‖ < ε}) = fun ε => {p | dist p.1 p.2 < ε}
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι<VAR>c : R<VAR>t✝ : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>s t : Set E<GOAL>(convexHull R) (s - t) = (convexHull R) s - (convexHull R) t
<GOAL>isomorphisms Scheme = (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓ stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f
<GOAL>(((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => OpenEmbedding) ⊓ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective) ⊓ stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f) = (isomorphisms TopCat).inverseImage Scheme.forgetToTop ⊓ stalkwise fun {R S} [CommRing R] [CommRing S] f => Function.Bijective ⇑f
<VAR>X Y : Scheme<VAR>f : X ⟶ Y<GOAL>((topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => OpenEmbedding) ⊓ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => Function.Surjective) f ↔ (isomorphisms TopCat).inverseImage Scheme.forgetToTop f
<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>x y : E<VAR>s t : Set E<VAR>a b : ℝ<VAR>hab : a < b<GOAL>(interior (Ioc a b)).Nonempty
<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>x y : E<VAR>s t : Set E<VAR>a b : ℝ<VAR>hab : ¬a < b<GOAL>UniqueDiffOn ℝ (Ioc a b)
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>(l.set n a).get? n = some a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>c : 𝕜<VAR>f : α → F<GOAL>eLpNorm (c • f) p μ = ↑‖c‖₊ * eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>f : α → F<GOAL>eLpNorm (0 • f) p μ = ↑‖0‖₊ * eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>c : 𝕜<VAR>f : α → F<VAR>hc : c ≠ 0<GOAL>eLpNorm (c • f) p μ = ↑‖c‖₊ * eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>c : 𝕜<VAR>f : α → F<VAR>hc : c ≠ 0<GOAL>↑‖c‖₊ * eLpNorm f p μ ≤ eLpNorm (c • f) p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedAddCommGroup G<VAR>𝕜 : Type u_5<VAR>inst✝⁴ : NormedDivisionRing 𝕜<VAR>inst✝³ : MulActionWithZero 𝕜 E<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : BoundedSMul 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 F<VAR>c : 𝕜<VAR>f : α → F<VAR>hc : c ≠ 0<VAR>this : eLpNorm (c⁻¹ • c • f) p μ ≤ ‖c⁻¹‖₊ • eLpNorm (c • f) p μ<GOAL>↑‖c‖₊ * eLpNorm f p μ ≤ eLpNorm (c • f) p μ
<VAR>x : PGame<VAR>IHl : ∀ (i : x.LeftMoves) {y : PGame}, x.moveLeft i ≡r y → (x.moveLeft i).Numeric → y.Numeric<VAR>IHr : ∀ (j : x.RightMoves) {y : PGame}, x.moveRight j ≡r y → (x.moveRight j).Numeric → y.Numeric<VAR>y : PGame<VAR>r : x ≡r y<VAR>ox : x.Numeric<GOAL>y.Numeric
<VAR>x : PGame<VAR>IHl : ∀ (i : x.LeftMoves) {y : PGame}, x.moveLeft i ≡r y → (x.moveLeft i).Numeric → y.Numeric<VAR>IHr : ∀ (j : x.RightMoves) {y : PGame}, x.moveRight j ≡r y → (x.moveRight j).Numeric → y.Numeric<VAR>y : PGame<VAR>r : x ≡r y<VAR>ox : x.Numeric<VAR>i : y.LeftMoves<VAR>j : y.RightMoves<GOAL>y.moveLeft i < y.moveRight j
<VAR>x : PGame<VAR>IHl : ∀ (i : x.LeftMoves) {y : PGame}, x.moveLeft i ≡r y → (x.moveLeft i).Numeric → y.Numeric<VAR>IHr : ∀ (j : x.RightMoves) {y : PGame}, x.moveRight j ≡r y → (x.moveRight j).Numeric → y.Numeric<VAR>y : PGame<VAR>r : x ≡r y<VAR>ox : x.Numeric<VAR>i : y.LeftMoves<GOAL>(y.moveLeft i).Numeric
<VAR>x : PGame<VAR>IHl : ∀ (i : x.LeftMoves) {y : PGame}, x.moveLeft i ≡r y → (x.moveLeft i).Numeric → y.Numeric<VAR>IHr : ∀ (j : x.RightMoves) {y : PGame}, x.moveRight j ≡r y → (x.moveRight j).Numeric → y.Numeric<VAR>y : PGame<VAR>r : x ≡r y<VAR>ox : x.Numeric<VAR>j : y.RightMoves<GOAL>(y.moveRight j).Numeric
<VAR>ι : Type u_1<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>G : ι → Type u_4<VAR>inst✝² : Semigroup G₁<VAR>inst✝¹ : Semigroup G₂<VAR>inst✝ : (i : ι) → Semigroup (G i)<VAR>fst✝¹ : G₁<VAR>snd✝¹ : G₂<VAR>fst✝ : G₁<VAR>snd✝ : G₂<GOAL>(fst✝¹, snd✝¹) ∣ (fst✝, snd✝) ↔ (fst✝¹, snd✝¹).1 ∣ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 ∣ (fst✝, snd✝).2
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S : ι → Subsemigroup M<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>x : LaurentSeries R<GOAL>(ofPowerSeries ℤ R) x.powerSeriesPart = (single (-order x)) 1 * x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>x : LaurentSeries R<GOAL>(ofPowerSeries ℤ R) x.powerSeriesPart = (single (-order x)) 1 * ((single (order x)) 1 * (ofPowerSeries ℤ R) x.powerSeriesPart)
<VAR>n m : ℕ<VAR>a : Fin n<VAR>b : Fin (n + 1)<GOAL>a.succ.predAbove b.succ = (a.predAbove b).succ
<VAR>n m : ℕ<VAR>a : Fin n<VAR>b : Fin (n + 1)<VAR>h : a.succ ≤ b<GOAL>a.succ.predAbove b.succ = (a.predAbove b).succ
<VAR>n m : ℕ<VAR>a : Fin n<VAR>b : Fin (n + 1)<VAR>h : b < a.succ<GOAL>a.succ.predAbove b.succ = (a.predAbove b).succ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>x : SimplexCategory<GOAL>f.unop.right.op ≫ ((unop Y✝).hom.app (op x)).op = ((unop X✝).hom.app (op x)).op ≫ (f.unop.left.app (op x)).op
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>x : SimplexCategory<GOAL>((unop Y✝).hom.app (op x) ≫ f.unop.right).op = (f.unop.left.app (op x) ≫ (unop X✝).hom.app (op x)).op
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ<VAR>f : X✝ ⟶ Y✝<VAR>x : SimplexCategory<GOAL>(unop Y✝).hom.app (op x) ≫ f.unop.right = f.unop.left.app (op x) ≫ (unop X✝).hom.app (op x)
<VAR>R : Type u_1<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>ι : Type u_3<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Nonempty ι<VAR>e : Basis ι R M<VAR>x : Orientation R M ι<VAR>v : ι → M<GOAL>|(e.adjustToOrientation x).det v| = |e.det v|
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A A' : C<VAR>f : A' ⟶ A<GOAL>(mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv ≫ whiskerLeft F ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) (prod.functor.map (F.map f))) = whiskerRight ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) (prod.functor.map f)) F ≫ (mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A A' : C<VAR>f : A' ⟶ A<VAR>vcomp1 : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A'))) (leftAdjointSquareConjugate.vcomp (prodComparisonNatIso F A).inv (prod.functor.map (F.map f))) = rightAdjointSquareConjugate.vcomp ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv) ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) (prod.functor.map (F.map f)))<GOAL>(mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv ≫ whiskerLeft F ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) (prod.functor.map (F.map f))) = whiskerRight ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) (prod.functor.map f)) F ≫ (mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A A' : C<VAR>f : A' ⟶ A<VAR>vcomp1 : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A'))) (leftAdjointSquareConjugate.vcomp (prodComparisonNatIso F A).inv (prod.functor.map (F.map f))) = rightAdjointSquareConjugate.vcomp ((mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv) ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) (prod.functor.map (F.map f)))<VAR>vcomp2 : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A'))) (leftAdjointConjugateSquare.vcomp (prod.functor.map f) (prodComparisonNatIso F A').inv) = rightAdjointConjugateSquare.vcomp ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) (prod.functor.map f)) ((mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv)<GOAL>(mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv ≫ whiskerLeft F ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) (prod.functor.map (F.map f))) = whiskerRight ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) (prod.functor.map f)) F ≫ (mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A A' : C<VAR>f : A' ⟶ A<VAR>vcomp1 : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A'))) (whiskerLeft F (prod.functor.map (F.map f)) ≫ (prodComparisonNatIso F A).inv) = (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv ≫ whiskerLeft F ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) (prod.functor.map (F.map f)))<VAR>vcomp2 : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A'))) ((prodComparisonNatIso F A').inv ≫ whiskerRight (prod.functor.map f) F) = whiskerRight ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) (prod.functor.map f)) F ≫ (mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv<VAR>B : C<GOAL>(whiskerLeft F (prod.functor.map (F.map f)) ≫ (prodComparisonNatIso F A).inv).app B = ((prodComparisonNatIso F A').inv ≫ whiskerRight (prod.functor.map f) F).app B
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A A' : C<VAR>f : A' ⟶ A<VAR>vcomp1 : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A'))) (whiskerLeft F (prod.functor.map (F.map f)) ≫ (prodComparisonNatIso F A).inv) = (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv ≫ whiskerLeft F ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) (prod.functor.map (F.map f)))<VAR>vcomp2 : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A'))) ((prodComparisonNatIso F A').inv ≫ whiskerRight (prod.functor.map f) F) = whiskerRight ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) (prod.functor.map f)) F ≫ (mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv<VAR>B : C<GOAL>prod.map (F.map f) (𝟙 (F.obj B)) ≫ inv (prodComparison F A B) = inv (prodComparison F A' B) ≫ F.map (prod.map f (𝟙 B))
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>A A' : C<VAR>f : A' ⟶ A<VAR>vcomp1 : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A'))) (whiskerLeft F (prod.functor.map (F.map f)) ≫ (prodComparisonNatIso F A).inv) = (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A))) (prodComparisonNatIso F A).inv ≫ whiskerLeft F ((conjugateEquiv (exp.adjunction (F.obj A)) (exp.adjunction (F.obj A'))) (prod.functor.map (F.map f)))<VAR>vcomp2 : (mateEquiv (exp.adjunction A) (exp.adjunction (F.obj A'))) ((prodComparisonNatIso F A').inv ≫ whiskerRight (prod.functor.map f) F) = whiskerRight ((conjugateEquiv (exp.adjunction A) (exp.adjunction A')) (prod.functor.map f)) F ≫ (mateEquiv (exp.adjunction A') (exp.adjunction (F.obj A'))) (prodComparisonNatIso F A').inv<VAR>B : C<GOAL>prod.map (F.map f) (F.map (𝟙 B)) ≫ inv (prodComparison F A B) = inv (prodComparison F A' B) ≫ F.map (prod.map f (𝟙 B))
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<GOAL>Set.range ((⇑U.ι.val.base ∘ ⇑(↑U).isoSpec.inv.val.base) ∘ ⇑(Spec.map (X.presheaf.map (eqToHom ⋯).op)).val.base) = ↑U