ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>δ : α → Sort u_2<VAR>m✝ : Multiset α<VAR>a✝ a : α<VAR>b : δ a<VAR>m : Multiset α<VAR>f : (a : α) → a ∈ m → δ a<VAR>a'' : α<VAR>h₁ : a'' ≠ a<VAR>b' : δ a''<VAR>h : a ≠ a''<VAR>ha₁ : a'' ∈ a ::ₘ a'' ::ₘ m<VAR>ha₂ : a'' ∈ a'' ::ₘ a ::ₘ m<VAR>x✝ : HEq ha₁ ha₂<GOAL>HEq (cons (a'' ::ₘ m) a b (cons m a'' b' f) a'' ha₁) (cons (a ::ₘ m) a'' b' (cons m a b f) a'' ha₂)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>δ : α → Sort u_2<VAR>m✝ : Multiset α<VAR>a✝ a a' : α<VAR>b : δ a<VAR>b' : δ a'<VAR>m : Multiset α<VAR>f : (a : α) → a ∈ m → δ a<VAR>h : a ≠ a'<VAR>a'' : α<VAR>ha₁ : a'' ∈ a ::ₘ a' ::ₘ m<VAR>ha₂ : a'' ∈ a' ::ₘ a ::ₘ m<VAR>x✝ : HEq ha₁ ha₂<VAR>h₁ : a'' ≠ a<VAR>h₂ : a'' ≠ a'<GOAL>HEq (cons (a' ::ₘ m) a b (cons m a' b' f) a'' ha₁) (cons (a ::ₘ m) a' b' (cons m a b f) a'' ha₂)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝⁹ : NontriviallyNormedField 𝕜'<VAR>inst✝⁸ : NormedAlgebra 𝕜 𝕜'<VAR>E : Type u_3<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜' E<VAR>inst✝⁴ : IsScalarTower 𝕜 𝕜' E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>f : E → F<VAR>f' : E →L[𝕜'] F<VAR>s : Set E<VAR>x : E<VAR>g' : E →L[𝕜] F<VAR>h : HasFDerivWithinAt f (ContinuousLinearMap.restrictScalars 𝕜 f') s x<VAR>H : ContinuousLinearMap.restrictScalars 𝕜 f' = g'<GOAL>HasFDerivWithinAt f f' s x
<VAR>α : Type u_1<VAR>s t : Set α<GOAL>diagonal α = univ ↔ Subsingleton α
<VAR>m n✝ n : ℕ<GOAL>(last n).rev = ⊥
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>c : ℝ≥0∞<VAR>h : levyProkhorovEDist μ ν < c<VAR>B : Set Ω<VAR>B_mble : MeasurableSet B<GOAL>μ B ≤ ν (thickening c.toReal B) + c
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<VAR>c : ℝ≥0∞<VAR>h : levyProkhorovEDist μ ν < c<VAR>B : Set Ω<VAR>B_mble : MeasurableSet B<VAR>c' : ℝ≥0∞<VAR>hc' : c' ∈ {ε | ∀ (B : Set Ω), MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε}<VAR>lt_c : c' < c<GOAL>μ B ≤ ν (thickening c.toReal B) + c
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<GOAL>WithSeminorms p ↔ t = ⨅ i, UniformSpace.toTopologicalSpace
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<GOAL>𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = ⨅ i, 𝓝 0
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<VAR>i : ι<GOAL>comap (⇑(p i)) (𝓝 0) = 𝓝 0
<VAR>G : Type u_1<VAR>H✝ : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝¹ : Monoid G<VAR>a b x y✝ : G<VAR>n m : ℕ<VAR>H : Type u_6<VAR>inst✝ : Monoid H<VAR>y : H<GOAL>orderOf x = orderOf y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝³ : DecidableEq β<VAR>inst✝² : GroupWithZero α<VAR>inst✝¹ : MulAction α β<VAR>s✝ t : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : Fintype β<VAR>s : Finset α<VAR>hs : s.Nontrivial<GOAL>↑s • Set.univ = Set.univ
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ₁ θ₂ : Real.Angle<VAR>x : V<GOAL>(o.rotation θ₁) ((o.rotation θ₂) x) = (o.rotation (θ₁ + θ₂)) x
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ₁ θ₂ : Real.Angle<VAR>x : V<GOAL>(θ₁.cos * θ₂.cos) • x + (θ₁.cos * θ₂.sin) • o.rightAngleRotation x + ((θ₁.sin * θ₂.cos) • o.rightAngleRotation x + -((θ₁.sin * θ₂.sin) • x)) = (θ₁.cos * θ₂.cos) • x - (θ₁.sin * θ₂.sin) • x + ((θ₁.sin * θ₂.cos) • o.rightAngleRotation x + (θ₁.cos * θ₂.sin) • o.rightAngleRotation x)
<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 : Set P<VAR>hs : Cospherical s<VAR>p₁ p₂ p₃ : P<VAR>h₁ : p₁ ∈ s<VAR>h₂ : p₂ ∈ s<VAR>h₃ : p₃ ∈ s<VAR>h₁₂ : p₁ ≠ p₂<VAR>h₁₃ : p₁ ≠ p₃<VAR>h₂₃ : p₂ ≠ p₃<GOAL>AffineIndependent ℝ ![p₁, p₂, p₃]
<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 : Set P<VAR>hs : Cospherical s<VAR>p₁ p₂ p₃ : P<VAR>h₁ : p₁ ∈ s<VAR>h₂ : p₂ ∈ s<VAR>h₃ : p₃ ∈ s<VAR>h₁₂ : p₁ ≠ p₂<VAR>h₁₃ : p₁ ≠ p₃<VAR>h₂₃ : p₂ ≠ p₃<GOAL>Set.range ![p₁, p₂, p₃] ⊆ s
<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 : Set P<VAR>hs : Cospherical s<VAR>p₁ p₂ p₃ : P<VAR>h₁ : p₁ ∈ s<VAR>h₂ : p₂ ∈ s<VAR>h₃ : p₃ ∈ s<VAR>h₁₂ : p₁ ≠ p₂<VAR>h₁₃ : p₁ ≠ p₃<VAR>h₂₃ : p₂ ≠ p₃<GOAL>Function.Injective ![p₁, p₂, p₃]
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<GOAL>IsNowhereDense ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<GOAL>OpensMeasurableSpace α ↔ ∀ (s : Set α), IsOpen s → MeasurableSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s✝ t u : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>h : OpensMeasurableSpace α<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>MeasurableSet s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>I : Set ι<VAR>m : ι → OuterMeasure α<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>(⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>a : α<VAR>inst✝ : LawfulBEq α<VAR>l₁ l₂ : List α<VAR>h : a ∈ l₁<GOAL>(l₁ ++ l₂).erase a = l₁.erase a ++ l₂
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>a : α<VAR>inst✝ : LawfulBEq α<VAR>l₁ l₂ : List α<VAR>h : a ∈ l₁<GOAL>eraseP (fun x => a == x) (l₁ ++ l₂) = eraseP (fun x => a == x) l₁ ++ l₂
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hQ : Q ≠ 0<GOAL>Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0) ↔ P.degree < Q.degree
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hQ : Q ≠ 0<VAR>h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)<GOAL>P.degree < Q.degree
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>H : Valid' o₁ (Ordnode.node s l x r) o₂<GOAL>Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>H : Valid' o₁ (Ordnode.node s l x r) o₂<VAR>this : Valid' o₂ (r.dual.node' x l.dual).eraseMax ↑(findMax' x l.dual) ∧ (r.dual.node' x l.dual).size = (r.dual.node' x l.dual).eraseMax.size + 1<GOAL>Valid' (↑(l.findMin' x)) (l.node' x r).eraseMin o₂ ∧ (l.node' x r).size = (l.node' x r).eraseMin.size + 1
<VAR>R : Type u<VAR>inst✝ : AddGroupWithOne R<GOAL>↑1 = 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<VAR>h : Collinear R {x, y, z}<GOAL>Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<VAR>h : ∃ v, ∀ p ∈ {x, y, z}, ∃ r, p = r • v +ᵥ x<GOAL>Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<VAR>v : V<VAR>h : ∀ p ∈ {x, y, z}, ∃ r, p = r • v +ᵥ x<GOAL>Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y z : P<VAR>v : V<VAR>h : ∀ (p : P), p = x ∨ p = y ∨ p = z → ∃ r, p = r • v +ᵥ x<GOAL>Wbtw R x y z ∨ Wbtw R y z x ∨ Wbtw R z x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>ty tz : R<VAR>h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x<GOAL>Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>ty tz : R<VAR>h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x<VAR>hy0 : ty < 0<GOAL>Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>tz : R<VAR>h : ∀ (p : P), p = x ∨ p = 0 • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x<GOAL>Wbtw R x (0 • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (0 • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (0 • v +ᵥ x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>ty tz : R<VAR>h : ∀ (p : P), p = x ∨ p = ty • v +ᵥ x ∨ p = tz • v +ᵥ x → ∃ r, p = r • v +ᵥ x<VAR>hy0 : 0 < ty<GOAL>Wbtw R x (ty • v +ᵥ x) (tz • v +ᵥ x) ∨ Wbtw R (ty • v +ᵥ x) (tz • v +ᵥ x) x ∨ Wbtw R (tz • v +ᵥ x) x (ty • v +ᵥ x)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>f : α → Finset β<VAR>h : (range f).Finite<GOAL>(⋃ a, ↑(f a)).Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>f : α → Finset β<VAR>h : (range f).Finite<GOAL>(⋃ x ∈ range f, ↑x).Finite
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Semiring S<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁴ : CommSemiring R₁<VAR>inst✝³ : CommSemiring R₂<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R₁ A<VAR>inst✝ : Algebra R₂ A<VAR>I J : Ideal R<VAR>h : I ≤ J<VAR>x✝ : R<GOAL>x✝ ∈ comap (Quotient.mk I) (map (Quotient.mk I) J) ↔ x✝ ∈ J
<VAR>α : Type u_1<VAR>inst✝ : AddMonoidWithOne α<VAR>p : PosNum<GOAL>↑(↑p + ↑p) = ↑p + ↑p
<VAR>α : Type u_1<VAR>inst✝ : AddMonoidWithOne α<VAR>p : PosNum<GOAL>↑(↑p + ↑p + 1) = ↑p + ↑p + 1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>h : ∀ (x : X), f x ~ᵢ g x<GOAL>Continuous f ↔ Continuous g
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>h : ∀ (x : X), f x ~ᵢ g x<GOAL>Continuous (SeparationQuotient.mk ∘ f) ↔ Continuous (SeparationQuotient.mk ∘ g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T2Space Y<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<GOAL>IsProperMap f
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T2Space Y<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<GOAL>Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, ↑𝒰 ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T2Space Y<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : IsProperMap (g ∘ f)<VAR>𝒰 : Ultrafilter X<VAR>y : Y<VAR>h : Tendsto f (↑𝒰) (𝓝 y)<GOAL>∃ x, ↑𝒰 ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T2Space Y<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : Continuous (g ∘ f) ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄, Tendsto (g ∘ f) (↑𝒰) (𝓝 y) → ∃ x, (g ∘ f) x = y ∧ ↑𝒰 ≤ 𝓝 x<VAR>𝒰 : Ultrafilter X<VAR>y : Y<VAR>h : Tendsto f (↑𝒰) (𝓝 y)<GOAL>∃ x, ↑𝒰 ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>W : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace W<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝ : T2Space Y<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : Continuous (g ∘ f) ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄, Tendsto (g ∘ f) (↑𝒰) (𝓝 y) → ∃ x, (g ∘ f) x = y ∧ ↑𝒰 ≤ 𝓝 x<VAR>𝒰 : Ultrafilter X<VAR>y : Y<VAR>h : Tendsto f (↑𝒰) (𝓝 y)<VAR>x : X<VAR>hx : ↑𝒰 ≤ 𝓝 x<GOAL>∃ x, ↑𝒰 ≤ 𝓝 x
<VAR>R : Type u<VAR>S : Type v<VAR>a b c✝ d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>c : R<VAR>n : ℕ<GOAL>(C c * X ^ n).support.card ≤ 1
<VAR>R : Type u<VAR>S : Type v<VAR>a b c✝ d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>c : R<VAR>n : ℕ<GOAL>(C c * X ^ n).support.card ≤ {n}.card
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{u_4, u_2} D<VAR>L✝ : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝ : L✝.IsLocalization W<VAR>X Y : C<VAR>φ : W.RightFraction X Y<VAR>L : C ⥤ D<VAR>hL : W.IsInvertedBy L<GOAL>(L.map φ.f).op ≫ (inv (L.map φ.s)).op = (L.map φ.f).op ≫ inv (L.map φ.s).op
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>hf1 : IsUnit ((expand R p) f)<GOAL>IsUnit f
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>hf1 : IsUnit ((expand R p) f)<VAR>hf2 : (expand R p) f = C (((expand R p) f).coeff 0)<GOAL>IsUnit f
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>hf1 : IsUnit ((expand R p) f)<VAR>hf2 : (expand R p) f = C (f.coeff 0)<GOAL>IsUnit f
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>hf1 : IsUnit (f.coeff 0)<VAR>hf2 : (expand R p) f = C (f.coeff 0)<GOAL>IsUnit f
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p : ℕ<VAR>hp : 0 < p<VAR>f : R[X]<VAR>hf1 : IsUnit (f.coeff 0)<VAR>hf2 : f = C (f.coeff 0)<GOAL>IsUnit f
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : ↥(Submodule.span ℝ {v})ᗮ<GOAL>stereoInvFun hv w ≠ ⟨v, ⋯⟩
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : ↥(Submodule.span ℝ {v})ᗮ<GOAL>↑(stereoInvFun hv w) ≠ ↑⟨v, ⋯⟩
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : ↥(Submodule.span ℝ {v})ᗮ<GOAL>⟪↑(stereoInvFun hv w), v⟫_ℝ < 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : ↥(Submodule.span ℝ {v})ᗮ<GOAL>‖↑(stereoInvFun hv w)‖ = 1
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>p q : R[X]<GOAL>C ((Algebra.norm R[X]) (p • 1 + q • (mk W) Y)) - (C p + C q * Y) * (C p + C q * (-Y - C (C W.a₁ * X + C W.a₃))) = W.polynomial * C q ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>p q : R[X]<GOAL>C (p ^ 2 - p * q * (C W.a₁ * X + C W.a₃) - q ^ 2 * (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) - (C p + C q * Y) * (C p + C q * (-Y - C (C W.a₁ * X + C W.a₃))) = (Y ^ 2 + C (C W.a₁ * X + C W.a₃) * Y - C (X ^ 3 + C W.a₂ * X ^ 2 + C W.a₄ * X + C W.a₆)) * C q ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>p q : R[X]<GOAL>C p ^ 2 - C p * C q * (C (C W.a₁) * C X + C (C W.a₃)) - C q ^ 2 * (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆)) - (C p + C q * Y) * (C p + C q * (-Y - (C (C W.a₁) * C X + C (C W.a₃)))) = (Y ^ 2 + (C (C W.a₁) * C X + C (C W.a₃)) * Y - (C X ^ 3 + C (C W.a₂) * C X ^ 2 + C (C W.a₄) * C X + C (C W.a₆))) * C q ^ 2
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hR : 0 < ringChar R<VAR>φ : AddChar R ℂ<VAR>a : R<GOAL>((↑(starRingEnd ℂ)).compAddChar φ) a = φ⁻¹ a
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hR : 0 < ringChar R<VAR>φ : AddChar R ℂ<VAR>a : R<GOAL>(starRingEnd ℂ) (φ a) = (φ a)⁻¹
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hR : 0 < ringChar R<VAR>φ : AddChar R ℂ<VAR>a : R<VAR>H : ‖↑⋯.unit‖ = 1<GOAL>(starRingEnd ℂ) (φ a) = (φ a)⁻¹
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι✝ : Sort x<VAR>κ : ι✝ → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>l : α → β<VAR>u : β → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>ι : Sort x<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi<GOAL>l (⨅ i, ⨅ (hi : p i), f i hi) = ⨅ i, ⨅ (hi : p i), l (f i hi)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι✝ : Sort x<VAR>κ : ι✝ → Sort u_1<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>l : α → β<VAR>u : β → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : CompleteLattice β<VAR>gi : GaloisInsertion l u<VAR>ι : Sort x<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>hf : ∀ (i : ι) (hi : p i), u (l (f i hi)) = f i hi<GOAL>l (⨅ x, f ↑x ⋯) = ⨅ x, l (f ↑x ⋯)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx1 : 0 < x<VAR>hx2 : x < 1<VAR>hz : z < 0<GOAL>1 < x ^ z
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx1 : 0 < x<VAR>hx2 : x < 1<VAR>hz : z < 0<GOAL>1 = x ^ 0
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>s : Set K<VAR>p : K → Prop<VAR>x : K<VAR>h : x ∈ closure s<VAR>mem : ∀ x ∈ s, p x<VAR>one : p 1<VAR>add : ∀ (x y : K), p x → p y → p (x + y)<VAR>neg : ∀ (x : K), p x → p (-x)<VAR>inv : ∀ (x : K), p x → p x⁻¹<VAR>mul : ∀ (x y : K), p x → p y → p (x * y)<GOAL>p x
<VAR>K : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : DivisionRing L<VAR>inst✝ : DivisionRing M<VAR>s : Set K<VAR>p : K → Prop<VAR>x : K<VAR>h : x ∈ closure s<VAR>mem : ∀ x ∈ s, p x<VAR>one : p 1<VAR>add : ∀ (x y : K), p x → p y → p (x + y)<VAR>neg : ∀ (x : K), p x → p (-x)<VAR>inv : ∀ (x : K), p x → p x⁻¹<VAR>mul : ∀ (x y : K), p x → p y → p (x * y)<VAR>this : Subfield K := { carrier := p, mul_mem' := ⋯, one_mem' := one, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯, inv_mem' := inv }<GOAL>p x
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>H : Subgroup G<VAR>a b : α<VAR>h : ⟦a⟧ = ⟦b⟧<GOAL>⟦a⟧ = ⟦b⟧
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>H : Subgroup G<VAR>a b : α<VAR>h : a ≈ b<GOAL>a ≈ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a ∆ b \ (a ⊓ b) = a ∆ b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>p q : ℕ<GOAL>(fun x => x ^ p / x ^ q) =ᶠ[atTop] fun x => x ^ (↑p - ↑q)
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>p q : ℕ<GOAL>∀ (x : 𝕜), 0 < x → (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
<VAR>𝕜 : Type u_1<VAR>inst✝ : LinearOrderedField 𝕜<VAR>p q : ℕ<VAR>x : 𝕜<VAR>hx : 0 < x<GOAL>(fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>I : MultispanIndex C<VAR>K : Multicofork I<VAR>a : I.L<GOAL>I.fst a ≫ K.π (I.fstFrom a) = I.snd a ≫ K.π (I.sndFrom a)
<VAR>α✝ : Sort u<VAR>β✝ : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<GOAL>⇑e.symm '' t ⊆ s ↔ t ⊆ ⇑e '' s
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>S : Set (Set X)<VAR>ho : ∀ s ∈ S, IsOpen s<VAR>hS : S.Countable<VAR>hd : ∀ s ∈ S, Dense s<GOAL>Dense (⋂₀ S)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>S : Set (Set X)<VAR>ho : ∀ s ∈ S, IsOpen s<VAR>hS : S.Countable<VAR>hd : ∀ s ∈ S, Dense s<VAR>h : S = ∅<GOAL>Dense (⋂₀ S)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>S : Set (Set X)<VAR>ho : ∀ s ∈ S, IsOpen s<VAR>hS : S.Countable<VAR>hd : ∀ s ∈ S, Dense s<VAR>h : S.Nonempty<GOAL>Dense (⋂₀ S)
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : 0 < P.degree<GOAL>Tendsto (fun x => |eval x P|) atTop atTop
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : 0 < P.degree<VAR>hP : 0 ≤ P.leadingCoeff<GOAL>Tendsto (fun x => |eval x P|) atTop atTop
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NormedLinearOrderedField 𝕜<VAR>P Q : 𝕜[X]<VAR>inst✝ : OrderTopology 𝕜<VAR>hdeg : 0 < P.degree<VAR>hP : P.leadingCoeff ≤ 0<GOAL>Tendsto (fun x => |eval x P|) atTop atTop
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>hs : MeasurableSet s<GOAL>LocallyIntegrable (fun x => f ↑x) (comap Subtype.val μ) ↔ LocallyIntegrableOn f s μ