ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : IsIntegrallyClosed A<VAR>x : B<GOAL>IsIntegral A ((Algebra.linearMap B L) x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁸ : CommRing A<VAR>inst✝¹⁷ : Field K<VAR>inst✝¹⁶ : CommRing B<VAR>inst✝¹⁵ : Field L<VAR>inst✝¹⁴ : Algebra A K<VAR>inst✝¹³ : Algebra B L<VAR>inst✝¹² : Algebra A B<VAR>inst✝¹¹ : Algebra K L<VAR>inst✝¹⁰ : Algebra A L<VAR>inst✝⁹ : IsScalarTower A K L<VAR>inst✝⁸ : IsScalarTower A B L<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsFractionRing A K<VAR>inst✝⁵ : IsIntegralClosure B A L<VAR>inst✝⁴ : IsFractionRing B L<VAR>inst✝³ : FiniteDimensional K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : IsIntegrallyClosed A<VAR>x : B<GOAL>∃ y, (algebraMap B L) y = (Algebra.linearMap B L) x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>B : M →ₗ[R] M' →ₗ[R] R<VAR>x : M'<GOAL>x ∈ (range B).dualCoannihilator ↔ x ∈ ker B.flip
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommGroup X<VAR>inst✝ : Module R X<VAR>hS : S ≤ nonZeroDivisorsRight R<VAR>r₁ r₂ : R<VAR>h : numeratorHom r₁ = numeratorHom r₂<GOAL>r₁ = r₂
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommGroup X<VAR>inst✝ : Module R X<VAR>hS : S ≤ nonZeroDivisorsRight R<VAR>r₁ r₂ : R<VAR>h : ∃ u v, u • r₂ = v • r₁ ∧ ↑u * ↑1 = v * ↑1<GOAL>r₁ = r₂
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommGroup X<VAR>inst✝ : Module R X<VAR>hS : S ≤ nonZeroDivisorsRight R<VAR>r₁ r₂ : R<VAR>u : ↥S<VAR>v : R<VAR>h₁ : u • r₂ = v • r₁<VAR>h₂ : ↑u * ↑1 = v * ↑1<GOAL>r₁ = r₂
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommGroup X<VAR>inst✝ : Module R X<VAR>hS : S ≤ nonZeroDivisorsRight R<VAR>r₁ r₂ : R<VAR>u : ↥S<VAR>v : R<VAR>h₁ : ↑u * r₂ = v * r₁<VAR>h₂ : ↑u = v<GOAL>r₁ = r₂
<VAR>R : Type u_1<VAR>inst✝³ : Ring R<VAR>S : Submonoid R<VAR>inst✝² : OreSet S<VAR>X : Type u_2<VAR>inst✝¹ : AddCommGroup X<VAR>inst✝ : Module R X<VAR>hS : S ≤ nonZeroDivisorsRight R<VAR>r₁ r₂ : R<VAR>u : ↥S<VAR>v : R<VAR>h₁ : ↑u * (r₂ - r₁) = 0<VAR>h₂ : ↑u = v<GOAL>r₁ = r₂
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M : Matrix m n R<VAR>i : n<GOAL>((toLin v₁ v₂) M) (v₁ i) = ∑ j : m, M j i • v₂ j
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M : Matrix m n R<VAR>i : n<VAR>j : m<VAR>_hj : j ∈ Finset.univ<GOAL>(M *ᵥ ⇑(v₁.repr (v₁ i))) j • v₂ j = M j i • v₂ j
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M : Matrix m n R<VAR>i : n<VAR>j : m<VAR>_hj : j ∈ Finset.univ<GOAL>∀ b ∈ Finset.univ, b ≠ i → M j b * (Finsupp.single i 1) b = 0
<VAR>R : Type u_1<VAR>inst✝⁷ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁶ : Fintype n<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M : Matrix m n R<VAR>i : n<VAR>j : m<VAR>_hj : j ∈ Finset.univ<GOAL>i ∉ Finset.univ → M j i * (Finsupp.single i 1) i = 0
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>b✝ : B<VAR>a : F<VAR>b : B<GOAL>b ∈ (Z.localTrivAt b).baseSet
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>X : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace B<VAR>inst✝ : TopologicalSpace F<VAR>Z : FiberBundleCore ι B F<VAR>i : ι<VAR>b✝ : B<VAR>a : F<VAR>b : B<GOAL>b ∈ Z.baseSet (Z.indexAt b)
<VAR>x y : Class<VAR>h : Set.Nonempty x<GOAL>y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z
<VAR>x y : Class<VAR>h : Set.Nonempty x<VAR>H : ∀ z ∈ x, y ∈ z<GOAL>y ∈ ⋂₀ x
<VAR>x y : Class<VAR>h : Set.Nonempty x<VAR>H : ∀ z ∈ x, y ∈ z<GOAL>∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet), x z → x_1 ∈ z
<VAR>x y : Class<VAR>H : ∀ z ∈ x, y ∈ z<VAR>z : ZFSet<VAR>hz : z ∈ x<GOAL>∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet), x z → x_1 ∈ z
<VAR>x : Class<VAR>z : ZFSet<VAR>hz : z ∈ x<VAR>y : ZFSet<VAR>right✝ : ↑z y<VAR>H : ∀ z ∈ x, ↑y ∈ z<GOAL>∃ x_1, ↑x_1 = ↑y ∧ ∀ (z : ZFSet), x z → x_1 ∈ z
<VAR>x : Class<VAR>z : ZFSet<VAR>hz : z ∈ x<VAR>y : ZFSet<VAR>right✝ : ↑z y<VAR>H : ∀ z ∈ x, ↑y ∈ z<VAR>w : ZFSet<VAR>hxw : x w<GOAL>y ∈ w
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : NormedRing R<VAR>inst✝² : IsAbsoluteValue norm<VAR>F : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : CommRing F<VAR>inst✝ : NormedField K<VAR>B : ℝ<VAR>d : ℕ<VAR>f : F →+* K<VAR>p : F[X]<VAR>h1 : p.Monic<VAR>h2 : Splits f p<VAR>h3 : p.natDegree ≤ d<VAR>h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B<VAR>i : ℕ<GOAL>‖(map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : NormedRing R<VAR>inst✝² : IsAbsoluteValue norm<VAR>F : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : CommRing F<VAR>inst✝ : NormedField K<VAR>B : ℝ<VAR>d : ℕ<VAR>f : F →+* K<VAR>p : F[X]<VAR>h1 : p.Monic<VAR>h2 : Splits f p<VAR>h3 : p.natDegree ≤ d<VAR>h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B<VAR>i : ℕ<VAR>hB : 0 ≤ B<GOAL>‖(map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : NormedRing R<VAR>inst✝² : IsAbsoluteValue norm<VAR>F : Type u_3<VAR>K : Type u_4<VAR>inst✝¹ : CommRing F<VAR>inst✝ : NormedField K<VAR>B : ℝ<VAR>d : ℕ<VAR>f : F →+* K<VAR>p : F[X]<VAR>h1 : p.Monic<VAR>h2 : Splits f p<VAR>h3 : p.natDegree ≤ d<VAR>h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B<VAR>i : ℕ<VAR>hB : B < 0<GOAL>‖(map f p).coeff i‖ ≤ max B 1 ^ d * ↑(d.choose (d / 2))
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : StarRing R<VAR>inst✝¹¹ : Semiring A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarModule R A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : StarRing B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : StarModule R B<VAR>inst✝³ : Semiring C<VAR>inst✝² : StarRing C<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : StarModule R C<VAR>S : StarSubalgebra R A<VAR>s : Set A<VAR>z : A<GOAL>(∀ g ∈ s ∪ star s, g * z = z * g) ↔ ∀ g ∈ s, g * z = z * g ∧ star g * z = z * star g
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : StarRing R<VAR>inst✝¹¹ : Semiring A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarModule R A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : StarRing B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : StarModule R B<VAR>inst✝³ : Semiring C<VAR>inst✝² : StarRing C<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : StarModule R C<VAR>S : StarSubalgebra R A<VAR>s : Set A<VAR>z : A<GOAL>(∀ x ∈ s, x * z = z * x) → ((∀ x ∈ star s, x * z = z * x) ↔ ∀ x ∈ s, star x * z = z * star x)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y : C<VAR>f✝ g : X✝ ⟶ Y<VAR>X : C<VAR>f : X ⟶ X<VAR>hf : f ≫ f = f<VAR>c : Cofork (𝟙 X) f<VAR>i : IsColimit c<GOAL>i.desc (Cofork.ofπ f ⋯) ≫ c.π = 𝟙 (((Functor.const WalkingParallelPair).obj c.pt).obj one)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y : C<VAR>f✝ g : X✝ ⟶ Y<VAR>X : C<VAR>f : X ⟶ X<VAR>hf : f ≫ f = f<VAR>c : Cofork (𝟙 X) f<VAR>i : IsColimit c<VAR>this : Epi c.π := epi_of_isColimit_cofork i<GOAL>i.desc (Cofork.ofπ f ⋯) ≫ c.π = 𝟙 (((Functor.const WalkingParallelPair).obj c.pt).obj one)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y : C<VAR>f✝ g : X✝ ⟶ Y<VAR>X : C<VAR>f : X ⟶ X<VAR>hf : f ≫ f = f<VAR>c : Cofork (𝟙 X) f<VAR>i : IsColimit c<VAR>this : Epi c.π := epi_of_isColimit_cofork i<GOAL>𝟙 X ≫ c.π = c.π
<VAR>p : ℕ → Prop<VAR>k a : ℕ<VAR>h : a < nth p (k + 1)<VAR>ha : p a<GOAL>a ≤ nth p k
<VAR>p : ℕ → Prop<VAR>k a : ℕ<VAR>h : a < nth p (k + 1)<VAR>ha : p a<VAR>hf : (setOf p).Finite<GOAL>a ≤ nth p k
<VAR>p : ℕ → Prop<VAR>k a : ℕ<VAR>h : a < nth p (k + 1)<VAR>ha : p a<VAR>hf : (setOf p).Infinite<GOAL>a ≤ nth p k
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>s : Set ↑(ofOpenSubsets U).glued<VAR>hs : IsOpen s<GOAL>IsOpen (⇑(fromOpenSubsetsGlue U) '' s)
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>s : Set ↑(ofOpenSubsets U).glued<VAR>hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑((ofOpenSubsets U).ι i) ⁻¹' s)<GOAL>IsOpen (⇑(fromOpenSubsetsGlue U) '' s)
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>s : Set ↑(ofOpenSubsets U).glued<VAR>hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑((ofOpenSubsets U).ι i) ⁻¹' s)<GOAL>∀ x ∈ ⇑(fromOpenSubsetsGlue U) '' s, ∃ t ⊆ ⇑(fromOpenSubsetsGlue U) '' s, IsOpen t ∧ x ∈ t
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>s : Set ↑(ofOpenSubsets U).glued<VAR>hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑((ofOpenSubsets U).ι i) ⁻¹' s)<VAR>x : ↑(ofOpenSubsets U).glued<VAR>hx : x ∈ s<GOAL>∃ t ⊆ ⇑(fromOpenSubsetsGlue U) '' s, IsOpen t ∧ (fromOpenSubsetsGlue U) x ∈ t
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>s : Set ↑(ofOpenSubsets U).glued<VAR>hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑((ofOpenSubsets U).ι i) ⁻¹' s)<VAR>i : (ofOpenSubsets U).J<VAR>x : ↑(of α)<VAR>hx' : x ∈ U i<VAR>hx : ((ofOpenSubsets U).ι i) ⟨x, hx'⟩ ∈ s<GOAL>∃ t ⊆ ⇑(fromOpenSubsetsGlue U) '' s, IsOpen t ∧ (fromOpenSubsetsGlue U) (((ofOpenSubsets U).ι i) ⟨x, hx'⟩) ∈ t
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>s : Set ↑(ofOpenSubsets U).glued<VAR>hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑((ofOpenSubsets U).ι i) ⁻¹' s)<VAR>i : (ofOpenSubsets U).J<VAR>x : ↑(of α)<VAR>hx' : x ∈ U i<VAR>hx : ((ofOpenSubsets U).ι i) ⟨x, hx'⟩ ∈ s<GOAL>⇑(fromOpenSubsetsGlue U) '' s ∩ Set.range ⇑(U i).inclusion ⊆ ⇑(fromOpenSubsetsGlue U) '' s ∧ IsOpen (⇑(fromOpenSubsetsGlue U) '' s ∩ Set.range ⇑(U i).inclusion) ∧ (fromOpenSubsetsGlue U) (((ofOpenSubsets U).ι i) ⟨x, hx'⟩) ∈ ⇑(fromOpenSubsetsGlue U) '' s ∩ Set.range ⇑(U i).inclusion
<VAR>D : GlueData<VAR>α : Type u<VAR>inst✝ : TopologicalSpace α<VAR>J : Type u<VAR>U : J → Opens α<VAR>s : Set ↑(ofOpenSubsets U).glued<VAR>hs : ∀ (i : (ofOpenSubsets U).J), IsOpen (⇑((ofOpenSubsets U).ι i) ⁻¹' s)<VAR>i : (ofOpenSubsets U).J<VAR>x : ↑(of α)<VAR>hx' : x ∈ U i<VAR>hx : ((ofOpenSubsets U).ι i) ⟨x, hx'⟩ ∈ s<GOAL>IsOpen (⇑(fromOpenSubsetsGlue U) '' s ∩ Set.range ⇑(U i).inclusion) ∧ (fromOpenSubsetsGlue U) (((ofOpenSubsets U).ι i) ⟨x, hx'⟩) ∈ ⇑(fromOpenSubsetsGlue U) '' s ∩ Set.range ⇑(U i).inclusion
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r r₁ r₂ : α → α → Prop<VAR>s t : Set α<VAR>a b x : α<VAR>rlt : α → α → Prop<VAR>inst✝ : IsNonstrictStrictOrder α r rlt<GOAL>x ∈ minimals r s ↔ x ∈ s ∧ ∀ ⦃y : α⦄, rlt y x → y ∉ s
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : ¬(x = 0 ∧ y = 0)<GOAL>Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : ¬x = 0 ∨ ¬y = 0<GOAL>Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : ¬x = 0 ∨ ¬y = 0<GOAL>‖x + y‖ ≠ 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : ¬x = 0 ∨ ¬y = 0<GOAL>‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ≠ 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : ¬x = 0 ∨ ¬y = 0<GOAL>0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x✝ : (i : ι) → E i<GOAL>((↑(mapL f)).compMultilinearMap (tprod 𝕜)) x✝ = ((map fun i => ↑(f i)).compMultilinearMap (tprod 𝕜)) x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>g : β → β<VAR>x : α × β<VAR>a : α<VAR>b : β<VAR>m n : ℕ<GOAL>minimalPeriod g x.2 ∣ minimalPeriod (Prod.map f g) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → α<VAR>g : β → β<VAR>x : α × β<VAR>a : α<VAR>b : β<VAR>m n : ℕ<GOAL>minimalPeriod g x.2 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace α<VAR>inst✝ : CountablyGenerated α<GOAL>generateFrom (range (natGeneratingSequence α)) = m
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>r : ℝ<GOAL>⟪↑r • x, y⟫_𝕜 = r • ⟪x, y⟫_𝕜
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>P : MorphismProperty D<VAR>inst✝ : P.RespectsIso<VAR>E : C ≌ D<GOAL>P.inverseImage E.functor = P.map E.inverse
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>P : MorphismProperty D<VAR>inst✝ : P.RespectsIso<VAR>E : C ≌ D<GOAL>P.inverseImage E.functor ≤ P.map E.inverse
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} D<VAR>P : MorphismProperty D<VAR>inst✝ : P.RespectsIso<VAR>E : C ≌ D<GOAL>P.map E.inverse ≤ P.inverseImage E.functor
<VAR>α✝ : Type u<VAR>m n o : ℕ<VAR>m' : Type u_1<VAR>n' : Type u_2<VAR>o' : Type u_3<VAR>α : Type u_4<VAR>h : 0 = 0 + 0<GOAL>vecAlt1 h ![] = ![]
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(C a).degree = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>a : R<VAR>a0 : a ≠ 0<GOAL>(C a * T 0).degree = 0
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>n✝ : ℕ<VAR>n : ℕ∞<GOAL>n ≤ minOrder α ↔ ∀ ⦃s : Subgroup α⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s : Subgroup α<VAR>n✝ : ℕ<VAR>n : ℕ∞<GOAL>(∀ ⦃a : α⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)) ↔ ∀ ⦃s : Subgroup α⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s t : Multiset α<GOAL>s.ndinter t = 0 ↔ s.Disjoint t
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s t : Multiset α<GOAL>s.ndinter t ⊆ 0 ↔ s.Disjoint t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>hs : autoParam s.Finite _auto✝<GOAL>s.ncard = 0 ↔ s = ∅
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f g : α → γ<VAR>k : γ → β<VAR>h : ∀ x ∈ s, p x<GOAL>∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (f x)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g✝ : α → β<VAR>inst✝ : CommMonoid β<VAR>p : α → Prop<VAR>hp : DecidablePred p<VAR>f g : α → γ<VAR>k : γ → β<VAR>h : ∀ x ∈ s, p x<GOAL>(∏ x ∈ s, if p x then k (f x) else k (g x)) = ∏ x ∈ s, k (f x)
<VAR>x y b : Ordinal.{u_1}<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>hb : ¬1 < b<GOAL>log b x + log b y ≤ log b (x * y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ s : Set ℝ≥0∞<VAR>hs : s.Nonempty<GOAL>sSup s + a = ⨆ b ∈ s, b + a
<VAR>a x z : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : x.im < 0<GOAL>arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / abs x) - π
<VAR>a x z : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : x.im < 0<GOAL>∀ᶠ (y : ℂ) in 𝓝 x, y.re < 0 ∧ y.im < 0
<VAR>a x z : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : x.im < 0<GOAL>IsOpen fun y => y.re < 0 ∧ y.im < 0
<VAR>I : Type u<VAR>inst✝⁴ : LinearOrder I<VAR>inst✝³ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>J K L : I → Prop<VAR>inst✝² : (i : I) → Decidable (J i)<VAR>inst✝¹ : (i : I) → Decidable (K i)<VAR>inst✝ : (i : I) → Decidable (L i)<VAR>hJK : ∀ (i : I), J i → K i<VAR>hKL : ∀ (i : I), K i → L i<VAR>x : ↑(π C L)<VAR>i : I<GOAL>↑((ProjRestricts C hJK ∘ ProjRestricts C hKL) x) i = ↑(ProjRestricts C ⋯ x) i
<VAR>I : Type u<VAR>inst✝⁴ : LinearOrder I<VAR>inst✝³ : IsWellOrder I fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>J K L : I → Prop<VAR>inst✝² : (i : I) → Decidable (J i)<VAR>inst✝¹ : (i : I) → Decidable (K i)<VAR>inst✝ : (i : I) → Decidable (L i)<VAR>hJK : ∀ (i : I), J i → K i<VAR>hKL : ∀ (i : I), K i → L i<VAR>x : ↑(π C L)<VAR>i : I<GOAL>(if J i then if K i then ↑x i else false else false) = if J i then ↑x i else false
<VAR>E : Type uE<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>H : Type uH<VAR>inst✝³ : TopologicalSpace H<VAR>I : ModelWithCorners ℝ E H<VAR>M : Type uM<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : SmoothManifoldWithCorners I M<VAR>c : M<VAR>f : SmoothBumpFunction I c<VAR>x : M<GOAL>support ↑f = ↑(extChartAt I c).symm '' (ball (↑(extChartAt I c) c) f.rOut ∩ range ↑I)
<VAR>s t : ℂ<VAR>hs : 0 < s.re<VAR>ht : 0 < t.re<GOAL>Gamma s * Gamma t = Gamma (s + t) * s.betaIntegral t
<VAR>s t : ℂ<VAR>hs : 0 < s.re<VAR>ht : 0 < t.re<VAR>conv_int : ∫ (x : ℝ) in Ioi 0, ∫ (t_1 : ℝ) in 0 ..x, ((ContinuousLinearMap.mul ℝ ℂ) (↑(rexp (-t_1)) * ↑t_1 ^ (s - 1))) (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume = ((ContinuousLinearMap.mul ℝ ℂ) (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume)) (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume)<GOAL>Gamma s * Gamma t = Gamma (s + t) * s.betaIntegral t
<VAR>s t : ℂ<VAR>hs : 0 < s.re<VAR>ht : 0 < t.re<VAR>conv_int : ∫ (x : ℝ) in Ioi 0, ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume = (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume<GOAL>Gamma s * Gamma t = Gamma (s + t) * s.betaIntegral t
<VAR>s t : ℂ<VAR>hs : 0 < s.re<VAR>ht : 0 < t.re<VAR>conv_int : ∫ (x : ℝ) in Ioi 0, ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume = (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume<VAR>hst : 0 < (s + t).re<GOAL>Gamma s * Gamma t = Gamma (s + t) * s.betaIntegral t
<VAR>s t : ℂ<VAR>hs : 0 < s.re<VAR>ht : 0 < t.re<VAR>conv_int : ∫ (x : ℝ) in Ioi 0, ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume = (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume<VAR>hst : 0 < (s + t).re<GOAL>∫ (x : ℝ) in Ioi 0, ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume = ∫ (a : ℝ) in Ioi 0, ↑(rexp (-a)) * ↑a ^ (s + t - 1) * s.betaIntegral t
<VAR>s t : ℂ<VAR>hs : 0 < s.re<VAR>ht : 0 < t.re<VAR>conv_int : ∫ (x : ℝ) in Ioi 0, ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume = (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume<VAR>hst : 0 < (s + t).re<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) = ↑(rexp (-x)) * ↑x ^ (s + t - 1) * s.betaIntegral t
<VAR>s t : ℂ<VAR>hs : 0 < s.re<VAR>ht : 0 < t.re<VAR>conv_int : ∫ (x : ℝ) in Ioi 0, ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume = (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume<VAR>hst : 0 < (s + t).re<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<GOAL>∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) = ∫ (x_1 : ℝ) in 0 ..x, ↑(rexp (-x)) * (↑x_1 ^ (s - 1) * (↑x - ↑x_1) ^ (t - 1))
<VAR>s t : ℂ<VAR>hs : 0 < s.re<VAR>ht : 0 < t.re<VAR>conv_int : ∫ (x : ℝ) in Ioi 0, ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume = (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume<VAR>hst : 0 < (s + t).re<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<VAR>y : ℝ<GOAL>cexp (-↑x) = cexp (-↑y) * cexp (-(↑x - ↑y))
<VAR>s t : ℂ<VAR>hs : 0 < s.re<VAR>ht : 0 < t.re<VAR>conv_int : ∫ (x : ℝ) in Ioi 0, ∫ (t_1 : ℝ) in 0 ..x, ↑(rexp (-t_1)) * ↑t_1 ^ (s - 1) * (↑(rexp (-(x - t_1))) * ↑(x - t_1) ^ (t - 1)) ∂volume = (∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (s - 1) ∂volume) * ∫ (x : ℝ) in Ioi 0, ↑(rexp (-x)) * ↑x ^ (t - 1) ∂volume<VAR>hst : 0 < (s + t).re<VAR>x : ℝ<VAR>hx : x ∈ Ioi 0<VAR>y : ℝ<GOAL>cexp (-↑x) = cexp (-↑y + -(↑x - ↑y))
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁹ : PartialOrder Γ✝<VAR>inst✝⁸ : PartialOrder Γ'<VAR>inst✝⁷ : VAdd Γ✝ Γ'<VAR>inst✝⁶ : IsOrderedCancelVAdd Γ✝ Γ'<VAR>inst✝⁵ : AddCommMonoid V<VAR>Γ : Type u_5<VAR>inst✝⁴ : OrderedAddCommMonoid Γ<VAR>inst✝³ : AddAction Γ Γ'<VAR>inst✝² : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>r : R<VAR>x : HahnModule Γ' R V<VAR>x✝ : Γ'<GOAL>((of R).symm ((HahnSeries.single 0) r • x)).coeff x✝ = ((of R).symm (r • x)).coeff x✝
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>inst✝¹ : (i : o) → Fintype (n' i)<VAR>inst✝ : Fintype o<VAR>M : (i : o) → Matrix (m' i) (n' i) α<VAR>N : (i : o) → Matrix (n' i) (p' i) α<VAR>k : o<VAR>i : m' k<VAR>k' : o<VAR>j : p' k'<GOAL>blockDiagonal' (fun k => M k * N k) ⟨k, i⟩ ⟨k', j⟩ = (blockDiagonal' M * blockDiagonal' N) ⟨k, i⟩ ⟨k', j⟩