ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x : ℝ<VAR>h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0<VAR>h : (2 * cos (π / 3) - 1) ^ 2 = 0<GOAL>cos (π / 3) = 1 / 2
<VAR>x : ℝ<VAR>h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0<VAR>h : 2 * cos (π / 3) + 2 = 0<GOAL>cos (π / 3) = 1 / 2
<VAR>q✝ q r : ℚ<GOAL>q * r = mkRat (q.num * r.num) (q.den * r.den)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>inst✝ : Nonempty α<VAR>f : α → β<VAR>a : α<VAR>b✝ : β<VAR>g : β → α<VAR>hf : Injective f<VAR>hg : RightInverse g f<VAR>b : β<GOAL>f (invFun f b) = b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>v : ι → M<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing R₂<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>c d : R<VAR>x y : M<VAR>b : Basis ι R M<VAR>hli : LinearIndependent R v<VAR>hsp : ⊤ ≤ span R (Set.range v)<VAR>i j : ι<VAR>h : j ≠ i<GOAL>(hli.repr ⟨v j, ⋯⟩) i = 0
<VAR>a✝ b✝ c d : ℝ≥0∞<VAR>r✝ p q : ℝ≥0<VAR>a b r : ℝ≥0∞<VAR>hr₀ : r ≠ 0<VAR>hr₁ : r ≠ ⊤<GOAL>r * a ≤ b ↔ a ≤ r⁻¹ * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Monoid α<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : MulAction α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : SMulPosStrictMono α β<VAR>hb : 0 < b<VAR>h : 1 < a<GOAL>b < a • b
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>n₂ : ℕ+<VAR>h₁ : e₁.cmp e₁ = Ordering.eq<VAR>h₂ : _root_.cmp ↑n₁ ↑n₂ = Ordering.eq<VAR>h : Ordering.eq.orElse (Ordering.eq.orElse (a₁.cmp a₁)) = Ordering.eq<GOAL>e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>n₂ : ℕ+<VAR>h₁ : e₁.cmp e₁ = Ordering.eq<VAR>h₂ : ¬↑n₁ < ↑n₂ ∧ ¬↑n₂ < ↑n₁<VAR>h : Ordering.eq.orElse (Ordering.eq.orElse (a₁.cmp a₁)) = Ordering.eq<GOAL>e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁
<VAR>e₁ : ONote<VAR>n₁ : ℕ+<VAR>a₁ : ONote<VAR>h₁ : e₁.cmp e₁ = Ordering.eq<VAR>h : Ordering.eq.orElse (Ordering.eq.orElse (a₁.cmp a₁)) = Ordering.eq<VAR>h₂ : ¬↑n₁ < ↑n₁ ∧ ¬↑n₁ < ↑n₁<GOAL>e₁.oadd n₁ a₁ = e₁.oadd n₁ a₁
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : AddMonoid B<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>ψ✝ : AddChar A M<VAR>f : A →+ B<VAR>hf : Surjective ⇑f<VAR>ψ χ : AddChar B M<VAR>h : (fun ψ => ψ.compAddMonoidHom f) ψ = (fun ψ => ψ.compAddMonoidHom f) χ<GOAL>ψ = χ
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : AddMonoid B<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>ψ✝ : AddChar A M<VAR>f : A →+ B<VAR>hf : Surjective ⇑f<VAR>ψ χ : AddChar B M<VAR>h : ⇑((fun ψ => ψ.compAddMonoidHom f) ψ) = ⇑((fun ψ => ψ.compAddMonoidHom f) χ)<GOAL>⇑ψ = ⇑χ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : SDiff α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>ma \ mb ∈ a \ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : SDiff α<VAR>a b : Part α<VAR>ma mb : α<VAR>ha : ma ∈ a<VAR>hb : mb ∈ b<GOAL>∃ a_1 ∈ a, ∃ a ∈ b, a_1 \ a = ma \ mb
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I<GOAL>|(latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e)| = ↑(FractionalIdeal.absNorm ↑I)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I<GOAL>(latticeBasis K).det (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) = (algebraMap ℚ ℝ) ((integralBasis K).det (⇑(basisOfFractionalIdeal K I) ∘ ⇑e))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I<GOAL>((latticeBasis K).toMatrix (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e)).det = ((algebraMap ℚ ℝ).mapMatrix ((integralBasis K).toMatrix (⇑(basisOfFractionalIdeal K I) ∘ ⇑e))).det
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I<VAR>i j : ChooseBasisIndex ℤ (𝓞 K)<GOAL>(latticeBasis K).toMatrix (⇑(mixedEmbedding K) ∘ ⇑(basisOfFractionalIdeal K I) ∘ ⇑e) i j = (algebraMap ℚ ℝ).mapMatrix ((integralBasis K).toMatrix (⇑(basisOfFractionalIdeal K I) ∘ ⇑e)) i j
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>I : (FractionalIdeal (𝓞 K)⁰ K)ˣ<VAR>e : ChooseBasisIndex ℤ (𝓞 K) ≃ ChooseBasisIndex ℤ ↥↑↑I<VAR>i j : ChooseBasisIndex ℤ (𝓞 K)<GOAL>((latticeBasis K).repr ((mixedEmbedding K) ((basisOfFractionalIdeal K I) (e j)))) i = (algebraMap ℚ ℝ) (((integralBasis K).repr ((basisOfFractionalIdeal K I) (e j))) i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing S<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>A : Subalgebra K L<VAR>x : L<VAR>p : K[X]<VAR>aeval_ne : (aeval x) p.divX ≠ 0<GOAL>x⁻¹ = (aeval x) p.divX / ((aeval x) p - (algebraMap K L) (p.coeff 0))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing S<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>A : Subalgebra K L<VAR>x : L<VAR>p : K[X]<VAR>aeval_ne : (aeval x) p.divX ≠ 0<GOAL>(aeval x) p = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing S<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>A : Subalgebra K L<VAR>x : L<VAR>p : K[X]<VAR>aeval_ne : (aeval x) p.divX ≠ 0<GOAL>(aeval x) p.divX ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : CommRing S<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>A : Subalgebra K L<VAR>x : L<VAR>p : K[X]<VAR>aeval_ne : (aeval x) p.divX ≠ 0<GOAL>(aeval x) (p.divX * X + C (p.coeff 0)) = (aeval x) p.divX * x + (algebraMap K L) (p.coeff 0)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>S : Type u_3<VAR>M₀ : Type u_4<VAR>M₁ : Type u_5<VAR>R : Type u_6<VAR>G : Type u_7<VAR>G₀ : Type u_8<VAR>inst✝⁷ : Mul M<VAR>inst✝⁶ : Monoid N<VAR>inst✝⁵ : Semigroup S<VAR>inst✝⁴ : MulZeroClass M₀<VAR>inst✝³ : MulOneClass M₁<VAR>inst✝² : NonAssocRing R<VAR>inst✝¹ : Group G<VAR>inst✝ : CancelMonoidWithZero G₀<VAR>p q : S<VAR>h : Commute p q<VAR>h₁ : IsIdempotentElem p<VAR>h₂ : IsIdempotentElem q<GOAL>IsIdempotentElem (p * q)
<VAR>F : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : Monoid α✝<VAR>s t : Set α✝<VAR>a : α✝<VAR>m n✝ : ℕ<VAR>α : Type u_5<VAR>inst✝ : AddMonoid α<VAR>n : ℕ<VAR>x✝ : n + 2 ≠ 0<GOAL>(n + 2) • univ = univ
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b : ι → M<VAR>N O : Submodule R M<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>y : M<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)<VAR>ψ : ↥O →ₗ[R] R<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>d : R := generator (span R {a, ψ ⟨y, ⋯⟩})<GOAL>generator (ϕ.submoduleImage N) ∣ ψ ⟨y, ⋯⟩
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b : ι → M<VAR>N O : Submodule R M<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>y : M<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)<VAR>ψ : ↥O →ₗ[R] R<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>d : R := generator (span R {a, ψ ⟨y, ⋯⟩})<VAR>d_dvd_left : d ∣ a<GOAL>generator (ϕ.submoduleImage N) ∣ ψ ⟨y, ⋯⟩
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b : ι → M<VAR>N O : Submodule R M<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>y : M<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)<VAR>ψ : ↥O →ₗ[R] R<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>d : R := generator (span R {a, ψ ⟨y, ⋯⟩})<VAR>d_dvd_left : d ∣ a<VAR>d_dvd_right : d ∣ ψ ⟨y, ⋯⟩<GOAL>generator (ϕ.submoduleImage N) ∣ ψ ⟨y, ⋯⟩
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b : ι → M<VAR>N O : Submodule R M<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>y : M<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)<VAR>ψ : ↥O →ₗ[R] R<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>d : R := generator (span R {a, ψ ⟨y, ⋯⟩})<VAR>d_dvd_left : d ∣ a<VAR>d_dvd_right : d ∣ ψ ⟨y, ⋯⟩<GOAL>generator (ϕ.submoduleImage N) ∣ d
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b : ι → M<VAR>N O : Submodule R M<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>y : M<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)<VAR>ψ : ↥O →ₗ[R] R<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>d : R := generator (span R {a, ψ ⟨y, ⋯⟩})<VAR>d_dvd_left : d ∣ a<VAR>d_dvd_right : d ∣ ψ ⟨y, ⋯⟩<GOAL>span R {generator (span R {a, ψ ⟨y, ⋯⟩})} = span R {generator (ϕ.submoduleImage N)}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>M : Type u_3<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>b : ι → M<VAR>N O : Submodule R M<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N<VAR>inst✝ : (ϕ.submoduleImage N).IsPrincipal<VAR>y : M<VAR>yN : y ∈ N<VAR>ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)<VAR>ψ : ↥O →ₗ[R] R<VAR>a : R := generator (ϕ.submoduleImage N)<VAR>d : R := generator (span R {a, ψ ⟨y, ⋯⟩})<VAR>d_dvd_left : d ∣ a<VAR>d_dvd_right : d ∣ ψ ⟨y, ⋯⟩<GOAL>generator (ϕ.submoduleImage N) ∈ span R {a, ψ ⟨y, ⋯⟩}
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>s t : Set A<VAR>h1 : (Subalgebra.toSubmodule (adjoin R s)).FG<VAR>h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG<GOAL>(Subalgebra.toSubmodule (adjoin R (s ∪ t))).FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>s t : Set A<VAR>h1 : (Subalgebra.toSubmodule (adjoin R s)).FG<VAR>h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG<VAR>p : Set A<VAR>hp : p.Finite<VAR>hp' : span R p = Subalgebra.toSubmodule (adjoin R s)<GOAL>(Subalgebra.toSubmodule (adjoin R (s ∪ t))).FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>s t : Set A<VAR>h1 : (Subalgebra.toSubmodule (adjoin R s)).FG<VAR>h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG<VAR>p : Set A<VAR>hp : p.Finite<VAR>hp' : span R p = Subalgebra.toSubmodule (adjoin R s)<VAR>q : Set A<VAR>hq : q.Finite<VAR>hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)<GOAL>(Subalgebra.toSubmodule (adjoin R (s ∪ t))).FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>s t : Set A<VAR>h1 : (Subalgebra.toSubmodule (adjoin R s)).FG<VAR>h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG<VAR>p : Set A<VAR>hp : p.Finite<VAR>hp' : span R p = Subalgebra.toSubmodule (adjoin R s)<VAR>q : Set A<VAR>hq : q.Finite<VAR>hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)<GOAL>span R (p * q) ≤ Subalgebra.toSubmodule (adjoin R (s ∪ t))
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>s t : Set A<VAR>h1 : (Subalgebra.toSubmodule (adjoin R s)).FG<VAR>h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG<VAR>p : Set A<VAR>hp : p.Finite<VAR>hp' : span R p = Subalgebra.toSubmodule (adjoin R s)<VAR>q : Set A<VAR>hq : q.Finite<VAR>hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)<GOAL>Subalgebra.toSubmodule (adjoin R (s ∪ t)) ≤ span R (p * q)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>m : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : SecondCountableTopology E<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>AEMeasurable (fun x => ⟪f x, g x⟫_𝕜) μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>m : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : SecondCountableTopology E<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<GOAL>(fun x => ⟪f x, g x⟫_𝕜) =ᵐ[μ] fun x => ⟪mk f hf x, mk g hg x⟫_𝕜
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>m : MeasurableSpace α<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : SecondCountableTopology E<VAR>μ : MeasureTheory.Measure α<VAR>f g : α → E<VAR>hf : AEMeasurable f μ<VAR>hg : AEMeasurable g μ<VAR>x : α<VAR>hxg : g x = mk g hg x<VAR>hxf : f x = mk f hf x<GOAL>(fun x => ⟪f x, g x⟫_𝕜) x = (fun x => ⟪mk f hf x, mk g hg x⟫_𝕜) x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>k : ℕ<VAR>N N₁ N₂ : LieSubmodule R L M<GOAL>ucs 1 ⊥ = LieModule.maxTrivSubmodule R L M
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<GOAL>p.applyComposition (Composition.ones n) = fun v i => (p 1) fun x => v (Fin.castLE ⋯ i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>v : Fin n → E<VAR>i : Fin (Composition.ones n).length<GOAL>p.applyComposition (Composition.ones n) v i = (p 1) fun x => v (Fin.castLE ⋯ i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>v : Fin n → E<VAR>i : Fin (Composition.ones n).length<GOAL>∀ (i_1 : ℕ) (him : i_1 < (Composition.ones n).blocksFun i), i_1 < 1 → (v ∘ ⇑((Composition.ones n).embedding i)) ⟨i_1, him⟩ = v (Fin.castLE ⋯ i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>v : Fin n → E<VAR>i : Fin (Composition.ones n).length<VAR>hjn : 0 < (Composition.ones n).blocksFun i<VAR>hj1 : 0 < 1<GOAL>((Composition.ones n).embedding i) ⟨0, hjn⟩ = Fin.castLE ⋯ i
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝ : AddCommGroup G<VAR>f : α → α<VAR>g : α → G<VAR>n : ℕ<VAR>x : α<GOAL>birkhoffSum f g n (f x) - birkhoffSum f g n x = g (f^[n] x) - g x
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>n : ℕ<GOAL>(mapRingHom f) (X ^ n) = X ^ n
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{?u.117, u_1} C<VAR>inst✝⁶ : Category.{?u.121, u_2} D<VAR>inst✝⁵ : Category.{?u.125, u_3} E<VAR>inst✝⁴ : Category.{?u.129, 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>functor : A → C ⥤ D<VAR>shiftIso : (n a a' : A) → n + a = a' → (functor a' ⋙ shiftFunctor D n ≅ functor a)<VAR>shiftIso_zero : ∀ (a : A), shiftIso 0 a a ⋯ = isoWhiskerLeft (functor a) (shiftFunctorZero D A)<VAR>n m a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>m + n + a = a''
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b : α<VAR>s : Finset α<VAR>a x : α<GOAL>x ∈ (insert a s).erase a ↔ x ∈ s.erase a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : Zero β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T2Space β<VAR>fs : ℕ → α →ₛ β<VAR>hT_lt_top : ∀ (n : ℕ), μ (support ↑(fs n)) < ⊤<VAR>h_approx : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))<VAR>T : ℕ → Set α := fun n => support ↑(fs n)<GOAL>∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : Zero β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T2Space β<VAR>fs : ℕ → α →ₛ β<VAR>hT_lt_top : ∀ (n : ℕ), μ (support ↑(fs n)) < ⊤<VAR>h_approx : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))<VAR>T : ℕ → Set α := fun n => support ↑(fs n)<VAR>hT_meas : ∀ (n : ℕ), MeasurableSet (T n)<GOAL>∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : Zero β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T2Space β<VAR>fs : ℕ → α →ₛ β<VAR>hT_lt_top : ∀ (n : ℕ), μ (support ↑(fs n)) < ⊤<VAR>h_approx : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))<VAR>T : ℕ → Set α := fun n => support ↑(fs n)<VAR>hT_meas : ∀ (n : ℕ), MeasurableSet (T n)<VAR>t : Set α := ⋃ n, T n<GOAL>∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : Zero β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T2Space β<VAR>fs : ℕ → α →ₛ β<VAR>hT_lt_top : ∀ (n : ℕ), μ (support ↑(fs n)) < ⊤<VAR>h_approx : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))<VAR>T : ℕ → Set α := fun n => support ↑(fs n)<VAR>hT_meas : ∀ (n : ℕ), MeasurableSet (T n)<VAR>t : Set α := ⋃ n, T n<GOAL>∀ x ∈ tᶜ, f x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝² : Zero β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T2Space β<VAR>fs : ℕ → α →ₛ β<VAR>hT_lt_top : ∀ (n : ℕ), μ (support ↑(fs n)) < ⊤<VAR>h_approx : ∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))<VAR>T : ℕ → Set α := fun n => support ↑(fs n)<VAR>hT_meas : ∀ (n : ℕ), MeasurableSet (T n)<VAR>t : Set α := ⋃ n, T n<GOAL>SigmaFinite (μ.restrict t)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>H : Subgroup G<VAR>x : Quotient G α<VAR>a b : ↑x.orbit<GOAL>⟦a⟧ = ⟦b⟧ ↔ ⟦↑a⟧ = ⟦↑b⟧
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>H : Subgroup G<VAR>x : Quotient G α<VAR>a b : ↑x.orbit<GOAL>Setoid.r a b ↔ Setoid.r ↑a ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u v : Finset α<VAR>a b : α<VAR>s t : Finset α<VAR>x : α<GOAL>s \ insert x t = (s \ t).erase x
<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>Λ p = Real.log ↑p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>p q r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>inst✝ : Semiring T<GOAL>eval₂ f x (p * X) = eval₂ f x p * x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>p q r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>x : S<VAR>inst✝ : Semiring T<VAR>k : ℕ<GOAL>Commute (f (X.coeff k)) x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k✝ l k : ℕ+<VAR>ζ : Mˣ<GOAL>ζ ∈ rootsOfUnity k M ↔ ↑ζ ^ ↑k = 1
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : CommMonoid N<VAR>inst✝ : DivisionCommMonoid G<VAR>k✝ l k : ℕ+<VAR>ζ : Mˣ<GOAL>ζ ^ ↑k = 1 ↔ ↑ζ ^ ↑k = 1
<VAR>x : ℝ<GOAL>oddKernel 0 x = 0
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r✝ : α → α → Prop<VAR>a b : α<VAR>l : List α<VAR>r : α → α → Prop<VAR>hl : l.Nodup<VAR>h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b<GOAL>Pairwise r l
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r✝ : α → α → Prop<VAR>a b : α<VAR>l : List α<VAR>r : α → α → Prop<VAR>hl : l.Nodup<VAR>h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b<GOAL>∀ {a b : α}, [a, b] <+ l → r a b
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r✝ : α → α → Prop<VAR>a✝ b✝ : α<VAR>l : List α<VAR>r : α → α → Prop<VAR>hl : l.Nodup<VAR>h : ∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b<VAR>a b : α<VAR>hab : [a, b] <+ l<GOAL>r a b