ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>P : Sylow (Nat.card ↥N).minFac ↥N<VAR>this : Fact (Nat.Prime (Nat.card ↥N).minFac)<GOAL>↑P ≠ ⊥
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>inst✝¹ : Finite G<VAR>N : Subgroup G<VAR>inst✝ : N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>P : Sylow (Nat.card ↥N).minFac ↥N<VAR>this : Fact (Nat.Prime (Nat.card ↥N).minFac)<GOAL>(Nat.card ↥N).minFac ∣ Nat.card ↥N
<VAR>α : Type u_1<VAR>inst✝ : AddCommGroup α<VAR>c : ℤ<GOAL>smulg c 0 = 0
<VAR>x : ℂ<VAR>n : ℕ<GOAL>abs (x ^ (↑n)⁻¹) = abs x ^ (↑n)⁻¹
<VAR>x : ℂ<VAR>n : ℕ<GOAL>abs (x ^ (↑n)⁻¹) = abs (x ^ ↑(↑n)⁻¹)
<VAR>X : Type u_3<VAR>Y : ?m.21441<VAR>A✝ : Type ?u.21450<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace A✝<VAR>E : Type u_1<VAR>A : Type u_2<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalSpace A<VAR>p : E → X<VAR>sep : IsSeparatedMap p<VAR>inj : IsLocallyInjective p<VAR>s : Set A<VAR>hs : IsPreconnected s<VAR>g g₁ g₂ : A → E<VAR>inst✝ : PreconnectedSpace A<VAR>h₁ : Continuous g₁<VAR>h₂ : Continuous g₂<VAR>he : p ∘ g₁ = p ∘ g₂<VAR>a : A<VAR>ha : g₁ a = g₂ a<VAR>a' : A<GOAL>g₁ a' = g₂ a'
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCommMonoid G<GOAL>∀ (x y : k[G]ᵐᵒᵖ), __src✝.toFun (x * y) = __src✝.toFun x * __src✝.toFun y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCommMonoid G<GOAL>∀ (x y : k[G]ᵐᵒᵖ), ↑__src✝ (x * y) = ↑__src✝ x * ↑__src✝ y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCommMonoid G<GOAL>∀ (x y : k[G]ᵐᵒᵖ), __src✝ (x * y) = __src✝ x * __src✝ y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCommMonoid G<GOAL>∀ (x y : k[G]ᵐᵒᵖ), __src✝.toAddMonoidHom (x * y) = __src✝.toAddMonoidHom x * __src✝.toAddMonoidHom y
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCommMonoid G<GOAL>AddMonoidHom.mul.compr₂ __src✝.toAddMonoidHom = (AddMonoidHom.mul.comp __src✝.toAddMonoidHom).compl₂ __src✝.toAddMonoidHom
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCommMonoid G<VAR>i₁ : G<VAR>r₁ : k<VAR>i₂ : G<VAR>r₂ : k<GOAL>((((((AddMonoidHom.mul.compr₂ __src✝.toAddMonoidHom).comp opAddEquiv.toAddMonoidHom).comp (singleAddHom i₁)) r₁).comp opAddEquiv.toAddMonoidHom).comp (singleAddHom i₂)) r₂ = (((((((AddMonoidHom.mul.comp __src✝.toAddMonoidHom).compl₂ __src✝.toAddMonoidHom).comp opAddEquiv.toAddMonoidHom).comp (singleAddHom i₁)) r₁).comp opAddEquiv.toAddMonoidHom).comp (singleAddHom i₂)) r₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCommMonoid G<VAR>i₁ : G<VAR>r₁ : k<VAR>i₂ : G<VAR>r₂ : k<GOAL>↑(opAddEquiv.symm.trans (mapRange.addEquiv opAddEquiv)) (opAddEquiv (Finsupp.single i₁ r₁) * opAddEquiv (Finsupp.single i₂ r₂)) = ↑(opAddEquiv.symm.trans (mapRange.addEquiv opAddEquiv)) (opAddEquiv (Finsupp.single i₁ r₁)) * ↑(opAddEquiv.symm.trans (mapRange.addEquiv opAddEquiv)) (opAddEquiv (Finsupp.single i₂ r₂))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCommMonoid G<VAR>i₁ : G<VAR>r₁ : k<VAR>i₂ : G<VAR>r₂ : k<GOAL>(mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₁ r₁) * opAddEquiv (Finsupp.single i₂ r₂))) = (mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₁ r₁))) * (mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₂ r₂)))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCommMonoid G<VAR>i₁ : G<VAR>r₁ : k<VAR>i₂ : G<VAR>r₂ : k<GOAL>(mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₂ r₂)) * unop (opAddEquiv (Finsupp.single i₁ r₁))) = (mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₁ r₁))) * (mapRange.addEquiv opAddEquiv) (unop (opAddEquiv (Finsupp.single i₂ r₂)))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCommMonoid G<VAR>i₁ : G<VAR>r₁ : k<VAR>i₂ : G<VAR>r₂ : k<GOAL>mapRange op ⋯ (unop (opAddEquiv (Finsupp.single i₂ r₂)) * unop (opAddEquiv (Finsupp.single i₁ r₁))) = mapRange op ⋯ (unop (opAddEquiv (Finsupp.single i₁ r₁))) * mapRange op ⋯ (unop (opAddEquiv (Finsupp.single i₂ r₂)))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCommMonoid G<VAR>i₁ : G<VAR>r₁ : k<VAR>i₂ : G<VAR>r₂ : k<GOAL>Finsupp.single (i₂ + i₁) (op (r₂ * r₁)) = Finsupp.single i₁ (op r₁) * Finsupp.single i₂ (op r₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Finite α<VAR>this : Fintype α<GOAL>Nat.card (α → β) = Nat.card β ^ Nat.card α
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>n : ℕ<GOAL>∑ k ∈ range n, 2 ^ k • f (2 ^ (k + 1)) ≤ ∑ k ∈ Ico 2 (2 ^ n + 1), f k
<VAR>M : Type u_1<VAR>inst✝ : OrderedAddCommMonoid M<VAR>f : ℕ → M<VAR>u : ℕ → ℕ<VAR>hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m<VAR>n x✝ : ℕ<VAR>a✝ : x✝ ∈ range n<GOAL>2 ^ x✝ • f (2 ^ (x✝ + 1)) = (2 ^ (x✝ + 1) - 2 ^ x✝) • f (2 ^ (x✝ + 1))
<VAR>R : Type u<VAR>X : Type v<VAR>inst✝² : CommRing R<VAR>L : Type w<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>f : X → L<VAR>x : X<GOAL>((lift R) f) (of R x) = f x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>N a b : ℕ<VAR>hab : revAtFun N a = revAtFun N b<GOAL>a = b
<VAR>C : Type u<VAR>𝒞 : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>W ◁ (f ≫ g) = W ◁ f ≫ W ◁ g
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>as : Array α<VAR>f : α → m β<VAR>motive : Nat → Prop<VAR>h0 : motive 0<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])<GOAL>SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ arr[i]) (mapM f as)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>as : Array α<VAR>f : α → m β<VAR>motive : Nat → Prop<VAR>h0 : motive 0<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])<GOAL>SatisfiesM (fun arr => motive as.size ∧ ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ arr[i]) (foldlM (fun bs a => bs.push <$> f a) #[] as 0)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>as : Array α<VAR>f : α → m β<VAR>motive : Nat → Prop<VAR>h0 : motive 0<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])<GOAL>(fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) 0 #[]
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>as : Array α<VAR>f : α → m β<VAR>motive : Nat → Prop<VAR>h0 : motive 0<VAR>p : Fin as.size → β → Prop<VAR>hs : ∀ (i : Fin as.size), motive ↑i → SatisfiesM (fun x => p i x ∧ motive (↑i + 1)) (f as[i])<GOAL>∀ (i : Fin as.size) (b : Array β), (fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) (↑i) b → SatisfiesM ((fun i arr => motive i ∧ arr.size = i ∧ ∀ (i : Fin as.size) (h2 : ↑i < arr.size), p i arr[↑i]) (↑i + 1)) (b.push <$> f as[i])
<VAR>R : Type u_1<VAR>m : Type u_2<VAR>m₁ : Type u_3<VAR>m₂ : Type u_4<VAR>n : Type u_5<VAR>n₁ : Type u_6<VAR>n₂ : Type u_7<VAR>inst✝¹² : Fintype m<VAR>inst✝¹¹ : Fintype m₁<VAR>inst✝¹⁰ : Fintype m₂<VAR>inst✝⁹ : Fintype n<VAR>inst✝⁸ : Fintype n₁<VAR>inst✝⁷ : Fintype n₂<VAR>inst✝⁶ : DecidableEq m<VAR>inst✝⁵ : DecidableEq m₁<VAR>inst✝⁴ : DecidableEq m₂<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : DecidableEq n₁<VAR>inst✝¹ : DecidableEq n₂<VAR>inst✝ : Semiring R<VAR>A : Matrix m n R<VAR>B₁ : Matrix n n₁ R<VAR>B₂ : Matrix n n₂ R<GOAL>A * B₁.fromColumns B₂ = (A * B₁).fromColumns (A * B₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq β<VAR>f g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b c : β<GOAL>image f s ⊆ t ↔ f '' ↑s ⊆ ↑t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>as₀ as₁ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁<VAR>bs : Multiset β<GOAL>Rel r (a ::ₘ s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r (a ::ₘ s) bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>p : γ → δ → Prop<VAR>as₀ as₁ : Multiset α<VAR>a : α<VAR>s : Multiset α<VAR>ih : ∀ {bs : Multiset β}, Rel r (s + as₁) bs ↔ ∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁<VAR>bs : Multiset β<GOAL>(∃ b bs', r a b ∧ (∃ bs₀ bs₁, Rel r s bs₀ ∧ Rel r as₁ bs₁ ∧ bs' = bs₀ + bs₁) ∧ bs = b ::ₘ bs') ↔ ∃ bs₀ bs₁, (∃ b bs', r a b ∧ Rel r s bs' ∧ bs₀ = b ::ₘ bs') ∧ Rel r as₁ bs₁ ∧ bs = bs₀ + bs₁
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Mono f ↔ Function.Injective ⇑((forget₂ C Ab).map f)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>inst✝⁵ : ConcreteCategory C<VAR>inst✝⁴ : HasForget₂ C Ab<VAR>inst✝³ : Preadditive C<VAR>inst✝² : (forget₂ C Ab).Additive<VAR>inst✝¹ : (forget₂ C Ab).PreservesHomology<VAR>inst✝ : HasZeroObject C<VAR>S : ShortComplex C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Mono f ↔ Mono ((forget₂ C Ab).map f)
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>F : Type u_2<VAR>E : Type u_3<VAR>inst✝² : CommRing F<VAR>inst✝¹ : Ring E<VAR>inst✝ : Algebra F E<GOAL>finrank F ↥⊤ = finrank F ↥⊤
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝¹⁰ : Ring R<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>F : Type u_2<VAR>E : Type u_3<VAR>inst✝² : CommRing F<VAR>inst✝¹ : Ring E<VAR>inst✝ : Algebra F E<GOAL>finrank F ↥⊤ = finrank F ↥(Subalgebra.toSubmodule ⊤)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁵ : Countable ι<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>f g : α → β<VAR>M : Type u_5<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ContinuousMul M<VAR>s : Multiset (α → M)<VAR>hs : ∀ f ∈ s, AEStronglyMeasurable f μ<GOAL>AEStronglyMeasurable (fun x => (Multiset.map (fun f => f x) s).prod) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>hl : l.HasBasis p s<VAR>x : α<GOAL>(l ⊔ pure x).HasBasis p fun i => s i ∪ {x}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>x : M<VAR>ht : t ∈ 𝓝 x<GOAL>↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝 (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>x : M<VAR>ht : t ∈ 𝓝 x<GOAL>t ∈ 𝓝 (↑(extChartAt I x).symm (↑(extChartAt I x) x))
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : NormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousSMul 𝕜 E<VAR>inst✝ : ContinuousAdd E<VAR>s t : Set E<GOAL>IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<GOAL>(s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t
<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsArtinian R M<VAR>h_wf : WellFounded fun x x_1 => x > x_1<GOAL>∀ᶠ (l : ℕ) in Filter.atTop, ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l
<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsArtinian R M<VAR>h_wf : WellFounded fun x x_1 => x > x_1<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m<GOAL>∀ᶠ (l : ℕ) in Filter.atTop, ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l
<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsArtinian R M<VAR>h_wf : WellFounded fun x x_1 => x > x_1<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m<VAR>l : ℕ<VAR>hl : l ≥ n<VAR>m : ℕ<GOAL>lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m
<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsArtinian R M<VAR>h_wf : WellFounded fun x x_1 => x > x_1<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m<VAR>l : ℕ<VAR>hl : l ≥ n<VAR>m : ℕ<VAR>h : l ≤ m<GOAL>lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m
<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R M₂<VAR>inst✝² : LieRingModule L M₂<VAR>inst✝¹ : LieModule R L M₂<VAR>inst✝ : IsArtinian R M<VAR>h_wf : WellFounded fun x x_1 => x > x_1<VAR>n : ℕ<VAR>hn : ∀ (m : ℕ), n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m<VAR>l : ℕ<VAR>hl : l ≥ n<VAR>m : ℕ<VAR>h : m < l<GOAL>lowerCentralSeries R L M l ≤ lowerCentralSeries R L M m
<VAR>a b c : Ordinal.{u}<GOAL>a ♯ 0 = a
<VAR>a✝ b c a : Ordinal.{u}<VAR>IH : ∀ k < a, k ♯ 0 = k<GOAL>a ♯ 0 = a
<VAR>a✝ b c a : Ordinal.{u}<VAR>IH : ∀ k < a, k ♯ 0 = k<GOAL>(a.blsub fun a' x => a' ♯ 0) = a
<VAR>a✝ b c a : Ordinal.{u}<VAR>IH : ∀ k < a, k ♯ 0 = k<VAR>x✝¹ : Ordinal.{u}<VAR>x✝ : x✝¹ < a<GOAL>x✝¹ ♯ 0 = x✝¹
<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>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z✝<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>Z : Type u_7<VAR>f : X → Y → Z<VAR>tas : Set (TopologicalSpace X)<VAR>tbs : Set (TopologicalSpace Y)<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tc : TopologicalSpace Z<VAR>hX : tX ∈ tas<VAR>hY : tY ∈ tbs<VAR>hf : Continuous fun p => f p.1 p.2<GOAL>Continuous fun p => f p.1 p.2
<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>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z✝<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>Z : Type u_7<VAR>f : X → Y → Z<VAR>tas : Set (TopologicalSpace X)<VAR>tbs : Set (TopologicalSpace Y)<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tc : TopologicalSpace Z<VAR>hX✝ : tX ∈ tas<VAR>hY : tY ∈ tbs<VAR>hf : Continuous fun p => f p.1 p.2<VAR>hX : Continuous id<GOAL>Continuous fun p => f p.1 p.2
<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>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z✝<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>Z : Type u_7<VAR>f : X → Y → Z<VAR>tas : Set (TopologicalSpace X)<VAR>tbs : Set (TopologicalSpace Y)<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tc : TopologicalSpace Z<VAR>hX✝ : tX ∈ tas<VAR>hY✝ : tY ∈ tbs<VAR>hf : Continuous fun p => f p.1 p.2<VAR>hX : Continuous id<VAR>hY : Continuous id<GOAL>Continuous fun p => f p.1 p.2
<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>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z✝<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>X : Type u_5<VAR>Y : Type u_6<VAR>Z : Type u_7<VAR>f : X → Y → Z<VAR>tas : Set (TopologicalSpace X)<VAR>tbs : Set (TopologicalSpace Y)<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tc : TopologicalSpace Z<VAR>hX✝ : tX ∈ tas<VAR>hY✝ : tY ∈ tbs<VAR>hf : Continuous fun p => f p.1 p.2<VAR>hX : Continuous id<VAR>hY : Continuous id<VAR>h_continuous_id : Continuous fun p => (id p.1, id p.2)<GOAL>Continuous fun p => f p.1 p.2
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<GOAL>LinearIndependent (ι := { x // x ∈ ofVectorSpaceIndex K V }) K Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<GOAL>Subtype.val = ⇑(ofVectorSpace K V)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x✝ y z : V<VAR>x : { x // x ∈ ofVectorSpaceIndex K V }<GOAL>↑x = (ofVectorSpace K V) x
<VAR>a : ℝ<VAR>ha : 0 ≤ a<GOAL>∃ p, 0 < p ∧ F_nat 1 a =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : 0 ≤ a<GOAL>∃ p, 0 < p ∧ (fun t => rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1<GOAL>∃ p, 0 < p ∧ (fun t => rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t => rexp (-p * t)
<VAR>aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1<VAR>ha : 0 ≤ 0<GOAL>∃ p, 0 < p ∧ (fun t => rexp (-π * (0 ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + 0 * rexp (-π * 0 ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t => rexp (-p * t)
<VAR>a : ℝ<VAR>ha : 0 ≤ a<VAR>aux' : (fun t => ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x => 1<VAR>ha' : 0 < a<GOAL>∃ p, 0 < p ∧ (fun t => rexp (-π * (a ^ 2 + 1) * t) / (1 - rexp (-π * t)) ^ 2 + a * rexp (-π * a ^ 2 * t) / (1 - rexp (-π * t))) =O[atTop] fun t => rexp (-p * t)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p q : R[X]<VAR>inst✝ : Nontrivial R<VAR>hη : 0 ∈ nthRootsFinset n R<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<GOAL>Tendsto (fun x => ↑⌈a * x⌉₊ / x) atTop (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<VAR>A : Tendsto (fun x => a + x⁻¹) atTop (𝓝 (a + 0))<GOAL>Tendsto (fun x => ↑⌈a * x⌉₊ / x) atTop (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<VAR>A : Tendsto (fun x => a + x⁻¹) atTop (𝓝 a)<GOAL>Tendsto (fun x => ↑⌈a * x⌉₊ / x) atTop (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<VAR>A : Tendsto (fun x => a + x⁻¹) atTop (𝓝 a)<GOAL>∀ᶠ (b : R) in atTop, a ≤ ↑⌈a * b⌉₊ / b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : LinearOrderedField R<VAR>inst✝¹ : OrderTopology R<VAR>inst✝ : FloorRing R<VAR>a : R<VAR>ha : 0 ≤ a<VAR>A : Tendsto (fun x => a + x⁻¹) atTop (𝓝 a)<GOAL>∀ᶠ (b : R) in atTop, ↑⌈a * b⌉₊ / b ≤ a + b⁻¹