Two State probability fst

lemma twoState_probability_fst (E₀ E₁ : ℝ) (T : Temperature) :    (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + Real.tanh (β T * (E₁ - E₀) / 2)) := by  set x := β T * (E₁ - E₀) / 2  set C := β T * (E₀ + E₁) / 2  have hE0 : - β T * E₀ = x - C := by    simp [x, C]; ring  have hE1 : - β T * E₁ = -x - C := by    simp [x, C]; ring  rw [probability, mathematicalPartitionFunction_of_fintype]  simp only [twoState, Fin.sum_univ_two, Fin.isValue]  rw [hE0, hE1]  rw [Real.tanh_eq_sinh_div_cosh, Real.sinh_eq, Real.cosh_eq]  simp only [Real.exp_sub, Real.exp_neg]  field_simp  ring