ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x✝ : E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>x y : E<VAR>hy : y ∈ p.closedBall 0 r<VAR>h : (fun x => k • x) y = x<GOAL>x ∈ p.closedBall 0 (‖k‖ * r)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x✝ : E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>x y : E<VAR>hy : y ∈ p.closedBall 0 r<VAR>h : (fun x => k • x) y = x<GOAL>‖k‖ * p y ≤ ‖k‖ * r
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>A B : Set E<VAR>a : 𝕜<VAR>r✝ : ℝ<VAR>x✝ : E<VAR>p : Seminorm 𝕜 E<VAR>k : 𝕜<VAR>r : ℝ<VAR>x y : E<VAR>hy : p y ≤ r<VAR>h : (fun x => k • x) y = x<GOAL>‖k‖ * p y ≤ ‖k‖ * r
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt g (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x<VAR>hg : Tendsto g atTop (𝓝 l)<VAR>hcont : ContinuousOn g (Ici a)<GOAL>IntegrableOn g' (Ioi a) volume
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt g (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x<VAR>hg : Tendsto g atTop (𝓝 l)<VAR>hcont : ContinuousOn g (Ici a)<VAR>x : ℝ<GOAL>IntegrableOn g' (Ioc a (id x)) volume
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt g (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x<VAR>hg : Tendsto g atTop (𝓝 l)<VAR>hcont : ContinuousOn g (Ici a)<GOAL>Tendsto (fun i => ∫ (x : ℝ) in a..id i, ‖g' x‖) atTop (𝓝 (l - g a))
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt g (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x<VAR>hg : Tendsto g atTop (𝓝 l)<VAR>hcont : ContinuousOn g (Ici a)<GOAL>(fun x => g x - g a) =ᶠ[atTop] fun i => ∫ (x : ℝ) in a..id i, ‖g' x‖
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt g (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x<VAR>hg : Tendsto g atTop (𝓝 l)<VAR>hcont : ContinuousOn g (Ici a)<VAR>x : ℝ<VAR>hx : x ∈ Ioi a<GOAL>g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hcont✝ : ContinuousWithinAt g (Ici a) a<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x<VAR>hg : Tendsto g atTop (𝓝 l)<VAR>hcont : ContinuousOn g (Ici a)<VAR>x : ℝ<VAR>hx : x ∈ Ioi a<VAR>h'x : a ≤ id x<GOAL>g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
<VAR>X : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : RCLike 𝕜<VAR>inst✝ : TopologicalSpace X<VAR>f : C(X, ℝ≥0)<VAR>c : ℝ≥0<VAR>hc : 0 < c<VAR>x : X<VAR>hx : x ∈ {x | c ≤ f x}<GOAL>({ toFun := (⇑f ⊔ ⇑(const X c))⁻¹, continuous_toFun := ⋯ } * f) x = 1 x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>α : L → R<VAR>β : Weight R L M<VAR>hα : α ≠ 0<GOAL>chainBotCoeff (-α) β = chainTopCoeff α β
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I J X Y : Set α<VAR>M : Matroid α<VAR>inst✝ : M.Finite<VAR>R : Set α<VAR>hR : R ⊆ M.E<GOAL>(M ↾ R).Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<GOAL>s ∪ t \ s = t ∪ s \ t
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>p : Prop<VAR>f g : p → M<VAR>hfg : ∀ (h : p), f ⋯ = g h<GOAL>finprod f = finprod g
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<GOAL>orderOf x = 1 ↔ x = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : LiftRel R s t<VAR>b : β<VAR>h : b ∈ t<GOAL>∃ a, a ∈ s ∧ R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>s : WSeq α<VAR>t : WSeq β<VAR>H : swap (LiftRel fun x y => R y x) s t<VAR>b : β<VAR>h : b ∈ t<GOAL>∃ a, a ∈ s ∧ R a b
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : DecidableEq L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsFractionRing R K<VAR>inst✝³ : Algebra K L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : IsScalarTower R K L<VAR>I : (FractionalIdeal R⁰ K)ˣ<VAR>x : Kˣ<GOAL>{ toFun := fun x => { val := spanSingleton R⁰ ↑x, inv := spanSingleton R⁰ (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ } x = I ↔ spanSingleton R⁰ ↑x = ↑I
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>f : R[X]<GOAL>f ∈ reesAlgebra I ↔ ∀ i ∈ f.support, f.coeff i ∈ I ^ i
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>f : R[X]<GOAL>∀ (a : ℕ), f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>f : R[X]<VAR>a : ℕ<GOAL>f.coeff a ∈ I ^ a ↔ a ∈ f.support → f.coeff a ∈ I ^ a
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>f : R[X]<VAR>a : ℕ<GOAL>f.coeff a = 0 → f.coeff a ∈ I ^ a
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>hs : IsPreconnected s<VAR>hinj : Injective f<VAR>hf : IsOpenMap f<VAR>hsf : s ⊆ range f<VAR>u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>hsuv : f ⁻¹' s ⊆ u ∪ v<VAR>hsu : (f ⁻¹' s ∩ u).Nonempty<VAR>hsv : (f ⁻¹' s ∩ v).Nonempty<GOAL>(f ⁻¹' s ∩ (u ∩ v)).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s✝ t u✝ v✝ : Set α<VAR>inst✝ : TopologicalSpace β<VAR>f : α → β<VAR>s : Set β<VAR>hs : IsPreconnected s<VAR>hinj : Injective f<VAR>hf : IsOpenMap f<VAR>u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>hsuv : f ⁻¹' s ⊆ u ∪ v<VAR>hsu : (f ⁻¹' s ∩ u).Nonempty<VAR>hsv : (f ⁻¹' s ∩ v).Nonempty<VAR>hsf : f '' (f ⁻¹' s) = s<GOAL>(f ⁻¹' s ∩ (u ∩ v)).Nonempty
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>inst✝ : Fact (finrank ℝ F = n + 1)<VAR>x : Fin (n + 1) → F<GOAL>((map (Fin (n + 1)) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>inst✝ : Fact (finrank ℝ F = n + 1)<VAR>x : Fin (n + 1) → F<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<GOAL>((map (Fin (n + 1)) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>inst✝ : Fact (finrank ℝ F = n + 1)<VAR>x : Fin (n + 1) → F<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<VAR>he : e.toBasis.orientation = o<GOAL>((map (Fin (n + 1)) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>inst✝ : Fact (finrank ℝ F = n + 1)<VAR>x : Fin (n + 1) → F<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<VAR>he : e.toBasis.orientation = o<VAR>heφ : (e.map φ).toBasis.orientation = (map (Fin n.succ) φ.toLinearEquiv) o<GOAL>((map (Fin (n + 1)) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>inst✝ : Fact (finrank ℝ F = n + 1)<VAR>x : Fin (n + 1) → F<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<VAR>he : e.toBasis.orientation = o<VAR>heφ : (e.map φ).toBasis.orientation = (map (Fin n.succ) φ.toLinearEquiv) o<GOAL>(e.map φ).toBasis.det x = o.volumeForm (⇑φ.symm ∘ x)
<VAR>E : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>φ : E ≃ₗᵢ[ℝ] F<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ E = n + 1)<VAR>o : Orientation ℝ E (Fin (n + 1))<VAR>inst✝ : Fact (finrank ℝ F = n + 1)<VAR>x : Fin (n + 1) → F<VAR>e : OrthonormalBasis (Fin n.succ) ℝ E := Orientation.finOrthonormalBasis ⋯ ⋯ o<VAR>he : e.toBasis.orientation = o<VAR>heφ : (e.map φ).toBasis.orientation = (map (Fin n.succ) φ.toLinearEquiv) o<GOAL>(e.map φ).toBasis.det x = e.toBasis.det (⇑φ.symm ∘ x)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingRight<VAR>i : n<GOAL>¬B.IsOrtho (v i) (v i)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.flip.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingRight<VAR>i : n<GOAL>¬B.IsOrtho (v i) (v i)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup M₁<VAR>inst✝¹ : Module R M₁<VAR>I I' : R →+* R<VAR>inst✝ : Nontrivial R<VAR>B : M →ₛₗ[I] M →ₛₗ[I'] M₁<VAR>v : Basis n R M<VAR>h : B.flip.IsOrthoᵢ ⇑v<VAR>hB : B.SeparatingRight<VAR>i : n<GOAL>¬B.flip.IsOrtho (v i) (v i)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>s✝ : Set G<VAR>inst✝ : Group H<VAR>f : G → H<VAR>hf : IsGroupHom f<VAR>s : Set G<VAR>x : G<VAR>hx : x ∈ closure s<GOAL>f x ∈ closure (f '' s)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : MetricSpace R<VAR>inst✝⁶ : TopologicalSemiring R<VAR>inst✝⁵ : ContinuousStar R<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : ContinuousFunctionalCalculus R p<VAR>f g : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a✝)) _auto✝<VAR>hg : autoParam (ContinuousOn g (spectrum R a✝)) _auto✝<VAR>q : R[X]<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (fun a => eval a q) a = (aeval a) q
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : OrderTop R<VAR>s : Finset S<VAR>f : S → Tropical R<GOAL>untrop (∑ i ∈ s, f i) = s.inf (untrop ∘ f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : LinearOrder R<VAR>inst✝ : OrderTop R<VAR>s : Finset S<VAR>f : S → Tropical R<GOAL>s.inf (untrop ∘ f) = (Multiset.map untrop (Multiset.map f s.val)).inf
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>(t \ s).encard + s.encard = t.encard
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c * g ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c * g ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c * g ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n<VAR>hc₁_pos : 0 < c₁<GOAL>∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c * g ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n<VAR>hc₁_pos : 0 < c₁<GOAL>∀ᶠ (n : ℕ) in atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n<VAR>hc₁_pos : 0 < c₁<VAR>n : ℕ<VAR>hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n<VAR>hrpos : ∀ (i : α), 0 < r i n<VAR>hr_lt_n : ∀ (i : α), r i n < n<VAR>hn_pos : 0 < n<GOAL>∀ (i : α), sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n<VAR>hc₁_pos : 0 < c₁<VAR>n : ℕ<VAR>hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n<VAR>hrpos : ∀ (i : α), 0 < r i n<VAR>hr_lt_n : ∀ (i : α), r i n < n<VAR>hn_pos : 0 < n<VAR>i : α<VAR>hrpos_i : 0 < r i n<GOAL>sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g ↑n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ ∈ Set.Ioo 0 1<VAR>hc₁ : ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hc₂ : ∀ᶠ (n : ℕ) in atTop, ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n<VAR>hc₁_pos : 0 < c₁<VAR>n : ℕ<VAR>hn₁ : ∀ (i : α), c₁ * ↑n ≤ ↑(r i n)<VAR>hn₂ : ∀ u ∈ Set.Icc (c₁ * ↑n) ↑n, g u ≤ c₂ * g ↑n<VAR>hrpos : ∀ (i : α), 0 < r i n<VAR>hr_lt_n : ∀ (i : α), r i n < n<VAR>hn_pos : 0 < n<VAR>i : α<VAR>hrpos_i : 0 < r i n<VAR>g_nonneg : 0 ≤ g ↑n<GOAL>sumTransform (p a b) g (r i n) n ≤ max c₂ (c₂ / c₁ ^ (p a b + 1)) * g ↑n
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Semiring R<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x y : M<GOAL>LinearIndependent R fun (x : ↑∅) => ↑x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<VAR>n : ℤ<GOAL>(∃ b, (f ^ (Equiv.symm (Equiv.addRight n)) b) ((f ^ n) x) = y) ↔ f.SameCycle x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>hab : a ≤ b<GOAL>Ioc a b ∪ {a} = Icc a b
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>hconv : Convex ℝ s<VAR>hne : s.Nonempty<GOAL>IsPathConnected s
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>hconv : Convex ℝ s<VAR>hne : s.Nonempty<GOAL>∀ x ∈ s, ∀ y ∈ s, JoinedIn s x y
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s : Set E<VAR>hconv : Convex ℝ s<VAR>hne : s.Nonempty<VAR>x : E<VAR>x_in : x ∈ s<VAR>y : E<VAR>y_in : y ∈ s<GOAL>JoinedIn s x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CommGroup β<VAR>s : Set α<VAR>t u : Finset α<VAR>d : ℕ<VAR>a : α<GOAL>MulDissociated ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : CommMonoid α<VAR>inst✝⁶ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a b : α<VAR>s : Finset β<VAR>inst✝⁵ : CommMonoid γ<VAR>inst✝⁴ : TopologicalSpace γ<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>inst✝³ : FunLike G α γ<VAR>inst✝² : MonoidHomClass G α γ<VAR>inst✝¹ : FunLike G' γ α<VAR>inst✝ : MonoidHomClass G' γ α<VAR>g : G<VAR>g' : G'<VAR>hg : Continuous ⇑g<VAR>hg' : Continuous ⇑g'<VAR>hinv : LeftInverse ⇑g' ⇑g<VAR>h : Multipliable (⇑g ∘ f)<GOAL>Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁷ : CommMonoid α<VAR>inst✝⁶ : TopologicalSpace α<VAR>f g✝ : β → α<VAR>a b : α<VAR>s : Finset β<VAR>inst✝⁵ : CommMonoid γ<VAR>inst✝⁴ : TopologicalSpace γ<VAR>G : Type u_5<VAR>G' : Type u_6<VAR>inst✝³ : FunLike G α γ<VAR>inst✝² : MonoidHomClass G α γ<VAR>inst✝¹ : FunLike G' γ α<VAR>inst✝ : MonoidHomClass G' γ α<VAR>g : G<VAR>g' : G'<VAR>hg : Continuous ⇑g<VAR>hg' : Continuous ⇑g'<VAR>hinv : LeftInverse ⇑g' ⇑g<VAR>h : Multipliable (⇑g ∘ f)<VAR>this : Multipliable (⇑g' ∘ ⇑g ∘ f)<GOAL>Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>x₁ x₂ : Fin n.succ → ℕ<VAR>hx₁ : ∀ (i : Fin n.succ), x₁ i < d<VAR>hx₂ : ∀ (i : Fin n.succ), x₂ i < d<GOAL>(map d) x₁ = (map d) x₂ ↔ x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>x₁ x₂ : Fin n.succ → ℕ<VAR>hx₁ : ∀ (i : Fin n.succ), x₁ i < d<VAR>hx₂ : ∀ (i : Fin n.succ), x₂ i < d<VAR>h : (map d) x₁ = (map d) x₂<GOAL>x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>x₁ x₂ : Fin n.succ → ℕ<VAR>hx₁ : ∀ (i : Fin n.succ), x₁ i < d<VAR>hx₂ : ∀ (i : Fin n.succ), x₂ i < d<VAR>h : (map d) x₁ = (map d) x₂<VAR>this : x₁ 0 = x₂ 0<GOAL>x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>x₁ x₂ : Fin n.succ → ℕ<VAR>hx₁ : ∀ (i : Fin n.succ), x₁ i < d<VAR>hx₂ : ∀ (i : Fin n.succ), x₂ i < d<VAR>h : ∑ x : Fin n, x₁ x.succ * d ^ ↑x = ∑ x : Fin n, x₂ x.succ * d ^ ↑x ∨ d = 0<VAR>this : x₁ 0 = x₂ 0<GOAL>x₁ 0 = x₂ 0 ∧ (map d) (x₁ ∘ Fin.succ) = (map d) (x₂ ∘ Fin.succ)
<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>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<GOAL>↑N = ⊥ ↔ N = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<GOAL>weightSpaceChain M (-χ₁) χ₂ (-q) (-p) = weightSpaceChain M χ₁ χ₂ p q
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : LieAlgebra.IsNilpotent R L<VAR>χ₁ χ₂ : L → R<VAR>p q : ℤ<VAR>e : ℤ ≃ ℤ := Involutive.toPerm Neg.neg ⋯<GOAL>weightSpaceChain M (-χ₁) χ₂ (-q) (-p) = weightSpaceChain M χ₁ χ₂ p q