ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<VAR>s1 s2 : AffineSubspace k P<GOAL>Submodule.span k (↑s1 -ᵥ ↑s1) ⊔ Submodule.span k (↑s2 -ᵥ ↑s2) ≤ Submodule.span k (↑(s1 ⊔ s2) -ᵥ ↑(s1 ⊔ s2))
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪x, o.rightAngleRotation y⟫_ℝ = -(o.areaForm x) y
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪x, (LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) ⋯ ⋯) y⟫_ℝ = -(o.areaForm x) y
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Ioi a = Ioi ↑a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>x : E<GOAL>gauge (-s) x = gauge s (-x)
<VAR>α : Type<VAR>d✝ : ℕ<VAR>ds✝ ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>d : ℕ<VAR>ds : List ℕ<VAR>x : Holor α (d :: ds)<GOAL>CPRankMax (d :: ds).prod x
<VAR>α : Type<VAR>d✝ : ℕ<VAR>ds✝ ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>d : ℕ<VAR>ds : List ℕ<VAR>x : Holor α (d :: ds)<VAR>h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)<GOAL>CPRankMax (d :: ds).prod x
<VAR>α : Type<VAR>d✝ : ℕ<VAR>ds✝ ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>d : ℕ<VAR>ds : List ℕ<VAR>x : Holor α (d :: ds)<VAR>h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)<VAR>h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod<GOAL>CPRankMax (d :: ds).prod x
<VAR>α : Type<VAR>d✝ : ℕ<VAR>ds✝ ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>d : ℕ<VAR>ds : List ℕ<VAR>x : Holor α (d :: ds)<VAR>h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)<VAR>h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod<VAR>this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)<GOAL>CPRankMax (d :: ds).prod x
<VAR>α : Type<VAR>d✝ : ℕ<VAR>ds✝ ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>d : ℕ<VAR>ds : List ℕ<VAR>x : Holor α (d :: ds)<VAR>h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)<VAR>h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod<VAR>this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)<VAR>h_cprankMax_sum : CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)<GOAL>CPRankMax (d :: ds).prod x
<VAR>α : Type<VAR>d✝ : ℕ<VAR>ds✝ ds₁ ds₂ ds₃ : List ℕ<VAR>inst✝ : Ring α<VAR>d : ℕ<VAR>ds : List ℕ<VAR>x : Holor α (d :: ds)<VAR>h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax ds.prod (unitVec d ↑i ⊗ x.slice ↑i ⋯)<VAR>h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod<VAR>this : CPRankMax ((Finset.range d).attach.card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)<VAR>h_cprankMax_sum : CPRankMax ((Finset.range d).card * ds.prod) (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)<GOAL>CPRankMax (d :: ds).prod (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>hm : m ≤ m0<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f (μ.trim hm)<GOAL>∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddMonoid G<VAR>a : G<VAR>b : k<GOAL>single a b ^ 0 = single (0 • a) (b ^ 0)
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddMonoid G<VAR>a : G<VAR>b : k<GOAL>1 = single 0 1
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddMonoid G<VAR>a : G<VAR>b : k<VAR>n : ℕ<GOAL>single a b ^ (n + 1) = single ((n + 1) • a) (b ^ (n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>s : Set (β × Ω)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : β), (ρ.condKernel x) {y | (x, y) ∈ s} ∂ρ.fst = ρ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>s : Set (β × Ω)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : β), (ρ.condKernel x) {y | (x, y) ∈ s} ∂ρ.fst = (ρ.fst ⊗ₘ ρ.condKernel) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : CountableOrCountablyGenerated α β<VAR>ρ : Measure (β × Ω)<VAR>inst✝ : IsFiniteMeasure ρ<VAR>f : β × Ω → ℝ≥0∞<VAR>s : Set (β × Ω)<VAR>hs : MeasurableSet s<GOAL>∫⁻ (x : β), (ρ.condKernel x) {y | (x, y) ∈ s} ∂ρ.fst = ∫⁻ (a : β), (ρ.condKernel a) (Prod.mk a ⁻¹' s) ∂ρ.fst
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : i ⟶ j<GOAL>F.eventualRange j = range (F.map f) ↔ ∀ ⦃k : J⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map (g ≫ f))
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : i ⟶ j<GOAL>(∀ (i_1 : J) (j_1 : i_1 ⟶ j), range (F.map f) ⊆ range (F.map j_1)) ↔ ∀ ⦃k : J⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map (g ≫ f))
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : i ⟶ j<VAR>h : ∀ ⦃k : J⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map (g ≫ f))<VAR>j' : J<VAR>f' : j' ⟶ j<GOAL>range (F.map f) ⊆ range (F.map f')
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k✝ : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : i ⟶ j<VAR>h : ∀ ⦃k : J⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map (g ≫ f))<VAR>j' : J<VAR>f' : j' ⟶ j<VAR>k : J<VAR>g : k ⟶ i<VAR>g' : k ⟶ j'<VAR>he : g ≫ f = g' ≫ f'<GOAL>range (F.map f) ⊆ range (F.map f')
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k✝ : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : i ⟶ j<VAR>h : ∀ ⦃k : J⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map (g ≫ f))<VAR>j' : J<VAR>f' : j' ⟶ j<VAR>k : J<VAR>g : k ⟶ i<VAR>g' : k ⟶ j'<VAR>he : g ≫ f = g' ≫ f'<GOAL>range (F.map (g ≫ f)) ⊆ range (F.map f')
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j k✝ : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>f : i ⟶ j<VAR>h : ∀ ⦃k : J⦄ (g : k ⟶ i), range (F.map f) ⊆ range (F.map (g ≫ f))<VAR>j' : J<VAR>f' : j' ⟶ j<VAR>k : J<VAR>g : k ⟶ i<VAR>g' : k ⟶ j'<VAR>he : g ≫ f = g' ≫ f'<GOAL>range (F.map g' ≫ F.map f') ⊆ range (F.map f')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup P'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<GOAL>Surjective ⇑(map g g')
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝¹⁴ : CommRing R<VAR>inst✝¹³ : AddCommGroup M<VAR>inst✝¹² : AddCommGroup N<VAR>inst✝¹¹ : AddCommGroup P<VAR>inst✝¹⁰ : Module R M<VAR>inst✝⁹ : Module R N<VAR>inst✝⁸ : Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>Q : Type u_5<VAR>inst✝⁷ : AddCommGroup Q<VAR>inst✝⁶ : Module R Q<VAR>hfg : Exact ⇑f ⇑g<VAR>hg : Surjective ⇑g<VAR>M' : Type u_6<VAR>N' : Type u_7<VAR>P' : Type u_8<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup N'<VAR>inst✝³ : AddCommGroup P'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R N'<VAR>inst✝ : Module R P'<VAR>f' : M' →ₗ[R] N'<VAR>g' : N' →ₗ[R] P'<VAR>hfg' : Exact ⇑f' ⇑g'<VAR>hg' : Surjective ⇑g'<GOAL>Surjective (⇑(lTensor P g') ∘ ⇑(rTensor N' g))
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>trunc n X = Polynomial.X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>f : α → β<VAR>hf : Injective f<VAR>g : α → γ<VAR>g' : β → γ<GOAL>range (extend f g g') = range g ∪ g' '' (range f)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>f : α → β<VAR>hf : Injective f<VAR>g : α → γ<VAR>g' : β → γ<GOAL>range g ∪ g' '' (range f)ᶜ ⊆ range (extend f g g')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>f : α → β<VAR>hf : Injective f<VAR>g : α → γ<VAR>g' : β → γ<VAR>x : α<GOAL>g x ∈ range (extend f g g')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>f : α → β<VAR>hf : Injective f<VAR>g : α → γ<VAR>g' : β → γ<VAR>y : β<VAR>hy : y ∈ (range f)ᶜ<GOAL>g' y ∈ range (extend f g g')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>o : Option α<GOAL>a ∈ o.toList ↔ a ∈ o
<VAR>x : PartENat<GOAL>x + ⊤ = ⊤
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : AddCommMonoid M₃<VAR>inst✝² : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝¹ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝ : (i : ι) → Module R (φ i)<VAR>f : (i : ι) → M₂ →ₗ[R] φ i<GOAL>pi f = 0 ↔ ∀ (i : ι), f i = 0
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>ι' : Type x'<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : AddCommMonoid M₃<VAR>inst✝² : Module R M₃<VAR>φ : ι → Type i<VAR>inst✝¹ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝ : (i : ι) → Module R (φ i)<VAR>f : (i : ι) → M₂ →ₗ[R] φ i<GOAL>(∀ (x : M₂) (a : ι), (f a) x = 0 x a) ↔ ∀ (i : ι) (x : M₂), (f i) x = 0 x
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : Finite Rˣ<VAR>χ : MulChar R ℂ<GOAL>star χ = χ⁻¹
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : Finite Rˣ<VAR>χ : MulChar R ℂ<VAR>val✝ : Fintype Rˣ<GOAL>star χ = χ⁻¹
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : Finite Rˣ<VAR>χ : MulChar R ℂ<VAR>val✝ : Fintype Rˣ<VAR>a : Rˣ<GOAL>(star χ) ↑a = χ⁻¹ ↑a
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : Finite Rˣ<VAR>χ : MulChar R ℂ<VAR>val✝ : Fintype Rˣ<VAR>a : Rˣ<GOAL>(star χ) ↑a = (χ ↑a)⁻¹
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>0 = m * n ↔ m = 0 ∨ n = 0
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>N : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>I₀ : WithTop (Box ι)<VAR>I J : Box ι<VAR>i✝ : ι<VAR>f : ι →ᵇᵃ[I₀] M<VAR>hI : ↑I ≤ I₀<VAR>i : ι<VAR>x : ℝ<GOAL>Option.elim' 0 (⇑f) (I.splitLower i x) + Option.elim' 0 (⇑f) (I.splitUpper i x) = f I
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1
<VAR>R : Type u<VAR>inst✝¹² : CommRing R<VAR>M N P Q : Type u<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : AddCommGroup Q<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Coalgebra R M<VAR>inst✝² : Coalgebra R N<VAR>inst✝¹ : Coalgebra R P<VAR>inst✝ : Coalgebra R Q<GOAL>((comonEquivalence R).symm.inverse.obj (of R M) ⊗ (comonEquivalence R).symm.inverse.obj (of R N)).comul = Coalgebra.comul
<VAR>R : Type u<VAR>inst✝¹² : CommRing R<VAR>M N P Q : Type u<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : AddCommGroup N<VAR>inst✝⁹ : AddCommGroup P<VAR>inst✝⁸ : AddCommGroup Q<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Coalgebra R M<VAR>inst✝² : Coalgebra R N<VAR>inst✝¹ : Coalgebra R P<VAR>inst✝ : Coalgebra R Q<GOAL>(tensor_μ (ModuleCat R)ᵒᵖ (Opposite.op (ModuleCat.mk M), Opposite.op (ModuleCat.mk N)) (Opposite.op (ModuleCat.mk M), Opposite.op (ModuleCat.mk N))).unop ∘ₗ map Coalgebra.comul Coalgebra.comul = ↑(tensorTensorTensorComm R M M N N) ∘ₗ map Coalgebra.comul Coalgebra.comul
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>I✝ : Ideal R<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>H : I.IsMaximal<GOAL>map f I = ⊤ ∨ (map f I).IsMaximal
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Ring R<VAR>inst✝² : Ring S<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : RingHomClass F R S<VAR>f : F<VAR>I✝ : Ideal R<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>H : I.IsMaximal<VAR>ne_top : ¬map f I = ⊤<VAR>J : Ideal S<VAR>hJ : map f I < J<GOAL>J = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝¹ : Monoid R<VAR>inst✝ : MulAction R M<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝¹ : Monoid R<VAR>inst✝ : MulAction R M<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsSMulRegular M (a ^ n) → IsSMulRegular M a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>a b : R<VAR>s : S<VAR>inst✝¹ : Monoid R<VAR>inst✝ : MulAction R M<VAR>n : ℕ<VAR>n0 : 0 < n<GOAL>IsSMulRegular M (a ^ n.pred • a) → IsSMulRegular M a
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<GOAL>IsUnramified k (σ • w) ↔ IsUnramified k w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>m : ι → β<VAR>hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x x_1 => x ≤ x_1) x (m i)<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => s.sup fun i => F i a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>m : ι → β<VAR>hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x x_1 => x ≤ x_1) x (m i)<GOAL>∀ᶠ (x : β) in Filter.map (fun a => s.sup fun i => F i a) f, (fun x x_1 => x ≤ x_1) x (s.sup m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>m : ι → β<VAR>hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i<GOAL>∀ᶠ (a : α) in f, (s.sup fun i => F i a) ≤ s.sup m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝¹ : LinearOrder β<VAR>inst✝ : OrderBot β<VAR>f : Filter α<VAR>F : ι → α → β<VAR>s : Finset ι<VAR>m : ι → β<VAR>hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i<GOAL>∀ᶠ (a : α) in f, (s.sup fun i => F i a) ≤ s.sup m
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<GOAL>AEStronglyMeasurable' m (↑↑(condexpIndSMul hm hs hμs x)) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>h : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ<GOAL>AEStronglyMeasurable' m (↑↑(condexpIndSMul hm hs hμs x)) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>h : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ<GOAL>AEStronglyMeasurable' m (↑↑((compLpL 2 μ (toSpanSingleton ℝ x)) ↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1)))) μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>𝕜 : Type u_7<VAR>p : ℝ≥0∞<VAR>inst✝¹⁹ : RCLike 𝕜<VAR>inst✝¹⁸ : NormedAddCommGroup E<VAR>inst✝¹⁷ : InnerProductSpace 𝕜 E<VAR>inst✝¹⁶ : CompleteSpace E<VAR>inst✝¹⁵ : NormedAddCommGroup E'<VAR>inst✝¹⁴ : InnerProductSpace 𝕜 E'<VAR>inst✝¹³ : CompleteSpace E'<VAR>inst✝¹² : NormedSpace ℝ E'<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup G'<VAR>inst✝⁷ : NormedSpace ℝ G'<VAR>inst✝⁶ : CompleteSpace G'<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>E'' : Type u_8<VAR>𝕜' : Type u_9<VAR>inst✝⁵ : RCLike 𝕜'<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : InnerProductSpace 𝕜' E''<VAR>inst✝² : CompleteSpace E''<VAR>inst✝¹ : NormedSpace ℝ E''<VAR>inst✝ : NormedSpace ℝ G<VAR>hm✝ hm : m ≤ m0<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : G<VAR>h : AEStronglyMeasurable' m (↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ<GOAL>AEStronglyMeasurable' m (⇑(toSpanSingleton ℝ x) ∘ ↑↑↑((condexpL2 ℝ ℝ hm) (indicatorConstLp 2 hs hμs 1))) μ
<VAR>R S : CommRingCat<VAR>φ ψ : R ⟶ S<VAR>f : Spec S ⟶ Spec R<GOAL>map φ = map ψ ↔ φ = ψ
<VAR>R S : CommRingCat<VAR>φ ψ : R ⟶ S<VAR>f : Spec S ⟶ Spec R<GOAL>Scheme.Spec.map φ.op = Scheme.Spec.map ψ.op ↔ map φ = map ψ
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>j : J<GOAL>∃ i_1 f, ∀ ⦃k : J⦄ (g : k ⟶ i_1), range ((F.toPreimages s).map f) ⊆ range ((F.toPreimages s).map (g ≫ f))
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>j j₁ : J<VAR>g₁ : j₁ ⟶ i<VAR>f₁ : j₁ ⟶ j<GOAL>∃ i_1 f, ∀ ⦃k : J⦄ (g : k ⟶ i_1), range ((F.toPreimages s).map f) ⊆ range ((F.toPreimages s).map (g ≫ f))
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>j j₁ : J<VAR>g₁ : j₁ ⟶ i<VAR>f₁ : j₁ ⟶ j<VAR>j₂ : J<VAR>f₂ : j₂ ⟶ j₁<VAR>h₂ : F.eventualRange j₁ = range (F.map f₂)<GOAL>∃ i_1 f, ∀ ⦃k : J⦄ (g : k ⟶ i_1), range ((F.toPreimages s).map f) ⊆ range ((F.toPreimages s).map (g ≫ f))
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>j j₁ : J<VAR>g₁ : j₁ ⟶ i<VAR>f₁ : j₁ ⟶ j<VAR>j₂ : J<VAR>f₂ : j₂ ⟶ j₁<VAR>h₂ : F.eventualRange j₁ = range (F.map f₂)<VAR>j₃ : J<VAR>f₃ : j₃ ⟶ j₂<VAR>x : F.obj j₂<VAR>hx : x ∈ ⋂ f, F.map f ⁻¹' s<VAR>this : F.map f₂ x ∈ F.eventualRange j₁<GOAL>(F.toPreimages s).map (f₂ ≫ f₁) ⟨x, hx⟩ ∈ range ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁))
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>j j₁ : J<VAR>g₁ : j₁ ⟶ i<VAR>f₁ : j₁ ⟶ j<VAR>j₂ : J<VAR>f₂ : j₂ ⟶ j₁<VAR>h₂ : F.eventualRange j₁ = range (F.map f₂)<VAR>j₃ : J<VAR>f₃ : j₃ ⟶ j₂<VAR>x : F.obj j₂<VAR>hx : x ∈ ⋂ f, F.map f ⁻¹' s<VAR>this : F.map f₂ x ∈ F.eventualRange j₁<VAR>y : F.obj j₃<VAR>hy : y ∈ F.eventualRange j₃<VAR>h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x<GOAL>(F.toPreimages s).map (f₂ ≫ f₁) ⟨x, hx⟩ ∈ range ((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁))
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>j j₁ : J<VAR>g₁ : j₁ ⟶ i<VAR>f₁ : j₁ ⟶ j<VAR>j₂ : J<VAR>f₂ : j₂ ⟶ j₁<VAR>h₂ : F.eventualRange j₁ = range (F.map f₂)<VAR>j₃ : J<VAR>f₃ : j₃ ⟶ j₂<VAR>x : F.obj j₂<VAR>hx : x ∈ ⋂ f, F.map f ⁻¹' s<VAR>this : F.map f₂ x ∈ F.eventualRange j₁<VAR>y : F.obj j₃<VAR>hy : y ∈ F.eventualRange j₃<VAR>h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x<VAR>g₂ : j₃ ⟶ i<GOAL>y ∈ F.map g₂ ⁻¹' s
<VAR>J : Type u<VAR>inst✝¹ : Category.{u_1, u} J<VAR>F : J ⥤ Type v<VAR>i j✝ k : J<VAR>s : Set (F.obj i)<VAR>inst✝ : IsCofilteredOrEmpty J<VAR>h : F.IsMittagLeffler<VAR>j j₁ : J<VAR>g₁ : j₁ ⟶ i<VAR>f₁ : j₁ ⟶ j<VAR>j₂ : J<VAR>f₂ : j₂ ⟶ j₁<VAR>h₂ : F.eventualRange j₁ = range (F.map f₂)<VAR>j₃ : J<VAR>f₃ : j₃ ⟶ j₂<VAR>x : F.obj j₂<VAR>hx : x ∈ ⋂ f, F.map f ⁻¹' s<VAR>this : F.map f₂ x ∈ F.eventualRange j₁<VAR>y : F.obj j₃<VAR>hy : y ∈ F.eventualRange j₃<VAR>h₃ : F.map (f₃ ≫ f₂) y = F.map f₂ x<GOAL>↑((F.toPreimages s).map (f₃ ≫ f₂ ≫ f₁) ⟨y, ⋯⟩) = ↑((F.toPreimages s).map (f₂ ≫ f₁) ⟨x, hx⟩)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : OrderTopology α<VAR>a : α<GOAL>𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a