F alpha le at optimizer

theorem f_alpha_le_at_optimizer (hα : 1 < α) (ρ σ : MState d)    (H : HermitianMat d ℂ) (hH : 0 ≤ H) (hker : σ.M.ker ≤ ρ.M.ker) :    f_alpha α H ρ σ ≤ f_alpha α (H_hat α ρ σ) ρ σ := by  rw [f_alpha_at_optimizer hα]  -- Goal: f_alpha α H ρ σ ≤ Q̃_α(ρ‖σ)  set γ : ℝ := (1 - α) / (2 * α) with hγ_def  have hγ : γ ≠ 0 := by    intro h; have h1 : (1 - α) / (2 * α) = 0 := hγ_def ▸ h    have h2 : (2 : ℝ) * α ≠ 0 := by positivity    rw [div_eq_zero_iff] at h1; rcases h1 with h1 | h1 <;> linarith  set A := ρ.M.conj (σ.M ^ γ).mat  set B := H.conj (σ.M ^ (-γ)).mat  have hA_nn : 0 ≤ A := HermitianMat.conj_nonneg _ ρ.nonneg  have hB_nn : 0 ≤ B := HermitianMat.conj_nonneg _ hH  have h_inner : ⟪ρ.M, H⟫_ℝ = ⟪A, B⟫_ℝ :=    inner_eq_inner_conj_of_ker_le ρ σ H hker γ hγ  have hpq : 1 / α + 1 / (α / (α - 1)) = 1 := by field_simp; ring  have h_young := HermitianMat.trace_young A B hA_nn hB_nn α (α / (α - 1)) hα hpq  have hα_pos : (0 : ℝ) < α := by linarith  have hαm1_pos : (0 : ℝ) < α - 1 := by linarith  -- Multiply h_young by α and simplify  have h_scaled : α * ⟪A, B⟫_ℝ ≤      (A ^ α).trace + (α - 1) * (B ^ (α / (α - 1))).trace := by    have := mul_le_mul_of_nonneg_left h_young hα_pos.le    have h_simp : α * ((A ^ α).trace / α + (B ^ (α / (α - 1))).trace / (α / (α - 1))) =        (A ^ α).trace + (α - 1) * (B ^ (α / (α - 1))).trace := by      field_simp    linarith  -- Goal is definitionally: α * ⟪ρ.M, H⟫ - (α-1) * (B ^ (α/(α-1))).trace ≤ (A ^ α).trace  -- which follows from h_scaled and h_inner  change α * ⟪ρ.M, H⟫_ℝ - (α - 1) * (B ^ (α / (α - 1))).trace ≤ (A ^ α).trace  have h_inner_scaled : α * ⟪ρ.M, H⟫_ℝ = α * ⟪A, B⟫_ℝ := by rw [h_inner]  linarith [h_scaled, h_inner_scaled]