Not achieves Rate gt log dim out

theorem not_achievesRate_gt_log_dim_out (Λ : CPTPMap d₁ d₂) {R : ℝ} (hR : Real.logb 2 (Fintype.card d₂) < R): ¬Λ.AchievesRate R := by  intro h;  -- We show that the identity channel on the output space `d₂` emulates `Λ`. Since capacity is monotonic under emulation, `Q(Λ) ≤ Q(id_{d₂})`.  have h_emulate : (CPTPMap.id (dIn := d₂)).Emulates Λ := by    exact ⟨Λ, CPTPMap.id, by simp⟩  -- If `Λ` achieves rate `R`, then `id_{d₂}` achieves rate `R`. This follows because if `Λ^{\otimes n}` emulates `B`, and `id^{\otimes n}` emulates `Λ^{\otimes n}` (by functoriality of tensor product), then `id^{\otimes n}` emulates `B`.  have h_id_achieves : (CPTPMap.id (dIn := d₂)).AchievesRate R := by    intro ε hε_pos    obtain ⟨n, hn, dimB, B, hB_emulate, hB_rate, hB_approx⟩ := h ε hε_pos    have h_id_emulate : (CPTPMap.piProd (fun (_ : Fin n) => CPTPMap.id (dIn := d₂))).Emulates B := by      -- Since `id_{d₂}` emulates `Λ`, we can use the fact that the tensor product of emulations is an emulation.      have h_tensor_emulate : ∀ (n : ℕ), (CPTPMap.piProd (fun (_ : Fin n) => CPTPMap.id (dIn := d₂))).Emulates (CPTPMap.piProd (fun (_ : Fin n) => Λ)) := by        intro n        obtain ⟨E, D, hD⟩ := h_emulate        use CPTPMap.piProd (fun (_ : Fin n) => E), CPTPMap.piProd (fun (_ : Fin n) => D);        simp [ ← hD, ← CPTPMap.piProd_comp];      exact emulates_trans _ _ _ ( h_tensor_emulate n ) hB_emulate;    exact ⟨ n, hn, dimB, B, h_id_emulate, hB_rate, hB_approx ⟩;  refine not_le_of_gt hR <| not_lt.mp fun h => ?_  exact not_lt_of_ge ( le_of_not_gt fun h' => not_achievesRate_gt_log_dim_in _ h' h_id_achieves ) h