ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : IsCyclotomicExtension {n} A B<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : NeZero ↑↑n<GOAL>(cyclotomic (↑n) B).IsRoot (zeta n A B) ↔ (aeval (zeta n A B)) (cyclotomic (↑n) A) = 0
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s s₁ s₂ t t₁ t₂ : Set E<VAR>hs : Balanced 𝕜 s<VAR>ht : Balanced 𝕜 t<GOAL>Balanced 𝕜 (s - t)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s s₁ s₂ t t₁ t₂ : Set E<VAR>hs : Balanced 𝕜 s<VAR>ht : Balanced 𝕜 t<GOAL>Balanced 𝕜 (s + -t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>s : Set α<VAR>ha : 0 ≤ a<VAR>hs : IsGLB s b<GOAL>IsGLB ((fun b => a * b) '' s) (a * b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>s : Set α<VAR>ha✝ : 0 ≤ a<VAR>hs : IsGLB s b<VAR>ha : 0 < a<GOAL>IsGLB ((fun b => a * b) '' s) (a * b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>b c d e : α<VAR>m n : ℤ<VAR>s : Set α<VAR>hs : IsGLB s b<VAR>ha : 0 ≤ 0<GOAL>IsGLB ((fun b => 0 * b) '' s) (0 * b)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<GOAL>x = y ∨ y = z ∨ x = z
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<VAR>hne : ¬(x = y ∨ y = z ∨ x = z)<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<VAR>hne : x ≠ y ∧ y ≠ z ∧ x ≠ z<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<VAR>hne : x ≠ y ∧ y ≠ z ∧ x ≠ z<VAR>h₁ : x < y<VAR>h₂ : y < z<VAR>h₃ : x < z<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<VAR>hne : x ≠ y ∧ y ≠ z ∧ x ≠ z<VAR>h₁ : x < y<VAR>h₂ : y < z<VAR>h₃ : z < x<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<VAR>hne : x ≠ y ∧ y ≠ z ∧ x ≠ z<VAR>h₁ : x < y<VAR>h₂ : z < y<VAR>h₃ : x < z<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<VAR>hne : x ≠ y ∧ y ≠ z ∧ x ≠ z<VAR>h₁ : x < y<VAR>h₂ : z < y<VAR>h₃ : z < x<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<VAR>hne : x ≠ y ∧ y ≠ z ∧ x ≠ z<VAR>h₁ : y < x<VAR>h₂ : y < z<VAR>h₃ : x < z<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<VAR>hne : x ≠ y ∧ y ≠ z ∧ x ≠ z<VAR>h₁ : y < x<VAR>h₂ : y < z<VAR>h₃ : z < x<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<VAR>hne : x ≠ y ∧ y ≠ z ∧ x ≠ z<VAR>h₁ : y < x<VAR>h₂ : z < y<VAR>h₃ : x < z<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : LinearOrder α<VAR>h : ∀ ⦃x y z : α⦄, x < y → y < z → False<VAR>x y z : α<VAR>hne : x ≠ y ∧ y ≠ z ∧ x ≠ z<VAR>h₁ : y < x<VAR>h₂ : z < y<VAR>h₃ : z < x<GOAL>False
<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>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : InnerProductSpace ℝ G<VAR>f : G ≃ₗᵢ[ℝ] ℂ<VAR>x y : G<GOAL>⟪x, y⟫_ℝ = ((starRingEnd ℂ) (f x) * f y).re
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<GOAL>star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary = diagonal (RCLike.ofReal ∘ hA.eigenvalues)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<GOAL>toEuclideanLin (star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary) = toEuclideanLin (diagonal (RCLike.ofReal ∘ hA.eigenvalues))
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<GOAL>∀ (i : n), (toEuclideanLin (star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary)) ((EuclideanSpace.basisFun n 𝕜).toBasis i) = (toEuclideanLin (diagonal (RCLike.ofReal ∘ hA.eigenvalues))) ((EuclideanSpace.basisFun n 𝕜).toBasis i)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<VAR>i : n<GOAL>(toEuclideanLin (star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary)) ((EuclideanSpace.basisFun n 𝕜).toBasis i) = (toEuclideanLin (diagonal (RCLike.ofReal ∘ hA.eigenvalues))) ((EuclideanSpace.basisFun n 𝕜).toBasis i)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<VAR>i : n<GOAL>↑(hA.eigenvalues i) • EuclideanSpace.single i 1 = EuclideanSpace.single i ↑(hA.eigenvalues i)
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<VAR>i : n<GOAL>∀ (i_1 : n), (↑(hA.eigenvalues i) • EuclideanSpace.single i 1) i_1 = EuclideanSpace.single i (↑(hA.eigenvalues i)) i_1
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>n : Type u_2<VAR>inst✝¹ : Fintype n<VAR>A : Matrix n n 𝕜<VAR>inst✝ : DecidableEq n<VAR>hA : A.IsHermitian<VAR>i j : n<GOAL>(↑(hA.eigenvalues i) • EuclideanSpace.single i 1) j = EuclideanSpace.single i (↑(hA.eigenvalues i)) j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f g : α → β<VAR>s s₁ : Set α<VAR>h : ContinuousOn f s<VAR>h' : EqOn g f s₁<VAR>h₁ : s₁ ⊆ s<VAR>x : α<VAR>hx : x ∈ s₁<GOAL>Tendsto g (𝓝[s₁] x) (𝓝 (g x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f g : α → β<VAR>s s₁ : Set α<VAR>h : ContinuousOn f s<VAR>h' : EqOn g f s₁<VAR>h₁ : s₁ ⊆ s<VAR>x : α<VAR>hx : x ∈ s₁<VAR>A : ContinuousWithinAt f s₁ x<GOAL>Tendsto g (𝓝[s₁] x) (𝓝 (g x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f g : α → β<VAR>s s₁ : Set α<VAR>h : ContinuousOn f s<VAR>h' : EqOn g f s₁<VAR>h₁ : s₁ ⊆ s<VAR>x : α<VAR>hx : x ∈ s₁<VAR>A : Tendsto f (𝓝[s₁] x) (𝓝 (g x))<GOAL>Tendsto g (𝓝[s₁] x) (𝓝 (g x))
<VAR>a b : EReal<VAR>h₁ : b ≠ ⊥<VAR>h₂ : b ≠ ⊤<VAR>h₃ : b ≠ 0<GOAL>a * b⁻¹ * b = a
<VAR>a b : EReal<VAR>h₁ : b ≠ ⊥<VAR>h₂ : b ≠ ⊤<VAR>h₃ : b ≠ 0<GOAL>a * (b * b⁻¹) = a
<VAR>a b : EReal<VAR>h₁ : b ≠ ⊥<VAR>h₂ : b ≠ ⊤<VAR>h₃ : b ≠ 0<GOAL>a * (b / b) = a
<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 L₁ L₂ : Filter 𝕜<VAR>c : 𝕜 → 𝕜<VAR>c' : 𝕜<VAR>n : ℕ<VAR>hc : HasDerivAt c c' x<GOAL>HasDerivAt (fun y => c y ^ n) (↑n * c x ^ (n - 1) * c') x
<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 L₁ L₂ : Filter 𝕜<VAR>c : 𝕜 → 𝕜<VAR>c' : 𝕜<VAR>n : ℕ<VAR>hc : HasDerivWithinAt c c' univ x<GOAL>HasDerivWithinAt (fun y => c y ^ n) (↑n * c x ^ (n - 1) * c') univ x
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ : List α<VAR>f : α → α<VAR>l₁ l₂ : List α<VAR>x✝ : l₂ ≠ []<GOAL>modifyLast f (l₁ ++ l₂) = l₁ ++ modifyLast f l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : UpperSet α<VAR>t : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>has : ∀ b ∈ s, b ≤ a → b = a<GOAL>Ici a ⊓ s.erase a = s
<VAR>n m : ℕ<VAR>p : Fin (n + 1)<VAR>i✝ j i : Fin n<GOAL>(last n).succAbove i = i.castSucc
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<GOAL>Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, 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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hc : Cospherical {p₁, p₂, p₃, p₄}<GOAL>Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, 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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hc : Collinear ℝ {p₁, p₂, p₃, p₄}<GOAL>Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
<VAR>m n a b c✝ d c : ℕ<VAR>h : a % n = b % n<GOAL>c * a % (c * n) = c * b % (c * n)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>f' : G' →g G''<VAR>u v u' v' : V<VAR>p : G.Walk u v<VAR>hinj : Injective ⇑f<GOAL>(Walk.map f p).IsTrail ↔ p.IsTrail
<VAR>k n m : Nat<VAR>H : k.Coprime n<GOAL>(m * k).gcd n = m.gcd n
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i j : n<GOAL>A.adjugateᵀ i j = Aᵀ.adjugate i j
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i j : n<GOAL>(A.updateRow i (Pi.single j 1)).det = (A.updateColumn j (Pi.single i 1)).det
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i j : n<GOAL>∑ σ : Perm n, ↑↑(sign σ) * ∏ i_1 : n, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∑ σ : Perm n, ↑↑(sign σ) * ∏ i_1 : n, A.updateColumn j (Pi.single i 1) (σ i_1) i_1
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>i j : n<GOAL>∀ x ∈ univ, ↑↑(sign x) * ∏ i_1 : n, A.updateRow i (Pi.single j 1) (x i_1) i_1 = ↑↑(sign x) * ∏ i_1 : n, A.updateColumn j (Pi.single i 1) (x i_1) i_1
<VAR>α β : Type u<VAR>c : Cardinal.{u}<GOAL>ℵ₀ ≤ lift.{v, u} c ↔ ℵ₀ ≤ c
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a✝ b : WithBot α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>↑a * ⊥ = Option.bind ⊥ fun b => Option.some (a * b)
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a✝ b : WithBot α<VAR>a : α<VAR>ha : a ≠ 0<GOAL>⊥ = Option.bind ⊥ fun b => Option.some (a * b)
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<GOAL>(u, v) ∈ P.nonUniforms G ε ↔ u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some ⁻¹' Ico ↑a ↑b = Ico a b
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>y : G<GOAL>μ ((fun x => x * y) ⁻¹' s) = 0 ↔ μ ((fun x => y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>y : G<GOAL>μ ((fun x => y⁻¹ * x) ⁻¹' s⁻¹)⁻¹ = 0 ↔ μ s = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : CoheytingAlgebra α<VAR>inst✝¹ : CoheytingAlgebra β<VAR>inst✝ : CoheytingHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>f (a ∆ b) = f a ∆ f b
<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>i : ℕ<GOAL>C.d (i + 2) 0 = 0
<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>C : ChainComplex V ℕ<VAR>i : ℕ<GOAL>¬(ComplexShape.down ℕ).Rel (i + 2) 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁶ : FunLike F α β<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : Preorder β<VAR>inst✝² : Zero β<VAR>inst✝¹ : OrderHomClass F α β<VAR>inst✝ : ZeroHomClass F α β<VAR>f : F<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>0 ≤ f a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝⁶ : FunLike F α β<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : Preorder β<VAR>inst✝² : Zero β<VAR>inst✝¹ : OrderHomClass F α β<VAR>inst✝ : ZeroHomClass F α β<VAR>f : F<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>f 0 ≤ f a
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Ioi l) = ⨅ a, ⨅ (_ : a ≠ ⊤), 𝓟 (Ioi a)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>m : ℕ<VAR>φ : L.BoundedFormula α m<VAR>v : α → M<VAR>h' : m ≤ m<VAR>xs : Fin m → M<GOAL>(castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast ⋯)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝⁴ : Countable G<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : SMulInvariantMeasure G α ν<VAR>inst✝¹ : MeasurableSMul G α<VAR>i : SigmaFinite ν<VAR>i' : HasFundamentalDomain G α ν<VAR>μ : Measure (Quotient α_mod_G)<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<GOAL>SigmaFinite μ
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝⁴ : Countable G<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : SMulInvariantMeasure G α ν<VAR>inst✝¹ : MeasurableSMul G α<VAR>i : SigmaFinite ν<VAR>i' : HasFundamentalDomain G α ν<VAR>μ : Measure (Quotient α_mod_G)<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<GOAL>Nonempty (μ.FiniteSpanningSetsIn univ)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝⁴ : Countable G<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : SMulInvariantMeasure G α ν<VAR>inst✝¹ : MeasurableSMul G α<VAR>i : SigmaFinite ν<VAR>i' : HasFundamentalDomain G α ν<VAR>μ : Measure (Quotient α_mod_G)<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<VAR>A : ℕ → Set α<VAR>hA_meas : ∀ (i : ℕ), A i ∈ {s | MeasurableSet s}<VAR>hA : ∀ (i : ℕ), ν (A i) < ⊤<VAR>hA' : ⋃ i, A i = univ<GOAL>Nonempty (μ.FiniteSpanningSetsIn univ)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>E : Type u_5<VAR>inst✝⁷ : Group G<VAR>inst✝⁶ : MulAction G α<VAR>inst✝⁵ : MeasurableSpace α<VAR>ν : Measure α<VAR>inst✝⁴ : Countable G<VAR>inst✝³ : MeasurableSpace G<VAR>inst✝² : SMulInvariantMeasure G α ν<VAR>inst✝¹ : MeasurableSMul G α<VAR>i : SigmaFinite ν<VAR>i' : HasFundamentalDomain G α ν<VAR>μ : Measure (Quotient α_mod_G)<VAR>inst✝ : QuotientMeasureEqMeasurePreimage ν μ<VAR>A : ℕ → Set α<VAR>hA_meas : ∀ (i : ℕ), MeasurableSet (A i)<VAR>hA : ∀ (i : ℕ), ν (A i) < ⊤<VAR>hA' : ⋃ i, A i = univ<GOAL>Nonempty (μ.FiniteSpanningSetsIn univ)
<VAR>α✝ β✝ : Type u_1<VAR>a✝¹ : α✝ → PGame<VAR>a✝ : β✝ → PGame<GOAL>(mk α✝ β✝ a✝¹ a✝).Numeric ↔ (∀ (i : (mk α✝ β✝ a✝¹ a✝).LeftMoves) (j : (mk α✝ β✝ a✝¹ a✝).RightMoves), (mk α✝ β✝ a✝¹ a✝).moveLeft i < (mk α✝ β✝ a✝¹ a✝).moveRight j) ∧ (∀ (i : (mk α✝ β✝ a✝¹ a✝).LeftMoves), ((mk α✝ β✝ a✝¹ a✝).moveLeft i).Numeric) ∧ ∀ (j : (mk α✝ β✝ a✝¹ a✝).RightMoves), ((mk α✝ β✝ a✝¹ a✝).moveRight j).Numeric
<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>e : α ↪o β<VAR>he : IsUpperSet (range ⇑e)<VAR>a : α<GOAL>⇑e '' Ici a = Ici (e a)
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>nk : (n % k).beq 0 = false<VAR>h : MinFacHelper n k<GOAL>MinFacHelper n k'
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>nk : (n % k).beq 0 = false<VAR>h : MinFacHelper n k<VAR>h2 : n.minFac = k<GOAL>False
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>nk✝ : (n % k).beq 0 = false<VAR>h : MinFacHelper n k<VAR>h2 : n.minFac = k<VAR>nk : ¬n % k = 0<GOAL>False
<VAR>n k k' : ℕ<VAR>e : k + 2 = k'<VAR>nk✝ : (n % k).beq 0 = false<VAR>h : MinFacHelper n k<VAR>h2 : n.minFac = k<VAR>nk : ¬n.minFac ∣ n<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>x : β<VAR>f : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : FirstCountableTopology β<VAR>inst✝ : OrderTopology β<VAR>hf : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) (ae μ) f) _auto✝<GOAL>μ {y | f y < essInf f μ} = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>x : β<VAR>f : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : FirstCountableTopology β<VAR>inst✝ : OrderTopology β<VAR>hf : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) (ae μ) f) _auto✝<GOAL>μ {y | ¬essInf f μ ≤ f y} = 0
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y✝ f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<VAR>x : ℝ<VAR>hx : x ∈ S<VAR>y : ℝ<VAR>hy : y ∈ S<VAR>hxy : x ≤ y<GOAL>derivWithin f S x ≤ derivWithin f S y
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<VAR>x : ℝ<VAR>hx hy : x ∈ S<VAR>hxy : x ≤ x<GOAL>derivWithin f S x ≤ derivWithin f S x
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x✝ y✝ f' : ℝ<VAR>hfc : ConvexOn ℝ S f<VAR>hfd : DifferentiableOn ℝ f S<VAR>x : ℝ<VAR>hx : x ∈ S<VAR>y : ℝ<VAR>hy : y ∈ S<VAR>hxy : x ≤ y<VAR>hxy' : x < y<GOAL>derivWithin f S x ≤ derivWithin f S y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a✝ b✝ c d a b : α<VAR>h : b ≤ a<GOAL>a ∆ b = a \ b
<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₂.LeftHomologyData<VAR>γ : LeftHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<GOAL>homologyMap φ ≫ h₂.homologyIso.hom = h₁.homologyIso.hom ≫ γ.φH
<VAR>n a✝ : ℕ<GOAL>a✝ ∈ image Prod.fst n.divisorsAntidiagonal ↔ a✝ ∈ n.divisors
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h✝ : ContfracLegendre.Ass ξ u v<VAR>q : ℚ<VAR>h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)<GOAL>∃ n, (GenContFract.of ξ).convs n = ↑q
<VAR>ξ : ℝ<VAR>u v : ℤ<VAR>hv : 2 ≤ v<VAR>h✝ : ContfracLegendre.Ass ξ u v<VAR>q : ℚ<VAR>h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)<VAR>n : ℕ<VAR>hn : q = ξ.convergent n<GOAL>∃ n, (GenContFract.of ξ).convs n = ↑q
<VAR>X Y : Compactum<VAR>f : X ⟶ Y<GOAL>Continuous f.f
<VAR>X Y : Compactum<VAR>f : X ⟶ Y<GOAL>∀ (x : X.A) (g : Ultrafilter X.A), ↑g ≤ 𝓝 x → Tendsto f.f (↑g) (𝓝 (f.f x))
<VAR>X Y : Compactum<VAR>f : X ⟶ Y<VAR>x : X.A<VAR>g : Ultrafilter X.A<VAR>h : ↑g ≤ 𝓝 x<GOAL>Tendsto f.f (↑g) (𝓝 (f.f x))
<VAR>X Y : Compactum<VAR>f : X ⟶ Y<VAR>x : X.A<VAR>g : Ultrafilter X.A<VAR>h : ↑g ≤ 𝓝 x<GOAL>↑(Ultrafilter.map f.f g) ≤ 𝓝 (f.f x)
<VAR>X Y : Compactum<VAR>f : X ⟶ Y<VAR>x : X.A<VAR>g : Ultrafilter X.A<VAR>h : ↑g ≤ 𝓝 x<GOAL>Y.str (Ultrafilter.map f.f g) = f.f x
<VAR>X Y : Compactum<VAR>f : X ⟶ Y<VAR>x : X.A<VAR>g : Ultrafilter X.A<VAR>h : ↑g ≤ 𝓝 x<GOAL>↑g ≤ 𝓝 x
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝¹ : MonoidalCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : IsIso f<VAR>Z : C<GOAL>inv f ▷ Z ≫ f ▷ Z = 𝟙 (Y ⊗ Z)
<GOAL>∀ (n : ℕ), ↑(Nat.fib n) = (φ ^ n - ψ ^ n) / √5
<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => (1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2) (hurwitzZetaEven (↑a) s)
<VAR>a : ℝ<VAR>ha : a ∈ Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>(1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2 = (1 / ↑|↑n + a| ^ s + 1 / ↑|↑n + 1 - a| ^ s) / 2
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<GOAL>IsNoetherianRing R
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<GOAL>∀ (f : ℕ →o Submodule R R), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<VAR>I : ℕ →o Submodule R R<VAR>floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)<VAR>suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}<VAR>minN : R → ℕ := fun s => sInf (suitableN s)<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → I n = I m
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<VAR>I : ℕ →o Submodule R R<VAR>floc : (s : R) → R →+* Localization.Away s := fun s => algebraMap R (Localization.Away s)<VAR>suitableN : R → Set ℕ := fun s => {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}<VAR>minN : R → ℕ := fun s => sInf (suitableN s)<VAR>hSuit : ∀ (s : { x // x ∈ S }), minN ↑s ∈ suitableN ↑s<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → I n = I m