ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<GOAL>comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃) = (Q₁.tmul Q₂).tmul Q₃
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<GOAL>(associatedHom R) (comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃)) = (associatedHom R) ((Q₁.tmul Q₂).tmul Q₃)
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₁' : M₃<VAR>m₂' : M₁<VAR>m₁'' : M₂<VAR>m₂'' : M₃<GOAL>(((TensorProduct.AlgebraTensorModule.curry (TensorProduct.AlgebraTensorModule.curry ((((TensorProduct.AlgebraTensorModule.curry (TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃))))) m₁) m₂) m₁'))) m₂') m₁'') m₂'' = (((TensorProduct.AlgebraTensorModule.curry (TensorProduct.AlgebraTensorModule.curry ((((TensorProduct.AlgebraTensorModule.curry (TensorProduct.AlgebraTensorModule.curry ((associatedHom R) ((Q₁.tmul Q₂).tmul Q₃)))) m₁) m₂) m₁'))) m₂') m₁'') m₂''
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₁' : M₃<VAR>m₂' : M₁<VAR>m₁'' : M₂<VAR>m₂'' : M₃<GOAL>(((associatedHom R) (comp (Q₁.tmul (Q₂.tmul Q₃)) ↑(TensorProduct.assoc R M₁ M₂ M₃))) ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁')) ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'') = (((associatedHom R) ((Q₁.tmul Q₂).tmul Q₃)) ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁')) ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'')
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : AddCommGroup M₃<VAR>inst✝⁵ : AddCommGroup M₄<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>m₁' : M₃<VAR>m₂' : M₁<VAR>m₁'' : M₂<VAR>m₂'' : M₃<GOAL>((LinearMap.compl₁₂ ((associated Q₁).tmul ((associated Q₂).tmul (associated Q₃))) ↑(TensorProduct.assoc R M₁ M₂ M₃) ↑(TensorProduct.assoc R M₁ M₂ M₃)) ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁')) ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'') = ((((associated Q₁).tmul (associated Q₂)).tmul (associated Q₃)) ((m₁ ⊗ₜ[R] m₂) ⊗ₜ[R] m₁')) ((m₂' ⊗ₜ[R] m₁'') ⊗ₜ[R] m₂'')
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{u_7, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>inst✝⁵ : Category.{?u.53320, u_3} E<VAR>inst✝⁴ : Category.{?u.53324, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>e : F ≅ G<VAR>n : A<GOAL>e.inv.hom n ≫ e.hom.hom n = 𝟙 (G.functor n)
<VAR>n✝¹ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ζ : B<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<VAR>n✝ : ℕ+<VAR>hi : n✝ ∈ {n}<GOAL>∃ r, IsPrimitiveRoot r ↑n✝
<VAR>n✝¹ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ζ : B<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<VAR>n✝ : ℕ+<VAR>hi : n✝ = n<GOAL>∃ r, IsPrimitiveRoot r ↑n✝
<VAR>n✝¹ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ζ : B<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<VAR>n✝ : ℕ+<VAR>hi : n✝ = n<GOAL>IsPrimitiveRoot ⟨ζ, ⋯⟩ ↑n✝
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ζ : B<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<VAR>x : ↥(adjoin A {ζ})<GOAL>x ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ζ : B<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<VAR>x : ↥(adjoin A {ζ})<VAR>b : B<VAR>hb : b ∈ {ζ}<GOAL>⟨b, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ζ : B<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<VAR>x : ↥(adjoin A {ζ})<VAR>a : A<GOAL>(algebraMap A ↥(adjoin A {ζ})) a ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ζ : B<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<VAR>x b₁ b₂ : ↥(adjoin A {ζ})<VAR>hb₁ : b₁ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}<VAR>hb₂ : b₂ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}<GOAL>b₁ + b₂ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
<VAR>n✝ : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>ζ : B<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<VAR>x b₁ b₂ : ↥(adjoin A {ζ})<VAR>hb₁ : b₁ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}<VAR>hb₂ : b₂ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}<GOAL>b₁ * b₂ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>M' : Type u_5<VAR>N' : Type u_6<VAR>ι : Type u_7<VAR>κ : Type u_8<VAR>τ : Type u_9<VAR>ι' : Type u_10<VAR>κ' : Type u_11<VAR>inst✝¹⁸ : DecidableEq ι<VAR>inst✝¹⁷ : DecidableEq κ<VAR>inst✝¹⁶ : DecidableEq τ<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : Fintype κ<VAR>inst✝¹³ : Fintype τ<VAR>inst✝¹² : Finite ι'<VAR>inst✝¹¹ : Finite κ'<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : AddCommGroup N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup N'<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R P<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R N'<VAR>bM : Basis ι R M<VAR>bN : Basis κ R N<VAR>bP : Basis τ R P<VAR>bM' : Basis ι' R M'<VAR>bN' : Basis κ' R N'<VAR>i : κ<VAR>j i' : ι<VAR>j' : κ<GOAL>(toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM)) ↑(TensorProduct.comm R M N) (i, j) (i', j') = submatrix 1 Prod.swap _root_.id (i, j) (i', j')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure (Measure α)<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (x : α), f x ∂m.join = ∫⁻ (μ : Measure α), ∫⁻ (x : α), f x ∂μ ∂m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure (Measure α)<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * ∫⁻ (μ : Measure α), μ (↑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m = ∫⁻ (μ : Measure α), ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (↑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure (Measure α)<VAR>f✝ : α → ℝ≥0∞<VAR>hf✝ : Measurable f✝<VAR>s : ℕ → Finset ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)<VAR>hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ<GOAL>⨆ n, ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (μ : Measure α), ⨆ n, ∑ r ∈ s n, r * f n r μ ∂m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure (Measure α)<VAR>f✝ : α → ℝ≥0∞<VAR>hf✝ : Measurable f✝<VAR>s : ℕ → Finset ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)<VAR>hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ<GOAL>⨆ n, ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ⨆ n, ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure (Measure α)<VAR>f✝ : α → ℝ≥0∞<VAR>hf✝ : Measurable f✝<VAR>s : ℕ → Finset ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)<VAR>hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ<GOAL>∀ (n : ℕ), Measurable fun μ => ∑ r ∈ s n, r * f n r μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure (Measure α)<VAR>f✝ : α → ℝ≥0∞<VAR>hf✝ : Measurable f✝<VAR>s : ℕ → Finset ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)<VAR>hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ<GOAL>(fun n => ∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m) = fun n => ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure (Measure α)<VAR>f✝ : α → ℝ≥0∞<VAR>hf✝ : Measurable f✝<VAR>s : ℕ → Finset ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)<VAR>hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ<VAR>n : ℕ<GOAL>∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∫⁻ (a : Measure α), ∑ r ∈ s n, r * f n r a ∂m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure (Measure α)<VAR>f✝ : α → ℝ≥0∞<VAR>hf✝ : Measurable f✝<VAR>s : ℕ → Finset ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)<VAR>hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ<VAR>n : ℕ<GOAL>∑ r ∈ s n, r * ∫⁻ (μ : Measure α), f n r μ ∂m = ∑ b ∈ s n, ∫⁻ (a : Measure α), b * f n b a ∂m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>m : Measure (Measure α)<VAR>f✝ : α → ℝ≥0∞<VAR>hf✝ : Measurable f✝<VAR>s : ℕ → Finset ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞ → Measure α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ) (r : ℝ≥0∞), Measurable (f n r)<VAR>hm : Monotone fun n μ => ∑ r ∈ s n, r * f n r μ<VAR>n : ℕ<GOAL>∀ b ∈ s n, Measurable fun a => b * f n b a
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>∫⁻ (a : α), ↑((f * g) a) ∂μ ≤ (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>f g : α → ℝ≥0<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>∫⁻ (a : α), ↑(f a) * ↑(g a) ∂μ ≤ (∫⁻ (a : α), ↑(f a) ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), ↑(g a) ^ q ∂μ) ^ (1 / q)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<GOAL>f.eraseLead.leadingCoeff = f.nextCoeff
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<VAR>this : 0 < f.natDegree<GOAL>f.eraseLead.leadingCoeff = f.nextCoeff
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>h : f.nextCoeff ≠ 0<VAR>this : 0 < f.natDegree<GOAL>¬f.natDegree = 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F✝ : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E<VAR>inst✝¹⁴ : Module 𝕜 E<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F✝<VAR>inst✝⁹ : Module 𝕜₂ F✝<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F✝<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>F : Type u_10<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕝₂ F<VAR>inst✝ : TopologicalSpace E<VAR>p : ι → Seminorm 𝕝 E<VAR>hp : WithSeminorms p<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : ∃ s C, (normSeminorm 𝕝₂ F).comp f ≤ C • s.sup p<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F✝ : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : AddCommGroup E<VAR>inst✝¹⁴ : Module 𝕜 E<VAR>inst✝¹³ : NormedField 𝕝<VAR>inst✝¹² : Module 𝕝 E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : AddCommGroup F✝<VAR>inst✝⁹ : Module 𝕜₂ F✝<VAR>inst✝⁸ : NormedField 𝕝₂<VAR>inst✝⁷ : Module 𝕝₂ F✝<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝⁶ : RingHomIsometric σ₁₂<VAR>τ₁₂ : 𝕝 →+* 𝕝₂<VAR>inst✝⁵ : RingHomIsometric τ₁₂<VAR>inst✝⁴ : Nonempty ι<VAR>inst✝³ : Nonempty ι'<VAR>F : Type u_10<VAR>inst✝² : SeminormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕝₂ F<VAR>inst✝ : TopologicalSpace E<VAR>p : ι → Seminorm 𝕝 E<VAR>hp : WithSeminorms p<VAR>f : E →ₛₗ[τ₁₂] F<VAR>hf : IsBounded p (fun x => normSeminorm 𝕝₂ F) f<GOAL>Continuous ⇑f
<VAR>M₀ : Type u_1<VAR>inst✝⁵ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁴ : MonoidWithZero M<VAR>inst✝³ : MonoidWithZero M'<VAR>inst✝² : CommMonoidWithZero M₁<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommRing R'<VAR>x y r : R'<VAR>hr : r ∈ R'⁰<VAR>x✝ : x * r ∣ y * r<VAR>z : R'<VAR>h✝ : y * r = x * r * z<GOAL>y = x * z
<VAR>M₀ : Type u_1<VAR>inst✝⁵ : MonoidWithZero M₀<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M₁ : Type u_4<VAR>R : Type u_5<VAR>R' : Type u_6<VAR>F : Type u_7<VAR>inst✝⁴ : MonoidWithZero M<VAR>inst✝³ : MonoidWithZero M'<VAR>inst✝² : CommMonoidWithZero M₁<VAR>inst✝¹ : Ring R<VAR>inst✝ : CommRing R'<VAR>x y r : R'<VAR>hr : r ∈ R'⁰<VAR>x✝ : x ∣ y<VAR>z : R'<VAR>h : y = x * z<GOAL>y * r = x * r * z
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>PartialFun ⥤ Pointed
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>U : Set ↑↑𝒰.gluedCover.glued.toPresheafedSpace<VAR>hU : _root_.IsOpen U<GOAL>_root_.IsOpen (⇑𝒰.fromGlued.val.base '' U)
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>U : Set ↑↑𝒰.gluedCover.glued.toPresheafedSpace<VAR>hU : _root_.IsOpen U<GOAL>∀ x ∈ ⇑𝒰.fromGlued.val.base '' U, ∃ t ⊆ ⇑𝒰.fromGlued.val.base '' U, _root_.IsOpen t ∧ x ∈ t
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>U : Set ↑↑𝒰.gluedCover.glued.toPresheafedSpace<VAR>hU : _root_.IsOpen U<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ ⇑𝒰.fromGlued.val.base '' U<GOAL>∃ t ⊆ ⇑𝒰.fromGlued.val.base '' U, _root_.IsOpen t ∧ x ∈ t
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>U : Set ↑↑𝒰.gluedCover.glued.toPresheafedSpace<VAR>hU : ∀ (i : 𝒰.gluedCover.J), _root_.IsOpen (⇑(𝒰.gluedCover.ι i).val.base ⁻¹' U)<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ ⇑𝒰.fromGlued.val.base '' U<GOAL>∃ t ⊆ ⇑𝒰.fromGlued.val.base '' U, _root_.IsOpen t ∧ x ∈ t
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>U : Set ↑↑𝒰.gluedCover.glued.toPresheafedSpace<VAR>hU : ∀ (i : 𝒰.gluedCover.J), _root_.IsOpen (⇑(𝒰.gluedCover.ι i).val.base ⁻¹' U)<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ ⇑𝒰.fromGlued.val.base '' U<GOAL>⇑𝒰.fromGlued.val.base '' U ∩ Set.range ⇑(𝒰.map (𝒰.f x)).val.base ⊆ ⇑𝒰.fromGlued.val.base '' U ∧ _root_.IsOpen (⇑𝒰.fromGlued.val.base '' U ∩ Set.range ⇑(𝒰.map (𝒰.f x)).val.base) ∧ x ∈ ⇑𝒰.fromGlued.val.base '' U ∩ Set.range ⇑(𝒰.map (𝒰.f x)).val.base
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>U : Set ↑↑𝒰.gluedCover.glued.toPresheafedSpace<VAR>hU : ∀ (i : 𝒰.gluedCover.J), _root_.IsOpen (⇑(𝒰.gluedCover.ι i).val.base ⁻¹' U)<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ ⇑𝒰.fromGlued.val.base '' U<GOAL>_root_.IsOpen (⇑𝒰.fromGlued.val.base '' U ∩ Set.range ⇑(𝒰.map (𝒰.f x)).val.base) ∧ x ∈ ⇑𝒰.fromGlued.val.base '' U ∩ Set.range ⇑(𝒰.map (𝒰.f x)).val.base
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>S : Finset ι<VAR>p : ι → Ideal R<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>hM : Module.IsTorsionBySet R M ↑(⨅ i ∈ S, p i)<GOAL>⨆ i, torsionBySet R M ↑(p ↑i) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>ι : Type u_3<VAR>inst✝ : DecidableEq ι<VAR>S : Finset ι<VAR>p : ι → Ideal R<VAR>hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤<VAR>hM : Module.IsTorsionBySet R M ↑(⨅ i ∈ S, p i)<GOAL>⨆ t ∈ ↑S, torsionBySet R M ↑(p t) = ⊤
<VAR>α : Type u_1<VAR>s : Multiset α<VAR>a✝ a : α<GOAL>s ⋖ a ::ₘ s
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>s : Finset V<VAR>hs : s.Nonempty<VAR>lin_ind : LinearIndependent K Subtype.val<VAR>card_eq : s.card = finrank K V<GOAL>⇑(basisOfLinearIndependentOfCardEqFinrank lin_ind ⋯) = Subtype.val
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a b : α<GOAL>∂ (a ⊔ b) ≤ ∂ a ⊔ ∂ b
<VAR>α : Type u_1<VAR>inst✝ : CoheytingAlgebra α<VAR>a b : α<GOAL>a ⊓ ￢(a ⊔ b) ⊔ b ⊓ ￢(a ⊔ b) ≤ ∂ a ⊔ ∂ b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y z : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 (x + z) s<GOAL>StarConvex 𝕜 x ((fun x => x + z) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>x y z : E<VAR>s : Set E<VAR>hs : StarConvex 𝕜 (z + x) s<GOAL>StarConvex 𝕜 x ((fun x => x + z) ⁻¹' s)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C × D ⥤ E<VAR>X Y Z : C<VAR>W : D<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>F.map (f ≫ g, 𝟙 W) = F.map (f, 𝟙 W) ≫ F.map (g, 𝟙 W)
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_2, u_1} C<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : IsIdempotentComplete C<VAR>inst✝ : HasFiniteCoproducts C<VAR>X : ChainComplex C ℕ<VAR>i✝ : ℕ<GOAL>(N₂.map (isoΓ₀.hom.app X)).f.f i✝ = PInfty.f i✝
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>ℙ {ω | c ≤ |X ω - ∫ (a : Ω), X a|} ≤ ENNReal.ofReal (variance X ℙ / c ^ 2)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>ℙ {ω | c ≤ |X ω - ∫ (a : Ω), X a|} ≤ evariance X ℙ / ENNReal.ofReal (c ^ 2)
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>ℙ {ω | c ≤ |X ω - ∫ (a : Ω), X a|} = ℙ {ω | ↑c.toNNReal ≤ |X ω - ∫ (a : Ω), X a|}
<VAR>Ω : Type u_1<VAR>m : MeasurableSpace Ω<VAR>X✝ : Ω → ℝ<VAR>μ : Measure Ω<VAR>inst✝¹ : MeasureSpace Ω<VAR>inst✝ : IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>hX : Memℒp X 2 ℙ<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>evariance X ℙ / ENNReal.ofReal (c ^ 2) = evariance X ℙ / ↑c.toNNReal ^ 2
<VAR>q a b c : ℚ<VAR>n₁ : ℤ<VAR>d₁ : ℕ<VAR>h₁ : d₁ ≠ 0<VAR>n₂ : ℤ<VAR>d₂ : ℕ<VAR>h₂ : d₂ ≠ 0<VAR>n₃ : ℤ<VAR>d₃ : ℕ<VAR>h₃ : d₃ ≠ 0<GOAL>n₁ /. ↑d₁ * (n₂ /. ↑d₂) * (n₃ /. ↑d₃) = n₁ /. ↑d₁ * (n₂ /. ↑d₂ * (n₃ /. ↑d₃))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(bind₁ (wittStructureInt p Φ)) (W_ ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(map (Int.castRingHom ℚ)) ((bind₁ (wittStructureInt p Φ)) (W_ ℤ n)) = (map (Int.castRingHom ℚ)) ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>this : (bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)<GOAL>(map (Int.castRingHom ℚ)) ((bind₁ (wittStructureInt p Φ)) (W_ ℤ n)) = (map (Int.castRingHom ℚ)) ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>x : A<VAR>hx : x ∈ carrier f_deg q<GOAL>∀ (c : A), c • x ∈ carrier f_deg q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>x : A<VAR>hx : x ∈ carrier f_deg q<GOAL>0 • x ∈ carrier f_deg q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>x : A<VAR>hx : x ∈ carrier f_deg q<GOAL>∀ {i : ℕ} (m_1 : ↥(𝒜 i)), ↑m_1 • x ∈ carrier f_deg q
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>x : A<VAR>hx : x ∈ carrier f_deg q<GOAL>∀ (m_1 m' : A), m_1 • x ∈ carrier f_deg q → m' • x ∈ carrier f_deg q → (m_1 + m') • x ∈ carrier f_deg q
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set α<VAR>U : Set (α × α)<VAR>hs : Dense s<VAR>hU : U ∈ 𝓤 α<GOAL>⋃ x ∈ s, ball x U = univ
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set α<VAR>U : Set (α × α)<VAR>hs : Dense s<VAR>hU : U ∈ 𝓤 α<VAR>y : α<GOAL>∃ i, ∃ (_ : i ∈ s), y ∈ ball i U
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>s : Set α<VAR>U : Set (α × α)<VAR>hs : Dense s<VAR>hU : U ∈ 𝓤 α<VAR>y x : α<VAR>hxs : x ∈ s<VAR>hxy : (x, y) ∈ U<GOAL>∃ i, ∃ (_ : i ∈ s), y ∈ ball i U
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>z : ℤ<GOAL>|x - ↑(round x)| ≤ |x - ↑z|
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>x : α<VAR>z : ℤ<GOAL>fract x ≤ |x - ↑z| ∨ 1 - fract x ≤ |x - ↑z|