ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι✝ : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>ι : Sort u_4<VAR>inst✝ : Countable ι<VAR>s : ι → Set X<VAR>this✝¹ : MeasurableSpace X := borel X<VAR>this✝ : BorelSpace X<VAR>d : ℝ≥0<VAR>hd : ⨆ i, dimH (s i) < ↑d<VAR>this : ∀ (i : ι), μH[↑d] (s i) = 0<GOAL>0 ≠ ⊤
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f' : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<GOAL>∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f' : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>Λ' : F × ℝ →ₗ[ℝ] ℝ<VAR>h0 : Λ' ≠ 0<VAR>hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker Λ'<GOAL>∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f' : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>Λ' : F × ℝ →ₗ[ℝ] ℝ<VAR>h0 : Λ' ≠ 0<VAR>hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker Λ'<VAR>e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ := (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ<GOAL>∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f' : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ := (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ<VAR>Λ : F →ₗ[ℝ] ℝ<VAR>Λ₀ : ℝ<VAR>h0 : e (Λ, Λ₀) ≠ 0<VAR>hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker (e (Λ, Λ₀))<GOAL>∃ Λ Λ₀, (Λ, Λ₀) ≠ 0 ∧ ∀ (x : E), Λ (f' x) + Λ₀ • φ' x = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f' : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ := (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ<VAR>Λ : F →ₗ[ℝ] ℝ<VAR>Λ₀ : ℝ<VAR>h0 : e (Λ, Λ₀) ≠ 0<VAR>hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker (e (Λ, Λ₀))<VAR>x : E<GOAL>Λ (f' x) + Λ₀ • φ' x = 0
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>φ : E → ℝ<VAR>x₀ : E<VAR>f' : E →L[ℝ] F<VAR>φ' : E →L[ℝ] ℝ<VAR>hextr : IsLocalExtrOn φ {x | f x = f x₀} x₀<VAR>hf' : HasStrictFDerivAt f f' x₀<VAR>hφ' : HasStrictFDerivAt φ φ' x₀<VAR>e : ((F →ₗ[ℝ] ℝ) × ℝ) ≃ₗ[ℝ] F × ℝ →ₗ[ℝ] ℝ := (LinearEquiv.refl ℝ (F →ₗ[ℝ] ℝ)).prod (LinearMap.ringLmapEquivSelf ℝ ℝ ℝ).symm ≪≫ₗ LinearMap.coprodEquiv ℝ<VAR>Λ : F →ₗ[ℝ] ℝ<VAR>Λ₀ : ℝ<VAR>h0 : e (Λ, Λ₀) ≠ 0<VAR>hΛ' : LinearMap.range (f'.prod φ') ≤ LinearMap.ker (e (Λ, Λ₀))<VAR>x : E<GOAL>Λ (f' x) + Λ₀ • φ' x = (e (Λ, Λ₀) ∘ₗ ↑(f'.prod φ')) x
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>h₁ : S.LeftHomologyData<VAR>h₂ : S.RightHomologyData<GOAL>h₁.π ≫ leftRightHomologyComparison' h₁ h₂ ≫ h₂.ι = h₁.i ≫ h₂.p
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → p a<GOAL>pmap f l H = [] ↔ l = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u v : α → β<VAR>h₁ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₂ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>h₃ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₄ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<GOAL>limsup (fun a => max (u a) (v a)) f = max (limsup u f) (limsup v f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u v : α → β<VAR>h₁ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₂ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>h₃ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₄ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>bddmax : IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => u a ⊔ v a<GOAL>limsup (fun a => max (u a) (v a)) f = max (limsup u f) (limsup v f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u v : α → β<VAR>h₁ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₂ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>h₃ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₄ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>bddmax : IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => u a ⊔ v a<VAR>cobddmax : IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun a => max (u a) (v a)<GOAL>limsup (fun a => max (u a) (v a)) f = max (limsup u f) (limsup v f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u v : α → β<VAR>h₁ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₂ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>h₃ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₄ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>bddmax : IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => u a ⊔ v a<VAR>cobddmax : IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun a => max (u a) (v a)<GOAL>limsup (fun a => max (u a) (v a)) f ≤ max (limsup u f) (limsup v f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : ConditionallyCompleteLinearOrder β<VAR>f : Filter α<VAR>u v : α → β<VAR>h₁ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₂ : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>h₃ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝<VAR>h₄ : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝<VAR>bddmax : IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun a => u a ⊔ v a<VAR>cobddmax : IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun a => max (u a) (v a)<GOAL>max (limsup u f) (limsup v f) ≤ limsup (fun a => max (u a) (v a)) f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<GOAL>SurjOn f ∅ t ↔ t = ∅
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>h_left : IntegrableOn f (Iio b) μ<VAR>h_right : IntegrableOn f (Ici b) μ<GOAL>∫ (x : ℝ) in Iio b, f x ∂μ + ∫ (x : ℝ) in Ici b, f x ∂μ = ∫ (x : ℝ), f x ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>h_left : IntegrableOn f (Iio b) μ<VAR>h_right : IntegrableOn f (Ici b) μ<GOAL>μ = μ.restrict (Iio b ∪ Ici b)
<VAR>x y z✝ : ℝ<VAR>n✝ : ℕ<VAR>hx : 0 ≤ x<VAR>n : ℕ<VAR>z : ℝ<GOAL>x ^ (↑n * z) = (x ^ n) ^ z
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : α ≃ₜ β<GOAL>∀ {a b : Opens α}, { toFun := ⇑(comap f.symm.toContinuousMap), invFun := ⇑(comap f.toContinuousMap), left_inv := ⋯, right_inv := ⋯ } a ≤ { toFun := ⇑(comap f.symm.toContinuousMap), invFun := ⇑(comap f.toContinuousMap), left_inv := ⋯, right_inv := ⋯ } b ↔ a ≤ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : α ≃ₜ β<GOAL>∀ {a b : Opens α}, ↑({ toFun := ⇑(comap f.symm.toContinuousMap), invFun := ⇑(comap f.toContinuousMap), left_inv := ⋯, right_inv := ⋯ } a) ⊆ ↑({ toFun := ⇑(comap f.symm.toContinuousMap), invFun := ⇑(comap f.toContinuousMap), left_inv := ⋯, right_inv := ⋯ } b) ↔ ↑a ⊆ ↑b
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R✝<VAR>inst✝⁹ : NonUnitalRing A✝<VAR>inst✝⁸ : Module R✝ A✝<VAR>inst✝⁷ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁶ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : Semifield R<VAR>inst✝⁴ : Semifield S<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>hf : Function.LeftInverse f ⇑(algebraMap R S)<VAR>h : spectrum S a ⊆ Set.range ⇑(algebraMap R S)<VAR>s : S<VAR>hs : s ∈ quasispectrum S a<GOAL>(algebraMap R S) (f s) = s
<VAR>R✝ : Type u_1<VAR>A✝ : Type u_2<VAR>inst✝¹⁰ : CommSemiring R✝<VAR>inst✝⁹ : NonUnitalRing A✝<VAR>inst✝⁸ : Module R✝ A✝<VAR>inst✝⁷ : IsScalarTower R✝ A✝ A✝<VAR>inst✝⁶ : SMulCommClass R✝ A✝ A✝<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A : Type u_5<VAR>inst✝⁵ : Semifield R<VAR>inst✝⁴ : Semifield S<VAR>inst✝³ : Ring A<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra S A<VAR>a : A<VAR>f : S → R<VAR>hf : Function.LeftInverse f ⇑(algebraMap R S)<VAR>h : spectrum S a ⊆ Set.range ⇑(algebraMap R S)<VAR>s : S<VAR>hs : s = 0 ∨ s ∈ spectrum S a<GOAL>(algebraMap R S) (f s) = s
<VAR>α : Type u_1<VAR>p q : α → Bool<VAR>l : List α<GOAL>0 < countP p l ↔ ∃ a, a ∈ l ∧ p a = true
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x z : M<VAR>v : E<VAR>h : z ∈ (extChartAt I x).source<GOAL>(tangentCoordChange I x x z) v = v
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x z : M<VAR>v : E<VAR>h : z ∈ (extChartAt I x).source<GOAL>z ∈ (tangentBundleCore I M).baseSet (achart H x)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>x z : M<VAR>v : E<VAR>h : z ∈ (extChartAt I x).source<GOAL>z ∈ (extChartAt I x).source
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q✝ r : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>h : ¬q = 0<GOAL>(p * q).degree = (q * p).degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q✝ r : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>h : ¬q = 0<GOAL>p.degree + q.degree = q.degree + p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q✝ r : R[X]<VAR>hp : p.Monic<VAR>q : R[X]<VAR>h : ¬q = 0<GOAL>p.leadingCoeff * q.leadingCoeff ≠ 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.632038<VAR>Bₘ : Type ?u.632041<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this : IsIntegralClosure B A (FractionRing B)<GOAL>(intNorm A B) x = 0 ↔ x = 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.632038<VAR>Bₘ : Type ?u.632041<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝ : IsIntegralClosure B A (FractionRing B)<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<GOAL>(intNorm A B) x = 0 ↔ x = 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.632038<VAR>Bₘ : Type ?u.632041<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝¹ : IsIntegralClosure B A (FractionRing B)<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>(intNorm A B) x = 0 ↔ x = 0
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³¹ : CommRing A<VAR>inst✝³⁰ : CommRing B<VAR>inst✝²⁹ : Algebra A B<VAR>inst✝²⁸ : Field K<VAR>inst✝²⁷ : Field L<VAR>inst✝²⁶ : Algebra A K<VAR>inst✝²⁵ : IsFractionRing A K<VAR>inst✝²⁴ : Algebra B L<VAR>inst✝²³ : Algebra K L<VAR>inst✝²² : Algebra A L<VAR>inst✝²¹ : IsScalarTower A B L<VAR>inst✝²⁰ : IsScalarTower A K L<VAR>inst✝¹⁹ : IsIntegralClosure B A L<VAR>inst✝¹⁸ : FiniteDimensional K L<VAR>Aₘ : Type ?u.632038<VAR>Bₘ : Type ?u.632041<VAR>inst✝¹⁷ : CommRing Aₘ<VAR>inst✝¹⁶ : CommRing Bₘ<VAR>inst✝¹⁵ : Algebra Aₘ Bₘ<VAR>inst✝¹⁴ : Algebra A Aₘ<VAR>inst✝¹³ : Algebra B Bₘ<VAR>inst✝¹² : Algebra A Bₘ<VAR>inst✝¹¹ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁰ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝⁹ : IsLocalization M Aₘ<VAR>inst✝⁸ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁷ : IsIntegrallyClosed A<VAR>inst✝⁶ : IsDomain A<VAR>inst✝⁵ : IsIntegrallyClosed A<VAR>inst✝⁴ : IsDomain B<VAR>inst✝³ : IsIntegrallyClosed B<VAR>inst✝² : Module.Finite A B<VAR>inst✝¹ : NoZeroSMulDivisors A B<VAR>inst✝ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>x : B<VAR>this✝¹ : IsIntegralClosure B A (FractionRing B)<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>(algebraMap A (FractionRing A)) ((intNorm A B) x) = (algebraMap A (FractionRing A)) 0 ↔ (algebraMap B (FractionRing B)) x = (algebraMap B (FractionRing B)) 0
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<GOAL>∃ n, Disjoint s (cylinder x n)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>x : (n : ℕ) → E n<VAR>hs : IsClosed ∅<VAR>hx : x ∉ ∅<GOAL>∃ n, Disjoint ∅ (cylinder x n)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hne : s.Nonempty<GOAL>∃ n, Disjoint s (cylinder x n)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hne : s.Nonempty<VAR>A : 0 < infDist x s<GOAL>∃ n, Disjoint s (cylinder x n)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hne : s.Nonempty<VAR>A : 0 < infDist x s<VAR>n : ℕ<VAR>hn : (1 / 2) ^ n < infDist x s<GOAL>∃ n, Disjoint s (cylinder x n)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hne : s.Nonempty<VAR>A : 0 < infDist x s<VAR>n : ℕ<VAR>hn : (1 / 2) ^ n < infDist x s<VAR>y : (n : ℕ) → E n<VAR>ys : y ∈ s<VAR>hy : y ∈ cylinder x n<GOAL>False
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>s : Set ((n : ℕ) → E n)<VAR>hs : IsClosed s<VAR>x : (n : ℕ) → E n<VAR>hx : x ∉ s<VAR>hne : s.Nonempty<VAR>A : 0 < infDist x s<VAR>n : ℕ<VAR>hn : (1 / 2) ^ n < infDist x s<VAR>y : (n : ℕ) → E n<VAR>ys : y ∈ s<VAR>hy : y ∈ cylinder x n<GOAL>infDist x s < infDist x s
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>x✝ : IsCoprime 0 x<VAR>a b : R<VAR>H : a * 0 + b * x = 1<GOAL>x * b = 1
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H : IsUnit x<VAR>b : R<VAR>hb : b * x = 1<GOAL>1 * 0 + b * x = 1
<VAR>R : Type u_1<VAR>inst✝² : Semiring R<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Semiring T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>r : R<VAR>n✝ : ℕ<GOAL>(coeff S n✝) ((map f) ((C R) r)) = (coeff S n✝) ((C S) (f r))
<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>f : E →ᴬ[ℝ] F<VAR>hs : IsCompact s<VAR>w : F<VAR>hw : w ∈ extremePoints ℝ (⇑f '' s)<GOAL>w ∈ ⇑f '' 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>f : E →ᴬ[ℝ] F<VAR>hs : IsCompact s<VAR>w : F<VAR>hw : w ∈ extremePoints ℝ (⇑f '' s)<VAR>ht : IsCompact {x | x ∈ s ∧ f x = w}<GOAL>w ∈ ⇑f '' 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>f : E →ᴬ[ℝ] F<VAR>hs : IsCompact s<VAR>w : F<VAR>hw : w ∈ extremePoints ℝ (⇑f '' s)<VAR>ht : IsCompact {x | x ∈ s ∧ f x = w}<VAR>ht₀ : {x | x ∈ s ∧ f x = w}.Nonempty<GOAL>w ∈ ⇑f '' extremePoints ℝ s