ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>A : Type u_3<VAR>T : Type u_4<VAR>B : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : Ring R'<VAR>inst✝³ : AddZeroClass A<VAR>inst✝² : SemilatticeSup B<VAR>inst✝¹ : Add B<VAR>inst✝ : OrderBot B<VAR>D : A → B<VAR>a : A<VAR>r : R<VAR>hr : r ≠ 0<GOAL>supDegree D (single a r) = D a
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → ℝ<VAR>s : Set α<VAR>h : LocallyBoundedVariationOn f s<GOAL>∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → ℝ<VAR>h : LocallyBoundedVariationOn f ∅<GOAL>∃ p q, MonotoneOn p ∅ ∧ MonotoneOn q ∅ ∧ f = p - q
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → ℝ<VAR>s : Set α<VAR>h : LocallyBoundedVariationOn f s<VAR>c : α<VAR>cs : c ∈ s<GOAL>∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J J' : FractionalIdeal S P<VAR>h : J ≤ J'<GOAL>(fun x => I * x) J ≤ (fun x => I * x) J'
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝¹ : CommRing P<VAR>inst✝ : Algebra R P<VAR>loc : IsLocalization S P<VAR>I J J' : FractionalIdeal S P<VAR>h : J ≤ J'<GOAL>⟨↑I * ↑J, ⋯⟩ ≤ ⟨↑I * ↑J', ⋯⟩
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.14125, u_1} C<VAR>inst✝ : Preadditive C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex (Karoubi C) c<VAR>f : K ⟶ L<VAR>i j : ι<VAR>hij : c.Rel i j<GOAL>(fun n => (f.f n).f) i ≫ (obj L).X.d i j = (obj K).X.d i j ≫ (fun n => (f.f n).f) j
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>x : ProjectiveSpectrum 𝒜<GOAL>x ∈ zeroLocus 𝒜 {f ^ n} ↔ x ∈ zeroLocus 𝒜 {f}
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁✝ : QuadraticForm R M₁<VAR>Q₂✝ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>f : Q₁ →qᵢ Q₂<VAR>hf : Function.Surjective ⇑f<VAR>r : R<GOAL>(map f) ((algebraMap R (CliffordAlgebra Q₁)) r) = (algebraMap R (CliffordAlgebra Q₂)) r
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁✝ : QuadraticForm R M₁<VAR>Q₂✝ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>f : Q₁ →qᵢ Q₂<VAR>hf : Function.Surjective ⇑f<VAR>y : M₂<VAR>x : M₁<VAR>hx : f x = y<GOAL>(map f) ((ι Q₁) x) = (ι Q₂) y
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁✝ : QuadraticForm R M₁<VAR>Q₂✝ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>f : Q₁ →qᵢ Q₂<VAR>hf : Function.Surjective ⇑f<VAR>x✝³ x✝² : CliffordAlgebra Q₂<VAR>x✝¹ : ∃ a, (map f) a = x✝³<VAR>x✝ : ∃ a, (map f) a = x✝²<VAR>x : CliffordAlgebra Q₁<VAR>hx : (map f) x = x✝³<VAR>y : CliffordAlgebra Q₁<VAR>hy : (map f) y = x✝²<GOAL>(map f) (x * y) = x✝³ * x✝²
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁✝ : QuadraticForm R M₁<VAR>Q₂✝ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>f : Q₁ →qᵢ Q₂<VAR>hf : Function.Surjective ⇑f<VAR>x✝³ x✝² : CliffordAlgebra Q₂<VAR>x✝¹ : ∃ a, (map f) a = x✝³<VAR>x✝ : ∃ a, (map f) a = x✝²<VAR>x : CliffordAlgebra Q₁<VAR>hx : (map f) x = x✝³<VAR>y : CliffordAlgebra Q₁<VAR>hy : (map f) y = x✝²<GOAL>(map f) (x + y) = x✝³ + x✝²
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c : α<VAR>hab : a ≤ b<GOAL>Ico a b ∪ {b} = Icc a b
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Semiring S<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁶ : CommSemiring R₁<VAR>inst✝⁵ : CommSemiring R₂<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R₁ A<VAR>inst✝² : Algebra R₂ A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : Algebra R₁ B<VAR>I : Ideal A<VAR>J : Ideal B<VAR>f : A →ₐ[R₁] B<VAR>H : I ≤ comap f J<VAR>x : A<GOAL>((quotientMapₐ J f H).comp (Quotient.mkₐ R₁ I)) x = ((Quotient.mkₐ R₁ J).comp f) x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>I : Type w<VAR>A B : I → C<VAR>f : (i : I) → A i ⟶ B i<VAR>S X Y Z : C<VAR>πX : X ⟶ S<VAR>πY : Y ⟶ S<VAR>φ : X ⟶ Y<VAR>inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C<VAR>inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C<VAR>hφ : φ ≫ πY = πX<VAR>i : I<VAR>t : A i ⟶ X<VAR>b : B i ⟶ S<VAR>w : t ≫ πX = f i ≫ b<GOAL>Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorObjLeft f πX ≫ functorMapTgt f πX πY φ hφ = Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorMapSrc f πX πY φ hφ ≫ functorObjLeft f πY
<VAR>a b c d n : ℕ<VAR>z : ℝ<VAR>hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2<GOAL>z ≤ (↑c / ↑d).sqrtTwoAddSeries (n + 1)
<VAR>a b c d n : ℕ<VAR>z : ℝ<VAR>hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2<GOAL>(↑a / ↑b).sqrtTwoAddSeries n ≤ (↑c / ↑d).sqrtTwoAddSeries (n + 1)
<VAR>a b c d n : ℕ<VAR>z : ℝ<VAR>hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2<GOAL>(↑a / ↑b).sqrtTwoAddSeries n ≤ (√(2 + ↑c / ↑d)).sqrtTwoAddSeries n
<VAR>a b c d n : ℕ<VAR>z : ℝ<VAR>hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2<GOAL>↑a / ↑b ≤ √(2 + ↑c / ↑d)
<VAR>a b c d n : ℕ<VAR>z : ℝ<VAR>hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2<GOAL>(↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d
<VAR>a b c d n : ℕ<VAR>z : ℝ<VAR>hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2<VAR>hb' : 0 < ↑b<GOAL>(↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d
<VAR>a b c d n : ℕ<VAR>z : ℝ<VAR>hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2<VAR>hb' : 0 < ↑b<VAR>hd' : 0 < ↑d<GOAL>(↑a / ↑b) ^ 2 ≤ 2 + ↑c / ↑d
<VAR>a b c d n : ℕ<VAR>z : ℝ<VAR>hz : z ≤ (↑a / ↑b).sqrtTwoAddSeries n<VAR>hb : 0 < b<VAR>hd : 0 < d<VAR>h : a ^ 2 * d ≤ (2 * d + c) * b ^ 2<VAR>hb' : 0 < ↑b<VAR>hd' : 0 < ↑d<GOAL>↑a ^ 2 * ↑d ≤ (2 * ↑d + ↑c) * ↑b ^ 2
<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<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<GOAL>⨆ i, N i = ⊤ ↔ ⨆ i, ↑(N i) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<GOAL>∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<VAR>w✝ : Submodule R M<VAR>N' : Submodule R N<VAR>left✝ : Module.Finite R ↥w✝<VAR>hfin : Module.Finite R ↥N'<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl w✝ N'))<GOAL>∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<VAR>w✝ : Submodule R M<VAR>N' : Submodule R N<VAR>left✝ : Module.Finite R ↥w✝<VAR>hfin : Module.Finite R ↥N'<VAR>h : s ⊆ ↑(LinearMap.range (mapIncl w✝ N'))<GOAL>s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>M₁ M₂ : Submodule R M<VAR>N₁ N₂ : Submodule R N<VAR>s : Set (M ⊗[R] N)<VAR>hs : s.Finite<VAR>w✝ : Submodule R M<VAR>N' : Submodule R N<VAR>left✝ : Module.Finite R ↥w✝<VAR>hfin : Module.Finite R ↥N'<VAR>h : s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype ∘ₗ LinearMap.rTensor (↥N') w✝.subtype))<GOAL>s ⊆ ↑(LinearMap.range (LinearMap.lTensor M N'.subtype))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>r : α → β → Prop<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>h : ∀ᶠ (x : α) in l, ∃ y, r x y<GOAL>∃ f, ∀ᶠ (x : α) in l, r x (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>r : α → β → Prop<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>h : ∀ᶠ (x : α) in l, ∃ y, r x y<VAR>this : Nonempty β<GOAL>∃ f, ∀ᶠ (x : α) in l, r x (f x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>r : α → β → Prop<VAR>l : Filter α<VAR>inst✝ : l.NeBot<VAR>h : ∀ᶠ (x : α) in l, ∃ y, r x y<VAR>this : Nonempty β<VAR>f : α → β<VAR>hf : ∀ (x : α), (∃ y, r x y) → r x (f x)<GOAL>∃ f, ∀ᶠ (x : α) in l, r x (f x)
<VAR>R : Type u_1<VAR>inst✝² : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝ : CommRing R''<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>x : Rˣ<GOAL>χ⁻¹ ↑x = χ ↑x
<VAR>R : Type u_1<VAR>inst✝² : CommMonoid R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>R'' : Type u_3<VAR>inst✝ : CommRing R''<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>x : Rˣ<GOAL>Ring.inverse (χ ↑x) = χ ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRootMonic S f<VAR>x y : S<VAR>hxy : ∀ i < f.natDegree, h.coeff x i = h.coeff y i<VAR>i : Fin f.natDegree<GOAL>h.basis.equivFun x i = h.basis.equivFun y i
<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 : Set ℝ≥0∞<VAR>ι : Sort u_4<VAR>R : Type u_5<VAR>inst✝¹ : SMul R ℝ≥0∞<VAR>inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞<VAR>f : ι → ℝ≥0∞<VAR>c : R<GOAL>c • ⨆ i, f i = ⨆ i, c • f i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝¹ : LE α<VAR>inst✝ : PartialOrder β<VAR>f : α ≃o β<VAR>x : α<VAR>y : β<VAR>hx : ∀ (x' : α), x ≤ x'<VAR>hy : ∀ (y' : β), y ≤ y'<GOAL>f x = y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝¹ : LE α<VAR>inst✝ : PartialOrder β<VAR>f : α ≃o β<VAR>x : α<VAR>y : β<VAR>hx : ∀ (x' : α), x ≤ x'<VAR>hy : ∀ (y' : β), y ≤ y'<GOAL>f x ≤ y
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝¹ : LE α<VAR>inst✝ : PartialOrder β<VAR>f : α ≃o β<VAR>x : α<VAR>y : β<VAR>hx : ∀ (x' : α), x ≤ x'<VAR>hy : ∀ (y' : β), y ≤ y'<GOAL>x ≤ f.symm y
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>x : R<VAR>h : v x ≠ 0<GOAL>{y | v y = v x} ∈ 𝓝 x
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>x : R<VAR>h : v x ≠ 0<GOAL>∃ γ, {y | v (y - x) < ↑γ} ⊆ {y | v y = v x}
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>x : R<VAR>h : v x ≠ 0<GOAL>{y | v (y - x) < ↑(Units.mk0 (v x) h)} ⊆ {y | v y = v x}
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>x : R<VAR>h : v x ≠ 0<GOAL>{y | v (y - x) < v x} ⊆ {y | v y = v x}
<VAR>R : Type u<VAR>inst✝¹ : Ring R<VAR>Γ₀ : Type v<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>_i : Valued R Γ₀<VAR>x : R<VAR>h : v x ≠ 0<VAR>y : R<VAR>y_in : y ∈ {y | v (y - x) < v x}<GOAL>y ∈ {y | v y = v x}
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>P y * Q z ^ 3 - Q y * P z ^ 3 + (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) = (P y - W'.negY P) * Q z ^ 3
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>Lagrange.basis s v i ≠ 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<GOAL>∀ (a : ι), a ≠ i ∧ a ∈ s → ¬basisDivisor (v i) (v a) = 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j✝ : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>j : ι<VAR>hij : j ≠ i<VAR>hj : j ∈ s<GOAL>¬basisDivisor (v i) (v j) = 0
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i j✝ : ι<VAR>hvs : Set.InjOn v ↑s<VAR>hi : i ∈ s<VAR>j : ι<VAR>hij : j ≠ i<VAR>hj : j ∈ s<GOAL>¬i = j
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : I.Boundaryless<VAR>x : M<GOAL>IsOpen (extChartAt I x).target
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁶ : NormedAddCommGroup E'<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : TopologicalSpace H'<VAR>inst✝³ : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝² : ChartedSpace H M<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : I.Boundaryless<VAR>x : M<GOAL>IsOpen (↑I.symm ⁻¹' (chartAt H x).target)
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁴ : RCLike 𝕂<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : NormedRing 𝔹<VAR>inst✝ : NormedAlgebra 𝕂 𝔹<GOAL>(expSeries 𝕂 𝔸).radius = ⊤
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁴ : RCLike 𝕂<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : NormedRing 𝔹<VAR>inst✝ : NormedAlgebra 𝕂 𝔹<VAR>r : NNReal<GOAL>Summable fun n => ‖expSeries 𝕂 𝔸 n‖ * ↑r ^ n
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁴ : RCLike 𝕂<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : NormedRing 𝔹<VAR>inst✝ : NormedAlgebra 𝕂 𝔹<VAR>r : NNReal<GOAL>∀ᶠ (i : ℕ) in cofinite, ‖‖expSeries 𝕂 𝔸 i‖ * ↑r ^ i‖ ≤ ↑r ^ i / ↑i !
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁴ : RCLike 𝕂<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : NormedRing 𝔹<VAR>inst✝ : NormedAlgebra 𝕂 𝔹<VAR>r : NNReal<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>‖‖expSeries 𝕂 𝔸 n‖ * ↑r ^ n‖ ≤ ↑r ^ n / ↑n !
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁴ : RCLike 𝕂<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : NormedRing 𝔹<VAR>inst✝ : NormedAlgebra 𝕂 𝔹<VAR>r : NNReal<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>‖(↑n !)⁻¹ • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ * ‖↑r ^ n‖ ≤ ↑r ^ n / ↑n !
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁴ : RCLike 𝕂<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : NormedRing 𝔹<VAR>inst✝ : NormedAlgebra 𝕂 𝔹<VAR>r : NNReal<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>‖(↑n !)⁻¹‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ * ‖↑r ^ n‖ ≤ ↑r ^ n / ↑n !
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁴ : RCLike 𝕂<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : NormedRing 𝔹<VAR>inst✝ : NormedAlgebra 𝕂 𝔹<VAR>r : NNReal<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>↑r ^ n / ↑n ! * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ ≤ ↑r ^ n / ↑n !
<VAR>𝕂 : Type u_1<VAR>𝔸 : Type u_2<VAR>𝔹 : Type u_3<VAR>inst✝⁴ : RCLike 𝕂<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedAlgebra 𝕂 𝔸<VAR>inst✝¹ : NormedRing 𝔹<VAR>inst✝ : NormedAlgebra 𝕂 𝔹<VAR>r : NNReal<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>this : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ ≤ 1<GOAL>↑r ^ n / ↑n ! * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸‖ ≤ ↑r ^ n / ↑n !
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p✝ q p : MvPolynomial σ R<GOAL>p.totalDegree ≤ Multiset.card p.degrees
<VAR>𝕜 : Type u<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : X → E →L[𝕜] F<VAR>s : Set X<GOAL>ContinuousOn f s ↔ ∀ (y : E), ContinuousOn (fun x => (f x) y) s
<VAR>𝕜 : Type u<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : X → E →L[𝕜] F<VAR>s : Set X<VAR>h : ∀ (y : E), ContinuousOn (fun x => (f x) y) s<GOAL>ContinuousOn f s
<VAR>𝕜 : Type u<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : X → E →L[𝕜] F<VAR>s : Set X<VAR>h : ∀ (y : E), ContinuousOn (fun x => (f x) y) s<VAR>d : ℕ := finrank 𝕜 E<GOAL>ContinuousOn f s
<VAR>𝕜 : Type u<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : X → E →L[𝕜] F<VAR>s : Set X<VAR>h : ∀ (y : E), ContinuousOn (fun x => (f x) y) s<VAR>d : ℕ := finrank 𝕜 E<VAR>hd : d = finrank 𝕜 (Fin d → 𝕜)<GOAL>ContinuousOn f s
<VAR>𝕜 : Type u<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : X → E →L[𝕜] F<VAR>s : Set X<VAR>h : ∀ (y : E), ContinuousOn (fun x => (f x) y) s<VAR>d : ℕ := finrank 𝕜 E<VAR>hd : d = finrank 𝕜 (Fin d → 𝕜)<VAR>e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd<VAR>e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F := (e₁.arrowCongr 1).trans (ContinuousLinearEquiv.piRing (Fin d))<GOAL>ContinuousOn f s
<VAR>𝕜 : Type u<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>E : Type v<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type w<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>F' : Type x<VAR>inst✝⁷ : AddCommGroup F'<VAR>inst✝⁶ : Module 𝕜 F'<VAR>inst✝⁵ : TopologicalSpace F'<VAR>inst✝⁴ : TopologicalAddGroup F'<VAR>inst✝³ : ContinuousSMul 𝕜 F'<VAR>inst✝² : CompleteSpace 𝕜<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>f : X → E →L[𝕜] F<VAR>s : Set X<VAR>h : ∀ (y : E), ContinuousOn (fun x => (f x) y) s<VAR>d : ℕ := finrank 𝕜 E<VAR>hd : d = finrank 𝕜 (Fin d → 𝕜)<VAR>e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd<VAR>e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F := (e₁.arrowCongr 1).trans (ContinuousLinearEquiv.piRing (Fin d))<GOAL>ContinuousOn ((⇑e₂.symm ∘ ⇑e₂) ∘ f) s
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra K 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>inst✝⁴ : Module.Finite K L<VAR>inst✝³ : Module.Finite R L<VAR>inst✝² : Module.Free R L<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Free R M<VAR>x y : L<VAR>r : R<GOAL>Polynomial.map (evalRingHom r) (LieAlgebra.engel_isBot_of_isMin.lieCharpoly R M x y) = charpoly (φ (r • y + x))
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁴ : Field K<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : Nontrivial R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra K 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>inst✝⁴ : Module.Finite K L<VAR>inst✝³ : Module.Finite R L<VAR>inst✝² : Module.Free R L<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Free R M<VAR>x y : L<VAR>r : R<GOAL>Polynomial.map ((evalRingHom r).comp ↑(MvPolynomial.aeval fun i => C (((chooseBasis R L).repr y) i) * X + C (((chooseBasis R L).repr x) i))) ((↑φ).polyCharpoly (chooseBasis R L)) = charpoly (φ (r • y + x))