ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace E<GOAL>IsOpen (range toContinuousLinearMap)
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace E<GOAL>∀ (i : E ≃L[𝕜] F), range toContinuousLinearMap ∈ 𝓝 ↑i
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃L[𝕜] F<GOAL>IsOpen (range toContinuousLinearMap)
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃L[𝕜] F<VAR>O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f<GOAL>IsOpen (range toContinuousLinearMap)
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃L[𝕜] F<VAR>O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f<VAR>h_O : Continuous O<GOAL>IsOpen (range toContinuousLinearMap)
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃L[𝕜] F<VAR>O : (E →L[𝕜] F) → E →L[𝕜] E := fun f => (↑e.symm).comp f<VAR>h_O : Continuous O<GOAL>range toContinuousLinearMap = O ⁻¹' {x | IsUnit x}
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>N : Subgroup G<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hN : N = f.ker<VAR>tH : IsTorsion H<VAR>tN : IsTorsion ↥N<VAR>g : G<VAR>ngn : ℕ<VAR>ngnpos : 0 < ngn<VAR>hngn : f g ^ ngn = 1<GOAL>IsOfFinOrder g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>N : Subgroup G<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hN : N = f.ker<VAR>tH : IsTorsion H<VAR>tN : IsTorsion ↥N<VAR>g : G<VAR>ngn : ℕ<VAR>ngnpos : 0 < ngn<VAR>hngn : f g ^ ngn = 1<VAR>hmem : g ^ ngn ∈ f.ker<GOAL>IsOfFinOrder g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>N : Subgroup G<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hN : N = f.ker<VAR>tH : IsTorsion H<VAR>tN : IsTorsion ↥N<VAR>g : G<VAR>ngn : ℕ<VAR>ngnpos : 0 < ngn<VAR>hngn : f g ^ ngn = 1<VAR>gn : ↥N<VAR>h : ↑gn = g ^ ngn<VAR>hmem✝ hmem : ↑gn ∈ f.ker<GOAL>IsOfFinOrder g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝¹ : Group G<VAR>N : Subgroup G<VAR>inst✝ : Group H<VAR>f : G →* H<VAR>hN : N = f.ker<VAR>tH : IsTorsion H<VAR>tN : IsTorsion ↥N<VAR>g : G<VAR>ngn : ℕ<VAR>ngnpos : 0 < ngn<VAR>hngn : f g ^ ngn = 1<VAR>gn : ↥N<VAR>h : ↑gn = g ^ ngn<VAR>hmem✝ hmem : ↑gn ∈ f.ker<VAR>nn : ℕ<VAR>nnpos : 0 < nn<VAR>hnn : gn ^ nn = 1<GOAL>IsOfFinOrder g
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D D1 D2 : LieDerivation R L M<VAR>a b : L<VAR>s : Set L<VAR>h : Set.EqOn (⇑D1) (⇑D2) s<VAR>z : L<VAR>hz : z ∈ ↑(LieSubalgebra.lieSpan R L s)<GOAL>D1 0 = D2 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D D1 D2 : LieDerivation R L M<VAR>a b : L<VAR>s : Set L<VAR>h : Set.EqOn (⇑D1) (⇑D2) s<VAR>z : L<VAR>hz : z ∈ ↑(LieSubalgebra.lieSpan R L s)<VAR>zero : D1 0 = D2 0<VAR>x✝¹ : R<VAR>x✝ : L<VAR>hx : D1 x✝ = D2 x✝<GOAL>D1 (x✝¹ • x✝) = D2 (x✝¹ • x✝)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D D1 D2 : LieDerivation R L M<VAR>a b : L<VAR>s : Set L<VAR>h : Set.EqOn (⇑D1) (⇑D2) s<VAR>z : L<VAR>hz : z ∈ ↑(LieSubalgebra.lieSpan R L s)<VAR>zero : D1 0 = D2 0<VAR>smul : ∀ (r : R) {x : L}, D1 x = D2 x → D1 (r • x) = D2 (r • x)<VAR>x✝¹ x✝ : L<VAR>hx : D1 x✝¹ = D2 x✝¹<VAR>hy : D1 x✝ = D2 x✝<GOAL>D1 (x✝¹ + x✝) = D2 (x✝¹ + x✝)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<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>D D1 D2 : LieDerivation R L M<VAR>a b : L<VAR>s : Set L<VAR>h : Set.EqOn (⇑D1) (⇑D2) s<VAR>z : L<VAR>hz : z ∈ ↑(LieSubalgebra.lieSpan R L s)<VAR>zero : D1 0 = D2 0<VAR>smul : ∀ (r : R) {x : L}, D1 x = D2 x → D1 (r • x) = D2 (r • x)<VAR>add : ∀ (x y : L), D1 x = D2 x → D1 y = D2 y → D1 (x + y) = D2 (x + y)<VAR>x✝¹ x✝ : L<VAR>hx : D1 x✝¹ = D2 x✝¹<VAR>hy : D1 x✝ = D2 x✝<GOAL>D1 ⁅x✝¹, x✝⁆ = D2 ⁅x✝¹, x✝⁆
<VAR>x y✝ z✝ : ZFSet<VAR>h : x.IsTransitive<VAR>y : ZFSet<VAR>hy : y ∈ ⋃₀ x<VAR>z : ZFSet<VAR>hz : z ∈ y<GOAL>z ∈ ⋃₀ x
<VAR>x y✝ z✝ : ZFSet<VAR>h : x.IsTransitive<VAR>y : ZFSet<VAR>hy : y ∈ ⋃₀ x<VAR>z : ZFSet<VAR>hz : z ∈ y<VAR>w : ZFSet<VAR>hw : w ∈ x<VAR>hw' : y ∈ w<GOAL>z ∈ ⋃₀ x
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<GOAL>eulerMascheroniSeq' 6 < 2 / 3
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<GOAL>rexp (49 / 20 - 2 / 3) < 6
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<GOAL>rexp (107 / 60) < 6
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<VAR>this : rexp 1 ^ (107 / 60) < 2.7182818286 ^ (107 / 60)<GOAL>rexp (107 / 60) < 6
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<VAR>this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)<GOAL>rexp (107 / 60) < 6
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<VAR>this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)<GOAL>2.7182818286 ^ (107 / 60) < 6
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<VAR>this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)<GOAL>2.7182818286 ^ 107 < 6 ^ OfNat.ofNat 60
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<VAR>this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)<GOAL>60 ≠ 0
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<VAR>this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)<GOAL>0 ≤ 2.7182818286
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<VAR>this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)<GOAL>0 ≤ 2.7182818286 ^ (107 / 60)
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<VAR>this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)<GOAL>0 ≤ 6
<VAR>h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6<VAR>this : rexp (107 / 60) < 2.7182818286 ^ (107 / 60)<GOAL>0 < 60
<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₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<VAR>A B : Matrix n n R<GOAL>(toLinAlgEquiv v₁) (A * B) = (toLinAlgEquiv v₁) A ∘ₗ (toLinAlgEquiv v₁) B
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>hb : 0 ≤ b<GOAL>|a| = b ↔ a = b ∨ a = -b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>hb : 0 ≤ b<GOAL>a = b ∨ a = -b → |a| = b
<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>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : P<VAR>h : ∑ i ∈ s, w i = 0<GOAL>(s.weightedVSub fun x => p) w = 0
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<GOAL>#(AddMonoidAlgebra R ℕ) = max #R ℵ₀
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Nontrivial R<GOAL>max (#R) (lift.{u, 0} #ℕ) = max #R ℵ₀
<VAR>d : ℕ<VAR>dnsq : Nonsquare d<VAR>a b : ℤ√↑d<VAR>ab : a ≤ b<VAR>ba : b ≤ a<GOAL>(-(a - b)).Nonneg
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝¹ p✝ q✝ : R[X]<VAR>ι : Type u_1<VAR>p q : R[X]<GOAL>(p * q).degree ≤ p.degree + q.degree
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b✝ c✝ a b c : α<GOAL>min (a / c) (b / c) = min a b / c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₁ : k₁ =o[l] k₂<VAR>h₂ : f' =O[l] g'<GOAL>(fun x => k₁ x • f' x) =o[l] fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₂ : f' =O[l] g'<VAR>h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂<GOAL>∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₂ : f' =O[l] g'<VAR>h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂<VAR>c : ℝ<VAR>cpos : 0 < c<GOAL>IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c'✝ c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜' F'<VAR>inst✝ : BoundedSMul 𝕜' F'<VAR>k₁ : α → R<VAR>k₂ : α → 𝕜'<VAR>h₂ : f' =O[l] g'<VAR>h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂<VAR>c : ℝ<VAR>cpos : 0 < c<VAR>c' : ℝ<VAR>c'pos : c' > 0<VAR>hc' : IsBigOWith c' l f' g'<GOAL>IsBigOWith c l (fun x => k₁ x • f' x) fun x => k₂ x • g' x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>M N : Submodule R A<VAR>h : M.FG<VAR>n : ℕ<GOAL>span R ↑{1} = M ^ Nat.zero
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>M N : Submodule R A<VAR>h : M.FG<VAR>n✝ n : ℕ<VAR>ih : (M ^ n).FG<GOAL>(M ^ n.succ).FG
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>a b c : ℤ<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>HF : a ^ n + b ^ n + c ^ n = 0<GOAL>IsCoprime a b
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m n : ℕ<VAR>a b c : ℤ<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>HF : a ^ 0 + b ^ 0 + c ^ 0 = 0<GOAL>IsCoprime a b
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>a b c : ℤ<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>HF : a ^ n + b ^ n + c ^ n = 0<VAR>hn : n ≠ 0<GOAL>IsCoprime a b
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>a b c : ℤ<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>HF : a ^ n + b ^ n + c ^ n = 0<VAR>hn : n ≠ 0<GOAL>¬(a = 0 ∧ b = 0)
<VAR>α : Type u_1<VAR>inst✝¹ : Semiring α<VAR>inst✝ : NoZeroDivisors α<VAR>m n✝ n : ℕ<VAR>a b c : ℤ<VAR>Hgcd : {a, b, c}.gcd id = 1<VAR>HF : a ^ n + b ^ n + c ^ n = 0<VAR>hn : n ≠ 0<VAR>p : ℤ<VAR>hp : Prime p<VAR>hpa : p ∣ a<VAR>hpb : p ∣ b<GOAL>p ∣ 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : Filter α<VAR>s : Set α<VAR>f : α → β<VAR>t : Set β<GOAL>t ∈ pmap (PFun.res f s) l ↔ t ∈ map f (l ⊓ 𝓟 s)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : Filter α<VAR>s : Set α<VAR>f : α → β<VAR>t : Set β<GOAL>sᶜ ∪ f ⁻¹' t ∈ l ↔ {x | x ∉ s ∨ x ∈ f ⁻¹' t} ∈ l
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>ω : List B<GOAL>(cs.leftInvSeq ω).length = ω.length
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>H : G.Subgraph<VAR>v : V<GOAL>H = G.singletonSubgraph v ↔ H.verts = {v}
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>H : G.Subgraph<VAR>v : V<VAR>h : H.verts = {v}<GOAL>H = G.singletonSubgraph v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f'✝ : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f' : α → E' × F'<GOAL>(fun x => (f' x).1) =O[l] f'
<VAR>G : Type u_1<VAR>inst✝³ : MeasurableSpace G<VAR>μ : Measure G<VAR>g✝ : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableMul G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → ℝ≥0∞<VAR>g : G<GOAL>∫⁻ (x : G), f (x / g) ∂μ = ∫⁻ (x : G), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<VAR>f : (i : ι) → κ i → UpperSet α<GOAL>a ∈ ⨅ i, ⨅ j, f i j ↔ ∃ i j, a ∈ f i j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : OrderedSemiring β<VAR>s : Set α<VAR>hs : s.Subsingleton<VAR>f : α → β<VAR>i j : α<VAR>hi : i ∈ s<VAR>hj : j ∈ s<GOAL>f j ≤ f j + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<GOAL>normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩<GOAL>normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩<VAR>g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩<GOAL>normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩<VAR>g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩<VAR>h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩<GOAL>normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩} = ⊤
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩<VAR>g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩<VAR>h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩<GOAL>normalClosure {⟨finRotate 5, ⋯⟩} ≤ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩<VAR>g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩<VAR>h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩<GOAL>{⟨finRotate 5, ⋯⟩} ⊆ ↑(normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩})
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩<VAR>g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩<VAR>h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩<GOAL>g1 * g2 * g1⁻¹ * g2⁻¹ ∈ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>g1 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 2 * swap 0 1, ⋯⟩<VAR>g2 : ↥(alternatingGroup (Fin 5)) := ⟨swap 0 4 * swap 1 3, ⋯⟩<VAR>h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨finRotate 5, ⋯⟩<VAR>h : g2 ∈ normalClosure {g2}<GOAL>g1 * g2 * g1⁻¹ * g2⁻¹ ∈ normalClosure {⟨swap 0 4 * swap 1 3, ⋯⟩}
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : P.degree < Q.degree<VAR>hP : ¬P = 0<GOAL>Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : P.natDegree < Q.natDegree<VAR>hP : ¬P = 0<GOAL>Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : P.natDegree < Q.natDegree<VAR>hP : ¬P = 0<GOAL>Tendsto (fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) atTop (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : P.natDegree < Q.natDegree<VAR>hP : ¬P = 0<GOAL>Tendsto (fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) atTop (𝓝 (?neg✝ * 0))
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : P.natDegree < Q.natDegree<VAR>hP : ¬P = 0<GOAL>𝕜
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : P.natDegree < Q.natDegree<VAR>hP : ¬P = 0<GOAL>↑P.natDegree - ↑Q.natDegree < 0
<VAR>θ : Angle<GOAL>θ.toReal ≤ π
<VAR>x✝ : ℝ<GOAL>(↑x✝).toReal ≤ π
<VAR>x✝ : ℝ<GOAL>π = -π + 2 * π
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' f'' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x<VAR>hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0<GOAL>ConcaveOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' f'' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x<VAR>hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0<VAR>this : EqOn (deriv f) f' (interior D)<GOAL>ConcaveOn ℝ D f
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' f'' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x<VAR>hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0<VAR>this : EqOn (deriv f) f' (interior D)<GOAL>DifferentiableOn ℝ (deriv f) (interior D)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' f'' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'' : ∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x<VAR>hf''₀ : ∀ x ∈ interior D, f'' x ≤ 0<VAR>this : EqOn (deriv f) f' (interior D)<GOAL>∀ x ∈ interior D, deriv^[2] f x ≤ 0
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype l<GOAL>(J l R)⁻¹ = -J l R
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype l<GOAL>J l R * -J l R = 1
<VAR>l : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq l<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Fintype l<GOAL>- -1 = 1
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : Nontrivial α<VAR>s : Multiset α<GOAL>s.lcm = 0 ↔ 0 ∈ s
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : Nontrivial α<GOAL>lcm 0 = 0 ↔ 0 ∈ 0
<VAR>α : Type u_1<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : NormalizedGCDMonoid α<VAR>inst✝ : Nontrivial α<VAR>a : α<VAR>s : Multiset α<VAR>ihs : s.lcm = 0 ↔ 0 ∈ s<GOAL>(a ::ₘ s).lcm = 0 ↔ 0 ∈ a ::ₘ s
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : ℍ → ℂ<VAR>A : SL(2, ℤ)<VAR>x : ℂ<GOAL>Function.const ℍ x ∣[0] A = Function.const ℍ x
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : ℍ → ℂ<VAR>A : SL(2, ℤ)<VAR>x : ℂ<VAR>this : (↑↑↑A).det = 1<GOAL>Function.const ℍ x ∣[0] A = Function.const ℍ x
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k : ℤ<VAR>f : ℍ → ℂ<VAR>A : SL(2, ℤ)<VAR>x : ℂ<VAR>this : (↑↑↑A).det = 1<VAR>x✝ : ℍ<GOAL>(Function.const ℍ x ∣[0] A) x✝ = Function.const ℍ x x✝