ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter β<GOAL>(comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>hα : IsEmpty α<GOAL>(comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter β<VAR>hα : Nonempty α<GOAL>(comap Prod.snd f).NeBot ↔ Nonempty α ∧ f.NeBot
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>α : Type u_1<VAR>inst✝¹ : SMul α ℂ<VAR>inst✝ : IsScalarTower α ℂ ℂ<VAR>k : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>c : α<GOAL>(c • f) ∣[k]A = c • f ∣[k]A
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>α : Type u_1<VAR>inst✝¹ : SMul α ℂ<VAR>inst✝ : IsScalarTower α ℂ ℂ<VAR>k : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>c : α<GOAL>((c • 1) • f) ∣[k]A = (c • 1) • f ∣[k]A
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>α : Type u_1<VAR>inst✝¹ : SMul α ℂ<VAR>inst✝ : IsScalarTower α ℂ ℂ<VAR>k : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>c : α<VAR>x✝ : ℍ<GOAL>((c • 1) • f) (A • x✝) * ↑(↑↑A).det ^ (k - 1) * denom A x✝ ^ (-k) = ((c • 1) • f ∣[k]A) x✝
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>α : Type u_1<VAR>inst✝¹ : SMul α ℂ<VAR>inst✝ : IsScalarTower α ℂ ℂ<VAR>k : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>c : α<VAR>x✝ : ℍ<GOAL>c • 1 * f (A • x✝) * ↑(↑↑A).det ^ (k - 1) * denom A x✝ ^ (-k) = c • 1 * (f (A • x✝) * ↑(↑↑A).det ^ (k - 1) * denom A x✝ ^ (-k))
<VAR>α : Type u_1<VAR>inst✝³ : ConditionallyCompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<GOAL>sInf s⁻¹ = (sSup s)⁻¹
<VAR>α : Type u_1<VAR>inst✝³ : ConditionallyCompleteLattice α<VAR>inst✝² : Group α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>s t : Set α<VAR>hs₀ : s.Nonempty<VAR>hs₁ : BddAbove s<GOAL>sInf (Inv.inv '' s) = (sSup s)⁻¹
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>M' : Matrix n m R<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<VAR>x : m → R<GOAL>(toLin' M) ({ toFun := ⇑(toLin' M'), map_add' := ⋯, map_smul' := ⋯ }.toFun x) = x
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m n R<VAR>M' : Matrix n m R<VAR>hMM' : M * M' = 1<VAR>hM'M : M' * M = 1<VAR>x : n → R<GOAL>(toLin' M') ((toLin' M) x) = x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : Invertible ↑p<VAR>n : ℕ<GOAL>xInTermsOfW p R n = (X n - ∑ i ∈ range n, C (↑p ^ i) * xInTermsOfW p R i ^ p ^ (n - i)) * C (⅟↑p ^ n)
<VAR>n✝ n : ℕ<GOAL>n.primeFactors = filter Prime n.divisors
<VAR>n : ℕ<GOAL>primeFactors 0 = filter Prime (divisors 0)
<VAR>n✝ n : ℕ<VAR>hn : n > 0<GOAL>n.primeFactors = filter Prime n.divisors
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>h : LieAlgebra.center R L = ⊥<GOAL>LieModule.maxTrivSubmodule R L (LieDerivation R L L) = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>h : LieAlgebra.center R L = ⊥<VAR>D : LieDerivation R L L<VAR>hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)<VAR>x : L<GOAL>D x = 0 x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>h : LieAlgebra.center R L = ⊥<VAR>D : LieDerivation R L L<VAR>hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)<VAR>x : L<VAR>this : (ad R L) (D x) = 0<GOAL>D x = 0 x
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>h : LieAlgebra.center R L = ⊥<VAR>D : LieDerivation R L L<VAR>hD : D ∈ LieModule.maxTrivSubmodule R L (LieDerivation R L L)<VAR>x : L<VAR>this : D x = 0<GOAL>D x = 0 x
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>inst✝ : IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>f : ℝ → ℝ<VAR>g : ℝ → ℝ≥0∞<VAR>hg : pdf X ℙ volume =ᶠ[ae volume] g<VAR>hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤<GOAL>∫⁻ (a : ℝ), ↑‖f a * (pdf X ℙ volume a).toReal‖₊ < ⊤
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : MeasurableSpace E<VAR>m : MeasurableSpace Ω<VAR>ℙ : Measure Ω<VAR>μ : Measure E<VAR>inst✝ : IsFiniteMeasure ℙ<VAR>X : Ω → ℝ<VAR>f : ℝ → ℝ<VAR>g : ℝ → ℝ≥0∞<VAR>hg : pdf X ℙ volume =ᶠ[ae volume] g<VAR>hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤<VAR>this : (fun x => ↑‖f x‖₊ * g x) =ᶠ[ae volume] fun x => ↑‖f x * (pdf X ℙ volume x).toReal‖₊<GOAL>∫⁻ (a : ℝ), ↑‖f a * (pdf X ℙ volume a).toReal‖₊ < ⊤
<VAR>α : Type u<VAR>l l' : List α<GOAL>l ~r l' ↔ l' ∈ map l.rotate (range (l.length + 1))
<VAR>α : Type u<VAR>l l' : List α<GOAL>(∃ n ≤ l.length, l.rotate n = l') ↔ ∃ a < l.length + 1, l.rotate a = l'
<VAR>x x₁✝ x₂✝ x₃ x' y y₁ y₂ y₃ y'✝ : PGame<VAR>h : IH1 x y<VAR>x₁ x₂ y' : PGame<VAR>h₁ : x₁.IsOption (-x)<VAR>h₂ : x₂.IsOption (-x)<VAR>hy : y' = y ∨ y'.IsOption y<GOAL>P24 x₁ x₂ y'
<VAR>x x₁✝ x₂✝ x₃ x' y y₁ y₂ y₃ y'✝ : PGame<VAR>h : IH1 x y<VAR>x₁ x₂ y' : PGame<VAR>h₁ : (-x₁).IsOption x<VAR>h₂ : (-x₂).IsOption x<VAR>hy : y' = y ∨ y'.IsOption y<GOAL>P24 x₁ x₂ y'
<VAR>α : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α<VAR>s✝ : Set α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : DiscreteTopology α<VAR>β : Type u_2<VAR>s : Set α<GOAL>Dense s ↔ s = univ
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ : Multiset α<VAR>a✝ b : α<VAR>s t : Multiset α<VAR>a : α<VAR>h : s ≤ a ::ₘ t<VAR>m : a ∈ s<GOAL>s.erase a ≤ t
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ : Multiset α<VAR>a✝ b : α<VAR>s t : Multiset α<VAR>a : α<VAR>h : a ::ₘ s.erase a ≤ a ::ₘ t<VAR>m : a ∈ s<GOAL>s.erase a ≤ t
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : DecidableEq m<VAR>d : o → m → α<VAR>i : m<VAR>k : o<VAR>j : m<VAR>k' : o<GOAL>blockDiagonal (fun k => diagonal (d k)) (i, k) (j, k') = diagonal (fun ik => d ik.2 ik.1) (i, k) (j, k')
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : DecidableEq m<VAR>d : o → m → α<VAR>i : m<VAR>k : o<VAR>j : m<VAR>k' : o<GOAL>(if k = k' ∧ i = j then d k i else 0) = if i = j ∧ k = k' then d k i else 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α : Type u_12<VAR>β : Type u_13<VAR>inst✝³ : DecidableEq o<VAR>inst✝² : Zero α<VAR>inst✝¹ : Zero β<VAR>inst✝ : DecidableEq m<VAR>d : o → m → α<VAR>i : m<VAR>k : o<VAR>j : m<VAR>k' : o<GOAL>(k = k' ∧ i = j) = (i = j ∧ k = k')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>h : InjOn f s<GOAL>(f '' s).encard = s.encard
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>motive : List α → Sort u_2<VAR>x : α<VAR>xs : List α<VAR>nil : motive []<VAR>append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])<GOAL>reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (reverseRecOn xs nil append_singleton)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>motive : List α → Sort u_2<VAR>x : α<VAR>xs : List α<VAR>nil : motive []<VAR>append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])<GOAL>∀ (ys : List α) (h : xs.reverse.reverse = ys), reverseRecOn (xs ++ [x]) nil append_singleton = cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>motive : List α → Sort u_2<VAR>x : α<VAR>xs : List α<VAR>nil : motive []<VAR>append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])<VAR>ys : List α<VAR>hy : xs.reverse.reverse = ys<VAR>head✝ : α<VAR>tail✝ : List α<VAR>heq✝ : (xs ++ [x]).reverse = head✝ :: tail✝<GOAL>cast ⋯ (append_singleton tail✝.reverse head✝ (reverseRecOn tail✝.reverse nil append_singleton)) = cast ⋯ (append_singleton ys x (reverseRecOn ys nil append_singleton))
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : NonarchimedeanGroup G<VAR>f : α → G<VAR>hf : Tendsto f cofinite (𝓝 1)<GOAL>CauchySeq fun s => ∏ i ∈ s, f i
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : NonarchimedeanGroup G<VAR>f : α → G<VAR>hf : Tendsto f cofinite (𝓝 1)<GOAL>∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ e
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : NonarchimedeanGroup G<VAR>f : α → G<VAR>hf : Tendsto f cofinite (𝓝 1)<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<GOAL>∃ s, ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : NonarchimedeanGroup G<VAR>f : α → G<VAR>hf : Tendsto f cofinite (𝓝 1)<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>V : OpenSubgroup G<VAR>hV : ↑V ⊆ U<GOAL>∃ s, ∀ (t : Finset α), Disjoint t s → ∏ b ∈ t, f b ∈ U
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : NonarchimedeanGroup G<VAR>f : α → G<VAR>hf : Tendsto f cofinite (𝓝 1)<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>V : OpenSubgroup G<VAR>hV : ↑V ⊆ U<GOAL>∀ (t : Finset α), Disjoint t (Set.Finite.toFinset ⋯) → ∏ b ∈ t, f b ∈ U
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : NonarchimedeanGroup G<VAR>f : α → G<VAR>hf : Tendsto f cofinite (𝓝 1)<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>V : OpenSubgroup G<VAR>hV : ↑V ⊆ U<VAR>t : Finset α<VAR>ht : Disjoint t (Set.Finite.toFinset ⋯)<GOAL>∏ b ∈ t, f b ∈ ↑V
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : NonarchimedeanGroup G<VAR>f : α → G<VAR>hf : Tendsto f cofinite (𝓝 1)<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>V : OpenSubgroup G<VAR>hV : ↑V ⊆ U<VAR>t : Finset α<VAR>ht : Disjoint t (Set.Finite.toFinset ⋯)<GOAL>∀ c ∈ t, f c ∈ ↑V
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : NonarchimedeanGroup G<VAR>f : α → G<VAR>hf : Tendsto f cofinite (𝓝 1)<VAR>U : Set G<VAR>hU : U ∈ 𝓝 1<VAR>V : OpenSubgroup G<VAR>hV : ↑V ⊆ U<VAR>t : Finset α<VAR>ht : Disjoint t (Set.Finite.toFinset ⋯)<VAR>i : α<VAR>hi : i ∈ t<GOAL>f i ∈ ↑V
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>K : Set X<VAR>K_closed : IsClosed K<VAR>x : X<VAR>x_notin_K : x ∉ K<GOAL>∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>K : Set X<VAR>K_closed : IsClosed K<VAR>x : X<VAR>x_notin_K : x ∉ K<VAR>g : X → ↑unitInterval<VAR>g_cont : Continuous g<VAR>gx_zero : g x = 0<VAR>g_one_on_K : EqOn g 1 K<GOAL>∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>K : Set X<VAR>K_closed : IsClosed K<VAR>x : X<VAR>x_notin_K : x ∉ K<VAR>g : X → ↑unitInterval<VAR>g_cont : Continuous g<VAR>gx_zero : g x = 0<VAR>g_one_on_K : EqOn g 1 K<VAR>g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1<GOAL>∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompletelyRegularSpace X<VAR>K : Set X<VAR>K_closed : IsClosed K<VAR>x : X<VAR>x_notin_K : x ∉ K<VAR>g : X → ↑unitInterval<VAR>g_cont : Continuous g<VAR>gx_zero : g x = 0<VAR>g_one_on_K : EqOn g 1 K<VAR>g_bdd : ∀ (x y : X), dist (↑(g x)).toNNReal (↑(g y)).toNNReal ≤ 1<VAR>g' : X →ᵇ ℝ≥0 := mkOfBound { toFun := fun x => (↑(g x)).toNNReal, continuous_toFun := ⋯ } 1 g_bdd<GOAL>∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P : Ideal A<VAR>hP : P ≠ ⊥<VAR>h : P.IsPrime<GOAL>Prime P
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>P : Ideal A<VAR>hP : P ≠ ⊥<VAR>h : P.IsPrime<VAR>I J : Ideal A<VAR>hIJ : P ∣ I * J<GOAL>P ∣ I ∨ P ∣ J
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r₁ : R<VAR>r₂ : ℝ<VAR>h : ‖r₁‖ < r₂<VAR>h0 : ¬r₁ = 0<GOAL>(fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r₁ : R<VAR>r₂ : ℝ<VAR>h : ‖r₁‖ < r₂<VAR>h0 : 0 < ‖r₁‖<GOAL>(fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r₁ : R<VAR>r₂ : ℝ<VAR>h : ‖r₁‖ < r₂<VAR>h0 : 0 < ‖r₁‖<VAR>A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n<GOAL>(fun n => ↑n ^ k * r₁ ^ n) =o[atTop] fun n => r₂ ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝ : NormedRing R<VAR>k : ℕ<VAR>r₁ : R<VAR>r₂ : ℝ<VAR>h : ‖r₁‖ < r₂<VAR>h0 : 0 < ‖r₁‖<VAR>A : (fun n => ↑n ^ k) =o[atTop] fun n => (r₂ / ‖r₁‖) ^ n<GOAL>(fun n => r₁ ^ n) =O[atTop] fun n => ‖r₁‖ ^ n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Finset α<VAR>a b : α<GOAL>preimage 1 (fun x => a * x) ⋯ = {a⁻¹}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>x✝ : Nontrivial R<GOAL>(∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)) ↔ ∀ (x : R), x ≠ 0 → IsUnit x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>x✝ : Nontrivial R<VAR>h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)<VAR>x : R<VAR>hx : x ≠ 0<GOAL>IsUnit x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>x✝ : Nontrivial R<VAR>h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)<VAR>x : R<VAR>hx : x ≠ 0<VAR>y : R<VAR>hyx : y * x = 1<GOAL>IsUnit x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>x✝ : Nontrivial R<VAR>h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)<VAR>x : R<VAR>hx : x ≠ 0<VAR>y : R<VAR>hyx : y * x = 1<VAR>hy : y ≠ 0<GOAL>IsUnit x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : Ring S<VAR>M : Type u_4<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>x✝ : Nontrivial R<VAR>h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)<VAR>x : R<VAR>hx : x ≠ 0<VAR>y : R<VAR>hyx : y * x = 1<VAR>hy : y ≠ 0<VAR>z : R<VAR>hzy : z * y = 1<GOAL>IsUnit x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>p : α → Prop<VAR>x y z : α<VAR>n : ℤ<VAR>x✝ : (f ^ n).SameCycle x y<VAR>m : ℤ<VAR>h : ((f ^ n) ^ m) x = y<GOAL>(f ^ (n * m)) x = y
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : z ≤ x<GOAL>x \ (y \ z) = x \ y ⊔ z
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>v : Set M<VAR>hv : span R v = ⊤<VAR>x : M'<VAR>x✝ : x ∈ ⊤<GOAL>x ∈ span Rₛ (⇑f '' v)
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>v : Set M<VAR>hv : span R v = ⊤<VAR>x : M'<VAR>x✝ : x ∈ ⊤<VAR>m : M<VAR>s : ↥S<VAR>h : (m, s).2 • x = f (m, s).1<GOAL>x ∈ span Rₛ (⇑f '' v)
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>v : Set M<VAR>hv : span R v = ⊤<VAR>x : M'<VAR>x✝ : x ∈ ⊤<VAR>m : M<VAR>s : ↥S<VAR>h : ⋯.unit⁻¹ • f (m, s).1 = x<GOAL>x ∈ span Rₛ (⇑f '' v)
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>v : Set M<VAR>hv : span R v = ⊤<VAR>x : M'<VAR>x✝ : x ∈ ⊤<VAR>m : M<VAR>s : ↥S<VAR>h : ⋯.unit⁻¹ • f (m, s).1 = x<GOAL>f (m, s).1 ∈ ↑(span R (⇑f '' v))
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>S : Submonoid R<VAR>inst✝¹⁰ : CommSemiring Rₛ<VAR>inst✝⁹ : Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module Rₛ M<VAR>inst✝⁵ : IsScalarTower R Rₛ M<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module Rₛ M'<VAR>inst✝¹ : IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>inst✝ : IsLocalizedModule S f<VAR>v : Set M<VAR>hv : span R v = ⊤<VAR>x : M'<VAR>x✝ : x ∈ ⊤<VAR>m : M<VAR>s : ↥S<VAR>h : ⋯.unit⁻¹ • f (m, s).1 = x<GOAL>(↑R f) (m, s).1 ∈ ↑(map (↑R f) ⊤)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>s : Finset α<GOAL>s.card ^ 2 ≤ (s \\ s).card ^ 2
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : IsNoetherian R M<VAR>f : End R M<VAR>μ : R<GOAL>f.maxGenEigenspace μ = (f.genEigenspace μ) (f.maxGenEigenspaceIndex μ)
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>h : WellFounded fun x x_1 => x > x_1<VAR>f : End R M<VAR>μ : R<GOAL>f.maxGenEigenspace μ = (f.genEigenspace μ) (f.maxGenEigenspaceIndex μ)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>h_zero : μ s = 0<VAR>x : F<GOAL>(weightedSMul μ s) x = 0 x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>h_zero : μ s = 0<VAR>x : F<GOAL>ENNReal.toReal 0 • x = 0 x
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>f₀ : 𝕜 → E<VAR>g₀ : 𝕜 → E'<VAR>n : ℕ∞<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : CompleteSpace F<VAR>μ : Measure 𝕜<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>hf : LocallyIntegrable f₀ μ<VAR>hcg : HasCompactSupport g₀<VAR>hg : ContDiff 𝕜 1 g₀<VAR>x₀ : 𝕜<GOAL>HasDerivAt (f₀ ⋆[L, μ] g₀) ((f₀ ⋆[L, μ] deriv g₀) x₀) x₀
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>f₀ : 𝕜 → E<VAR>g₀ : 𝕜 → E'<VAR>n : ℕ∞<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : CompleteSpace F<VAR>μ : Measure 𝕜<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>hf : LocallyIntegrable f₀ μ<VAR>hcg : HasCompactSupport g₀<VAR>hg : ContDiff 𝕜 1 g₀<VAR>x₀ : 𝕜<GOAL>(f₀ ⋆[L, μ] deriv g₀) x₀ = ((f₀ ⋆[precompR 𝕜 L, μ] fderiv 𝕜 g₀) x₀) 1
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝⁷ : RCLike 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>f₀ : 𝕜 → E<VAR>g₀ : 𝕜 → E'<VAR>n : ℕ∞<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : CompleteSpace F<VAR>μ : Measure 𝕜<VAR>inst✝¹ : μ.IsAddLeftInvariant<VAR>inst✝ : SFinite μ<VAR>hf : LocallyIntegrable f₀ μ<VAR>hcg : HasCompactSupport g₀<VAR>hg : ContDiff 𝕜 1 g₀<VAR>x₀ : 𝕜<GOAL>(f₀ ⋆[L, μ] deriv g₀) x₀ = (f₀ ⋆[L, μ] fun a => (fderiv 𝕜 g₀ a) 1) x₀