ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>hm₁ : m₁ ∈ 𝕎(M₁, χ₁, x)<VAR>m₂ : M₂<VAR>hm₂ : m₂ ∈ 𝕎(M₂, χ₂, x)<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<GOAL>∃ k, (F ^ k) (↑g (m₁ ⊗ₜ[R] m₂)) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>hm₁ : m₁ ∈ 𝕎(M₁, χ₁, x)<VAR>m₂ : M₂<VAR>hm₂ : m₂ ∈ 𝕎(M₂, χ₂, x)<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<GOAL>∃ k, ((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>hm₁ : ∃ k, (((toEnd R L M₁) x - χ₁ • 1) ^ k) m₁ = 0<VAR>hm₂ : ∃ k, (((toEnd R L M₂) x - χ₂ • 1) ^ k) m₂ = 0<GOAL>∃ k, ((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<GOAL>∃ k, ((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<VAR>hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0<GOAL>∃ k, ((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<VAR>hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0<GOAL>∃ k, ((f₁ + f₂) ^ k) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<VAR>hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0<GOAL>((f₁ + f₂) ^ (k₁ + k₂ - 1)) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<VAR>hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf_comm : Commute f₁ f₂<GOAL>((f₁ + f₂) ^ (k₁ + k₂ - 1)) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<VAR>hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf_comm : Commute f₁ f₂<GOAL>(∑ m ∈ Finset.antidiagonal (k₁ + k₂ - 1), (k₁ + k₂ - 1).choose m.1 • (f₁ ^ m.1 * f₂ ^ m.2)) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<VAR>hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf_comm : Commute f₁ f₂<GOAL>∑ x ∈ Finset.antidiagonal (k₁ + k₂ - 1), (k₁ + k₂ - 1).choose x.1 • (f₁ ^ x.1 * f₂ ^ x.2) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<VAR>hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf_comm : Commute f₁ f₂<GOAL>∀ x ∈ Finset.antidiagonal (k₁ + k₂ - 1), (k₁ + k₂ - 1).choose x.1 • (f₁ ^ x.1 * f₂ ^ x.2) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<VAR>hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf_comm : Commute f₁ f₂<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)<GOAL>(k₁ + k₂ - 1).choose (i, j).1 • (f₁ ^ (i, j).1 * f₂ ^ (i, j).2) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<VAR>hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf_comm : Commute f₁ f₂<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)<GOAL>(f₁ ^ i * f₂ ^ j) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<VAR>hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf_comm : Commute f₁ f₂<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)<VAR>hi : k₁ ≤ (i, j).1<GOAL>(f₁ ^ i * f₂ ^ j) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁹ : CommRing R<VAR>inst✝¹⁸ : LieRing L<VAR>inst✝¹⁷ : LieAlgebra R L<VAR>inst✝¹⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝¹⁵ : AddCommGroup M<VAR>inst✝¹⁴ : Module R M<VAR>inst✝¹³ : LieRingModule L M<VAR>inst✝¹² : LieModule R L M<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>inst✝¹¹ : AddCommGroup M₁<VAR>inst✝¹⁰ : Module R M₁<VAR>inst✝⁹ : LieRingModule L M₁<VAR>inst✝⁸ : LieModule R L M₁<VAR>inst✝⁷ : AddCommGroup M₂<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : LieRingModule L M₂<VAR>inst✝⁴ : LieModule R L M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₃<VAR>inst✝¹ : LieRingModule L M₃<VAR>inst✝ : LieModule R L M₃<VAR>g : M₁ ⊗[R] M₂ →ₗ⁅R,L⁆ M₃<VAR>χ₁ χ₂ : R<VAR>x : L<VAR>t : ↥𝕎(M₁, χ₁, x) ⊗[R] ↥𝕎(M₂, χ₂, x)<VAR>F : Module.End R M₃ := (toEnd R L M₃) x - (χ₁ + χ₂) • 1<VAR>m₁ : M₁<VAR>m₂ : M₂<VAR>f₁ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.rTensor M₂ ((toEnd R L M₁) x - χ₁ • 1)<VAR>f₂ : Module.End R (M₁ ⊗[R] M₂) := LinearMap.lTensor M₁ ((toEnd R L M₂) x - χ₂ • 1)<VAR>h_comm_square : F ∘ₗ ↑g = ↑g ∘ₗ (f₁ + f₂)<VAR>k₁ : ℕ<VAR>hk₁ : (((toEnd R L M₁) x - χ₁ • 1) ^ k₁) m₁ = 0<VAR>k₂ : ℕ<VAR>hk₂ : (((toEnd R L M₂) x - χ₂ • 1) ^ k₂) m₂ = 0<VAR>hf₁ : (f₁ ^ k₁) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf₂ : (f₂ ^ k₂) (m₁ ⊗ₜ[R] m₂) = 0<VAR>hf_comm : Commute f₁ f₂<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal (k₁ + k₂ - 1)<VAR>hj : k₂ ≤ (i, j).2<GOAL>(f₁ ^ i * f₂ ^ j) (m₁ ⊗ₜ[R] m₂) = 0
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ₁ δ₂ : ℝ<VAR>δ₁_pos : 0 < δ₁<VAR>δ₂_pos : 0 < δ₂<VAR>hle : δ₁ ≤ δ₂<VAR>E : Set α<VAR>x : α<GOAL>(thickenedIndicator δ₁_pos E) x ≤ (thickenedIndicator δ₂_pos E) x
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ₁ δ₂ : ℝ<VAR>δ₁_pos : 0 < δ₁<VAR>δ₂_pos : 0 < δ₂<VAR>hle : δ₁ ≤ δ₂<VAR>E : Set α<VAR>x : α<GOAL>thickenedIndicatorAux δ₁ E x ≤ thickenedIndicatorAux δ₂ E x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : Monoid M<VAR>l : List M<GOAL>op l.prod = (map op l).reverse.prod
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedRing 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : AddCommGroup F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s t : Set E<VAR>h : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>MapsTo (⇑(AffineMap.lineMap x y)) (Icc 0 1) s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁶ : EMetricSpace X<VAR>inst✝⁵ : EMetricSpace Y<VAR>C K r : ℝ≥0<VAR>f : X → Y<VAR>s✝ t : Set X<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>e : E ≃L[𝕜] F<VAR>s : Set F<GOAL>dimH (⇑e ⁻¹' s) = dimH s
<VAR>S : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>inst✝ : CancelCommMonoid M<VAR>a x y : M<VAR>h : x = y<GOAL>SemiconjBy a x y
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>a : E<VAR>r : ℝ<GOAL>Convex ℝ (ball a r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalGroup G<VAR>f : α → G<VAR>inst✝ : T2Space G<VAR>a : G<GOAL>∏' (x : β), a = a ^ Nat.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalGroup G<VAR>f : α → G<VAR>inst✝ : T2Space G<VAR>a : G<VAR>hβ : Finite β<GOAL>∏' (x : β), a = a ^ Nat.card β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>G : Type u_5<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalGroup G<VAR>f : α → G<VAR>inst✝ : T2Space G<VAR>a : G<VAR>hβ : Infinite β<GOAL>∏' (x : β), a = a ^ Nat.card β
<VAR>α β : Type u<VAR>ι : Type v<VAR>f : ι → Cardinal.{w}<VAR>hf : BddAbove (range f)<GOAL>lift.{u, w} (iSup f) = ⨆ i, lift.{u, w} (f i)
<VAR>α β : Type u<VAR>ι : Type v<VAR>f : ι → Cardinal.{w}<VAR>hf : BddAbove (range f)<GOAL>sSup (range (lift.{u, w} ∘ f)) = sSup (range fun i => lift.{u, w} (f i))
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M<GOAL>‖cderiv r f z‖ ≤ M / r
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M<VAR>hM : 0 ≤ M<GOAL>‖cderiv r f z‖ ≤ M / r
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>U K : Set ℂ<VAR>z : ℂ<VAR>M r δ : ℝ<VAR>φ : Filter ι<VAR>F : ι → ℂ → E<VAR>f g : ℂ → E<VAR>hr : 0 < r<VAR>hf : ∀ w ∈ sphere z r, ‖f w‖ ≤ M<VAR>hM : 0 ≤ M<VAR>h1 : ∀ w ∈ sphere z r, ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2<GOAL>‖cderiv r f z‖ ≤ M / r