ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀✝ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>x₀ : F<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g x₀<VAR>f : F → E := fun x => g (x₀ - x)<VAR>If : Integrable f μ<VAR>this : Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • f x ∂μ) atTop (𝓝 (f 0))<GOAL>Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀✝ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>x₀ : F<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g x₀<VAR>f : F → E := fun x => g (x₀ - x)<VAR>If : Integrable f μ<VAR>this : Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))<GOAL>Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) atTop (𝓝 (g x₀))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀✝ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>x₀ : F<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g x₀<VAR>f : F → E := fun x => g (x₀ - x)<VAR>If : Integrable f μ<VAR>this : Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))<VAR>c : ℝ<GOAL>∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ = ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>hm : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : BorelSpace α<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>g✝ : α → E<VAR>l : Filter ι<VAR>x₀✝ : α<VAR>s t : Set α<VAR>φ✝ : ι → α → ℝ<VAR>a : E<VAR>inst✝⁶ : CompleteSpace E<VAR>F : Type u_4<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>inst✝³ : FiniteDimensional ℝ F<VAR>inst✝² : MeasurableSpace F<VAR>inst✝¹ : BorelSpace F<VAR>μ : Measure F<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>φ : F → ℝ<VAR>hφ : ∀ (x : F), 0 ≤ φ x<VAR>h'φ : ∫ (x : F), φ x ∂μ = 1<VAR>h : Tendsto (fun x => ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)<VAR>g : F → E<VAR>x₀ : F<VAR>hg : Integrable g μ<VAR>h'g : ContinuousAt g x₀<VAR>f : F → E := fun x => g (x₀ - x)<VAR>If : Integrable f μ<VAR>this : Tendsto (fun c => ∫ (x : F), (c ^ finrank ℝ F * φ (c • x)) • g (x₀ - x) ∂μ) atTop (𝓝 (g x₀))<VAR>c : ℝ<GOAL>∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ = ∫ (x : F), (c ^ finrank ℝ F * φ (c • (x₀ + -x))) • g (x₀ - (x₀ + -x)) ∂μ
<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<VAR>E : LinearRecurrence α<VAR>u v : ℕ → α<VAR>hu : E.IsSolution u<VAR>hv : E.IsSolution v<VAR>h : Set.EqOn u v ↑(range E.order)<VAR>u' : ↥E.solSpace := ⟨u, hu⟩<VAR>v' : ↥E.solSpace := ⟨v, hv⟩<GOAL>u' = v'
<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<VAR>E : LinearRecurrence α<VAR>u v : ℕ → α<VAR>hu : E.IsSolution u<VAR>hv : E.IsSolution v<VAR>h : Set.EqOn u v ↑(range E.order)<VAR>u' : ↥E.solSpace := ⟨u, hu⟩<VAR>v' : ↥E.solSpace := ⟨v, hv⟩<GOAL>E.toInit u' = E.toInit v'
<VAR>α : Type u_1<VAR>inst✝ : CommSemiring α<VAR>E : LinearRecurrence α<VAR>u v : ℕ → α<VAR>hu : E.IsSolution u<VAR>hv : E.IsSolution v<VAR>h : Set.EqOn u v ↑(range E.order)<VAR>u' : ↥E.solSpace := ⟨u, hu⟩<VAR>v' : ↥E.solSpace := ⟨v, hv⟩<VAR>x : Fin E.order<GOAL>E.toInit u' x = E.toInit v' x
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hn : cornersTheoremBound (ε / 9) ≤ n<VAR>A : Finset (ℕ × ℕ)<VAR>hAn : A ⊆ range n ×ˢ range n<VAR>hAε : ε * ↑n ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree ↑A<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hn : cornersTheoremBound (ε / 9) ≤ n<VAR>A : Finset (ℕ × ℕ)<VAR>hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)<VAR>hAε : ε * ↑n ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree ↑A<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hn : cornersTheoremBound (ε / 9) ≤ n<VAR>A : Finset (ℕ × ℕ)<VAR>hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)<VAR>hAε : ε * ↑n ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree ↑A<VAR>this : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hn : cornersTheoremBound (ε / 9) ≤ n<VAR>A : Finset (ℕ × ℕ)<VAR>hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)<VAR>hAε : ε * ↑n ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))<VAR>this : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hn : cornersTheoremBound (ε / 9) ≤ n<VAR>A : Finset (ℕ × ℕ)<VAR>hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)<VAR>hAε : ε * ↑n ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))<VAR>this✝ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)<VAR>this : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hn : cornersTheoremBound (ε / 9) ≤ n<VAR>A : Finset (ℕ × ℕ)<VAR>hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)<VAR>hAε : ε * ↑n ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))<VAR>this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)<VAR>this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val<VAR>this : IsCornerFree (Prod.map Nat.cast Nat.cast '' ↑A)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hn : cornersTheoremBound (ε / 9) ≤ n<VAR>A : Finset (ℕ × ℕ)<VAR>hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)<VAR>hAε : ε * ↑n ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))<VAR>this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)<VAR>this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val<VAR>this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)<GOAL>False
<VAR>G : Type u_1<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Fintype G<VAR>A✝ B : Finset (G × G)<VAR>a b c d x y : G<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hn : cornersTheoremBound (ε / 9) ≤ n<VAR>A : Finset (ℕ × ℕ)<VAR>hAn : ↑A ⊆ ↑(range n) ×ˢ ↑(range n)<VAR>hAε : ε * ↑n ^ 2 ≤ ↑A.card<VAR>hA : IsCornerFree (Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A))<VAR>this✝¹ : ↑A = Prod.map Fin.val Fin.val '' (Prod.map Nat.cast Nat.cast '' ↑A)<VAR>this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val<VAR>this : IsCornerFree ↑(image (Prod.map Nat.cast Nat.cast) A)<GOAL>ε / 9 * ↑(Fintype.card (Fin (2 * n + 1))) ^ 2 ≤ ↑(image (Prod.map Nat.cast Nat.cast) A).card
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ f : R →+* S₁<VAR>g : S₂ → MvPolynomial S₃ R<VAR>p : MvPolynomial S₂ R<GOAL>(map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ f : R →+* S₁<VAR>g : S₂ → MvPolynomial S₃ R<VAR>p : MvPolynomial S₂ R<GOAL>∀ (a : R), (map f) (eval₂ C g (C a)) = eval₂ C (⇑(map f) ∘ g) ((map f) (C a))
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ f : R →+* S₁<VAR>g : S₂ → MvPolynomial S₃ R<VAR>p : MvPolynomial S₂ R<GOAL>∀ (p q : MvPolynomial S₂ R), (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p) → (map f) (eval₂ C g q) = eval₂ C (⇑(map f) ∘ g) ((map f) q) → (map f) (eval₂ C g (p + q)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p + q))
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f✝ f : R →+* S₁<VAR>g : S₂ → MvPolynomial S₃ R<VAR>p : MvPolynomial S₂ R<GOAL>∀ (p : MvPolynomial S₂ R) (n : S₂), (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p) → (map f) (eval₂ C g (p * X n)) = eval₂ C (⇑(map f) ∘ g) ((map f) (p * X n))
<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>f₁ f₂ : End R M<VAR>μ₁ μ₂ : R<VAR>h : Commute f₁ f₂<VAR>m : M<VAR>hm : m ∈ (⨆ k, (f₁.genEigenspace μ₁) k) ⊓ ⨆ k, (f₂.genEigenspace μ₂) k<GOAL>m ∈ ⨆ k, ((f₁ + f₂).genEigenspace (μ₁ + μ₂)) k
<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>f₁ f₂ : End R M<VAR>μ₁ μ₂ : R<VAR>h : Commute f₁ f₂<VAR>m : M<VAR>hm : (∃ k, ((f₁ - μ₁ • 1) ^ k) m = 0) ∧ ∃ k, ((f₂ - μ₂ • 1) ^ k) m = 0<GOAL>∃ k, ((f₁ + f₂ - (μ₁ + μ₂) • 1) ^ k) m = 0
<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>f₁ f₂ : End R M<VAR>μ₁ μ₂ : R<VAR>h : Commute f₁ f₂<VAR>m : M<VAR>k₁ : ℕ<VAR>hk₁ : ((f₁ - μ₁ • 1) ^ k₁) m = 0<VAR>k₂ : ℕ<VAR>hk₂ : ((f₂ - μ₂ • 1) ^ k₂) m = 0<GOAL>∃ k, ((f₁ + f₂ - (μ₁ + μ₂) • 1) ^ k) m = 0
<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>f₁ f₂ : End R M<VAR>μ₁ μ₂ : R<VAR>h : Commute f₁ f₂<VAR>m : M<VAR>k₁ : ℕ<VAR>hk₁ : ((f₁ - μ₁ • 1) ^ k₁) m = 0<VAR>k₂ : ℕ<VAR>hk₂ : ((f₂ - μ₂ • 1) ^ k₂) m = 0<GOAL>((f₁ + f₂ - (μ₁ + μ₂) • 1) ^ (k₁ + k₂ - 1)) m = 0
<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>f₁ f₂ : End R M<VAR>μ₁ μ₂ : R<VAR>h : Commute f₁ f₂<VAR>m : M<VAR>k₁ : ℕ<VAR>hk₁ : ((f₁ - μ₁ • 1) ^ k₁) m = 0<VAR>k₂ : ℕ<VAR>hk₂ : ((f₂ - μ₂ • 1) ^ k₂) m = 0<VAR>this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)<GOAL>((f₁ + f₂ - (μ₁ + μ₂) • 1) ^ (k₁ + k₂ - 1)) m = 0
<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>f₁ f₂ : End R M<VAR>μ₁ μ₂ : R<VAR>m : M<VAR>k₁ : ℕ<VAR>hk₁ : ((f₁ - μ₁ • 1) ^ k₁) m = 0<VAR>k₂ : ℕ<VAR>hk₂ : ((f₂ - μ₂ • 1) ^ k₂) m = 0<VAR>this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)<VAR>h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)<GOAL>((f₁ + f₂ - (μ₁ + μ₂) • 1) ^ (k₁ + k₂ - 1)) m = 0
<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>f₁ f₂ : End R M<VAR>μ₁ μ₂ : R<VAR>m : M<VAR>k₁ : ℕ<VAR>hk₁ : ((f₁ - μ₁ • 1) ^ k₁) m = 0<VAR>k₂ : ℕ<VAR>hk₂ : ((f₂ - μ₂ • 1) ^ k₂) m = 0<VAR>this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)<VAR>h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)<GOAL>∑ c ∈ Finset.antidiagonal (k₁ + k₂ - 1), ((k₁ + k₂ - 1).choose c.1 • ((f₁ - μ₁ • 1) ^ c.1 * (f₂ - μ₂ • 1) ^ c.2)) m = 0
<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>f₁ f₂ : End R M<VAR>μ₁ μ₂ : R<VAR>m : M<VAR>k₁ : ℕ<VAR>hk₁ : ((f₁ - μ₁ • 1) ^ k₁) m = 0<VAR>k₂ : ℕ<VAR>hk₂ : ((f₂ - μ₂ • 1) ^ k₂) m = 0<VAR>this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)<VAR>h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)<VAR>x✝ : ℕ × ℕ<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)<GOAL>((k₁ + k₂ - 1).choose (i, j).1 • ((f₁ - μ₁ • 1) ^ (i, j).1 * (f₂ - μ₂ • 1) ^ (i, j).2)) m = 0
<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>f₁ f₂ : End R M<VAR>μ₁ μ₂ : R<VAR>m : M<VAR>k₁ : ℕ<VAR>hk₁ : ((f₁ - μ₁ • 1) ^ k₁) m = 0<VAR>k₂ : ℕ<VAR>hk₂ : ((f₂ - μ₂ • 1) ^ k₂) m = 0<VAR>this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)<VAR>h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)<VAR>x✝ : ℕ × ℕ<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)<GOAL>((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
<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>f₁ f₂ : End R M<VAR>μ₁ μ₂ : R<VAR>m : M<VAR>k₁ : ℕ<VAR>hk₁ : ((f₁ - μ₁ • 1) ^ k₁) m = 0<VAR>k₂ : ℕ<VAR>hk₂ : ((f₂ - μ₂ • 1) ^ k₂) m = 0<VAR>this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)<VAR>h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)<VAR>x✝ : ℕ × ℕ<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)<VAR>hi : k₁ ≤ (i, j).1<GOAL>((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
<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>f₁ f₂ : End R M<VAR>μ₁ μ₂ : R<VAR>m : M<VAR>k₁ : ℕ<VAR>hk₁ : ((f₁ - μ₁ • 1) ^ k₁) m = 0<VAR>k₂ : ℕ<VAR>hk₂ : ((f₂ - μ₂ • 1) ^ k₂) m = 0<VAR>this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)<VAR>h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)<VAR>x✝ : ℕ × ℕ<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)<VAR>hj : k₂ ≤ (i, j).2<GOAL>((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{u_5, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>E : Type u_3<VAR>inst✝¹ : Category.{?u.11396, u_3} E<VAR>inst✝ : L.IsLocalization W<VAR>X : C<VAR>hX : W (𝟙 X)<GOAL>(isoOfHom L W (𝟙 X) hX).inv = 𝟙 (L.obj X)
<VAR>α : Type u_1<VAR>i : Nat<VAR>xs : List α<VAR>p : α → Bool<GOAL>findIdx? p xs = some i ↔ map p (take (i + 1) xs) = replicate i false ++ [true]
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁶ : Ring R<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 : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>h : ker f ⊔ ker g = ⊤<GOAL>range (f.prod g) = (range f).prod (range g)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁶ : Ring R<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 : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>h : ker f ⊔ ker g = ⊤<GOAL>(range f).prod (range g) ≤ range (f.prod g)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁶ : Ring R<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 : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>h : ker f ⊔ ker g = ⊤<GOAL>∀ (a : M₂) (b : M₃) (x : M), f x = a → ∀ (x : M), g x = b → ∃ y, (f y, g y) = (a, b)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁶ : Ring R<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 : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>h : ker f ⊔ ker g = ⊤<VAR>x y : M<GOAL>∃ y_1, (f y_1, g y_1) = (f x, g y)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁶ : Ring R<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 : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>h : ker f ⊔ ker g = ⊤<VAR>x y : M<GOAL>∃ y_1, y_1 - x ∈ ker f ∧ g y_1 = g y
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁶ : Ring R<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 : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>h : ker f ⊔ ker g = ⊤<VAR>x y : M<VAR>this : y - x ∈ ker f ⊔ ker g<GOAL>∃ y_1, y_1 - x ∈ ker f ∧ g y_1 = g y
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁶ : Ring R<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 : M →ₗ[R] M₂<VAR>g : M →ₗ[R] M₃<VAR>h : ker f ⊔ ker g = ⊤<VAR>x y : M<VAR>this : y - x ∈ ker f ⊔ ker g<VAR>x' : M<VAR>hx' : x' ∈ ker f<VAR>y' : M<VAR>hy' : y' ∈ ker g<VAR>H : x' + y' = y - x<GOAL>∃ y_1, y_1 - x ∈ ker f ∧ g y_1 = g y
<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>s : Set (Set α)<GOAL>(∀ {i : Set (Set α)}, i.Finite ∧ i ⊆ s → (⋂₀ i).Nonempty) ↔ ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
<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✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>h0 : ¬orderOf x = 0<GOAL>orderOf y ∣ (orderOf x).lcm (orderOf (x * y))
<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✝ : Monoid G<VAR>a b x y : G<VAR>n m : ℕ<VAR>h : Commute x y<VAR>h0 : ¬orderOf x = 0<GOAL>orderOf (x ^ (orderOf x).pred * (x * y)) ∣ (orderOf x).lcm (orderOf (x * y))
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>hf : Injective f<VAR>x y z : α<VAR>hx : ¬z = x<VAR>hy : ¬z = y<GOAL>(Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)
<VAR>α : Type u_1<VAR>inst✝ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>x : α<VAR>s : Set (Set α)<GOAL>s ∈ v.filterAt x ↔ ∃ ε > 0, ∀ a ∈ v.setsAt x, a ⊆ closedBall x ε → a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>r : α → α → Prop<VAR>f g : Filter α<GOAL>IsBounded r ⊥ ↔ Nonempty α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν<VAR>n : ℕ<GOAL>⨆ k, ⨆ (_ : k ≤ n), f k ∈ measurableLE μ ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : ℕ → α → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), f n ∈ measurableLE μ ν<VAR>n : ℕ<VAR>x✝ : α<GOAL>(⨆ k, ⨆ (_ : k ≤ n), f k) x✝ = ⨆ k, ⨆ (_ : k ≤ n), f k x✝
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>t u s x✝¹ : Multiset α<VAR>x✝ : α<GOAL>s + t + {x✝} = s + u + x✝¹ ↔ t + {x✝} = u + x✝¹
<VAR>𝕜 : Type u<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>inst✝ : SeparableSpace 𝕜<VAR>f : 𝕜 → F<GOAL>IsSeparable (range (deriv f))
<VAR>𝕜 : Type u<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>inst✝ : SeparableSpace 𝕜<VAR>f : 𝕜 → F<GOAL>IsSeparable (range (derivWithin f univ))
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>adj3 : F'' ⊣ G''<VAR>f : F' ⟶ F<VAR>g : F'' ⟶ F'<GOAL>(adj1.natTransEquiv adj2).symm f ≫ (adj2.natTransEquiv adj3).symm g = (adj1.natTransEquiv adj3).symm (g ≫ f)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} C<VAR>inst✝ : Category.{u_4, u_2} D<VAR>F F' F'' : C ⥤ D<VAR>G G' G'' : D ⥤ C<VAR>adj1 : F ⊣ G<VAR>adj2 : F' ⊣ G'<VAR>adj3 : F'' ⊣ G''<VAR>f : F' ⟶ F<VAR>g : F'' ⟶ F'<GOAL>(adj1.natTransEquiv adj3) ((adj1.natTransEquiv adj2).symm f ≫ (adj2.natTransEquiv adj3).symm g) = (adj1.natTransEquiv adj3) ((adj1.natTransEquiv adj3).symm (g ≫ f))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>t : Set β<GOAL>Nat.card ↑({a} ×ˢ t) = Nat.card ↑t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Algebra R B<VAR>f : R →+* S<VAR>g : S →+* T<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R A B<VAR>x : T<VAR>h : (g.comp f).IsIntegralElem x<VAR>p : R[X]<VAR>hp : p.Monic<VAR>hp' : eval₂ (g.comp f) x p = 0<GOAL>eval₂ g x (Polynomial.map f p) = 0