ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>N : Type u_9<VAR>N₂ : Type u_10<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : CommSemiring R₂<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R₂ M₂<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R N₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair τ₁₂ τ₂₁<VAR>inst✝ : RingHomInvPair τ₂₁ τ₁₂<VAR>p : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>pₗ : Submodule R N<VAR>qₗ : Submodule R N₂<VAR>fₗ : N →ₗ[R] N₂<VAR>c : R<GOAL>∀ ⦃x : N⦄, x ∈ comap fₗ qₗ → x ∈ comap (c • fₗ) qₗ
<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>N : Type u_9<VAR>N₂ : Type u_10<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : CommSemiring R₂<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R₂ M₂<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : AddCommMonoid N₂<VAR>inst✝³ : Module R N<VAR>inst✝² : Module R N₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>inst✝¹ : RingHomInvPair τ₁₂ τ₂₁<VAR>inst✝ : RingHomInvPair τ₂₁ τ₁₂<VAR>p : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>pₗ : Submodule R N<VAR>qₗ : Submodule R N₂<VAR>fₗ : N →ₗ[R] N₂<VAR>c : R<VAR>m : N<VAR>h : fₗ m ∈ qₗ<GOAL>c • fₗ m ∈ qₗ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<GOAL>Prime (minpoly R x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>a b : R[X]<VAR>h : minpoly R x ∣ a * b<VAR>h' : ¬minpoly R x ∣ a<GOAL>minpoly R x ∣ b
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>a b : R[X]<VAR>h : (Polynomial.aeval x) (a * b) = 0<VAR>h' : ¬(Polynomial.aeval x) a = 0<GOAL>(Polynomial.aeval x) b = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : Algebra R S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : NoZeroSMulDivisors R S<VAR>inst✝ : IsIntegrallyClosed R<VAR>x : S<VAR>hx : IsIntegral R x<VAR>a b : R[X]<VAR>h : (Polynomial.aeval x) a * (Polynomial.aeval x) b = 0<VAR>h' : ¬(Polynomial.aeval x) a = 0<GOAL>(Polynomial.aeval x) b = 0
<VAR>x y : ℤ[i]<GOAL>toComplex x / toComplex y - toComplex (x / y) = ↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re + (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I
<VAR>x y : ℤ[i]<GOAL>normSq (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re + (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I) ≤ normSq (1 / 2 + 1 / 2 * I)
<VAR>x y : ℤ[i]<VAR>this : |2⁻¹| = 2⁻¹<GOAL>normSq (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re + (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I) ≤ normSq (1 / 2 + 1 / 2 * I)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝ : DecidableEq ιM<VAR>bₘ : Basis ιM R M<GOAL>φ.polyCharpoly b = Polynomial.map (↑(MvPolynomial.bind₁ (toMvPolynomial b bₘ.end φ))) (charpoly.univ R ιM)
<VAR>R : Type u_1<VAR>p k : ℕ<VAR>hp : Nat.Prime p<GOAL>Ω (p ^ k) = k
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<GOAL>index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K₁.carrier V<GOAL>index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K₁.carrier V<VAR>t : Finset G<VAR>h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index K₂.carrier V<GOAL>index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K₁.carrier V<VAR>t : Finset G<VAR>h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index K₂.carrier V<GOAL>index (K₁.carrier ∪ K₂.carrier) V ≤ s.card + t.card
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K₁.carrier V<VAR>t : Finset G<VAR>h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index K₂.carrier V<GOAL>index (K₁.carrier ∪ K₂.carrier) V ≤ (s ∪ t).card
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K₁.carrier V<VAR>t : Finset G<VAR>h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index K₂.carrier V<GOAL>(s ∪ t).card ∈ Finset.card '' {t | K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K₁.carrier V<VAR>t : Finset G<VAR>h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index K₂.carrier V<GOAL>s ∪ t ∈ {t | K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₁ K₂ : Compacts G<VAR>V : Set G<VAR>hV : (interior V).Nonempty<VAR>s : Finset G<VAR>h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V<VAR>h2s : s.card = index K₁.carrier V<VAR>t : Finset G<VAR>h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V<VAR>h2t : t.card = index K₂.carrier V<GOAL>K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s ∪ t, (fun h => g * h) ⁻¹' V
<VAR>E : Type u_1<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>f✝ : V → E<VAR>f : ℝ → E<VAR>hf : Integrable f volume<VAR>hf' : Integrable (fun x => x • f x) volume<VAR>x : ℝ<GOAL>deriv (𝓕 f) x = 𝓕 (fun x => (-2 * ↑π * I * ↑x) • f x) x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f p : R[X]<VAR>n : ℕ<VAR>ih : (p * X ^ n).reverse = p.reverse<GOAL>(p * X ^ (n + 1)).reverse = p.reverse
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>n : ℕ<VAR>h : n ∈ σ.cycleType<GOAL>2 ≤ n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>n : ℕ<VAR>h : ∃ a, (a.IsCycle ∧ ∀ a_1 ∈ a.support, a a_1 = σ a_1) ∧ a.support.card = n<GOAL>2 ≤ n
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ w✝ : Perm α<VAR>hc : w✝.IsCycle<GOAL>2 ≤ w✝.support.card
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>hscomp : IsCompact s<VAR>hAconv : Convex ℝ s<GOAL>closure ((convexHull ℝ) (extremePoints ℝ s)) = s
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>hscomp : IsCompact s<VAR>hAconv : Convex ℝ s<GOAL>s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>hscomp : IsCompact s<VAR>hAconv : Convex ℝ s<VAR>hs : ¬s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>hscomp : IsCompact s<VAR>hAconv : Convex ℝ s<VAR>hs : ¬s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))<VAR>x : E<VAR>hxA : x ∈ s<VAR>hxt : x ∉ closure ((convexHull ℝ) (extremePoints ℝ s))<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>hscomp : IsCompact s<VAR>hAconv : Convex ℝ s<VAR>hs : ¬s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))<VAR>x : E<VAR>hxA : x ∈ s<VAR>hxt : x ∉ closure ((convexHull ℝ) (extremePoints ℝ s))<VAR>l : E →L[ℝ] ℝ<VAR>r : ℝ<VAR>hlr : ∀ a ∈ closure ((convexHull ℝ) (extremePoints ℝ s)), l a < r<VAR>hrx : r < l x<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>hscomp : IsCompact s<VAR>hAconv : Convex ℝ s<VAR>hs : ¬s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))<VAR>x : E<VAR>hxA : x ∈ s<VAR>hxt : x ∉ closure ((convexHull ℝ) (extremePoints ℝ s))<VAR>l : E →L[ℝ] ℝ<VAR>r : ℝ<VAR>hlr : ∀ a ∈ closure ((convexHull ℝ) (extremePoints ℝ s)), l a < r<VAR>hrx : r < l x<VAR>h : IsExposed ℝ s {y | y ∈ s ∧ ∀ z ∈ s, l z ≤ l y}<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>hscomp : IsCompact s<VAR>hAconv : Convex ℝ s<VAR>hs : ¬s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))<VAR>x : E<VAR>hxA : x ∈ s<VAR>hxt : x ∉ closure ((convexHull ℝ) (extremePoints ℝ s))<VAR>l : E →L[ℝ] ℝ<VAR>r : ℝ<VAR>hlr : ∀ a ∈ closure ((convexHull ℝ) (extremePoints ℝ s)), l a < r<VAR>hrx : r < l x<VAR>h : IsExposed ℝ s {y | y ∈ s ∧ ∀ z ∈ s, l z ≤ l y}<VAR>z : E<VAR>hzA : z ∈ s<VAR>hz : IsMaxOn (⇑l) s z<GOAL>False
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : Module ℝ E<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : T2Space E<VAR>inst✝⁶ : TopologicalAddGroup E<VAR>inst✝⁵ : ContinuousSMul ℝ E<VAR>inst✝⁴ : LocallyConvexSpace ℝ E<VAR>s : Set E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module ℝ F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : T1Space F<VAR>hscomp : IsCompact s<VAR>hAconv : Convex ℝ s<VAR>hs : ¬s ⊆ closure ((convexHull ℝ) (extremePoints ℝ s))<VAR>x : E<VAR>hxA : x ∈ s<VAR>hxt : x ∉ closure ((convexHull ℝ) (extremePoints ℝ s))<VAR>l : E →L[ℝ] ℝ<VAR>r : ℝ<VAR>hlr : ∀ a ∈ closure ((convexHull ℝ) (extremePoints ℝ s)), l a < r<VAR>hrx : r < l x<VAR>h : IsExposed ℝ s {y | y ∈ s ∧ ∀ z ∈ s, l z ≤ l y}<VAR>z : E<VAR>hzA : z ∈ s<VAR>hz : IsMaxOn (⇑l) s z<VAR>y : E<VAR>hy : y ∈ extremePoints ℝ {y | y ∈ s ∧ ∀ z ∈ s, l z ≤ l y}<GOAL>False
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Mul M<VAR>s✝ : Set M<VAR>inst✝ : Add A<VAR>t : Set A<VAR>S : Subsemigroup M<VAR>p : M → Prop<VAR>x : M<VAR>s : Set M<VAR>hs : closure s = ⊤<VAR>mem : ∀ x ∈ s, p x<VAR>mul : ∀ (x y : M), p x → p y → p (x * y)<GOAL>p x
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : Mul M<VAR>s✝ : Set M<VAR>inst✝ : Add A<VAR>t : Set A<VAR>S : Subsemigroup M<VAR>p : M → Prop<VAR>x : M<VAR>s : Set M<VAR>hs : closure s = ⊤<VAR>mem : ∀ x ∈ s, p x<VAR>mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>this : ∀ x ∈ closure s, p x<GOAL>p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Finset α<VAR>a b : α<VAR>s : Finset α<GOAL>s.sym2.card = (s.card + 1).choose 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y✝ : E<VAR>r R : ℝ≥0<VAR>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<VAR>x y : E<GOAL>‖((p.changeOriginSeriesTerm k l s hs) fun x_1 => x) fun x => y‖₊ ≤ ‖p (k + l)‖₊ * ‖x‖₊ ^ l * ‖y‖₊ ^ k
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y✝ : E<VAR>r R : ℝ≥0<VAR>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<VAR>x y : E<GOAL>‖((p.changeOriginSeriesTerm k l s hs) fun x_1 => x) fun x => y‖₊ ≤ (‖p.changeOriginSeriesTerm k l s hs‖₊ * ∏ _i : Fin l, ‖x‖₊) * ∏ _i : Fin k, ‖y‖₊
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x✝ y✝ : E<VAR>r R : ℝ≥0<VAR>k l : ℕ<VAR>s : Finset (Fin (k + l))<VAR>hs : s.card = l<VAR>x y : E<GOAL>‖(p.changeOriginSeriesTerm k l s hs) fun x_1 => x‖₊ ≤ ‖p.changeOriginSeriesTerm k l s hs‖₊ * ∏ _i : Fin l, ‖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>inst✝¹² : Semiring R<VAR>inst✝¹¹ : Semiring R₂<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>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>p p' : Submodule R M<VAR>q q' : Submodule R₂ M₂<VAR>x : M<VAR>inst✝² : RingHomSurjective σ₁₂<VAR>F : Type u_9<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>f g : M →ₛₗ[σ₁₂] M₂<VAR>m : M<VAR>hm : m ∈ ↑p<GOAL>(f + g) m ∈ map f p ⊔ map g p
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableWithinAt I I' f s x<GOAL>HasMFDerivWithinAt I I' f s x (mfderivWithin I I' f s x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableWithinAt I I' f s x<GOAL>HasFDerivWithinAt (writtenInExtChartAt I I' x f) (mfderivWithin I I' f s x) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : MDifferentiableWithinAt I I' f s x<GOAL>HasFDerivWithinAt ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (fderivWithin 𝕜 ((↑I' ∘ ↑(chartAt H' (f x))) ∘ f ∘ ↑(chartAt H x).symm ∘ ↑I.symm) (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))) (↑(chartAt H x).symm ∘ ↑I.symm ⁻¹' s ∩ range ↑I) (↑I (↑(chartAt H x) x))
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<GOAL>‖x‖ ^ 2 = re (4⁻¹ * (𝓚 ‖x + x‖ * 𝓚 ‖x + x‖ - 𝓚 ‖x - x‖ * 𝓚 ‖x - x‖ + I * 𝓚 ‖I • x + x‖ * 𝓚 ‖I • x + x‖ - I * 𝓚 ‖I • x - x‖ * 𝓚 ‖I • x - x‖))
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>h₁ : normSq 4 = 16<GOAL>‖x‖ ^ 2 = re (4⁻¹ * (𝓚 ‖x + x‖ * 𝓚 ‖x + x‖ - 𝓚 ‖x - x‖ * 𝓚 ‖x - x‖ + I * 𝓚 ‖I • x + x‖ * 𝓚 ‖I • x + x‖ - I * 𝓚 ‖I • x - x‖ * 𝓚 ‖I • x - x‖))
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>h₁ : normSq 4 = 16<VAR>h₂ : ‖x + x‖ = 2 * ‖x‖<GOAL>‖x‖ ^ 2 = re (4⁻¹ * (𝓚 ‖x + x‖ * 𝓚 ‖x + x‖ - 𝓚 ‖x - x‖ * 𝓚 ‖x - x‖ + I * 𝓚 ‖I • x + x‖ * 𝓚 ‖I • x + x‖ - I * 𝓚 ‖I • x - x‖ * 𝓚 ‖I • x - x‖))
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>x : E<VAR>h₁ : normSq 4 = 16<VAR>h₂ : ‖x + x‖ = 2 * ‖x‖<GOAL>‖x‖ ^ 2 = 4 / 16 * (2 * ‖x‖ * (2 * ‖x‖) - 0 * 0 - 0 + ((0 * ‖I • x + x‖ - im I * 0) * ‖I • x + x‖ - (0 * 0 + im I * ‖I • x + x‖) * 0) - ((0 * ‖I • x - x‖ - im I * 0) * ‖I • x - x‖ - (0 * 0 + im I * ‖I • x - x‖) * 0)) - -0 / 16 * (2 * ‖x‖ * 0 + 0 * (2 * ‖x‖) - (0 * 0 + 0 * 0) + ((0 * ‖I • x + x‖ - im I * 0) * 0 + (0 * 0 + im I * ‖I • x + x‖) * ‖I • x + x‖) - ((0 * ‖I • x - x‖ - im I * 0) * 0 + (0 * 0 + im I * ‖I • x - x‖) * ‖I • x - x‖))
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>p : ℝ≥0∞<VAR>inst✝ : Finite α<VAR>f : (i : α) → E i<GOAL>Memℓp f p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>inst✝ : Finite α<VAR>f : (i : α) → E i<GOAL>Memℓp f 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>inst✝ : Finite α<VAR>f : (i : α) → E i<GOAL>Memℓp f ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>inst✝¹ : (i : α) → NormedAddCommGroup (E i)<VAR>p : ℝ≥0∞<VAR>inst✝ : Finite α<VAR>f : (i : α) → E i<VAR>_h : 0 < p.toReal<GOAL>Memℓp f p
<VAR>u v m n : ℤ<GOAL>Even (n - 1) ↔ ¬Even n
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<VAR>S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient<VAR>ff : Quotient S.toSetoid → α := ⇑f.lift<GOAL>∃ j g, f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<VAR>S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient<VAR>ff : Quotient S.toSetoid → α := ⇑f.lift<VAR>h✝ : IsEmpty (Quotient S.toSetoid)<GOAL>∃ j g, f = LocallyConstant.comap (C.π.app j) g
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>inst✝ : IsCofiltered J<VAR>F : J ⥤ Profinite<VAR>C : Cone F<VAR>α : Type u_1<VAR>hC : IsLimit C<VAR>f : LocallyConstant (↑C.pt.toTop) α<VAR>S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient<VAR>ff : Quotient S.toSetoid → α := ⇑f.lift<VAR>h✝ : Nonempty (Quotient S.toSetoid)<GOAL>∃ j g, f = LocallyConstant.comap (C.π.app j) g
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>X : Type u_3<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : SMul M X<VAR>ts : Set (TopologicalSpace X)<VAR>h : ∀ t ∈ ts, ContinuousSMul M X<GOAL>Continuous fun p => p.1 • p.2