ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>a : α<VAR>h1 : ∀ (h : ↥H), h • a = a → h = 1<VAR>h2 : ∀ (g : G), ∃ h, h • g • a = a<GOAL>H.IsComplement' (MulAction.stabilizer G a)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>a : α<VAR>h1 : ∀ (h : ↥H), h • a = a → h = 1<VAR>h2 : ∀ (g : G), ∃ h, h • g • a = a<VAR>g : G<GOAL>∃! x, ↑x.1 * ↑x.2 = g
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>a : α<VAR>h1 : ∀ (h : ↥H), h • a = a → h = 1<VAR>h2 : ∀ (g : G), ∃ h, h • g • a = a<VAR>g : G<VAR>h : ↥H<VAR>hh : h • g • a = a<GOAL>∃! x, ↑x.1 * ↑x.2 = g
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>a : α<VAR>h1 : ∀ (h : ↥H), h • a = a → h = 1<VAR>h2 : ∀ (g : G), ∃ h, h • g • a = a<VAR>g : G<VAR>h : ↥H<VAR>hh : h • g • a = a<VAR>hh' : (↑h * g) • a = a<GOAL>∃! x, ↑x.1 * ↑x.2 = g
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>a : α<VAR>h1 : ∀ (h : ↥H), h • a = a → h = 1<VAR>h2 : ∀ (g : G), ∃ h, h • g • a = a<VAR>g : G<VAR>h : ↥H<VAR>hh : h • g • a = a<VAR>hh' : (↑h * g) • a = a<GOAL>∀ (y : ↑↑H × ↑↑(MulAction.stabilizer G a)), (fun x => ↑x.1 * ↑x.2 = g) y → y = (h⁻¹, ⟨↑h * g, hh'⟩)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>a : α<VAR>h1 : ∀ (h : ↥H), h • a = a → h = 1<VAR>h2 : ∀ (g : G), ∃ h, h • g • a = a<VAR>h : ↥H<VAR>h' : ↑↑H<VAR>g : G<VAR>hg : g • a = a<VAR>hh : h • (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2) • a = a<VAR>hh' : (↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2)) • a = a<GOAL>(h', ⟨g, hg⟩) = (h⁻¹, ⟨↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2), hh'⟩)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>a : α<VAR>h2 : ∀ (g : G), ∃ h, h • g • a = a<VAR>h : ↥H<VAR>h' : ↑↑H<VAR>g : G<VAR>hg : g • a = a<VAR>hh : h • (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2) • a = a<VAR>hh' : (↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2)) • a = a<VAR>h1 : h * h' = 1<GOAL>(h', ⟨g, hg⟩) = (h⁻¹, ⟨↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2), hh'⟩)
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>α : Type u_2<VAR>inst✝ : MulAction G α<VAR>a : α<VAR>h2 : ∀ (g : G), ∃ h, h • g • a = a<VAR>h : ↥H<VAR>h' : ↑↑H<VAR>g : G<VAR>hg : g • a = a<VAR>hh : h • (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2) • a = a<VAR>hh' : (↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2)) • a = a<VAR>h1 : h * h' = 1<GOAL>↑(h', ⟨g, hg⟩).2 = ↑(h⁻¹, ⟨↑h * (↑(h', ⟨g, hg⟩).1 * ↑(h', ⟨g, hg⟩).2), hh'⟩).2
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : StrictOrderedRing R<VAR>inst✝ : Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in atBot, p x<GOAL>∀ᶠ (n : ℤ) in atBot, p ↑n
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : StrictOrderedRing R<VAR>inst✝ : Archimedean R<VAR>p : R → Prop<VAR>h : ∀ᶠ (x : R) in atBot, p x<GOAL>∀ᶠ (n : ℤ) in Filter.comap Int.cast atBot, p ↑n
<VAR>p : Char → Bool<VAR>s : String<GOAL>s.find p = { byteIdx := utf8Len (List.takeWhile (fun x => !p x) s.data) }
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>X : Type u<VAR>inst✝ : PseudoMetricSpace X<VAR>δ : ℝ<VAR>E : Set X<VAR>x : X<GOAL>x ∈ thickening δ E ↔ x ∈ ⋃ x ∈ E, ball x δ
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>δ✝ : ℝ<VAR>s : Set α<VAR>x✝ : α<VAR>X : Type u<VAR>inst✝ : PseudoMetricSpace X<VAR>δ : ℝ<VAR>E : Set X<VAR>x : X<GOAL>x ∈ thickening δ E ↔ ∃ i ∈ E, x ∈ ball i δ
<VAR>u✝ u : XgcdType<VAR>h : u.r ≠ 0<GOAL>(if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.step.reduce.flip
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Encodable β<VAR>f : β → Set α<VAR>C : Set α → Prop<VAR>H0 : C ∅<VAR>H1 : ∀ (b : β), C (f b)<VAR>n : ℕ<GOAL>C (⋃ b ∈ none, f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Encodable β<VAR>f : β → Set α<VAR>C : Set α → Prop<VAR>H0 : C ∅<VAR>H1 : ∀ (b : β), C (f b)<VAR>n : ℕ<GOAL>C ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Encodable β<VAR>f : β → Set α<VAR>C : Set α → Prop<VAR>H0 : C ∅<VAR>H1 : ∀ (b : β), C (f b)<VAR>n : ℕ<VAR>b : β<GOAL>⋃ b_1 ∈ some b, f b_1 = f b
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : M.Basis' I X<VAR>hJ : M.Basis' J X<GOAL>I.encard = J.encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J✝ X Y B J : Set α<VAR>e : α<VAR>hI : (M ↾ X).Base I<VAR>hJ : (M ↾ X).Base J<GOAL>I.encard = J.encard
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : AddCommMonoid R<VAR>s : Multiset R<GOAL>∀ (a : List R), trop (sum ⟦a⟧) = (map trop ⟦a⟧).prod
<VAR>a b c p q : ℚ<GOAL>p ≤ q ↔ p.num * ↑q.den ≤ q.num * ↑p.den
<VAR>a b c p q : ℚ<GOAL>p.num /. ↑p.den ≤ q.num /. ↑q.den ↔ (p.num /. ↑p.den).num * ↑(q.num /. ↑q.den).den ≤ (q.num /. ↑q.den).num * ↑(p.num /. ↑p.den).den
<VAR>a b c p q : ℚ<GOAL>p.num /. ↑p.den ≤ q.num /. ↑q.den ↔ p.num * ↑q.den ≤ q.num * ↑p.den
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X Y : C<VAR>f : J → C<VAR>g h : X ⊗ ⨁ f ⟶ Y<VAR>w : ∀ (j : J), X ◁ biproduct.ι f j ≫ g = X ◁ biproduct.ι f j ≫ h<GOAL>g = h
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X Y : C<VAR>f : J → C<VAR>g h : X ⊗ ⨁ f ⟶ Y<VAR>w : ∀ (j : J), X ◁ biproduct.ι f j ≫ g = X ◁ biproduct.ι f j ≫ h<GOAL>(leftDistributor X f).inv ≫ g = (leftDistributor X f).inv ≫ h
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X Y : C<VAR>f : J → C<VAR>g h : X ⊗ ⨁ f ⟶ Y<VAR>w : ∀ (j : J), X ◁ biproduct.ι f j ≫ g = X ◁ biproduct.ι f j ≫ h<VAR>j✝ : J<GOAL>biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ g = biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ h
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X Y : C<VAR>f : J → C<VAR>g h : X ⊗ ⨁ f ⟶ Y<VAR>w : ∀ (j : J), X ◁ biproduct.ι f j ≫ g = X ◁ biproduct.ι f j ≫ h<VAR>j✝ : J<GOAL>X ◁ biproduct.ι f j✝ ≫ g = X ◁ biproduct.ι f j✝ ≫ h
<VAR>θ : Angle<GOAL>↑θ.toReal = θ
<VAR>x✝ : ℝ<GOAL>↑(↑x✝).toReal = ↑x✝
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ ν : Measure Ω<GOAL>levyProkhorovEDist μ ν = levyProkhorovEDist ν μ
<VAR>x y : ℂ<VAR>n : ℕ<VAR>z : ℂ<GOAL>(cos z + sin z * I) ^ n = cos (↑n * z) + sin (↑n * z) * I
<VAR>x y : ℂ<VAR>n : ℕ<VAR>z : ℂ<GOAL>cexp (z * I) ^ n = cexp (↑n * z * I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>inst✝ : CommGroup G<GOAL>[].alternatingProd = ∏ i : Fin [].length, [].get i ^ (-1) ^ ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>inst✝ : CommGroup G<GOAL>∀ x ∈ univ, [].get x ^ (-1) ^ ↑x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>inst✝ : CommGroup G<VAR>g : G<GOAL>g = ∏ i : Fin 1, [g].get i ^ (-1) ^ ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>inst✝ : CommGroup G<VAR>g : G<GOAL>g = [g].get 0 ^ (-1) ^ ↑0 * ∏ i : Fin 0, [g].get i.succ ^ (-1) ^ ↑i.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>inst✝ : CommGroup G<VAR>g h : G<VAR>L : List G<GOAL>g * h⁻¹ * ∏ i : Fin L.length, L.get i ^ (-1) ^ ↑i = ∏ i : Fin (L.length + 2), (g :: h :: L).get i ^ (-1) ^ ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>inst✝ : CommGroup G<VAR>g h : G<VAR>L : List G<GOAL>g * (h⁻¹ * ∏ i : Fin L.length, L.get i ^ (-1) ^ ↑i) = (g :: h :: L).get 0 ^ (-1) ^ ↑0 * ((g :: h :: L).get (Fin.succ 0) ^ (-1) ^ ↑(Fin.succ 0) * ∏ i : Fin L.length, (g :: h :: L).get i.succ.succ ^ (-1) ^ ↑i.succ.succ)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>ι : Type u_3<VAR>b : ι → Set E<VAR>p : ι → Prop<VAR>hbasis : (𝓝 0).HasBasis p b<VAR>hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)<VAR>x : E<GOAL>(𝓝 x).HasBasis ((fun x => p) x) ((fun x i => (fun x_1 => x + x_1) '' b i) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>ι : Type u_3<VAR>b : ι → Set E<VAR>p : ι → Prop<VAR>hbasis : (𝓝 0).HasBasis p b<VAR>hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)<VAR>x : E<GOAL>(map (fun x_1 => x + x_1) (𝓝 0)).HasBasis ((fun x => p) x) ((fun x i => (fun x_1 => x + x_1) '' b i) x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>s✝ t : Interval α<VAR>a b : α<VAR>s : Interval α<GOAL>↑(dual s) = ⇑ofDual ⁻¹' ↑s
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>↑p ^ (n + 1) * polyOfInterest p n = remainder p n - wittPolyProdRemainder p (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>↑p ^ (n + 1) * wittMul p (n + 1) + ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) = ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) + (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) + (remainder p n - wittPolyProdRemainder p (n + 1)))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : Type u_1<VAR>inst✝ : CommRing k<VAR>n : ℕ<GOAL>-(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) + ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) + ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) + (remainder p n - wittPolyProdRemainder p (n + 1)) + ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) = ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) + (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) + (remainder p n - wittPolyProdRemainder p (n + 1)))
<VAR>F : Type u_1<VAR>inst✝¹⁰ : Field F<VAR>E : Type u_2<VAR>inst✝⁹ : Field E<VAR>inst✝⁸ : Algebra F E<VAR>S✝ : Set E<VAR>L : Type u_3<VAR>L' : Type u_4<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field L'<VAR>inst✝⁵ : Algebra F L<VAR>inst✝⁴ : Algebra L E<VAR>inst✝³ : Algebra F L'<VAR>inst✝² : Algebra L' E<VAR>inst✝¹ : IsScalarTower F L E<VAR>inst✝ : IsScalarTower F L' E<VAR>i : L ≃ₐ[F] L'<VAR>hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i<VAR>S : Set E<GOAL>restrictScalars F (adjoin L S) = restrictScalars F (adjoin L' S)
<VAR>F : Type u_1<VAR>inst✝¹⁰ : Field F<VAR>E : Type u_2<VAR>inst✝⁹ : Field E<VAR>inst✝⁸ : Algebra F E<VAR>S✝ : Set E<VAR>L : Type u_3<VAR>L' : Type u_4<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field L'<VAR>inst✝⁵ : Algebra F L<VAR>inst✝⁴ : Algebra L E<VAR>inst✝³ : Algebra F L'<VAR>inst✝² : Algebra L' E<VAR>inst✝¹ : IsScalarTower F L E<VAR>inst✝ : IsScalarTower F L' E<VAR>i : L ≃ₐ[F] L'<VAR>hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i<VAR>S : Set E<GOAL>(restrictScalars F (adjoin L S)).toSubfield = (restrictScalars F (adjoin L' S)).toSubfield
<VAR>F : Type u_1<VAR>inst✝¹⁰ : Field F<VAR>E : Type u_2<VAR>inst✝⁹ : Field E<VAR>inst✝⁸ : Algebra F E<VAR>S✝ : Set E<VAR>L : Type u_3<VAR>L' : Type u_4<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : Field L'<VAR>inst✝⁵ : Algebra F L<VAR>inst✝⁴ : Algebra L E<VAR>inst✝³ : Algebra F L'<VAR>inst✝² : Algebra L' E<VAR>inst✝¹ : IsScalarTower F L E<VAR>inst✝ : IsScalarTower F L' E<VAR>i : L ≃ₐ[F] L'<VAR>hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i<VAR>S : Set E<VAR>x : E<GOAL>x ∈ Set.range ⇑(algebraMap L E) ↔ x ∈ Set.range ⇑(algebraMap L' E)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<GOAL>IsNilpotent ⊥.jacobson
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<GOAL>IsNilpotent ⊥.jacobson
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<GOAL>IsNilpotent ⊥.jacobson
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<GOAL>⊥.jacobson ^ n = 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<GOAL>J = ⊤
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<VAR>hJ : ¬J = ⊤<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<VAR>hJ : J ≠ ⊤<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<VAR>hJ : J ≠ ⊤<VAR>J' : Submodule R R<VAR>hJJ' : J < J'<VAR>hJ' : ∀ (I : Ideal R), J < I → ¬I < J'<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<VAR>hJ : J ≠ ⊤<VAR>J' : Submodule R R<VAR>hJJ' : J < J'<VAR>hJ' : ∀ (I : Ideal R), J < I → ¬I < J'<VAR>x : R<VAR>hxJ' : x ∈ J'<VAR>hxJ : x ∉ J<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<VAR>hJ : J ≠ ⊤<VAR>x : R<VAR>hxJ : x ∉ J<VAR>hJJ' : J < J ⊔ Ideal.span {x}<VAR>hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}<VAR>hxJ' : x ∈ J ⊔ Ideal.span {x}<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<VAR>hJ : J ≠ ⊤<VAR>x : R<VAR>hxJ : x ∉ J<VAR>hJJ' : J < J ⊔ Ideal.span {x}<VAR>hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}<VAR>hxJ' : x ∈ J ⊔ Ideal.span {x}<VAR>this : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<VAR>hJ : J ≠ ⊤<VAR>x : R<VAR>hxJ : x ∉ J<VAR>hJJ' : J < J ⊔ Ideal.span {x}<VAR>hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}<VAR>hxJ' : x ∈ J ⊔ Ideal.span {x}<VAR>this✝ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}<VAR>this : Jac * Ideal.span {x} ≤ J<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<VAR>hJ : J ≠ ⊤<VAR>x : R<VAR>hxJ : x ∉ J<VAR>hJJ' : J < J ⊔ Ideal.span {x}<VAR>hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}<VAR>hxJ' : x ∈ J ⊔ Ideal.span {x}<VAR>this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}<VAR>this✝ : Jac * Ideal.span {x} ≤ J<VAR>this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<VAR>hJ : J ≠ ⊤<VAR>x : R<VAR>hxJ : x ∉ J<VAR>hJJ' : J < J ⊔ Ideal.span {x}<VAR>hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}<VAR>hxJ' : x ∈ J ⊔ Ideal.span {x}<VAR>this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}<VAR>this✝ : Jac * Ideal.span {x} ≤ J<VAR>this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥<VAR>y : R<VAR>hy : y ∈ Jac ^ n<GOAL>x • y ∈ ⊥
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsArtinianRing R<VAR>Jac : Ideal R := ⊥.jacobson<VAR>f : ℕ →o (Ideal R)ᵒᵈ := { toFun := fun n => Jac ^ n, monotone' := ⋯ }<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → Jac ^ n = Jac ^ m<VAR>J : Ideal R := annihilator (Jac ^ n)<VAR>hJ : J ≠ ⊤<VAR>x : R<VAR>hxJ : x ∉ J<VAR>hJJ' : J < J ⊔ Ideal.span {x}<VAR>hJ' : ∀ (I : Ideal R), J < I → ¬I < J ⊔ Ideal.span {x}<VAR>hxJ' : x ∈ J ⊔ Ideal.span {x}<VAR>this✝¹ : J ⊔ Jac • Ideal.span {x} ≤ J ⊔ Ideal.span {x}<VAR>this✝ : Jac * Ideal.span {x} ≤ J<VAR>this : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥<VAR>y : R<VAR>hy : y ∈ Jac ^ n<GOAL>y ∈ Jac ^ (n + 1)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>n : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : NeZero ↑n<GOAL>(cyclotomic n R).roots = (primitiveRoots n R).val
<VAR>s : Set Ordinal.{u}<VAR>a✝ : Ordinal.{u}<VAR>a : Ordinal.{u_1}<GOAL>𝓝[≤] a = 𝓝 a
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J✝ K L : Ideal R<VAR>s : Finset ι<VAR>J : ι → Ideal R<VAR>h : ∀ i ∈ s, J i ⊔ I = ⊤<GOAL>(⨅ i ∈ s, J i) ⊔ I = ⊤
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J✝ K L : Ideal R<VAR>s : Finset ι<VAR>J : ι → Ideal R<VAR>h : ∀ i ∈ s, J i ⊔ I = ⊤<GOAL>∀ i ∈ s, I ⊔ J i = ⊤
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J✝ K L : Ideal R<VAR>s : Finset ι<VAR>J : ι → Ideal R<VAR>h : ∀ i ∈ s, J i ⊔ I = ⊤<VAR>i : ι<VAR>hi : i ∈ s<GOAL>I ⊔ J i = ⊤
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemiring α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>⌈a⌉₊ = 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<VAR>f : ι → UpperSet α<GOAL>a ∈ ⨅ i, f i ↔ ∃ i, a ∈ f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<VAR>f : ι → UpperSet α<GOAL>a ∈ ⋃ i, ↑(f i) ↔ ∃ i, a ∈ f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>f : α → Finset β<VAR>s : Finset α<VAR>b a : β<GOAL>a ∈ (s.biUnion f).erase b ↔ a ∈ s.biUnion fun x => (f x).erase b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>f : α → Finset β<VAR>s : Finset α<VAR>b a : β<GOAL>(¬a = b ∧ ∃ a_1 ∈ s, a ∈ f a_1) ↔ ∃ a_1 ∈ s, ¬a = b ∧ a ∈ f a_1
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<GOAL>(ad R L).IsIdealMorphism
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<GOAL>∀ (x : LieDerivation R L L) (y : L), ∃ z, (ad R L) (x y) = (ad R L) z
<VAR>α : Type u_1<GOAL>∀ (m n : Num), ↑(m.ldiff n) = (↑m).ldiff ↑n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<GOAL>1 + ω = ω
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<GOAL>1 + ω ≤ ω
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<GOAL>type (Sum.Lex EmptyRelation fun x x_1 => x < x_1) ≤ type fun x x_1 => x < x_1
<VAR>α : Type u_2<VAR>n : ℕ<VAR>xs : Vector α n<VAR>σ₁ : Type<VAR>β : Type u_1<VAR>σ₂ : Type<VAR>f₁ : α → σ₁ → σ₁ × β<VAR>f₂ : α → σ₂ → σ₂ × β<VAR>R : σ₁ → σ₂ → Prop<VAR>hR : ∀ {s : σ₁} {q : σ₂} (a : α), R s q → R (f₁ a s).1 (f₂ a q).1 ∧ (f₁ a s).2 = (f₂ a q).2<VAR>n✝ : ℕ<VAR>xs✝ : Vector α n✝<VAR>x✝ : α<VAR>a✝ : ∀ {s₁ : σ₁} {s₂ : σ₂}, R s₁ s₂ → R (mapAccumr f₁ xs✝ s₁).1 (mapAccumr f₂ xs✝ s₂).1 ∧ (mapAccumr f₁ xs✝ s₁).2 = (mapAccumr f₂ xs✝ s₂).2<VAR>s₁ : σ₁<VAR>s₂ : σ₂<VAR>h₀ : R s₁ s₂<GOAL>R (mapAccumr f₁ (xs✝.snoc x✝) s₁).1 (mapAccumr f₂ (xs✝.snoc x✝) s₂).1 ∧ (mapAccumr f₁ (xs✝.snoc x✝) s₁).2 = (mapAccumr f₂ (xs✝.snoc x✝) s₂).2
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>s U F : Set X<VAR>x : X<VAR>hU : IsOpen U<GOAL>U =ᶠ[ae μ] ∅ ↔ U = ∅
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝⁵ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝² : (i : ι) → Module R (M₁ i)<VAR>inst✝¹ : Module R M₂<VAR>f f' : MultilinearMap R M₁ M₂<VAR>inst✝ : Fintype ι<VAR>c : ι → R<VAR>m : (i : ι) → M₁ i<GOAL>(f fun i => c i • m i) = (∏ i : ι, c i) • f m
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z✝ : ℤ<VAR>a✝ : α<VAR>z a : ℤ<GOAL>⌈↑z⌉ ≤ a ↔ z ≤ a
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>V : Set G<GOAL>index ∅ V = 0
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>V : Set G<GOAL>0 ∈ Finset.card '' {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V} ∨ Finset.card '' {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V} = ∅
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>V : Set G<GOAL>0 ∈ Finset.card '' {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V}
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>V : Set G<GOAL>∅ ∈ {t | ∅ ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V} ∧ ∅.card = 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Lattice (α i)<VAR>inst✝ : DecidableEq ι<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>b : α i<GOAL>update f i '' uIcc (f i) b = uIcc f (update f i b)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike K<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace K E<VAR>inst✝ : FiniteDimensional K E<VAR>this : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E<GOAL>ProperSpace E
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : RCLike K<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace K E<VAR>inst✝ : FiniteDimensional K E<VAR>this✝ : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ K E<VAR>this : FiniteDimensional ℝ E := trans ℝ K E<GOAL>ProperSpace E
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F G H : Cᵒᵖ ⥤ D<VAR>α : F.rightOp ⟶ G.rightOp<VAR>X Y : Cᵒᵖ<VAR>f : X ⟶ Y<GOAL>(G.map f ≫ (fun X => (α.app (unop X)).unop) Y).op = ((fun X => (α.app (unop X)).unop) X ≫ F.map f).op
<VAR>X : Scheme<VAR>ι : Sort u_1<VAR>S : ι → ↑X.affineOpens<VAR>hS : ⨆ i, ↑(S i) = ⊤<VAR>hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))<VAR>U : ↑X.affineOpens<GOAL>IsNoetherianRing ↑Γ(X, ↑U)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<GOAL>IsIntegralClosure (CyclotomicRing p ℤ ℚ) ℤ (CyclotomicField p ℚ)