ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X✝ Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>J✝ B : Set α<VAR>f✝ x y : α<VAR>Js : Set (Set α)<VAR>hne : Js.Nonempty<VAR>hiI : M.Indep (⋂₀ Js)<VAR>e : α<VAR>he : ∀ i ∈ Js, e ∈ M.closure i<VAR>he' : M.Indep (insert e (⋂₀ Js))<VAR>J : Set α<VAR>heJ : insert e (⋂₀ Js) ⊆ J<VAR>f : α<VAR>hI : M.Indep (insert f (J \ {e}))<VAR>hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})<VAR>hiX : ⋂₀ Js ⊆ insert f (J \ {e})<VAR>heEI : e ∈ M.E \ insert f (J \ {e})<VAR>hJI : M.Basis J (insert e (insert f (J \ {e})))<VAR>hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))<VAR>hfIJ : f ∈ insert f (J \ {e}) \ J<VAR>hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))<VAR>X : Set α<VAR>hX' : X ∈ Js<VAR>hfX : f ∉ X<GOAL>False
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X✝ Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>J✝ B : Set α<VAR>f✝ x y : α<VAR>Js : Set (Set α)<VAR>hne : Js.Nonempty<VAR>hiI : M.Indep (⋂₀ Js)<VAR>e : α<VAR>he : ∀ i ∈ Js, e ∈ M.closure i<VAR>he' : M.Indep (insert e (⋂₀ Js))<VAR>J : Set α<VAR>heJ : insert e (⋂₀ Js) ⊆ J<VAR>f : α<VAR>hI : M.Indep (insert f (J \ {e}))<VAR>hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})<VAR>hiX : ⋂₀ Js ⊆ insert f (J \ {e})<VAR>heEI : e ∈ M.E \ insert f (J \ {e})<VAR>hJI : M.Basis J (insert e (insert f (J \ {e})))<VAR>hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))<VAR>hfIJ : f ∈ insert f (J \ {e}) \ J<VAR>hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))<VAR>X : Set α<VAR>hX' : X ∈ Js<VAR>hfX : f ∉ X<VAR>hd : M.Dep (insert e X)<GOAL>False
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X✝ Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>J✝ B : Set α<VAR>f✝ x y : α<VAR>Js : Set (Set α)<VAR>hne : Js.Nonempty<VAR>hiI : M.Indep (⋂₀ Js)<VAR>e : α<VAR>he : ∀ i ∈ Js, e ∈ M.closure i<VAR>he' : M.Indep (insert e (⋂₀ Js))<VAR>J : Set α<VAR>heJ : insert e (⋂₀ Js) ⊆ J<VAR>f : α<VAR>hI : M.Indep (insert f (J \ {e}))<VAR>hIs : ∀ J_1 ∈ Js, J_1 ⊆ insert f (J \ {e})<VAR>hiX : ⋂₀ Js ⊆ insert f (J \ {e})<VAR>heEI : e ∈ M.E \ insert f (J \ {e})<VAR>hJI : M.Basis J (insert e (insert f (J \ {e})))<VAR>hIb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))<VAR>hfIJ : f ∈ insert f (J \ {e}) \ J<VAR>hfb : M.Basis (insert f (J \ {e})) (insert e (insert f (J \ {e})))<VAR>X : Set α<VAR>hX' : X ∈ Js<VAR>hfX : f ∉ X<VAR>heX : e ∈ X<GOAL>False
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set (ULift.{v, u} X)<GOAL>IsOpen s ↔ IsOpen (up ⁻¹' s)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>w : ι → k<VAR>p : ι → P<VAR>b : P<GOAL>(s.weightedVSubOfPoint p b) w = ∑ i ∈ s, w i • (p i -ᵥ b)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>Q : Fin 3 → R<VAR>u : Rˣ<GOAL>W'.Nonsingular ((fun m => m • Q) u) ↔ W'.Nonsingular Q
<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>p : FormalMultilinearSeries 𝕜 E F<GOAL>p.radius = liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)<GOAL>p.radius = liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)<VAR>r : ℝ≥0<VAR>hr : ↑r < p.radius<GOAL>↑r ≤ liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop
<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>p : FormalMultilinearSeries 𝕜 E F<VAR>this : ∀ (r : ℝ≥0) {n : ℕ}, 0 < n → (↑r ≤ 1 / ↑(‖p n‖₊ ^ (1 / ↑n)) ↔ ‖p n‖₊ * r ^ n ≤ 1)<VAR>r : ℝ≥0<VAR>hr : ↑r < liminf (fun n => 1 / ↑(‖p n‖₊ ^ (1 / ↑n))) atTop<GOAL>↑r ≤ p.radius
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>V : ℕ → Set (α × α)<VAR>hV : ∀ (n : ℕ), V n ∈ 𝓤 α<VAR>u : ℕ → α<VAR>a : α<VAR>hu : Tendsto u atTop (𝓝 a)<GOAL>∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>V : ℕ → Set (α × α)<VAR>hV : ∀ (n : ℕ), V n ∈ 𝓤 α<VAR>u : ℕ → α<VAR>a : α<VAR>hu : Tendsto u atTop (𝓝 a)<VAR>n : ℕ<VAR>hn : ∀ b ≥ n, b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)<GOAL>∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>V : ℕ → Set (α × α)<VAR>hV : ∀ (n : ℕ), V n ∈ 𝓤 α<VAR>u : ℕ → α<VAR>a : α<VAR>hu : Tendsto u atTop (𝓝 a)<VAR>n : ℕ<VAR>hn : ∀ b ≥ n, b ∈ u ⁻¹' ball a (Prod.swap ⁻¹' V 0)<VAR>φ : ℕ → ℕ<VAR>φ_mono : StrictMono φ<VAR>hφV : ∀ (n_1 : ℕ), ((u ∘ fun a => a + n) (φ (n_1 + 1)), (u ∘ fun a => a + n) (φ n_1)) ∈ V (n_1 + 1)<GOAL>∃ φ, StrictMono φ ∧ (u (φ 0), a) ∈ V 0 ∧ ∀ (n : ℕ), (u (φ (n + 1)), u (φ n)) ∈ V (n + 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<GOAL>A = adjoint B ↔ ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<VAR>h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜<GOAL>A = adjoint B
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁹ : RCLike 𝕜<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : InnerProductSpace 𝕜 E<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : InnerProductSpace 𝕜 G<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : FiniteDimensional 𝕜 F<VAR>inst✝ : FiniteDimensional 𝕜 G<VAR>A : E →ₗ[𝕜] F<VAR>B : F →ₗ[𝕜] E<VAR>h : ∀ (x : E) (y : F), ⟪A x, y⟫_𝕜 = ⟪x, B y⟫_𝕜<VAR>x : E<GOAL>A x = (adjoint B) x
<VAR>x y : ℝ*<VAR>hx : ¬x.Infinitesimal<VAR>hy : y.Infinite<GOAL>(x * y).Infinite
<VAR>x y : ℝ*<VAR>hx : ¬x.Infinitesimal<VAR>hy : y.Infinite<GOAL>(y * x).Infinite
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>↑(ofZNum (ZNum.pos p)) = (↑p).toNat
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>↑(ofZNum (ZNum.pos p)) = (↑↑p).toNat
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G₁ G₂ : G.Subgraph<VAR>a b : V<VAR>H₁ H₂ : G.Subgraph<VAR>h : Disjoint H₁ H₂<GOAL>H₁.edgeSet ⊓ H₂.edgeSet ≤ ⊥
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b c d : X ⟶ Y<GOAL>a - c - (b - d) = a - b - (c - d)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b c d : X ⟶ Y<GOAL>prod.lift (prod.lift a b ≫ σ) (prod.lift c d ≫ σ) ≫ σ = a - b - (c - d)
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ TypeMax<VAR>x✝¹ : Cone F<VAR>x✝ : x✝¹.pt ⟶ (limitCone F).pt<VAR>w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j<GOAL>x✝ = (fun s v => ⟨fun j => s.π.app j v, ⋯⟩) x✝¹
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ TypeMax<VAR>x✝¹ : Cone F<VAR>x✝ : x✝¹.pt ⟶ (limitCone F).pt<VAR>w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j<VAR>x : x✝¹.pt<GOAL>x✝ x = (fun s v => ⟨fun j => s.π.app j v, ⋯⟩) x✝¹ x
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ TypeMax<VAR>x✝¹ : Cone F<VAR>x✝ : x✝¹.pt ⟶ (limitCone F).pt<VAR>w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j<VAR>x : x✝¹.pt<GOAL>↑(x✝ x) = ↑((fun s v => ⟨fun j => s.π.app j v, ⋯⟩) x✝¹ x)
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ TypeMax<VAR>x✝¹ : Cone F<VAR>x✝ : x✝¹.pt ⟶ (limitCone F).pt<VAR>w : ∀ (j : J), x✝ ≫ (limitCone F).π.app j = x✝¹.π.app j<VAR>x : x✝¹.pt<VAR>j : J<GOAL>↑(x✝ x) j = ↑((fun s v => ⟨fun j => s.π.app j v, ⋯⟩) x✝¹ x) j
<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>u v : V<VAR>h : G.Adj u v<GOAL>(Walk.cons h Walk.nil).IsPath
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t : Set α<VAR>Φ : α → β<VAR>hΦ : Isometry Φ<GOAL>infEdist (Φ x) (Φ '' t) = infEdist x t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>e'' : PartialEquiv γ δ<GOAL>((e.trans e').trans e'').source = (e.trans (e'.trans e'')).source
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>n : ℤ<GOAL>f (normEDS b c d n) = normEDS (f b) (f c) (f d) n
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulStrictMono α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a / b
<VAR>α : Type u_1<VAR>inst✝⁴ : Semifield α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : PosMulReflectLT α<VAR>inst✝¹ : ZeroLEOneClass α<VAR>a b : α<VAR>inst✝ : PosMulStrictMono α<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>0 < a * b⁻¹
<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>r.sign = 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<GOAL>s.max = ↑(s.max' H)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>H : s.Nonempty<VAR>x : α<GOAL>s.sup WithBot.some = s.sup (WithBot.some ∘ fun x => x)
<VAR>m n : ℕ<GOAL>max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
<VAR>m n : ℕ<VAR>h : m < n<GOAL>max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>max m n ^ 2 + min m n ≤ if m < n then n * n + m else m * m + m + n
<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>n ≤ m + n
<VAR>S : Type u_1<VAR>R R' : Type u<VAR>M : Type v<VAR>inst✝¹⁸ : CommSemiring S<VAR>inst✝¹⁷ : Semiring R<VAR>inst✝¹⁶ : CommSemiring R'<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Algebra S R<VAR>inst✝¹³ : Algebra S R'<VAR>inst✝¹² : Module S M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module Rᵐᵒᵖ M<VAR>inst✝⁹ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁸ : IsScalarTower S R M<VAR>inst✝⁷ : IsScalarTower S Rᵐᵒᵖ M<VAR>inst✝⁶ : Module R' M<VAR>inst✝⁵ : Module R'ᵐᵒᵖ M<VAR>inst✝⁴ : IsCentralScalar R' M<VAR>inst✝³ : IsScalarTower S R' M<VAR>A : Type u_2<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : Algebra R' A<VAR>f : R →ₐ[S] A<VAR>g : M →ₗ[S] A<VAR>hg : ∀ (x y : M), g x * g y = 0<VAR>hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x<VAR>hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r<VAR>r : R<GOAL>f r + g 0 = f r
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>k n : ℕ<VAR>μ : R<VAR>n' : ℕ<VAR>hn : k < n' + 1<VAR>hμ : IsPrimitiveRoot μ (n' + 1)<GOAL>∃ z ∈ adjoin ℤ {μ}, ↑(n' + 1) = z * (μ - 1) ^ k
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>k n : ℕ<VAR>μ : R<VAR>m : ℕ<VAR>hn : k < m + k + 1<VAR>hμ : IsPrimitiveRoot μ (m + k + 1)<GOAL>∃ z ∈ adjoin ℤ {μ}, ↑(m + k + 1) = z * (μ - 1) ^ k
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>k n : ℕ<VAR>μ : R<VAR>m : ℕ<VAR>hn : k < m + k + 1<VAR>hμ : IsPrimitiveRoot μ (m + k + 1)<VAR>hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)<VAR>Z : ℕ → R := fun k => Classical.choose ⋯<GOAL>∃ z ∈ adjoin ℤ {μ}, ↑(m + k + 1) = z * (μ - 1) ^ k
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>k n : ℕ<VAR>μ : R<VAR>m : ℕ<VAR>hn : k < m + k + 1<VAR>hμ : IsPrimitiveRoot μ (m + k + 1)<VAR>hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)<VAR>Z : ℕ → R := fun k => Classical.choose ⋯<VAR>Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)<GOAL>∃ z ∈ adjoin ℤ {μ}, ↑(m + k + 1) = z * (μ - 1) ^ k
<VAR>α✝ : Sort u_1<VAR>β✝ : Sort u_2<VAR>γ : Sort u_3<VAR>α : Type u_4<VAR>β : Type u_5<GOAL>IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : NonUnitalNonAssocSemiring α<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>v : n → R<VAR>j : n<VAR>x : R<VAR>i : n<GOAL>(Pi.single j x ᵥ* diagonal v) i = Pi.single j (x * v j) i
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : NonUnitalNonAssocSemiring α<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : NonUnitalNonAssocSemiring R<VAR>v : n → R<VAR>j : n<VAR>x : R<VAR>i : n<GOAL>Pi.single j x i * v i = Pi.single j (x * v j) i
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u} → Ordinal.{u}<VAR>c : Ordinal.{u}<VAR>hc : ℵ₀ < c.cof<VAR>hc' : o.card < c.cof<VAR>hf : ∀ (i : Ordinal.{u}) (hi : i < o), ∀ b < c, f i hi b < c<VAR>a : Ordinal.{u}<GOAL>Cardinal.lift.{u, u} o.card < c.cof
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>hs✝ : (map f S).FG<VAR>s : Finset B<VAR>hs : Algebra.adjoin R ↑s = map f S<GOAL>map f (Algebra.adjoin R ↑(s.preimage ⇑f ⋯)) = map f S
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>hs✝ : (map f S).FG<VAR>s : Finset B<VAR>hs : Algebra.adjoin R ↑s = map f S<GOAL>↑s ⊆ Set.range ⇑f
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>hs✝ : (map f S).FG<VAR>s : Finset B<VAR>hs : Algebra.adjoin R ↑s = map f S<GOAL>map f S ≤ map f ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s : Finset α<VAR>f : α ≃ β<VAR>b : β<GOAL>b ∈ map f.toEmbedding s ↔ f.symm b ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ : α ↪ β<VAR>s : Finset α<VAR>f : α ≃ β<VAR>b : β<GOAL>(∃ a ∈ s, f.toEmbedding a = b) ↔ f.symm b ∈ s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α✝<VAR>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_6<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>μ : Measure α<VAR>A_mble : MeasurableSet A<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>B : Set α<VAR>B_mble : MeasurableSet B<VAR>B_finmeas : μ B ≠ ⊤<VAR>As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>Tendsto (fun i => μ (As i)) L (𝓝 (μ A))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α✝<VAR>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_6<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>μ : Measure α<VAR>A_mble : MeasurableSet A<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>B : Set α<VAR>B_mble : MeasurableSet B<VAR>B_finmeas : μ B ≠ ⊤<VAR>As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>Tendsto (fun i => ∫⁻ (a : α), (As i).indicator 1 a ∂μ) L (𝓝 (∫⁻ (a : α), A.indicator 1 a ∂μ))
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α✝<VAR>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_6<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>μ : Measure α<VAR>A_mble : MeasurableSet A<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>B : Set α<VAR>B_mble : MeasurableSet B<VAR>B_finmeas : μ B ≠ ⊤<VAR>As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>∀ (x : ι), Measurable ((As x).indicator 1)
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α✝<VAR>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_6<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>μ : Measure α<VAR>A_mble : MeasurableSet A<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>B : Set α<VAR>B_mble : MeasurableSet B<VAR>B_finmeas : μ B ≠ ⊤<VAR>As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>∀ᶠ (n : ι) in L, ∀ᵐ (a : α) ∂μ, (As n).indicator 1 a ≤ B.indicator 1 a
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α✝<VAR>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_6<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>μ : Measure α<VAR>A_mble : MeasurableSet A<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>B : Set α<VAR>B_mble : MeasurableSet B<VAR>B_finmeas : μ B ≠ ⊤<VAR>As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ⊤
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m m0 : MeasurableSpace α✝<VAR>α : Type u_5<VAR>inst✝¹ : MeasurableSpace α<VAR>A : Set α<VAR>ι : Type u_6<VAR>L : Filter ι<VAR>inst✝ : L.IsCountablyGenerated<VAR>As : ι → Set α<VAR>μ : Measure α<VAR>A_mble : MeasurableSet A<VAR>As_mble : ∀ (i : ι), MeasurableSet (As i)<VAR>B : Set α<VAR>B_mble : MeasurableSet B<VAR>B_finmeas : μ B ≠ ⊤<VAR>As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B<VAR>h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A<GOAL>∀ᵐ (a : α) ∂μ, Tendsto (fun n => (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>R : Type u_12<VAR>R' : Type u_13<VAR>𝕜 : Type u_14<VAR>𝕜' : Type u_15<VAR>inst✝¹² : Norm E<VAR>inst✝¹¹ : Norm F<VAR>inst✝¹⁰ : Norm G<VAR>inst✝⁹ : SeminormedAddCommGroup E'<VAR>inst✝⁸ : SeminormedAddCommGroup F'<VAR>inst✝⁷ : SeminormedAddCommGroup G'<VAR>inst✝⁶ : NormedAddCommGroup E''<VAR>inst✝⁵ : NormedAddCommGroup F''<VAR>inst✝⁴ : NormedAddCommGroup G''<VAR>inst✝³ : SeminormedRing R<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedField 𝕜<VAR>inst✝ : NormedField 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>l l' : Filter α<VAR>h : f' =Θ[l] g'<GOAL>IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f') ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ g')
<VAR>B : Type u_1<VAR>W : Type u_2<VAR>inst✝ : Group W<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>t : W<VAR>ht : cs.IsReflection t<VAR>w : W<GOAL>cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A✝ B✝ A B : Matrix n n α<VAR>h : IsUnit A ↔ IsUnit B<GOAL>A⁻¹ - B⁻¹ = A⁻¹ * (B - A) * B⁻¹
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>u : R<GOAL>W'.dblZ (u • P) = u ^ 4 * W'.dblZ P
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → R<VAR>u : R<GOAL>u * P z * (u ^ 3 * P y - u ^ 3 * W'.negY P) = u ^ 4 * (P z * (P y - W'.negY P))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n : ℕ<VAR>h : n ≤ m<GOAL>Even (m - n) ↔ (Odd m ↔ Odd n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β<VAR>g : β → α<VAR>h : IsOrderRightAdjoint f g<VAR>e : γ ≃o α<VAR>y : β<GOAL>IsLUB (⇑e ⁻¹' {x | f x ≤ y}) (e.symm (g y))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β<VAR>g : β → α<VAR>h : IsOrderRightAdjoint f g<VAR>e : γ ≃o α<VAR>y : β<GOAL>IsLUB {x | f x ≤ y} (g y)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹¹ : Semifield R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : HasContinuousInv₀ R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f : R → R<VAR>a✝ : A<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>a : Aˣ<VAR>n : ℤ<GOAL>spectrum R ↑a ⊆ {0}ᶜ
<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>h : HasDerivAtFilter f f' x L<VAR>hL : f₁ =ᶠ[L] f<VAR>hx : f₁ x = f x<GOAL>HasDerivAtFilter f₁ f' x L
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : Fintype m<VAR>inst✝ : LinearOrderedField R<VAR>A : Matrix m n R<GOAL>finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin) = finrank R ↥(LinearMap.range A.mulVecLin)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>R : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : Fintype m<VAR>inst✝ : LinearOrderedField R<VAR>A : Matrix m n R<GOAL>(fun x => x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range (Aᵀ * A).mulVecLin)) = (fun x => x + finrank R ↥(LinearMap.ker A.mulVecLin)) (finrank R ↥(LinearMap.range A.mulVecLin))
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>N : Submodule R M<VAR>h : ∀ {x : L} {m : M}, m ∈ N.carrier → ⁅x, m⁆ ∈ N.carrier<GOAL>{ toSubmodule := N, lie_mem := h } = ⊤ ↔ N = ⊤
<VAR>R✝ : Type uR<VAR>inst✝⁴ : Semiring R✝<VAR>S : Type uS<VAR>inst✝³ : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>R : Type uR<VAR>inst✝ : Ring R<VAR>r : R → R → Prop<VAR>a b c : R<VAR>h : Rel r b c<GOAL>Rel r (a - b) (a - c)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : CommMonoid M<VAR>inst✝³ : CommMonoid N<VAR>inst✝² : DivisionCommMonoid G<VAR>k l : ℕ+<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>ζ : Rˣ<GOAL>ζ ∈ rootsOfUnity k R ↔ ↑ζ ∈ nthRoots (↑k) 1