ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>g : N → N'<VAR>r : Set N<VAR>y : N<VAR>fst✝ : M<VAR>snd✝ : N<VAR>hf : ContMDiffAt I I' n f (fst✝, snd✝).1<VAR>hg : ContMDiffAt J J' n g (fst✝, snd✝).2<GOAL>ContMDiffAt (I.prod J) (I'.prod J') n (Prod.map f g) (fst✝, snd✝)
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝⁶ : GroupWithZero G₀<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : MulActionWithZero G₀ α<VAR>inst✝³ : MeasurableSpace G₀<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSMul G₀ α<VAR>inst✝ : MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : G₀<GOAL>MeasurableSet (a • s)
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝⁶ : GroupWithZero G₀<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : MulActionWithZero G₀ α<VAR>inst✝³ : MeasurableSpace G₀<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSMul G₀ α<VAR>inst✝ : MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (0 • s)
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝⁶ : GroupWithZero G₀<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : MulActionWithZero G₀ α<VAR>inst✝³ : MeasurableSpace G₀<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : MeasurableSMul G₀ α<VAR>inst✝ : MeasurableSingletonClass α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>a : G₀<VAR>ha : a ≠ 0<GOAL>MeasurableSet (a • s)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f : α → ℝ<VAR>hf : IntegrableOn f s μ<VAR>hf₀ : 0 ≤ᶠ[ae (μ.restrict s)] f<GOAL>ENNReal.ofReal (⨍ (x : α) in s, f x ∂μ) = (∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ) / μ s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X Y : C<GOAL>(BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫ (ℬ X Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ 𝟙 X) (BinaryFan.snd (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ BinaryFan.snd (ℬ 𝒯.cone.pt Y).cone)) = (ℬ X Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ BinaryFan.fst (ℬ X 𝒯.cone.pt).cone) (BinaryFan.snd (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ 𝟙 Y))
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ : C<VAR>𝒯 : LimitCone (Functor.empty C)<VAR>ℬ : (X Y : C) → LimitCone (pair X Y)<VAR>X Y : C<GOAL>∀ (j : Discrete WalkingPair), ((BinaryFan.associatorOfLimitCone ℬ X 𝒯.cone.pt Y).hom ≫ (ℬ X Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ 𝟙 X) (BinaryFan.snd (ℬ X (ℬ 𝒯.cone.pt Y).cone.pt).cone ≫ BinaryFan.snd (ℬ 𝒯.cone.pt Y).cone))) ≫ (ℬ X Y).cone.π.app j = (ℬ X Y).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ BinaryFan.fst (ℬ X 𝒯.cone.pt).cone) (BinaryFan.snd (ℬ (ℬ X 𝒯.cone.pt).cone.pt Y).cone ≫ 𝟙 Y)) ≫ (ℬ X Y).cone.π.app j
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>HasFTaylorSeriesUpTo ⊤ f p ↔ ∀ (n : ℕ), HasFTaylorSeriesUpTo (↑n) f p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>(ν.rnDeriv μ)⁻¹ =ᶠ[ae μ] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>x : α<VAR>hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x<GOAL>(ν.rnDeriv μ)⁻¹ x = μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<GOAL>(μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun x => f x * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<VAR>hμ'ν : μ' ≪ ν<GOAL>(μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun x => f x * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<VAR>hμ'ν : μ' ≪ ν<VAR>h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun x => f x * μ'.rnDeriv ν x<GOAL>(μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun x => f x * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<VAR>hμ'ν : μ' ≪ ν<VAR>h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun x => f x * μ'.rnDeriv ν x<VAR>h1 : μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν<GOAL>(μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun x => f x * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<VAR>hμ'ν : μ' ≪ ν<VAR>h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun x => f x * μ'.rnDeriv ν x<VAR>h1 : μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν<VAR>h2 : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν<GOAL>(μ.withDensity f).rnDeriv ν =ᶠ[ae ν] fun x => f x * μ.rnDeriv ν x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝¹ ν✝¹ μ✝ ν✝ : Measure α<VAR>f : α → ℝ≥0∞<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hfν : AEMeasurable f ν<VAR>hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤<VAR>μ' : Measure α := ν.withDensity (μ.rnDeriv ν)<VAR>hμ'ν : μ' ≪ ν<VAR>h : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] fun x => f x * μ'.rnDeriv ν x<VAR>h1 : μ'.rnDeriv ν =ᶠ[ae ν] μ.rnDeriv ν<VAR>h2 : (μ'.withDensity f).rnDeriv ν =ᶠ[ae ν] (μ.withDensity f).rnDeriv ν<VAR>x : α<VAR>hx : (μ'.withDensity f).rnDeriv ν x = f x * μ'.rnDeriv ν x<VAR>hx1 : μ'.rnDeriv ν x = μ.rnDeriv ν x<VAR>hx2 : (μ'.withDensity f).rnDeriv ν x = (μ.withDensity f).rnDeriv ν x<GOAL>(μ.withDensity f).rnDeriv ν x = f x * μ.rnDeriv ν x
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x : P<GOAL>↑(spanSingleton S x) = span R {x}
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x : P<GOAL>↑⟨span R {x}, ⋯⟩ = span R {x}
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b x y : α<VAR>hy : IsUnit y<GOAL>y * x ∈ I ↔ x ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b x y : α<VAR>hy : IsUnit y<VAR>h : y * x ∈ I<GOAL>x ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b x y : α<VAR>hy : IsUnit y<VAR>h : y * x ∈ I<VAR>y' : α<VAR>hy' : y' * y = 1<GOAL>x ∈ I
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b x y : α<VAR>hy : IsUnit y<VAR>h : y * x ∈ I<VAR>y' : α<VAR>hy' : y' * y = 1<VAR>this : y' * (y * x) ∈ I<GOAL>x ∈ I
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>e : K ≃ₐ[F] E<VAR>inst✝ : IsPurelyInseparable F K<GOAL>IsPurelyInseparable F E
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>e : K ≃ₐ[F] E<VAR>inst✝ : IsPurelyInseparable F K<VAR>x : E<VAR>h : IsSeparable F x<GOAL>x ∈ (algebraMap F E).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>e : K ≃ₐ[F] E<VAR>inst✝ : IsPurelyInseparable F K<VAR>x : E<VAR>h : (minpoly F (e.symm x)).Separable<GOAL>x ∈ (algebraMap F E).range
<VAR>b x y : ℝ<VAR>hb : 1 < b<VAR>hx : 0 < x<GOAL>0 ≤ logb b x ↔ 1 ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : a < b<GOAL>a / b = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : a < b<GOAL>a < b * succ 0
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a s : ℂ<VAR>hs : 0 < s.re + a.re<GOAL>HasMellin ((Ioc 0 1).indicator fun t => ↑t ^ a) s (1 / (s + a))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a s : ℂ<VAR>hs : 0 < s.re + a.re<VAR>this : HasMellin ((Ioc 0 1).indicator fun x => 1) (s + a) (1 / (s + a))<GOAL>HasMellin ((Ioc 0 1).indicator fun t => ↑t ^ a) s (1 / (s + a))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>a s : ℂ<VAR>hs : 0 < s.re + a.re<VAR>this : MellinConvergent ((Ioc 0 1).indicator fun a_1 => ↑a_1 ^ a) s ∧ mellin ((Ioc 0 1).indicator fun a_1 => ↑a_1 ^ a) s = 1 / (s + a)<GOAL>HasMellin ((Ioc 0 1).indicator fun t => ↑t ^ a) s (1 / (s + 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>na nb nc : ℕ<VAR>a : ⨂[R]^na M<VAR>b : ⨂[R]^nb M<VAR>c : ⨂[R]^nc M<VAR>mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M := fun n m => (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv<GOAL>(cast R M ⋯) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb nc : ℕ<VAR>a : ⨂[R]^na M<VAR>b : ⨂[R]^nb M<VAR>c : ⨂[R]^nc M<VAR>mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M := fun n m => (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv<VAR>e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯<GOAL>(cast R M ⋯) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb nc : ℕ<VAR>a : ⨂[R]^na M<VAR>b : ⨂[R]^nb M<VAR>c : ⨂[R]^nc M<VAR>mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M := fun n m => (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv<VAR>e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯<VAR>lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ mul na nb<VAR>lhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)<VAR>rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) LinearMap.lflip) ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) (mul na (nb + nc)).flip ∘ₗ mul nb nc)).flip<VAR>rhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)<GOAL>(cast R M ⋯) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb nc : ℕ<VAR>a : ⨂[R]^na M<VAR>b : ⨂[R]^nb M<VAR>c : ⨂[R]^nc M<VAR>mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M := fun n m => (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv<VAR>e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯<VAR>lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ mul na nb<VAR>lhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)<VAR>rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) LinearMap.lflip) ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) (mul na (nb + nc)).flip ∘ₗ mul nb nc)).flip<VAR>rhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)<GOAL>lhs = rhs
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb nc : ℕ<VAR>a✝ : ⨂[R]^na M<VAR>b✝ : ⨂[R]^nb M<VAR>c✝ : ⨂[R]^nc M<VAR>mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M := fun n m => (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv<VAR>e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯<VAR>lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ mul na nb<VAR>lhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)<VAR>rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) LinearMap.lflip) ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) (mul na (nb + nc)).flip ∘ₗ mul nb nc)).flip<VAR>rhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)<VAR>a : Fin na → M<VAR>b : Fin nb → M<VAR>c : Fin nc → M<GOAL>(((((lhs.compMultilinearMap (tprod R)) a).compMultilinearMap (tprod R)) b).compMultilinearMap (tprod R)) c = (((((rhs.compMultilinearMap (tprod R)) a).compMultilinearMap (tprod R)) b).compMultilinearMap (tprod R)) c
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb nc : ℕ<VAR>a✝ : ⨂[R]^na M<VAR>b✝ : ⨂[R]^nb M<VAR>c✝ : ⨂[R]^nc M<VAR>mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M := fun n m => (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv<VAR>e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯<VAR>lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ mul na nb<VAR>lhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)<VAR>rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) LinearMap.lflip) ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) (mul na (nb + nc)).flip ∘ₗ mul nb nc)).flip<VAR>rhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)<VAR>a : Fin na → M<VAR>b : Fin nb → M<VAR>c : Fin nc → M<GOAL>(tprod R) (Fin.append (Fin.append a b) c ∘ Fin.cast ⋯) = (tprod R) (Fin.append a (Fin.append b c))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb nc : ℕ<VAR>a✝ : ⨂[R]^na M<VAR>b✝ : ⨂[R]^nb M<VAR>c✝ : ⨂[R]^nc M<VAR>mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M := fun n m => (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv<VAR>e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯<VAR>lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ mul na nb<VAR>lhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)<VAR>rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) LinearMap.lflip) ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) (mul na (nb + nc)).flip ∘ₗ mul nb nc)).flip<VAR>rhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)<VAR>a : Fin na → M<VAR>b : Fin nb → M<VAR>c : Fin nc → M<VAR>j : Fin (na + (nb + nc))<GOAL>(Fin.append (Fin.append a b) c ∘ Fin.cast ⋯) j = Fin.append a (Fin.append b c) j
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb nc : ℕ<VAR>a✝ : ⨂[R]^na M<VAR>b✝ : ⨂[R]^nb M<VAR>c✝ : ⨂[R]^nc M<VAR>mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M := fun n m => (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv<VAR>e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯<VAR>lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ mul na nb<VAR>lhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)<VAR>rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) LinearMap.lflip) ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) (mul na (nb + nc)).flip ∘ₗ mul nb nc)).flip<VAR>rhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)<VAR>a : Fin na → M<VAR>b : Fin nb → M<VAR>c : Fin nc → M<VAR>j : Fin (na + (nb + nc))<GOAL>((Fin.append a (Fin.append b c) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯) j = Fin.append a (Fin.append b c) j
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>na nb nc : ℕ<VAR>a✝ : ⨂[R]^na M<VAR>b✝ : ⨂[R]^nb M<VAR>c✝ : ⨂[R]^nc M<VAR>mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M := fun n m => (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv<VAR>e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯<VAR>lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ mul na nb<VAR>lhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)<VAR>rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M := (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M) (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) LinearMap.lflip) ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)) (mul na (nb + nc)).flip ∘ₗ mul nb nc)).flip<VAR>rhs_eq : ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)<VAR>a : Fin na → M<VAR>b : Fin nb → M<VAR>c : Fin nc → M<VAR>j : Fin (na + (nb + nc))<GOAL>↑(Fin.cast ⋯ (Fin.cast ⋯ j)) = ↑j
<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₂<GOAL>p ≤ comap LinearMap.id p
<VAR>M : Type u_1<VAR>inst✝¹ : Monoid M<VAR>s : Set M<VAR>A : Type u_2<VAR>inst✝ : AddMonoid A<VAR>t : Set A<VAR>S : Submonoid M<GOAL>IsSubmonoid ↑S
<VAR>R : Type u<VAR>S✝ : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring S✝<VAR>inst✝¹⁰ : AddCommMonoid A<VAR>inst✝⁹ : Algebra R S✝<VAR>inst✝⁸ : Module S✝ A<VAR>inst✝⁷ : Module R A<VAR>inst✝⁶ : IsScalarTower R S✝ A<VAR>S : Type u_1<VAR>T : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Semiring T<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>x : S<VAR>a : Set S<VAR>hx : x ∈ span R a<GOAL>(algebraMap S T) x ∈ span R (⇑(algebraMap S T) '' a)