ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>hp0 : p ≠ 0<VAR>h0q : 0 < q.degree<VAR>hpq : p.degree < q.degree<VAR>this : Nontrivial R<GOAL>degree 0 < ↑p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>hp0 : p ≠ 0<VAR>h0q : 0 < q.degree<VAR>hpq : ¬p.degree < q.degree<GOAL>(p /ₘ q).degree < p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>hp0 : p ≠ 0<VAR>h0q : 0 < q.degree<VAR>hpq : ¬p.degree < q.degree<VAR>this : Nontrivial R<GOAL>(p /ₘ q).degree < p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<VAR>hq : q.Monic<VAR>hp0 : p ≠ 0<VAR>h0q : 0 < q.degree<VAR>hpq : ¬p.degree < q.degree<VAR>this : Nontrivial R<GOAL>↑(p /ₘ q).natDegree < ↑q.natDegree + ↑(p /ₘ q).natDegree
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y z : E<GOAL>⟪x, y - z⟫_𝕜 = ⟪x, y⟫_𝕜 - ⟪x, z⟫_𝕜
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s : Set α<VAR>p : α → Prop<VAR>a✝ : α<VAR>inst✝ : NoMinOrder α<VAR>hs : IsLowerSet s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ lowerBounds s<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s : Set α<VAR>p : α → Prop<VAR>a✝ : α<VAR>inst✝ : NoMinOrder α<VAR>hs : IsLowerSet s<VAR>a : α<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ lowerBounds s<VAR>c : α<VAR>hc : c < b<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : PseudoMetricSpace α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<GOAL>∃ f, StrictMono f ∧ Summable fun i => dist (u (f (i + 1))) (u (f i))
<VAR>α : Type u_1<VAR>inst✝ : PseudoMetricSpace α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>f : ℕ → ℕ<VAR>hf₁ : StrictMono f<VAR>hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n<GOAL>∃ f, StrictMono f ∧ Summable fun i => dist (u (f (i + 1))) (u (f i))
<VAR>α : Type u_1<VAR>inst✝ : PseudoMetricSpace α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>f : ℕ → ℕ<VAR>hf₁ : StrictMono f<VAR>hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n<GOAL>Summable fun i => dist (u (f (i + 1))) (u (f i))
<VAR>α : Type u_1<VAR>inst✝ : PseudoMetricSpace α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>f : ℕ → ℕ<VAR>hf₁ : StrictMono f<VAR>hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n<GOAL>∀ (b : ℕ), dist (u (f (b + 1))) (u (f b)) ≤ (1 / 2) ^ b
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>α : E<VAR>hα : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)<VAR>this : Fintype (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯) := IntermediateField.fintypeOfAlgHomAdjoinIntegral F hα<GOAL>Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = finrank F ↥F⟮α⟯
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>α : E<VAR>hα : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)<VAR>this : Fintype (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯) := IntermediateField.fintypeOfAlgHomAdjoinIntegral F hα<GOAL>Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = (minpoly F α).natDegree
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>α : E<VAR>hα : IsIntegral F α<VAR>h_sep : IsSeparable F α<VAR>h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)<VAR>this : Fintype (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯) := IntermediateField.fintypeOfAlgHomAdjoinIntegral F hα<GOAL>Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = Fintype.card (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁸ : DecidableEq α'<VAR>inst✝⁷ : DecidableEq β'<VAR>inst✝⁶ : DecidableEq γ<VAR>inst✝⁵ : DecidableEq γ'<VAR>inst✝⁴ : DecidableEq δ<VAR>inst✝³ : DecidableEq δ'<VAR>inst✝² : DecidableEq ε<VAR>inst✝¹ : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝ : DecidableEq α<GOAL>image2 f (insert a ↑s) ↑t = (fun b => f a b) '' ↑t ∪ image2 f ↑s ↑t
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<GOAL>(span 𝕜 (Set.range fun i => b.repr.symm (lp.single 2 i 1))).topologicalClosure ≤ (⨆ J, span 𝕜 ↑(Finset.image (fun i => b.repr.symm (lp.single 2 i 1)) J)).topologicalClosure
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>cplt : CompleteSpace E<VAR>G : ι → Type u_4<VAR>inst✝¹ : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>b : HilbertBasis ι 𝕜 E<GOAL>(span 𝕜 (Set.range fun i => b.repr.symm (lp.single 2 i 1))).topologicalClosure ≤ (span 𝕜 (⋃ i, ↑(Finset.image (fun i => b.repr.symm (lp.single 2 i 1)) i))).topologicalClosure
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>inst✝ : DecidableEq ι<VAR>l : ⨁ (i : ι), G i<VAR>i : ι<VAR>v : G i<GOAL>(DFinsupp.sum l fun j w => if i = j then ⟪(V i) v, (V j) w⟫_𝕜 else 0) = ⟪v, l i⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁷ : _root_.RCLike 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>G : ι → Type u_5<VAR>inst✝² : (i : ι) → NormedAddCommGroup (G i)<VAR>inst✝¹ : (i : ι) → InnerProductSpace 𝕜 (G i)<VAR>V : (i : ι) → G i →ₗᵢ[𝕜] E<VAR>hV : OrthogonalFamily 𝕜 G V<VAR>dec_V : (i : ι) → (x : G i) → Decidable (x ≠ 0)<VAR>inst✝ : DecidableEq ι<VAR>l : ⨁ (i : ι), G i<VAR>i : ι<VAR>v : G i<GOAL>(if l i ≠ 0 then ⟪(V i) v, (V i) (l i)⟫_𝕜 else 0) = ⟪v, l i⟫_𝕜
<VAR>m n : ℕ<GOAL>m.gcd (m + n) = m.gcd n
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>hs : DirectedOn (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, SetIndependent a<GOAL>SetIndependent (⋃₀ s)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>hs : DirectedOn (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, SetIndependent a<GOAL>SetIndependent (⋃ i, ↑i)
<VAR>α✝ β : Type u<VAR>α : Type (max u v)<VAR>inst✝ : Small.{v, max u v} α<GOAL>lift.{u, v} #(Shrink.{v, max u v} α) = #α
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>c : F<GOAL>fderiv 𝕜 (fun y => c - f y) x = -fderiv 𝕜 f x
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C<GOAL>IsCoseparator (op G) ↔ IsSeparator G
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>f f' : PartialHomeomorph X Y<GOAL>(f.subtypeRestr hs).symm.trans (f'.subtypeRestr hs) ≈ (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>f f' : PartialHomeomorph X Y<GOAL>(f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans ((s.partialHomeomorphSubtypeCoe hs).trans f') ≈ (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>f f' : PartialHomeomorph X Y<VAR>openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)<GOAL>(f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans ((s.partialHomeomorphSubtypeCoe hs).trans f') ≈ (f.symm.trans f').restr (f.target ∩ ↑f.symm ⁻¹' ↑s)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>f f' : PartialHomeomorph X Y<VAR>openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)<GOAL>((f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs)).trans f' ≈ ((ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm).trans f'
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>f f' : PartialHomeomorph X Y<VAR>openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)<GOAL>(f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs) ≈ (ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>f f' : PartialHomeomorph X Y<VAR>openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)<VAR>set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s<GOAL>(f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs) ≈ (ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>f f' : PartialHomeomorph X Y<VAR>openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)<VAR>set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s<VAR>openness₂ : IsOpen ↑s<GOAL>(f.symm.trans (s.partialHomeomorphSubtypeCoe hs).symm).trans (s.partialHomeomorphSubtypeCoe hs) ≈ (ofSet (f.target ∩ ↑f.symm ⁻¹' ↑s) openness₁).trans f.symm
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>f f' : PartialHomeomorph X Y<VAR>openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)<VAR>set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s<VAR>openness₂ : IsOpen ↑s<GOAL>f.symm.trans ((s.partialHomeomorphSubtypeCoe hs).symm.trans (s.partialHomeomorphSubtypeCoe hs)) ≈ f.symm.trans (ofSet (↑s) openness₂)
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>f f' : PartialHomeomorph X Y<VAR>openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)<VAR>set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s<VAR>openness₂ : IsOpen ↑s<GOAL>(s.partialHomeomorphSubtypeCoe hs).symm.trans (s.partialHomeomorphSubtypeCoe hs) ≈ ofSet (↑s) openness₂
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>s : Opens X<VAR>hs : Nonempty ↥s<VAR>f f' : PartialHomeomorph X Y<VAR>openness₁ : IsOpen (f.target ∩ ↑f.symm ⁻¹' ↑s)<VAR>set_identity : f.symm.source ∩ (f.target ∩ ↑f.symm ⁻¹' ↑s) = f.symm.source ∩ ↑f.symm ⁻¹' ↑s<VAR>openness₂ : IsOpen ↑s<GOAL>ofSet (s.partialHomeomorphSubtypeCoe hs).target ⋯ ≈ ofSet (↑s) openness₂
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>l₁ l₂ : Filter α<GOAL>𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>f✝ : α → β<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<GOAL>(f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s : Multiset α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<GOAL>count True (map p s) = card (filter p s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<GOAL>((fun x => -u x) - fun x => -v x) =o[l] fun x => -v x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : NormedAddCommGroup β<VAR>u v w : α → β<VAR>l : Filter α<VAR>huv : u ~[l] v<VAR>x✝ : α<GOAL>((fun x => -u x) - fun x => -v x) x✝ = -(u - v) 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>p : ι → Prop<VAR>s : (i : ι) → p i → Set α<VAR>hp : ∃ i, p i<VAR>f : α → β<VAR>h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)<GOAL>f '' ⋂ i, ⋂ (hi : p i), s i hi = ⋂ i, ⋂ (hi : p i), f '' s i hi
<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>p : ι → Prop<VAR>s : (i : ι) → p i → Set α<VAR>hp : ∃ i, p i<VAR>f : α → β<VAR>h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)<GOAL>f '' ⨅ x, s ↑x ⋯ = ⨅ x, f '' s ↑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>p : ι → Prop<VAR>s : (i : ι) → p i → Set α<VAR>hp : ∃ i, p i<VAR>f : α → β<VAR>h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)<VAR>this : Nonempty { i // p i }<GOAL>f '' ⨅ x, s ↑x ⋯ = ⨅ x, f '' s ↑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>p : ι → Prop<VAR>s : (i : ι) → p i → Set α<VAR>hp : ∃ i, p i<VAR>f : α → β<VAR>h : InjOn f (⋃ i, ⋃ (hi : p i), s i hi)<VAR>this : Nonempty { i // p i }<GOAL>InjOn f (⋃ i, s ↑i ⋯)
<VAR>L : Language<VAR>T✝ : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>T' : L.Theory<VAR>ι : Type u_1<VAR>T : ι → L.Theory<GOAL>IsSatisfiable (⋃ i, T i) ↔ ∀ (s : Finset ι), IsSatisfiable (⋃ i ∈ s, T i)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : dist p₂ s.center ≤ s.radius<VAR>h : ¬p₁ = p₂<GOAL>0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : dist p₁ s.center = s.radius<VAR>hp₂ : dist p₂ s.center ≤ s.radius<VAR>h : ¬p₁ = p₂<GOAL>0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫_ℝ
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : dist p₁ s.center = s.radius<VAR>hp₂ : dist p₂ s.center ≤ s.radius<VAR>h : ¬p₁ = p₂<GOAL>⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫_ℝ < ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : dist p₁ s.center = s.radius<VAR>hp₂ : dist p₂ s.center ≤ s.radius<VAR>h : ¬p₁ = p₂<GOAL>‖p₂ -ᵥ s.center‖ ≤ ‖p₁ -ᵥ s.center‖
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>s : Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : dist p₁ s.center = s.radius<VAR>hp₂ : dist p₂ s.center ≤ s.radius<VAR>h : ¬p₁ = p₂<GOAL>⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫_ℝ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : α → Type u_3<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (σ a)<VAR>a : α<VAR>b : σ a<GOAL>⟨a, b⟩ ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>ι : Type u_4<VAR>inst✝ : PseudoMetricSpace β<VAR>b : ℝ → ℝ<VAR>b_lim : Tendsto b (𝓝 0) (𝓝 0)<VAR>F : ι → β → α<VAR>H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)<GOAL>UniformEquicontinuous F
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>ι : Type u_4<VAR>inst✝ : PseudoMetricSpace β<VAR>b : ℝ → ℝ<VAR>b_lim : Tendsto b (𝓝 0) (𝓝 0)<VAR>F : ι → β → α<VAR>H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)<GOAL>∀ ε > 0, ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>ι : Type u_4<VAR>inst✝ : PseudoMetricSpace β<VAR>b : ℝ → ℝ<VAR>b_lim : Tendsto b (𝓝 0) (𝓝 0)<VAR>F : ι → β → α<VAR>H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)<VAR>ε : ℝ<VAR>ε0 : ε > 0<GOAL>∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>ι : Type u_4<VAR>inst✝ : PseudoMetricSpace β<VAR>b : ℝ → ℝ<VAR>b_lim : Tendsto b (𝓝 0) (𝓝 0)<VAR>F : ι → β → α<VAR>H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>δ : ℝ<VAR>δ0 : δ > 0<VAR>hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε<GOAL>∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι✝ : Type u_3<VAR>inst✝¹ : PseudoMetricSpace α<VAR>ι : Type u_4<VAR>inst✝ : PseudoMetricSpace β<VAR>b : ℝ → ℝ<VAR>b_lim : Tendsto b (𝓝 0) (𝓝 0)<VAR>F : ι → β → α<VAR>H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>δ : ℝ<VAR>δ0 : δ > 0<VAR>hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε<VAR>x y : β<VAR>hxy : dist x y < δ<VAR>i : ι<GOAL>dist (F i x) (F i y) < ε
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>k : ℕ<VAR>hlt : ∀ (hf : (setOf p).Finite), k + 1 < hf.toFinset.card<GOAL>filter p (range (nth p (k + 1))) = insert (nth p k) (filter p (range (nth p k)))
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>k : ℕ<VAR>hlt : ∀ (hf : (setOf p).Finite), k + 1 < hf.toFinset.card<VAR>a : ℕ<VAR>ha : a ∈ insert (nth p k) (filter p (range (nth p k)))<GOAL>a ∈ filter p (range (nth p (k + 1)))
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>k : ℕ<VAR>hlt : ∀ (hf : (setOf p).Finite), k + 1 < hf.toFinset.card<VAR>a : ℕ<VAR>ha : a = nth p k ∨ a < nth p k ∧ p a<GOAL>a < nth p (k + 1) ∧ p a
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>k : ℕ<VAR>hlt : ∀ (hf : (setOf p).Finite), k + 1 < hf.toFinset.card<VAR>a : ℕ<VAR>ha : a = nth p k ∨ a < nth p k ∧ p a<VAR>this : nth p k < nth p (k + 1)<GOAL>a < nth p (k + 1) ∧ p a
<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>hq : q.Monic<VAR>hpq : p.degree < q.degree<GOAL>(p + q).Monic
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>I : Ideal S<GOAL>spanNorm R I = ⊥ ↔ I = ⊥
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>I : Ideal S<GOAL>(∀ a ∈ I, a = 0) ↔ ∀ ⦃x : S⦄, x ∈ I → x ∈ ⊥
<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 : MvPolynomial σ R<VAR>h : r ≠ 0<GOAL>((monomial s) r).vars = s.support
<VAR>n m : ℕ<VAR>inst✝ : NeZero n<VAR>k : Fin n<GOAL>0 * k = 0
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>inst✝⁵ : Semiring R₁<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝³ : TopologicalSpace M₁<VAR>inst✝² : AddCommMonoid M₁<VAR>inst✝¹ : TopologicalSpace M₂<VAR>inst✝ : T2Space M₂<VAR>f : M₁ → M₂<GOAL>IsCompactOperator f ↔ ∃ V ∈ 𝓝 0, IsCompact (closure (f '' V))
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>inst✝⁵ : Semiring R₁<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>inst✝³ : TopologicalSpace M₁<VAR>inst✝² : AddCommMonoid M₁<VAR>inst✝¹ : TopologicalSpace M₂<VAR>inst✝ : T2Space M₂<VAR>f : M₁ → M₂<GOAL>(∃ V ∈ 𝓝 0, ∃ K, IsCompact K ∧ f '' V ⊆ K) ↔ ∃ V ∈ 𝓝 0, IsCompact (closure (f '' V))