ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>inst✝ : Subsingleton E<GOAL>∀ (x : E), ‖f x‖ ≤ 0 * ‖x‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁷ : SeminormedAddCommGroup E<VAR>inst✝¹⁶ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁵ : SeminormedAddCommGroup F<VAR>inst✝¹⁴ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹³ : SeminormedAddCommGroup G<VAR>inst✝¹² : SeminormedAddCommGroup Gₗ<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁹ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁶ : NormedSpace 𝕜₂ F<VAR>inst✝⁵ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁴ : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>f : E →SL[σ₁₂] F<VAR>inst✝ : Subsingleton E<VAR>x : E<GOAL>‖f x‖ ≤ 0 * ‖x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝² : DecidablePred p<VAR>inst✝¹ : DecidablePred q<VAR>s t : Finset α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>x✝ : α<GOAL>x✝ ∈ s₁ \ s₂ ↔ x✝ ∈ filter (fun x => x ∉ s₂) s₁
<VAR>num : Int<VAR>den : Nat<VAR>nz : den ≠ 0<VAR>c : num.natAbs.Coprime den<GOAL>{ num := num, den := den, den_nz := nz, reduced := c } = mkRat num den
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>a b : α<GOAL>{a} ⊆ ↑s ↔ {a} ⊆ s
<VAR>R M : Type u<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Flat R M<VAR>N : Type u<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : Free R N<VAR>inst✝ : Finite R N<VAR>f : N<VAR>x : N →ₗ[R] M<VAR>h : x f = 0<GOAL>∃ κ x_1 a y, x = y ∘ₗ a ∧ a f = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : LinearOrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s t : Finset ι<VAR>Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i<GOAL>∃ i ∈ s, f i < g i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>G : Type u_6<VAR>k : Type u_7<VAR>R : Type u_8<VAR>inst✝ : LinearOrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s t : Finset ι<VAR>Hle : ∀ i ∈ s, g i ≤ f i<GOAL>∏ i ∈ s, g i ≤ ∏ i ∈ s, f i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>IsPiSystem (⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b} = {S | ∃ l u, ↑l < ↑u ∧ Ioo ↑l ↑u = S}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<VAR>x : Set ℝ<GOAL>x ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b} ↔ x ∈ {S | ∃ l u, ↑l < ↑u ∧ Ioo ↑l ↑u = S}
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<GOAL>span R {x} = ⊤ ↔ ∀ (v : M), ∃ r, r • x = v
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>x : M<GOAL>(∀ v ∈ ⊤, ∃ r, r • x = v) ↔ ∀ (v : M), ∃ r, r • x = v
<VAR>α β : Type u<VAR>c : Cardinal.{u}<VAR>f : α → β<VAR>hf : ∀ (b : β), #↑(f ⁻¹' {b}) ≤ c<GOAL>#α ≤ #β * c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u s t : Set α<VAR>x : α<GOAL>x ∈ s ∧ x ∉ t ↔ x ∈ s ∩ tᶜ
<VAR>ζ : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hn0 : ↑n ≠ 0<VAR>h : IsPrimitiveRoot ζ n<GOAL>∃ i < n, ∃ (_ : i.Coprime n), cexp (2 * ↑π * I * (↑i / ↑n)) = ζ
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hn0 : ↑n ≠ 0<VAR>i : ℕ<VAR>hi : i < n<VAR>h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n<GOAL>∃ i_1 < n, ∃ (_ : i_1.Coprime n), cexp (2 * ↑π * I * (↑i_1 / ↑n)) = cexp (2 * ↑π * I / ↑n) ^ i
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hn0 : ↑n ≠ 0<VAR>i : ℕ<VAR>hi : i < n<VAR>h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n<GOAL>cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (2 * ↑π * I / ↑n) ^ i
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hn0 : ↑n ≠ 0<VAR>i : ℕ<VAR>hi : i < n<VAR>h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n<GOAL>cexp (2 * ↑π * I * (↑i / ↑n)) = cexp (↑i * (2 * ↑π * I / ↑n))
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hn0 : ↑n ≠ 0<VAR>i : ℕ<VAR>hi : i < n<VAR>h : IsPrimitiveRoot (cexp (2 * ↑π * I / ↑n) ^ i) n<GOAL>2 * ↑π * I * (↑i / ↑n) = ↑i * (2 * ↑π * I / ↑n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : Set (Set α)<GOAL>⋃₀ s = ⋃ i ∈ s, i
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : Set (σ →₀ ℕ)<GOAL>x ∈ Ideal.span ((fun s => (monomial s) 1) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : Set (σ →₀ ℕ)<GOAL>(∀ m ∈ x.support, ∃ m' ∈ s, ∃ d, m = d + m') ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>x : MvPolynomial σ R<VAR>s : Set (σ →₀ ℕ)<GOAL>(∀ m ∈ x.support, ∃ m' ∈ s, ∃ d, m = m' + d) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, ∃ c, xi = si + c
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : PseudoEMetricSpace β<VAR>inst✝¹ : PseudoEMetricSpace γ<VAR>f : α → β<VAR>x✝ y✝ z : α<VAR>s : Set α<VAR>inst✝ : Subsingleton α<VAR>x y : α<GOAL>edist (f x) (f y) = edist x y
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : PseudoEMetricSpace α<VAR>inst✝² : PseudoEMetricSpace β<VAR>inst✝¹ : PseudoEMetricSpace γ<VAR>f : α → β<VAR>x✝ y✝ z : α<VAR>s : Set α<VAR>inst✝ : Subsingleton α<VAR>x y : α<GOAL>edist (f y) (f y) = edist y y
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalSpace Z<VAR>proj : Z → B<VAR>h : IsHomeomorphicTrivialFiberBundle F proj<GOAL>IsOpenMap proj
<VAR>B : Type u_1<VAR>F : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : TopologicalSpace Z<VAR>e : Z ≃ₜ B × F<VAR>h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ⇑e)<GOAL>IsOpenMap (Prod.fst ∘ ⇑e)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ✝ : Type u_5<VAR>γ' : Type u_6<VAR>δ✝ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝¹⁰ : DecidableEq α'<VAR>inst✝⁹ : DecidableEq β'<VAR>inst✝⁸ : DecidableEq γ✝<VAR>inst✝⁷ : DecidableEq γ'<VAR>inst✝⁶ : DecidableEq δ✝<VAR>inst✝⁵ : DecidableEq δ'<VAR>inst✝⁴ : DecidableEq ε<VAR>inst✝³ : DecidableEq ε'<VAR>f✝ f'✝ : α → β → γ✝<VAR>g✝ g'✝ : α → β → γ✝ → δ✝<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u✝ u' : Finset γ✝<VAR>a a' : α<VAR>b b' : β<VAR>c : γ✝<VAR>γ : Type u_14<VAR>δ : Type u_15<VAR>u : Finset γ<VAR>v : Finset δ<VAR>inst✝² : DecidableEq ζ<VAR>inst✝¹ : DecidableEq ζ'<VAR>inst✝ : DecidableEq ν<VAR>f : ε → ζ → ν<VAR>g : α → β → ε<VAR>h : γ → δ → ζ<VAR>f' : ε' → ζ' → ν<VAR>g' : α → γ → ε'<VAR>h' : β → δ → ζ'<VAR>h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)<GOAL>image2 f (image2 g ↑s ↑t) (image2 h ↑u ↑v) = image2 f' (image2 g' ↑s ↑u) (image2 h' ↑t ↑v)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : 0 < n<VAR>v : Fin n → E<VAR>j : Fin (Composition.single n hn).length<GOAL>p.applyComposition (Composition.single n hn) v j = (p n) v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : 0 < n<VAR>v : Fin n → E<VAR>j : Fin (Composition.single n hn).length<VAR>i : ℕ<VAR>hi1 : i < (Composition.single n hn).blocksFun j<VAR>hi2 : i < n<GOAL>(v ∘ ⇑((Composition.single n hn).embedding j)) ⟨i, hi1⟩ = v ⟨i, hi2⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : 0 < n<VAR>v : Fin n → E<VAR>j : Fin (Composition.single n hn).length<VAR>i : ℕ<VAR>hi1 : i < (Composition.single n hn).blocksFun j<VAR>hi2 : i < n<GOAL>((Composition.single n hn).embedding j) ⟨i, hi1⟩ = ⟨i, hi2⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : 0 < n<VAR>v : Fin n → E<VAR>j : Fin (Composition.single n hn).length<VAR>i : ℕ<VAR>hi1 : i < (Composition.single n hn).blocksFun j<VAR>hi2 : i < n<GOAL>((Composition.single n hn).embedding j) ⟨i, hi1⟩ = ((Composition.single n hn).embedding 0) ⟨i, hi2⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : 0 < n<VAR>v : Fin n → E<VAR>i : ℕ<VAR>hi2 : i < n<VAR>j_val : ℕ<VAR>j_property : j_val < (Composition.single n hn).length<VAR>hi1 : i < (Composition.single n hn).blocksFun ⟨j_val, j_property⟩<GOAL>((Composition.single n hn).embedding ⟨j_val, j_property⟩) ⟨i, hi1⟩ = ((Composition.single n hn).embedding 0) ⟨i, hi2⟩
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>H : Type u_5<VAR>inst✝¹⁵ : CommRing 𝕜<VAR>inst✝¹⁴ : AddCommGroup E<VAR>inst✝¹³ : AddCommGroup F<VAR>inst✝¹² : AddCommGroup G<VAR>inst✝¹¹ : Module 𝕜 E<VAR>inst✝¹⁰ : Module 𝕜 F<VAR>inst✝⁹ : Module 𝕜 G<VAR>inst✝⁸ : TopologicalSpace E<VAR>inst✝⁷ : TopologicalSpace F<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : TopologicalAddGroup E<VAR>inst✝⁴ : ContinuousConstSMul 𝕜 E<VAR>inst✝³ : TopologicalAddGroup F<VAR>inst✝² : ContinuousConstSMul 𝕜 F<VAR>inst✝¹ : TopologicalAddGroup G<VAR>inst✝ : ContinuousConstSMul 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hn : 0 < n<VAR>v : Fin n → E<VAR>i : ℕ<VAR>hi2 : i < n<VAR>j_val : ℕ<VAR>j_property : j_val < (Composition.single n hn).length<VAR>hi1 : i < (Composition.single n hn).blocksFun ⟨j_val, j_property⟩<VAR>this : j_val = 0<GOAL>((Composition.single n hn).embedding ⟨j_val, j_property⟩) ⟨i, hi1⟩ = ((Composition.single n hn).embedding 0) ⟨i, hi2⟩
<VAR>α β : Type u<VAR>m : Type u → Type v<VAR>x : OptionT m α<VAR>inst✝¹ : Monad m<VAR>f : α → β<VAR>inst✝ : LawfulMonad m<GOAL>(f <$> x).run = Option.map f <$> x.run
<VAR>α β : Type u<VAR>m : Type u → Type v<VAR>x : OptionT m α<VAR>inst✝¹ : Monad m<VAR>f : α → β<VAR>inst✝ : LawfulMonad m<GOAL>(f <$> x).run = do let a ← x.run pure (Option.map f a)
<VAR>α β : Type u<VAR>m : Type u → Type v<VAR>x : OptionT m α<VAR>inst✝¹ : Monad m<VAR>f : α → β<VAR>inst✝ : LawfulMonad m<GOAL>(do let x ← x.run match x with | some a => (pure (f a)).run | none => pure none) = do let a ← x.run pure (Option.map f a)
<VAR>α β : Type u<VAR>m : Type u → Type v<VAR>x : OptionT m α<VAR>inst✝¹ : Monad m<VAR>f : α → β<VAR>inst✝ : LawfulMonad m<GOAL>∀ (a : Option α), (match a with | some a => (pure (f a)).run | none => pure none) = pure (Option.map f a)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m✝ n✝ m n : ℕ<VAR>hn : Odd n<VAR>hm : Even m<GOAL>m % 2 + (m + n) % 2 = 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m✝ n✝ m n : ℕ<VAR>hn : Odd n<VAR>hm : Odd m<GOAL>m % 2 + (m + n) % 2 = 1
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<GOAL>l.Nodup ↔ Injective l.get
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<GOAL>(Injective fun i => l[↑i]) ↔ Injective l.get
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>ha : 1 < a.x<GOAL>0 < d
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>ha : 1 < a.x<GOAL>0 < d * a.y ^ 2
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>ha : 1 < a.x<GOAL>1 < a.x ^ 2
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Subgroup G<GOAL>stabilizer Gᵐᵒᵖ ↑s = s.op
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Subgroup G<GOAL>∀ (x : Gᵐᵒᵖ), (∀ (b : G), x • b ∈ ↑s ↔ b ∈ ↑s) ↔ x ∈ s.op
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Subgroup G<GOAL>∀ (x : Gᵐᵒᵖ), (∀ (b : G), b * unop x ∈ s ↔ b ∈ s) ↔ unop x ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a✝ : G<VAR>s : Subgroup G<VAR>a : Gᵐᵒᵖ<VAR>h : ∀ (b : G), b * unop a ∈ s ↔ b ∈ s<GOAL>unop a ∈ s
<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>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>e : ι → β<VAR>he : Injective e<VAR>f : ι → α<GOAL>⨆ j, extend e f ⊥ j = ⨆ i, f i
<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>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLattice α<VAR>f✝ g s t : ι → α<VAR>a b : α<VAR>e : ι → β<VAR>he : Injective e<VAR>f : ι → α<GOAL>(⨆ i, ⨆ (_ : ∃ i_1, e i_1 = i), extend e f ⊥ i) ⊔ ⨆ i, ⨆ (_ : ¬∃ i_1, e i_1 = i), extend e f ⊥ i = ⨆ i, f i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝ : PseudoEMetricSpace α<VAR>f g : α → ℝ<VAR>Kf Kg : ℝ≥0<VAR>hf : LipschitzWith Kf f<VAR>a : ℝ<GOAL>LipschitzWith Kf fun x => max (f x) a
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<GOAL>Prime (hζ.toInteger - 1)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : NumberField K := numberField {p ^ (k + 1)} ℚ K<GOAL>Prime (hζ.toInteger - 1)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : NumberField K := numberField {p ^ (k + 1)} ℚ K<VAR>h : hζ.toInteger - 1 = 0<GOAL>False
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : NumberField K := numberField {p ^ (k + 1)} ℚ K<GOAL>Irreducible (Ideal.absNorm (Ideal.span {hζ.toInteger - 1}))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : NumberField K := numberField {p ^ (k + 1)} ℚ K<GOAL>Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : NumberField K := numberField {p ^ (k + 1)} ℚ K<GOAL>(Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : NumberField K := numberField {p ^ (k + 1)} ℚ K<GOAL>(algebraMap ℤ ℚ) ((Algebra.norm ℤ) (hζ.toInteger - 1)) = (algebraMap ℤ ℚ) ↑↑p
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : NumberField K := numberField {p ^ (k + 1)} ℚ K<GOAL>(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = (algebraMap ℤ ℚ) ↑↑p
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝² : Field K<VAR>inst✝¹ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>this : NumberField K := numberField {p ^ (k + 1)} ℚ K<GOAL>(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) (hζ.toInteger - 1)) = ↑↑p
<VAR>x y : ZFSet<VAR>h : x.Nonempty<GOAL>y ∈ ⋂₀ x ↔ ∀ z ∈ x, y ∈ z
<VAR>x y : ZFSet<VAR>h : x.Nonempty<GOAL>y ∈ ZFSet.sep (fun y => ∀ z ∈ x, y ∈ z) (Set.Nonempty.some h) ↔ ∀ z ∈ x, y ∈ z
<VAR>x y : ZFSet<VAR>h : x.Nonempty<GOAL>(∀ z ∈ x, y ∈ z) → y ∈ Set.Nonempty.some h
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : UniformSpace β<VAR>K : Set α<VAR>V : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>inst✝ : WeaklyLocallyCompactSpace α<GOAL>Tendsto F p (𝓝 f) ↔ TendstoLocallyUniformly (fun i a => (F i) a) (⇑f) p
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : UniformSpace β<VAR>K : Set α<VAR>V✝ : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>inst✝ : WeaklyLocallyCompactSpace α<VAR>h : Tendsto F p (𝓝 f)<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<VAR>x : α<GOAL>∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ V
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : UniformSpace β<VAR>K : Set α<VAR>V✝ : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>inst✝ : WeaklyLocallyCompactSpace α<VAR>h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<VAR>x : α<GOAL>∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ V
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : UniformSpace β<VAR>K : Set α<VAR>V✝ : Set (β × β)<VAR>f : C(α, β)<VAR>ι : Type u₃<VAR>p : Filter ι<VAR>F : ι → C(α, β)<VAR>inst✝ : WeaklyLocallyCompactSpace α<VAR>h : ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => (F i) a) (⇑f) p K<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<VAR>x : α<VAR>n : Set α<VAR>hn₁ : IsCompact n<VAR>hn₂ : n ∈ 𝓝 x<GOAL>∃ t ∈ 𝓝 x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, (fun i a => (F i) a) n y) ∈ V
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X I : Set α<VAR>M : Matroid α<VAR>B : Set ↑X<GOAL>(M.restrictSubtype X).Base B ↔ M.Basis' (↑B) X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X I : Set α<VAR>M : Matroid α<VAR>B : Set ↑X<GOAL>(M ↾ X).Basis ↑B ↑(X ↓∩ (M ↾ X).E) ∧ InjOn Subtype.val B ∧ B ⊆ X ↓∩ (M ↾ X).E ↔ M.Basis' (↑B) X
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : DenselyOrdered α<VAR>inst✝ : SeparableSpace α<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : DenselyOrdered α<VAR>inst✝ : SeparableSpace α<VAR>s : Set α<VAR>hc : s.Countable<VAR>hd : Dense s<GOAL>SecondCountableTopology α
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : DenselyOrdered α<VAR>inst✝ : SeparableSpace α<VAR>s : Set α<VAR>hc : s.Countable<VAR>hd : Dense s<GOAL>(Ioi '' s ∪ Iio '' s).Countable
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l : List α<GOAL>(l ++ l.reverse).Palindrome
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l✝ l : List α<GOAL>(l ++ l.reverse).reverse = l ++ l.reverse
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hms : MeasurableSet s<VAR>hci : μ (s ∩ t) ≠ 0<GOAL>0 < μ[|s] t
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>inst✝ : IsFiniteMeasure μ<VAR>hms : MeasurableSet s<VAR>hci : μ (s ∩ t) ≠ 0<GOAL>0 < (μ s)⁻¹ * μ (s ∩ t)