ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>k : ℕ<VAR>hk : k < l.length<VAR>hx : l.nthLe k hk ∈ l<VAR>lpos : 0 < l.length<GOAL>l.reverse.prev (l.nthLe k hk) ⋯ = l.next (l.nthLe k hk) hx
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>k : ℕ<VAR>hk : k < l.length<VAR>hx : l.nthLe k hk ∈ l<VAR>lpos : 0 < l.length<VAR>key : l.length - 1 - k < l.length<GOAL>l.reverse.prev (l.nthLe k hk) ⋯ = l.next (l.nthLe k hk) hx
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>k : ℕ<VAR>hk : k < l.length<VAR>hx : l.nthLe k hk ∈ l<VAR>lpos : 0 < l.length<VAR>key : l.length - 1 - k < l.length<GOAL>l.reverse.prev (l.nthLe k hk) ⋯ = (pmap l.next l ⋯).nthLe k ⋯
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>k : ℕ<VAR>hk : k < l.length<VAR>hx : l.nthLe k hk ∈ l<VAR>lpos : 0 < l.length<VAR>key : l.length - 1 - k < l.length<GOAL>l.reverse.prev (l.reverse.nthLe (l.length - 1 - k) ⋯) ⋯ = (l.rotate 1).nthLe k ⋯
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>k : ℕ<VAR>hk : k < l.length<VAR>hx : l.nthLe k hk ∈ l<VAR>lpos : 0 < l.length<VAR>key : l.length - 1 - k < l.length<GOAL>(pmap l.reverse.prev l.reverse ⋯).nthLe (l.length - 1 - k) ?intro.intro = (l.rotate 1).nthLe k ⋯
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x : α<VAR>l : List α<VAR>h : l.Nodup<VAR>k : ℕ<VAR>hk : k < l.length<VAR>hx : l.nthLe k hk ∈ l<VAR>lpos : 0 < l.length<VAR>key : l.length - 1 - k < l.length<GOAL>l.length - 1 - k < (pmap l.reverse.prev l.reverse ⋯).length
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)<VAR>m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'<VAR>m'_eq : m' = Subtype.coind m mem_M'<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)<VAR>m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'<VAR>m'_eq : m' = Subtype.coind m mem_M'<VAR>hm' : span R (Set.range m') = ⊤<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)<VAR>m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'<VAR>m'_eq : m' = Subtype.coind m mem_M'<VAR>hm' : span R (Set.range m') = ⊤<VAR>hm'n : ∑ i : ι, m' i ⊗ₜ[R] n i = 0<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)<VAR>m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'<VAR>m'_eq : m' = Subtype.coind m mem_M'<VAR>hm' : span R (Set.range m') = ⊤<VAR>hm'n : ∑ i : ι, m' i ⊗ₜ[R] n i = 0<VAR>this : VanishesTrivially R m' n<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)<VAR>m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'<VAR>m'_eq : m' = Subtype.coind m mem_M'<VAR>hm' : span R (Set.range m') = ⊤<VAR>hm'n : ∑ i : ι, m' i ⊗ₜ[R] n i = 0<VAR>this : ∃ κ x a y, (∀ (i : ι), n i = ∑ j : κ, a i j • y j) ∧ ∀ (j : κ), ∑ i : ι, a i j • m' i = 0<VAR>κ : Type u<VAR>x✝ : Fintype κ<VAR>a : ι → κ → R<VAR>y : κ → N<VAR>j : κ<GOAL>∑ i : ι, a i j • m i = 0 ↔ ∑ i : ι, a i j • m' i = 0
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)<VAR>m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'<VAR>m'_eq : m' = Subtype.coind m mem_M'<VAR>hm' : span R (Set.range m') = ⊤<VAR>hm'n : ∑ i : ι, m' i ⊗ₜ[R] n i = 0<VAR>this : ∃ κ x a y, (∀ (i : ι), n i = ∑ j : κ, a i j • y j) ∧ ∀ (j : κ), ∑ i : ι, a i j • m' i = 0<VAR>κ : Type u<VAR>x✝ : Fintype κ<VAR>a : ι → κ → R<VAR>y : κ → N<VAR>j : κ<GOAL>∑ i : ι, a i j • m i = (span R (Set.range m)).subtype (∑ i : ι, a i j • m' i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>x y : List α<VAR>h : x <+: y<VAR>hl : x.length < y.length<GOAL>x ++ [y.get ⟨x.length, hl⟩] <+: y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>x y : List α<VAR>h : x <+: y<VAR>hl : x.length < y.length<GOAL>x ++ [y.get ⟨x.length, hl⟩] ++ drop (x.length + 1) y = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>x y : List α<VAR>h : x <+: y<VAR>hl : x.length < y.length<GOAL>take x.length y ++ [y.get ⟨x.length, hl⟩] ++ drop (x.length + 1) y = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>x y : List α<VAR>h : x <+: y<VAR>hl : x.length < y.length<GOAL>take x.length y ++ [y.get ⟨x.length, hl⟩] = take (x.length + 1) y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>x y : List α<VAR>h : x <+: y<VAR>hl : x.length < y.length<GOAL>take x.length y ++ [y.get ⟨x.length, hl⟩] = take x.length y ++ [y[x.length]]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l₁ l₂ l₃ : List α<VAR>a b : α<VAR>m n : ℕ<VAR>x y : List α<VAR>h : x <+: y<VAR>hl : x.length < y.length<GOAL>x.length < y.length
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s✝ : Set E<VAR>a x y✝ : E<VAR>s t : Set E<VAR>hst : s ≤ t<VAR>y : E<VAR>c : ℕ → ℝ<VAR>d : ℕ → E<VAR>hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s<VAR>hc : Tendsto c atTop atTop<VAR>hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)<GOAL>y ∈ (fun s => posTangentConeAt s a) t
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R T<VAR>ι κ : Type w<VAR>inst✝¹ : Fintype ι<VAR>b : Basis ι R S<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<GOAL>(BilinForm.toMatrix b) (traceForm R S) i j = (trace R S) (b i * b j)
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : M<GOAL>ιInv ((ι R) x) = x
<VAR>R : Type u1<VAR>inst✝⁴ : CommRing R<VAR>M : Type u2<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>A : Type u_1<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>x : M<VAR>this : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)<GOAL>ιInv ((ι R) x) = x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x✝ y : G<VAR>i : ℤ<VAR>x : G<GOAL>orderOf x⁻¹ = orderOf x
<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>inst✝³ : NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>inst✝² : Add L<VAR>inst✝¹ : FunLike F L (End R M)<VAR>inst✝ : AddHomClass F L (End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>h : ∀ (x y : L), Commute (f x) (f y)<VAR>x y : L<GOAL>μ (x + y) = μ x + μ y
<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>inst✝³ : NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>inst✝² : Add L<VAR>inst✝¹ : FunLike F L (End R M)<VAR>inst✝ : AddHomClass F L (End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>h : ∀ (x y : L), Commute (f x) (f y)<VAR>x y : L<VAR>contra : ¬μ (x + y) = μ x + μ y<GOAL>False
<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>inst✝³ : NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>inst✝² : Add L<VAR>inst✝¹ : FunLike F L (End R M)<VAR>inst✝ : AddHomClass F L (End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>h : ∀ (x y : L), Commute (f x) (f y)<VAR>x y : L<VAR>contra : ¬μ (x + y) = μ x + μ y<VAR>g : L → Submodule R M := fun x => ⨆ k, ((f x).genEigenspace (μ x)) k<GOAL>False
<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>inst✝³ : NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>inst✝² : Add L<VAR>inst✝¹ : FunLike F L (End R M)<VAR>inst✝ : AddHomClass F L (End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>h : ∀ (x y : L), Commute (f x) (f y)<VAR>x y : L<VAR>contra : ¬μ (x + y) = μ x + μ y<VAR>g : L → Submodule R M := fun x => ⨆ k, ((f x).genEigenspace (μ x)) k<VAR>this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)<GOAL>False
<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>inst✝³ : NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>inst✝² : Add L<VAR>inst✝¹ : FunLike F L (End R M)<VAR>inst✝ : AddHomClass F L (End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>h : ∀ (x y : L), Commute (f x) (f y)<VAR>x y : L<VAR>contra : ¬μ (x + y) = μ x + μ y<VAR>g : L → Submodule R M := fun x => ⨆ k, ((f x).genEigenspace (μ x)) k<VAR>this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)<GOAL>Disjoint (g x ⊓ g y) (g (x + y))
<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>inst✝³ : NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>inst✝² : Add L<VAR>inst✝¹ : FunLike F L (End R M)<VAR>inst✝ : AddHomClass F L (End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>h : ∀ (x y : L), Commute (f x) (f y)<VAR>x y : L<VAR>contra : ¬μ (x + y) = μ x + μ y<VAR>g : L → Submodule R M := fun x => ⨆ k, ((f x).genEigenspace (μ x)) k<VAR>this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)<GOAL>Disjoint (⨆ k, ((f x + f y).genEigenspace (μ x + μ y)) k) (g (x + y))
<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>inst✝³ : NoZeroSMulDivisors R M<VAR>L : Type u_1<VAR>F : Type u_2<VAR>inst✝² : Add L<VAR>inst✝¹ : FunLike F L (End R M)<VAR>inst✝ : AddHomClass F L (End R M)<VAR>f : F<VAR>μ : L → R<VAR>h_ne : ⨅ x, ⨆ k, ((f x).genEigenspace (μ x)) k ≠ ⊥<VAR>h : ∀ (x y : L), Commute (f x) (f y)<VAR>x y : L<VAR>contra : ¬μ (x + y) = μ x + μ y<VAR>g : L → Submodule R M := fun x => ⨆ k, ((f x).genEigenspace (μ x)) k<VAR>this : ⨅ x, g x ≤ g x ⊓ g y ⊓ g (x + y)<GOAL>Disjoint (⨆ k, ((f x + f y).genEigenspace (μ x + μ y)) k) (⨆ k, ((f x + f y).genEigenspace (μ (x + y))) k)
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>V₁ : Type u_3<VAR>V₂ : Type u_4<VAR>V₃ : Type u_5<VAR>inst✝⁴ : SeminormedAddCommGroup V<VAR>inst✝³ : SeminormedAddCommGroup W<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f : NormedAddGroupHom V₁ V₂<VAR>g : NormedAddGroupHom V₂ V₃<VAR>x✝ : V₁<GOAL>x✝ ∈ ker 0 ↔ x✝ ∈ ⊤
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>p : ℕ<VAR>f : σ → MvPolynomial τ R<VAR>φ : MvPolynomial σ R<GOAL>(expand p) ((bind₁ f) φ) = (bind₁ fun i => (expand p) (f i)) φ
<VAR>α✝ : Type u_1<VAR>R : α✝ → α✝ → Prop<VAR>l : List α✝<GOAL>Pairwise R l ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
<VAR>α✝ : Type u_1<VAR>R : α✝ → α✝ → Prop<VAR>l : List α✝<GOAL>(∀ (i j : Nat) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]) ↔ ∀ (i j : Fin l.length), i < j → R (l.get i) (l.get j)
<VAR>p k : ℕ<VAR>hp : 2 ≤ p<GOAL>↑(sMod' (2 ^ p - 1) k) = sMod p k
<VAR>p k : ℕ<VAR>hp : 2 ≤ p<VAR>h1 : 4 ≤ 2 ^ p<GOAL>↑(sMod' (2 ^ p - 1) k) = sMod p k
<VAR>p k : ℕ<VAR>hp : 2 ≤ p<VAR>h1 : 4 ≤ 2 ^ p<VAR>h2 : 1 ≤ 2 ^ p<GOAL>↑(sMod' (2 ^ p - 1) k) = sMod p k
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : K<GOAL>(mixedEmbedding K) x ∈ convexBodySum K B ↔ ∑ w : InfinitePlace K, ↑w.mult * ↑w x ≤ B
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>B : ℝ<VAR>x : K<GOAL>∑ x_1 : InfinitePlace K, ↑x_1.mult * x_1 x ≤ B ↔ ∑ w : InfinitePlace K, ↑w.mult * ↑w x ≤ B
<VAR>A : Type u_1<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : CstarRing A<VAR>inst✝⁴ : CompleteSpace A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : PartialOrder A<VAR>inst✝ : StarOrderedRing A<VAR>a : A<GOAL>a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
<VAR>A : Type u_1<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : CstarRing A<VAR>inst✝⁴ : CompleteSpace A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : PartialOrder A<VAR>inst✝ : StarOrderedRing A<VAR>a : A<VAR>this : a * star a ≤ (algebraMap ℝ A) ‖a * star a‖<GOAL>a * star a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.154709, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : HasPullbacks D<VAR>inst✝ : HasColimitsOfShape J D<VAR>F : J ⥤ C ⥤ D<VAR>c : Cocone F<VAR>hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)<VAR>F' : J ⥤ C ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c'.pt ⟶ c.pt<VAR>e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<GOAL>Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.154709, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : HasPullbacks D<VAR>inst✝ : HasColimitsOfShape J D<VAR>F : J ⥤ C ⥤ D<VAR>c : Cocone F<VAR>hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)<VAR>F' : J ⥤ C ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ F<VAR>f : c'.pt ⟶ c.pt<VAR>e : α ≫ c.ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>this : ∀ (x : C), Nonempty (IsColimit (((evaluation C D).obj x).mapCocone c')) ↔ ∀ (j : J), IsPullback ((((evaluation C D).obj x).mapCocone c').ι.app j) ((whiskerRight α ((evaluation C D).obj x)).app j) (((evaluation C D).obj x).map f) ((((evaluation C D).obj x).mapCocone c).ι.app j)<GOAL>Nonempty (IsColimit c') ↔ ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
<VAR>α : Type u<VAR>inst✝² : Ring α<VAR>a b : α<VAR>inst✝¹ : Invertible a<VAR>inst✝ : Invertible b<GOAL>⅟a - ⅟b = ⅟a * (b - a) * ⅟b
<VAR>x y : ℝ<VAR>f : CauSeq ℚ abs<GOAL>mk (-f) = -mk f
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Algebra R S<VAR>x : S<VAR>p q : R[X]<VAR>n : ℕ<GOAL>eval₂ (algebraMap R S) x (p ^ n) = eval₂ (algebraMap R S) x p ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<GOAL>(⨆ g, ⨆ (_ : ↑g ≤ fun a => f a), g.lintegral μ) + ⨆ g_1, ⨆ (_ : ↑g_1 ≤ fun a => g a), g_1.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ↑g_1 ≤ fun a => f a + g a), g_1.lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>f' : α →ₛ ℝ≥0∞<VAR>hf' : (fun h => ↑h ≤ f) f'<VAR>g' : α →ₛ ℝ≥0∞<VAR>hg' : (fun h => ↑h ≤ g) g'<GOAL>f'.lintegral μ + g'.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ↑g_1 ≤ fun a => f a + g a), g_1.lintegral μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s t : Set α<VAR>a b : α<VAR>hs : s.Nonempty<VAR>hb : b < sSup s<GOAL>∃ a ∈ s, b < a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝ : ConditionallyCompleteLinearOrder α<VAR>s t : Set α<VAR>a b : α<VAR>hs : s.Nonempty<VAR>hb : ∀ a ∈ s, a ≤ b<GOAL>sSup s ≤ b
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{?u.27192, u_1} C<VAR>inst✝⁸ : Category.{u_9, u_2} C₁<VAR>inst✝⁷ : Category.{u_12, u_3} C₂<VAR>inst✝⁶ : Category.{u_11, u_4} C₃<VAR>inst✝⁵ : Category.{u_8, u_5} D₁<VAR>inst✝⁴ : Category.{u_13, u_6} D₂<VAR>inst✝³ : Category.{u_10, u_7} D₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>W₃ : MorphismProperty C₃<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>Ψ : LocalizerMorphism W₂ W₃<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>L₃ : C₃ ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W₃<VAR>X Y Z : C₁<VAR>f : L₁.obj X ⟶ L₁.obj Y<VAR>G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂<VAR>G' : D₂ ⥤ D₃ := Ψ.localizedFunctor L₂ L₃<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso Φ.functor L₁ L₂ G<VAR>e' : Ψ.functor ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso Ψ.functor L₂ L₃ G'<GOAL>Ψ.homMap L₂ L₃ (Φ.homMap L₁ L₂ f) = (Φ.comp Ψ).homMap L₁ L₃ f
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{?u.27192, u_1} C<VAR>inst✝⁸ : Category.{u_9, u_2} C₁<VAR>inst✝⁷ : Category.{u_12, u_3} C₂<VAR>inst✝⁶ : Category.{u_11, u_4} C₃<VAR>inst✝⁵ : Category.{u_8, u_5} D₁<VAR>inst✝⁴ : Category.{u_13, u_6} D₂<VAR>inst✝³ : Category.{u_10, u_7} D₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>W₃ : MorphismProperty C₃<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>Ψ : LocalizerMorphism W₂ W₃<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>L₃ : C₃ ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W₃<VAR>X Y Z : C₁<VAR>f : L₁.obj X ⟶ L₁.obj Y<VAR>G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂<VAR>G' : D₂ ⥤ D₃ := Ψ.localizedFunctor L₂ L₃<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso Φ.functor L₁ L₂ G<VAR>e' : Ψ.functor ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso Ψ.functor L₂ L₃ G'<GOAL>e'.hom.app (Φ.functor.obj X) ≫ G'.map (e.hom.app X ≫ G.map f ≫ e.inv.app Y) ≫ e'.inv.app (Φ.functor.obj Y) = (Φ.functor.associator Ψ.functor L₃ ≪≫ isoWhiskerLeft Φ.functor e' ≪≫ (Φ.functor.associator L₂ G').symm ≪≫ isoWhiskerRight e G' ≪≫ L₁.associator G G').hom.app X ≫ (G ⋙ G').map f ≫ (Φ.functor.associator Ψ.functor L₃ ≪≫ isoWhiskerLeft Φ.functor e' ≪≫ (Φ.functor.associator L₂ G').symm ≪≫ isoWhiskerRight e G' ≪≫ L₁.associator G G').inv.app Y
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{?u.27192, u_1} C<VAR>inst✝⁸ : Category.{u_9, u_2} C₁<VAR>inst✝⁷ : Category.{u_12, u_3} C₂<VAR>inst✝⁶ : Category.{u_11, u_4} C₃<VAR>inst✝⁵ : Category.{u_8, u_5} D₁<VAR>inst✝⁴ : Category.{u_13, u_6} D₂<VAR>inst✝³ : Category.{u_10, u_7} D₃<VAR>W₁ : MorphismProperty C₁<VAR>W₂ : MorphismProperty C₂<VAR>W₃ : MorphismProperty C₃<VAR>Φ : LocalizerMorphism W₁ W₂<VAR>Ψ : LocalizerMorphism W₂ W₃<VAR>L₁ : C₁ ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W₁<VAR>L₂ : C₂ ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W₂<VAR>L₃ : C₃ ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W₃<VAR>X Y Z : C₁<VAR>f : L₁.obj X ⟶ L₁.obj Y<VAR>G : D₁ ⥤ D₂ := Φ.localizedFunctor L₁ L₂<VAR>G' : D₂ ⥤ D₃ := Ψ.localizedFunctor L₂ L₃<VAR>e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso Φ.functor L₁ L₂ G<VAR>e' : Ψ.functor ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso Ψ.functor L₂ L₃ G'<GOAL>e'.hom.app (Φ.functor.obj X) ≫ G'.map (e.hom.app X ≫ G.map f ≫ e.inv.app Y) ≫ e'.inv.app (Φ.functor.obj Y) = (𝟙 (L₃.obj (Ψ.functor.obj (Φ.functor.obj X))) ≫ e'.hom.app (Φ.functor.obj X) ≫ 𝟙 (G'.obj (L₂.obj (Φ.functor.obj X))) ≫ G'.map (e.hom.app X) ≫ 𝟙 (G'.obj (G.obj (L₁.obj X)))) ≫ G'.map (G.map f) ≫ (((𝟙 (G'.obj (G.obj (L₁.obj Y))) ≫ G'.map (e.inv.app Y)) ≫ 𝟙 (G'.obj (L₂.obj (Φ.functor.obj Y)))) ≫ e'.inv.app (Φ.functor.obj Y)) ≫ 𝟙 (L₃.obj (Ψ.functor.obj (Φ.functor.obj Y)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ✝ : Type u_3<VAR>τ : Type u_4<VAR>T : TopologicalSpace α<VAR>σ : Type u_5<VAR>F : Ctop α σ<VAR>H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a ↔ ∃ b, a ∈ F.f b ∧ F.f b ⊆ s<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ s ∈ 𝓝 x
<VAR>R : Type u_1<VAR>f : ArithmeticFunction ℤ<VAR>inst✝ : Ring R<VAR>h : f.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>↑f (m * n) = ↑f m * ↑f n
<VAR>𝕜 : Type u_1<VAR>inst✝¹³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝⁸ : NormedAddCommGroup G<VAR>inst✝⁷ : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝⁶ : NormedAddCommGroup G'<VAR>inst✝⁵ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>inst✝⁴ : Fintype ι<VAR>M : ι → Type u_7<VAR>inst✝³ : (i : ι) → NormedAddCommGroup (M i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (M i)<VAR>H : Type u_8<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>c : E → ContinuousMultilinearMap 𝕜 M H<VAR>c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H<VAR>hc : DifferentiableAt 𝕜 c x<VAR>u : (i : ι) → M i<VAR>m : E<GOAL>(fderiv 𝕜 (fun y => (c y) u) x) m = ((fderiv 𝕜 c x) m) u
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>f : X ≃ᵢ Y<GOAL>(map ⇑f) (mkMetric m) = mkMetric m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → α<VAR>H : ∀ (x : α), f x = x<VAR>o : Part α<GOAL>map f o = o
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → α<VAR>H : ∀ (x : α), f x = x<VAR>o : Part α<GOAL>map id o = o