ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁹ : PartialOrder Γ✝<VAR>inst✝⁸ : PartialOrder Γ'<VAR>inst✝⁷ : VAdd Γ✝ Γ'<VAR>inst✝⁶ : IsOrderedCancelVAdd Γ✝ Γ'<VAR>inst✝⁵ : AddCommMonoid V<VAR>Γ : Type u_5<VAR>inst✝⁴ : OrderedAddCommMonoid Γ<VAR>inst✝³ : AddAction Γ Γ'<VAR>inst✝² : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>r : R<VAR>x : HahnModule Γ' R V<VAR>a : Γ'<GOAL>((of R).symm ((HahnSeries.single 0) r • x)).coeff a = r • ((of R).symm x).coeff a
<VAR>Γ✝ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝⁹ : PartialOrder Γ✝<VAR>inst✝⁸ : PartialOrder Γ'<VAR>inst✝⁷ : VAdd Γ✝ Γ'<VAR>inst✝⁶ : IsOrderedCancelVAdd Γ✝ Γ'<VAR>inst✝⁵ : AddCommMonoid V<VAR>Γ : Type u_5<VAR>inst✝⁴ : OrderedAddCommMonoid Γ<VAR>inst✝³ : AddAction Γ Γ'<VAR>inst✝² : IsOrderedCancelVAdd Γ Γ'<VAR>inst✝¹ : MulZeroClass R<VAR>inst✝ : SMulWithZero R V<VAR>r : R<VAR>x : HahnModule Γ' R V<VAR>a : Γ'<GOAL>((of R).symm ((HahnSeries.single 0) r • x)).coeff (0 +ᵥ a) = r • ((of R).symm x).coeff a
<VAR>θ : Angle<VAR>h : ↑π = ↑(2 • (π / 2))<GOAL>2 • θ = ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
<VAR>θ : Angle<VAR>h : ↑π = ↑(2 • (π / 2))<GOAL>2 • θ = ↑(2 • (π / 2)) ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
<VAR>θ : Angle<VAR>h : ↑π = ↑(2 • (π / 2))<GOAL>θ = ↑(π / 2) ∨ θ = ↑(π / 2) + ↑π ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)
<VAR>θ : Angle<VAR>h : ↑π = ↑(2 • (π / 2))<GOAL>↑(-π / 2) = ↑(π / 2) + ↑π
<VAR>α : Type u_1<VAR>a : ZNum<GOAL>↑(0 * a) = ↑0 * ↑a
<VAR>α : Type u_1<VAR>b : ZNum<GOAL>↑(b * 0) = ↑b * ↑0
<VAR>α : Type u_1<VAR>a b : PosNum<GOAL>-↑(a * b) = ↑a * -↑b
<VAR>α : Type u_1<VAR>a b : PosNum<GOAL>-↑(a * b) = -↑a * ↑b
<VAR>α : Type u_1<VAR>a b : PosNum<GOAL>↑(a * b) = -↑a * -↑b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>x : E<VAR>r : ℝ<VAR>y : E<GOAL>y ∈ c • ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>x : E<VAR>r : ℝ<VAR>y : E<GOAL>c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>x : E<VAR>r : ℝ<VAR>y : E<GOAL>c⁻¹ • y ∈ ball (c⁻¹ • c • x) r ↔ y ∈ ball (c • x) (‖c‖ * r)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<GOAL>ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal} ≤ eLpNorm f p μ ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>this : 1 / p.toReal * p.toReal = 1<GOAL>ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal} ≤ eLpNorm f p μ ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>this : 1 / p.toReal * p.toReal = 1<GOAL>((ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal}) ^ (1 / p.toReal)) ^ p.toReal ≤ eLpNorm f p μ ^ p.toReal
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>f : α → E<VAR>hp_ne_zero : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>hf : AEStronglyMeasurable f μ<VAR>ε : ℝ≥0∞<VAR>this : 1 / p.toReal * p.toReal = 1<GOAL>(ε * μ {x | ε ≤ ↑‖f x‖₊ ^ p.toReal}) ^ (1 / p.toReal) ≤ eLpNorm f p μ
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>closedBall x ε = ∅ ↔ ε < 0
<VAR>q✝ q : ℚ<VAR>n : ℕ<GOAL>q ^ n = q.num ^ n /. ↑q.den ^ n
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>f : G ≃ₜ G<VAR>h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(μ.toFun s)) (Compacts.map ⇑f ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>U : Opens G<GOAL>μ.innerContent ((Opens.comap f.toContinuousMap) U) = μ.innerContent U
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>f : G ≃ₜ G<VAR>h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(μ.toFun s)) (Compacts.map ⇑f ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>U : Opens G<VAR>K : Compacts G<GOAL>↑K ⊆ ↑((Opens.comap f.toContinuousMap) U) → (fun s => ↑(μ.toFun s)) ((Compacts.equiv f) K) = (fun s => ↑(μ.toFun s)) K
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>f : G ≃ₜ G<VAR>h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(μ.toFun s)) (Compacts.map ⇑f ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>U : Opens G<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑((Opens.comap f.toContinuousMap) U)<GOAL>(fun s => ↑(μ.toFun s)) ((Compacts.equiv f) K) = (fun s => ↑(μ.toFun s)) K
<VAR>G : Type w<VAR>inst✝ : TopologicalSpace G<VAR>μ : Content G<VAR>f : G ≃ₜ G<VAR>h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(μ.toFun s)) (Compacts.map ⇑f ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>U : Opens G<VAR>K : Compacts G<VAR>hK : ↑K ⊆ ↑((Opens.comap f.toContinuousMap) U)<GOAL>↑(μ.toFun (Compacts.map ⇑f ⋯ K)) = ↑(μ.toFun K)
<VAR>x : ℂ<VAR>n : ℕ<VAR>hx : abs x / ↑n.succ ≤ 1 / 2<GOAL>abs (cexp x - ∑ m ∈ range n, x ^ m / ↑m.factorial) ≤ abs x ^ n / ↑n.factorial * 2
<VAR>x : ℂ<VAR>n : ℕ<VAR>hx : abs x / ↑n.succ ≤ 1 / 2<GOAL>(cauSeqAbs (exp' x + -const (⇑abs) (∑ m ∈ range n, x ^ m / ↑m.factorial))).lim ≤ abs x ^ n / ↑n.factorial * 2
<VAR>x : ℂ<VAR>n : ℕ<VAR>hx : abs x / ↑n.succ ≤ 1 / 2<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>↑(cauSeqAbs (exp' x + -const (⇑abs) (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤ ↑(const _root_.abs (abs x ^ n / ↑n.factorial * 2)) j
<VAR>x : ℂ<VAR>n : ℕ<VAR>hx : abs x / ↑n.succ ≤ 1 / 2<VAR>j : ℕ<VAR>hj : j ≥ n<GOAL>↑(cauSeqAbs (exp' x - const (⇑abs) (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤ ↑(const _root_.abs (abs x ^ n / ↑n.factorial * 2)) j
<VAR>x : ℂ<VAR>n : ℕ<VAR>hx : abs x / ↑n.succ ≤ 1 / 2<VAR>j : ℕ<VAR>hj : j ≥ n<VAR>k : ℕ := j - n<GOAL>abs (∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial) ≤ abs x ^ n / ↑n.factorial * 2
<VAR>x : ℂ<VAR>n : ℕ<VAR>hx : abs x / ↑n.succ ≤ 1 / 2<VAR>j : ℕ<VAR>hj✝ : j ≥ n<VAR>k : ℕ := j - n<VAR>hj : j = n + k<GOAL>abs (∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial) ≤ abs x ^ n / ↑n.factorial * 2
<VAR>x : ℂ<VAR>n : ℕ<VAR>hx : abs x / ↑n.succ ≤ 1 / 2<VAR>j : ℕ<VAR>hj✝ : j ≥ n<VAR>k : ℕ := j - n<VAR>hj : j = n + k<GOAL>abs (∑ k ∈ range k, x ^ (n + k) / ↑(n + k).factorial) ≤ abs x ^ n / ↑n.factorial * 2
<VAR>x : ℂ<VAR>n : ℕ<VAR>hx : abs x / ↑n.succ ≤ 1 / 2<VAR>j : ℕ<VAR>hj✝ : j ≥ n<VAR>k : ℕ := j - n<VAR>hj : j = n + k<GOAL>∑ i ∈ range k, abs x ^ (n + i) / ↑(n + i).factorial ≤ ∑ i ∈ range k, abs x ^ (n + i) / (↑n.factorial * ↑n.succ ^ i)
<VAR>x : ℂ<VAR>n : ℕ<VAR>hx : abs x / ↑n.succ ≤ 1 / 2<VAR>j : ℕ<VAR>hj✝ : j ≥ n<VAR>k : ℕ := j - n<VAR>hj : j = n + k<GOAL>∑ i ∈ range k, abs x ^ (n + i) / (↑n.factorial * ↑n.succ ^ i) = ∑ i ∈ range k, abs x ^ n / ↑n.factorial * (abs x ^ i / ↑n.succ ^ i)
<VAR>x : ℂ<VAR>n : ℕ<VAR>hx : abs x / ↑n.succ ≤ 1 / 2<VAR>j : ℕ<VAR>hj✝ : j ≥ n<VAR>k : ℕ := j - n<VAR>hj : j = n + k<GOAL>∑ i ∈ range k, abs x ^ n / ↑n.factorial * (abs x ^ i / ↑n.succ ^ i) ≤ abs x ^ n / ↑n.factorial * 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>p : α × β → Prop<GOAL>(∃ x ∈ s ×ˢ t, p x) ↔ ∃ x ∈ s, ∃ y ∈ t, p (x, y)
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>DifferentiableAt ℂ jacobiTheta τ
<VAR>τ : ℂ<VAR>hτ : 0 < τ.im<GOAL>DifferentiableAt ℂ (jacobiTheta₂ 0) τ
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Mon_ C<GOAL>((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ M.X).hom = M.one
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{u_9, u_1} C<VAR>inst✝⁸ : Category.{?u.43767, u_2} C₁<VAR>inst✝⁷ : Category.{?u.43771, u_3} C₂<VAR>inst✝⁶ : Category.{?u.43775, u_4} C₃<VAR>inst✝⁵ : Category.{u_8, u_5} D₁<VAR>inst✝⁴ : Category.{u_11, u_6} D₂<VAR>inst✝³ : Category.{u_10, u_7} D₃<VAR>W : MorphismProperty C<VAR>L₁ : C ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W<VAR>L₂ : C ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W<VAR>L₃ : C ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W<VAR>X Y Z : C<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>(homEquiv W L₂ L₃) ((homEquiv W L₁ L₂) f) = (homEquiv W L₁ L₃) f
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{u_9, u_1} C<VAR>inst✝⁸ : Category.{?u.43767, u_2} C₁<VAR>inst✝⁷ : Category.{?u.43771, u_3} C₂<VAR>inst✝⁶ : Category.{?u.43775, u_4} C₃<VAR>inst✝⁵ : Category.{u_8, u_5} D₁<VAR>inst✝⁴ : Category.{u_11, u_6} D₂<VAR>inst✝³ : Category.{u_10, u_7} D₃<VAR>W : MorphismProperty C<VAR>L₁ : C ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W<VAR>L₂ : C ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W<VAR>L₃ : C ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W<VAR>X Y Z : C<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>(LocalizerMorphism.id W).homMap L₂ L₃ ((LocalizerMorphism.id W).homMap L₁ L₂ f) = (LocalizerMorphism.id W).homMap L₁ L₃ f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>inst✝¹ : IsIso f<VAR>inst✝ : IsIso h<GOAL>inv (f ≫ h) = inv h ≫ inv f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<VAR>inst✝¹ : IsIso f<VAR>inst✝ : IsIso h<GOAL>(f ≫ h) ≫ inv h ≫ inv f = 𝟙 X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : CompleteLattice α<VAR>f : (i : ι) → κ i → α<GOAL>Ici (⨆ i, ⨆ j, f i j) = ⋂ i, ⋂ j, Ici (f i j)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>h : IsComplete ↑K<VAR>this✝ : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E<VAR>this : Module ℝ E := RestrictScalars.module ℝ 𝕜 E<VAR>K' : Submodule ℝ E := Submodule.restrictScalars ℝ K<GOAL>∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>x✝ : R<GOAL>x✝ ∈ M.subsemiringClosure ↔ x✝ ∈ Subsemiring.closure ↑M
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>x✝ : R<VAR>hx : x✝ ∈ M.subsemiringClosure<VAR>H1 : Subsemiring R<VAR>H2 : H1 ∈ {S | ↑M ⊆ ↑S}<GOAL>x✝ ∈ (fun h => ↑H1) H2
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : NonAssocSemiring R<VAR>M : Submonoid R<VAR>inst✝¹ : NonAssocSemiring S<VAR>inst✝ : NonAssocSemiring T<VAR>x✝ : R<VAR>hx : x✝ ∈ Subsemiring.closure ↑M<VAR>s : R<VAR>sM : s ∈ ↑M<VAR>H1 : AddSubmonoid R<VAR>H2 : H1 ∈ {S | ↑M ⊆ ↑S}<GOAL>s ∈ (fun h => ↑H1) H2
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>h : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => -f x) (-f') x
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LE α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a⁻¹ ≤ b⁻¹ ↔ b ≤ a
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LE α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a * a⁻¹ * b ≤ a * b⁻¹ * b ↔ b ≤ a
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s₁ : Set X<VAR>s₂ : Set Y<VAR>h₁ : IsClosed s₁<VAR>h₂ : IsClosed s₂<GOAL>closure (s₁ ×ˢ s₂) = s₁ ×ˢ s₂
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>projectiveSeminorm ∈ upperBounds {p | ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>∀ x ∈ {p | ∃ G x x_1, p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)}, x ≤ projectiveSeminorm
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<GOAL>∀ (x : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)) (x_1 : Type (max uι u𝕜 uE)) (x_2 : SeminormedAddCommGroup x_1) (x_3 : NormedSpace 𝕜 x_1), x = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E x_1 →L[𝕜] x_1)).comp (toDualContinuousMultilinearMap x_1) → x ≤ projectiveSeminorm
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)<VAR>G : Type (max uι u𝕜 uE)<VAR>x✝¹ : SeminormedAddCommGroup G<VAR>x✝ : NormedSpace 𝕜 G<VAR>hp : p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>(fun f => ⇑f) ((normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)) x ≤ (fun f => ⇑f) projectiveSeminorm x
<VAR>ι : Type uι<VAR>inst✝⁵ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝¹ : SeminormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>p : Seminorm 𝕜 (⨂[𝕜] (i : ι), E i)<VAR>G : Type (max uι u𝕜 uE)<VAR>x✝¹ : SeminormedAddCommGroup G<VAR>x✝ : NormedSpace 𝕜 G<VAR>hp : p = (normSeminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G →L[𝕜] G)).comp (toDualContinuousMultilinearMap G)<VAR>x : ⨂[𝕜] (i : ι), E i<GOAL>‖(toDualContinuousMultilinearMap G) x‖ ≤ projectiveSeminorm x
<VAR>F : Type u_1<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module ℝ F<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ContinuousSMul ℝ F<VAR>E : Submodule ℝ F<VAR>hcodim : 1 < Module.rank ℝ (F ⧸ E)<GOAL>IsPathConnected (↑E)ᶜ
<VAR>F : Type u_1<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module ℝ F<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ContinuousSMul ℝ F<VAR>E : Submodule ℝ F<VAR>hcodim : 1 < Module.rank ℝ (F ⧸ E)<VAR>E' : Submodule ℝ F<VAR>hE' : IsCompl E E'<GOAL>IsPathConnected (↑E)ᶜ
<VAR>F : Type u_1<VAR>inst✝⁴ : AddCommGroup F<VAR>inst✝³ : Module ℝ F<VAR>inst✝² : TopologicalSpace F<VAR>inst✝¹ : TopologicalAddGroup F<VAR>inst✝ : ContinuousSMul ℝ F<VAR>E : Submodule ℝ F<VAR>hcodim : 1 < Module.rank ℝ (F ⧸ E)<VAR>E' : Submodule ℝ F<VAR>hE' : IsCompl E E'<GOAL>1 < Module.rank ℝ ↥E'
<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>a b : M<VAR>h : QuadraticMap.IsOrtho Q a b<GOAL>(ι Q) a * (ι Q) b + (ι Q) b * (ι Q) a = 0
<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>a b : M<VAR>h : QuadraticMap.IsOrtho Q a b<GOAL>(algebraMap R (CliffordAlgebra Q)) 0 = 0
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>‖f x - g x‖ ≤ ‖f - g‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Set α → Filter β<VAR>hm : Monotone g<GOAL>(f.lift g).NeBot ↔ ∀ s ∈ f, (g s).NeBot
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>ι : Type u_1<VAR>U : ι → Opens ↑Y<GOAL>↑((map f).obj (iSup U)) = ↑(iSup ((map f).obj ∘ U))
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>ι : Type u_1<VAR>U : ι → Opens ↑Y<GOAL>↑{ carrier := ⇑f ⁻¹' ⋃ i, ↑(U i), is_open' := ⋯ } = ↑{ carrier := ⋃ i, ↑(((map f).obj ∘ U) i), is_open' := ⋯ }
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>ι : Type u_1<VAR>U : ι → Opens ↑Y<GOAL>⇑f ⁻¹' ⋃ i, ↑(U i) = ⋃ i, ⇑f ⁻¹' ↑(U i)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h✝ : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>h : p /ₘ (X - C x) = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h✝ : ∃ x, p.IsRoot x<VAR>x : R<VAR>hp : 0 ≠ 0<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>h : p /ₘ (X - C x) = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : (p /ₘ (X - C x)).degree < p.degree<VAR>t : Multiset R<VAR>htd : ↑(Multiset.card t) ≤ (p /ₘ (X - C x)).degree<VAR>htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))<GOAL>(X - C x).degree ≤ p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : (p /ₘ (X - C x)).degree < p.degree<VAR>t : Multiset R<VAR>htd : ↑(Multiset.card t) ≤ (p /ₘ (X - C x)).degree<VAR>htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))<GOAL>1 ≤ ↑p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < ↑p.natDegree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : (p /ₘ (X - C x)).degree < p.degree<VAR>t : Multiset R<VAR>htd : ↑(Multiset.card t) ≤ (p /ₘ (X - C x)).degree<VAR>htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))<GOAL>1 ≤ ↑p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : (p /ₘ (X - C x)).degree < p.degree<VAR>t : Multiset R<VAR>htd : ↑(Multiset.card t) ≤ (p /ₘ (X - C x)).degree<VAR>htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))<VAR>hdeg : (X - C x).degree ≤ p.degree<VAR>hdiv0 : p /ₘ (X - C x) ≠ 0<GOAL>Multiset.card (x ::ₘ t) = Add.add (↑(Multiset.card t)) 1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : (p /ₘ (X - C x)).degree < p.degree<VAR>t : Multiset R<VAR>htd : ↑(Multiset.card t) ≤ (p /ₘ (X - C x)).degree<VAR>htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))<VAR>hdeg : (X - C x).degree ≤ p.degree<VAR>hdiv0 : p /ₘ (X - C x) ≠ 0<GOAL>↑(Multiset.card t) + 1 ≤ p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : (p /ₘ (X - C x)).degree < p.degree<VAR>t : Multiset R<VAR>htd : ↑(Multiset.card t) ≤ (p /ₘ (X - C x)).degree<VAR>htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))<VAR>hdeg : (X - C x).degree ≤ p.degree<VAR>hdiv0 : p /ₘ (X - C x) ≠ 0<GOAL>1 + ↑(Multiset.card t) ≤ 1 + (p /ₘ (X - C x)).degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : (p /ₘ (X - C x)).degree < p.degree<VAR>t : Multiset R<VAR>htd : ↑(Multiset.card t) ≤ (p /ₘ (X - C x)).degree<VAR>htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))<VAR>hdeg : (X - C x).degree ≤ p.degree<VAR>hdiv0 : p /ₘ (X - C x) ≠ 0<VAR>a : R<GOAL>count a (x ::ₘ t) = rootMultiplicity a p
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : (p /ₘ (X - C x)).degree < p.degree<VAR>t : Multiset R<VAR>htd : ↑(Multiset.card t) ≤ (p /ₘ (X - C x)).degree<VAR>htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))<VAR>hdeg : (X - C x).degree ≤ p.degree<VAR>hdiv0 : p /ₘ (X - C x) ≠ 0<VAR>a : R<GOAL>count a (x ::ₘ t) = rootMultiplicity a ((X - C x) * (p /ₘ (X - C x)))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h : ∃ x, p.IsRoot x<VAR>x : R<VAR>hx : p.IsRoot x<VAR>hpd : 0 < p.degree<VAR>hd0 : p /ₘ (X - C x) ≠ 0<VAR>wf : (p /ₘ (X - C x)).degree < p.degree<VAR>t : Multiset R<VAR>htd : ↑(Multiset.card t) ≤ (p /ₘ (X - C x)).degree<VAR>htr : ∀ (a : R), count a t = rootMultiplicity a (p /ₘ (X - C x))<VAR>hdeg : (X - C x).degree ≤ p.degree<VAR>hdiv0 : p /ₘ (X - C x) ≠ 0<VAR>a : R<GOAL>count a (x ::ₘ t) = (if a = x then 1 else 0) + count a t
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>hp : p ≠ 0<VAR>this : Decidable (∃ x, p.IsRoot x)<VAR>h : ¬∃ x, p.IsRoot x<VAR>a : R<GOAL>count a 0 = rootMultiplicity a p