ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → α<VAR>g : α → γ → α<VAR>hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b<VAR>a : α<GOAL>Set.range (foldr (fun z w => f w z) a) ⊆ Set.range (foldr (fun z w => g w z) a)
<VAR>μ : ℝ<VAR>v : ℝ≥0<VAR>x y : ℝ<GOAL>gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>i : ℕ<GOAL>p.Coprime i ∨ p ∣ i
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>i : ℕ<GOAL>p.Coprime i ∨ ¬p.Coprime i
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h : x ≤ f x<VAR>a : Ordinal.{u}<GOAL>lfpApprox f x (a + 1) = f (lfpApprox f x a)
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h : x ≤ f x<VAR>a : Ordinal.{u}<GOAL>lfpApprox f x (a + 1) ≤ f (lfpApprox f x a)
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>h : x ≤ f x<VAR>a : Ordinal.{u}<GOAL>f (lfpApprox f x a) ≤ lfpApprox f x (a + 1)
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>m < n ↔ m + 1 ≤ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>inst✝ : LE α<VAR>a b : α<GOAL>1 * a ≤ 1 * b → a ≤ b
<VAR>α : Type u<VAR>inst✝ : CanonicallyOrderedCommMonoid α<VAR>a b c d : α<GOAL>1 < a * b ↔ 1 < a ∨ 1 < b
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>a : α<VAR>s : Multiset α<GOAL>a ∈ s.toList ↔ a ∈ s
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>Sym2.GameAdd.fix wf_isOption (fun x y le => (∀ (i : x.LeftMoves), ¬le y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬le (y.moveRight j) x ⋯) x y ↔ (∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>((∀ (i : x.LeftMoves), ¬(fun a' b' x => Sym2.GameAdd.fix wf_isOption (fun x y le => (∀ (i : x.LeftMoves), ¬le y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬le (y.moveRight j) x ⋯) a' b') y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬(fun a' b' x => Sym2.GameAdd.fix wf_isOption (fun x y le => (∀ (i : x.LeftMoves), ¬le y (x.moveLeft i) ⋯) ∧ ∀ (j : y.RightMoves), ¬le (y.moveRight j) x ⋯) a' b') (y.moveRight j) x ⋯) ↔ (∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j
<VAR>x y : ℝ<GOAL>MonotoneOn (fun x => log x * x) {x | 1 ≤ x}
<VAR>x y : ℝ<GOAL>∀ ⦃a : ℝ⦄, 1 ≤ a → ∀ ⦃b : ℝ⦄, 1 ≤ b → a ≤ b → log a * a ≤ log b * b
<VAR>x✝ y✝ x : ℝ<VAR>hex : 1 ≤ x<VAR>y : ℝ<VAR>hey : 1 ≤ y<VAR>hxy : x ≤ y<GOAL>log x * x ≤ log y * y
<VAR>x✝ y✝ x : ℝ<VAR>hex : 1 ≤ x<VAR>y : ℝ<VAR>hey : 1 ≤ y<VAR>hxy : x ≤ y<VAR>y_pos : 0 < y<GOAL>log x * x ≤ log y * y
<VAR>x✝ y✝ x : ℝ<VAR>hex : 1 ≤ x<VAR>y : ℝ<VAR>hey : 1 ≤ y<VAR>hxy : x ≤ y<VAR>y_pos : 0 < y<GOAL>0 ≤ log y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : C<GOAL>(adj1.unit ≫ whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x = adj2.unit.app x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' : C ⥤ D<VAR>G : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G<VAR>x : C<GOAL>adj1.unit.app x ≫ (whiskerRight (adj1.leftAdjointUniq adj2).hom G).app x = (adj1.homEquiv x (F'.obj x)) ((adj1.leftAdjointUniq adj2).hom.app x)
<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>contra : ⊥ = ⊤<GOAL>False
<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>contra : ∅ = univ<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>n : ℕ<GOAL>s.tail.drop n = s.drop (n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>n : ℕ<GOAL>s.tail.drop n = s.drop (1 + n)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<VAR>n : ℕ<GOAL>s.drop (1 + n) = s.tail.drop n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>x : α<VAR>S : Set (Set α)<GOAL>upperClosure (⋃₀ S) = ⨅ s ∈ S, upperClosure s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, Tendsto (f (a, t)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → ℚ → ℝ<VAR>hf : IsRatCondKernelCDFAux f κ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<GOAL>∀ᵐ (t : β) ∂ν a, Tendsto (fun n => f (a, t) ↑n) atTop (𝓝 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : SeminormedRing 𝕜<VAR>inst✝ : SMul 𝕜 E<VAR>s t : Set E<VAR>x✝ : E<VAR>ht : Balanced 𝕜 t<VAR>h : s ⊆ t<VAR>x : E<VAR>hx : x ∈ balancedHull 𝕜 s<GOAL>x ∈ t
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝¹ : SeminormedRing 𝕜<VAR>inst✝ : SMul 𝕜 E<VAR>s t : Set E<VAR>x : E<VAR>ht : Balanced 𝕜 t<VAR>h : s ⊆ t<VAR>r : 𝕜<VAR>hr : ‖r‖ ≤ 1<VAR>y : E<VAR>hy : y ∈ s<VAR>hx : (fun x => r • x) y ∈ balancedHull 𝕜 s<GOAL>(fun x => r • x) y ∈ t
<VAR>α : Type u<VAR>x : FreeCommRing α<GOAL>∃ a, ↑a = x
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>ι : Type u_2<VAR>hdec : DecidableEq ι<VAR>hfin : Fintype ι<VAR>H : ι → Subgroup G<VAR>f g : (i : ι) → ↥(H i)<VAR>hcomm : Pairwise fun i j => ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y<VAR>inst✝¹ : Finite ι<VAR>inst✝ : (i : ι) → Fintype ↥(H i)<VAR>hcoprime : Pairwise fun i j => (Fintype.card ↥(H i)).Coprime (Fintype.card ↥(H j))<GOAL>CompleteLattice.Independent H
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}<GOAL>map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}<VAR>h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f<GOAL>map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen
<VAR>α : Type u<VAR>inst✝² : UniformSpace α<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.2 ×ˢ ↑p.1}<VAR>h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f<VAR>h₂ : (𝓤 α).lift' f ≤ (𝓤 α).lift' gen<GOAL>map Prod.swap ((𝓤 α).lift' gen) ≤ (𝓤 α).lift' gen
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Monoid G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AddCommMonoid W<VAR>inst✝ : Module k W<VAR>ρV : Representation k G V<VAR>ρW : Representation k G W<VAR>r : MonoidAlgebra k G<VAR>x : V<VAR>y : W<GOAL>((ρV ⊗ 1).asAlgebraHom r) (x ⊗ₜ[k] y) = (ρV.asAlgebraHom r) x ⊗ₜ[k] y
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Monoid G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AddCommMonoid W<VAR>inst✝ : Module k W<VAR>ρV : Representation k G V<VAR>ρW : Representation k G W<VAR>r : MonoidAlgebra k G<VAR>x : V<VAR>y : W<GOAL>(Finsupp.sum r fun i d => d • (ρV i) x ⊗ₜ[k] y) = (Finsupp.sum r fun i d => d • (ρV i) x) ⊗ₜ[k] y
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : Monoid G<VAR>inst✝³ : AddCommMonoid V<VAR>inst✝² : Module k V<VAR>inst✝¹ : AddCommMonoid W<VAR>inst✝ : Module k W<VAR>ρV : Representation k G V<VAR>ρW : Representation k G W<VAR>r : MonoidAlgebra k G<VAR>x : V<VAR>y : W<GOAL>∑ x_1 ∈ r.support, r x_1 • (ρV x_1) x ⊗ₜ[k] y = ∑ a ∈ r.support, (r a • (ρV a) x) ⊗ₜ[k] y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest<VAR>r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y<VAR>x y : Cofix F α<VAR>rxy : r x y<GOAL>x = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest<VAR>r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y<VAR>x y : Cofix F α<VAR>rxy : r x y<GOAL>∀ (x : Cofix F α), r' x x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest<VAR>r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y<VAR>x y : Cofix F α<VAR>rxy : r x y<GOAL>∀ (x y : Cofix F α), r' x y → (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest<VAR>r' : Cofix F α → Cofix F α → Prop := fun x y => x = y ∨ r x y<VAR>x y : Cofix F α<VAR>rxy : r x y<GOAL>r' x y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<GOAL>(∃ y ∈ p, ∃ z ∈ p', y + z = x) ↔ ∃ y z, ↑y + ↑z = x
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>motive : M ⊗[R] N → Prop<VAR>z : M ⊗[R] N<VAR>zero : motive 0<VAR>tmul : ∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)<VAR>add : ∀ (x y : M ⊗[R] N), motive x → motive y → motive (x + y)<VAR>x : FreeAddMonoid (M × N)<VAR>x✝ : M × N<VAR>y : FreeAddMonoid (M × N)<VAR>ih : motive ↑y<VAR>m : M<VAR>n : N<GOAL>motive ↑(FreeAddMonoid.of (m, n) + y)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>motive : M ⊗[R] N → Prop<VAR>z : M ⊗[R] N<VAR>zero : motive 0<VAR>tmul : ∀ (x : M) (y : N), motive (x ⊗ₜ[R] y)<VAR>add : ∀ (x y : M ⊗[R] N), motive x → motive y → motive (x + y)<VAR>x : FreeAddMonoid (M × N)<VAR>x✝ : M × N<VAR>y : FreeAddMonoid (M × N)<VAR>ih : motive ↑y<VAR>m : M<VAR>n : N<GOAL>motive (↑(FreeAddMonoid.of (m, n)) + ↑y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : UpperSet α<VAR>t : Set α<VAR>a : α<GOAL>s.sdiff t = s ↔ Disjoint (↑s) t
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q n : ℕ<GOAL>HigherFacesVanish (q + 1) ((P (q + 1)).f (n + 1))
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q n : ℕ<GOAL>HigherFacesVanish (q + 1) ((P q ≫ (𝟙 K[X] + Hσ q)).f (n + 1))
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup Fₗ<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜₂ F<VAR>inst✝² : NormedSpace 𝕜₃ G<VAR>inst✝¹ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>inst✝ : Nontrivial E<GOAL>‖id 𝕜 E‖ = 1
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup Fₗ<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜₂ F<VAR>inst✝² : NormedSpace 𝕜₃ G<VAR>inst✝¹ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f g : E →SL[σ₁₂] F<VAR>x y z : E<VAR>inst✝ : Nontrivial E<GOAL>∃ x, ‖x‖ ≠ 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedAddCommGroup Fₗ<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁵ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedSpace 𝕜₂ F<VAR>inst✝² : NormedSpace 𝕜₃ G<VAR>inst✝¹ : NormedSpace 𝕜 Fₗ<VAR>c : 𝕜<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>f g : E →SL[σ₁₂] F<VAR>x✝ y z : E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>hx : x ≠ 0<GOAL>∃ x, ‖x‖ ≠ 0
<VAR>m n✝ a b c d n : ℕ<GOAL>n % 4 = 3 → n % 2 = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : AddCommMonoid E<VAR>inst✝⁴ : AddCommMonoid F<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f g : E → β<VAR>hf : ConvexOn 𝕜 s f<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<VAR>hxz : f x ≤ f (a • x + b • y)<GOAL>f (a • x + b • y) ≤ f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort u_6<VAR>s t u : Set α<VAR>S : Set (Set α)<GOAL>generateFrom (insert univ S) = generateFrom S
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : SetLike σ A<VAR>inst✝² : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>i j : ι<VAR>inst✝¹ : AddRightCancelMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>a : A<VAR>b : ↥(𝒜 j)<GOAL>↑(((decompose 𝒜) (a * ↑b)) (i + j)) = ↑(((decompose 𝒜) a) i) * ↑b
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.73452, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C 1<VAR>left : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>right : F.obj' 1 ⋯ ≅ G.obj' 1 ⋯<VAR>w : autoParam (F.map' 0 1 ⋯ ⋯ ≫ right.hom = left.hom ≫ G.map' 0 1 ⋯ ⋯) _auto✝<GOAL>G.map' 0 1 ⋯ ⋯ ≫ right.inv = left.inv ≫ F.map' 0 1 ⋯ ⋯
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.73452, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ : ComposableArrows C n<VAR>F G : ComposableArrows C 1<VAR>left : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯<VAR>right : F.obj' 1 ⋯ ≅ G.obj' 1 ⋯<VAR>w : autoParam (F.map' 0 1 ⋯ ⋯ ≫ right.hom = left.hom ≫ G.map' 0 1 ⋯ ⋯) _auto✝<GOAL>G.map' 0 1 ⋯ ⋯ ≫ 𝟙 (G.obj' 1 ⋯) = G.map' 0 1 ⋯ ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>f : α → β<VAR>x : ↑(range f)<GOAL>rangeFactorization f (rangeSplitting f x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>f : α → β<VAR>x : ↑(range f)<GOAL>↑(rangeFactorization f (rangeSplitting f x)) = ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : ι → α<VAR>s t : Set α<VAR>f : α → β<VAR>x : ↑(range f)<GOAL>f (rangeSplitting f x) = ↑x
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝⁶ : DecidableEq ι<VAR>inst✝⁵ : (i : ι) → Zero (β i)<VAR>inst✝⁴ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>inst✝³ : (i : ι) → Zero (β₁ i)<VAR>inst✝² : (i : ι) → Zero (β₂ i)<VAR>inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>f : (i : ι) → β₁ i → β₂ i → β i<VAR>hf : ∀ (i : ι), f i 0 0 = 0<VAR>g₁ : Π₀ (i : ι), β₁ i<VAR>g₂ : Π₀ (i : ι), β₂ i<GOAL>(zipWith f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r p q : α → α → Prop<VAR>f g : ι → α<VAR>s t u : Set α<VAR>a b : α<VAR>hr : Symmetric r<GOAL>(s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∧ r b a) ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}<VAR>lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}<VAR>lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤<VAR>rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}<VAR>lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤<VAR>rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤<VAR>rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}<VAR>lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤<VAR>rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤<VAR>rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤<GOAL>∫ (ω : α), f ω ∂μ = (∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ).toReal
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}<VAR>lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ⊤<VAR>rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a} < ⊤<VAR>rhs_integrand_finite : ∀ t > 0, μ {a | t < f a} < ⊤<GOAL>∫ (t : ℝ) in Ioi 0, (μ {a | t < f a}).toReal = (∫⁻ (t : ℝ) in Ioi 0, μ {a | t < f a}).toReal
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<VAR>M : n × n → S<GOAL>Polynomial.map (eval₂Hom f M) (univ R n) = (of (Function.curry M)).charpoly
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>n : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>f : R →+* S<VAR>M : n × n → S<GOAL>((mvPolynomialX n n R).map (eval₂ f M)).charpoly = ((mvPolynomialX n n R).map (eval₂ f fun p => of (Function.curry M) p.1 p.2)).charpoly
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>R : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>f g : α → β<VAR>μ ν : Measure α<VAR>a✝ : Nontrivial α<VAR>inhabited_h : Inhabited α<GOAL>AEMeasurable f 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>inst✝ : Nonempty α<VAR>f : ↥(lp E ⊤)<GOAL>IsLUB (Set.range fun i => ‖↑f i‖) ‖f‖
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>inst✝ : Nonempty α<VAR>f : ↥(lp E ⊤)<GOAL>IsLUB (Set.range fun i => ‖↑f i‖) (⨆ i, ‖↑f i‖)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : ↥(oneCocycles A)<VAR>g : G<GOAL>(A.ρ g) (↑f g⁻¹) = -↑f g
<VAR>x : ℍ<GOAL>‖(WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x)‖ = ‖x‖
<VAR>x : ℍ<GOAL>√(⟪(WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 0, (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 0⟫_ℝ + ⟪(WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 1, (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 1⟫_ℝ + ⟪(WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 2, (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 2⟫_ℝ + ⟪(WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 3, (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 3⟫_ℝ) = √(x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)
<VAR>x : ℍ<GOAL>√((WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 0 ^ 2 + (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 1 ^ 2 + (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 2 ^ 2 + (WithLp.equiv 2 (Fin 4 → ℝ)).symm ((equivTuple ℝ) x) 3 ^ 2) = √(x.re ^ 2 + x.imI ^ 2 + x.imJ ^ 2 + x.imK ^ 2)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>t : ℝ<VAR>hX : ¬Integrable (fun ω => rexp (t * X ω)) μ<GOAL>cgf X μ t = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>inst✝¹⁶ : EuclideanDomain R<VAR>inst✝¹⁵ : CommRing S<VAR>inst✝¹⁴ : IsDomain S<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Algebra R K<VAR>inst✝¹⁰ : IsFractionRing R K<VAR>inst✝⁹ : Algebra K L<VAR>inst✝⁸ : FiniteDimensional K L<VAR>inst✝⁷ : Algebra.IsSeparable K L<VAR>algRL : Algebra R L<VAR>inst✝⁶ : IsScalarTower R K L<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra S L<VAR>ist : IsScalarTower R S L<VAR>iic : IsIntegralClosure S R L<VAR>abv : AbsoluteValue R ℤ<VAR>ι : Type u_5<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>bS : Basis ι R S<VAR>adm : abv.IsAdmissible<VAR>inst✝¹ : Infinite R<VAR>inst✝ : DecidableEq R<GOAL>(algebraMap R S) (∏ m ∈ finsetApprox bS adm, m) ≠ 0