diff --git a/Physlib/StatisticalMechanics/CanonicalEnsemble/TwoState.lean b/Physlib/StatisticalMechanics/CanonicalEnsemble/TwoState.lean
index b67dc0c5b..3904ff30a 100644
--- a/Physlib/StatisticalMechanics/CanonicalEnsemble/TwoState.lean
+++ b/Physlib/StatisticalMechanics/CanonicalEnsemble/TwoState.lean
@@ -104,8 +104,28 @@ informal_lemma twoState_entropy_eq where
   deps := [``twoState, ``thermodynamicEntropy]
 
 /-- A simplification of the `helmholtzFreeEnergy` of the two-state canonical ensemble. -/
-informal_lemma twoState_helmholtzFreeEnergy_eq where
-  tag := "EVMPR"
-  deps := [``twoState]
+lemma twoState_helmholtzFreeEnergy_eq (E₀ E₁ : ℝ) (T : Temperature) :
+    (twoState E₀ E₁).helmholtzFreeEnergy T =
+      (β T  * (E₀ + E₁) / 2 - Real.log
+          (2 * Real.cosh (β T * (E₁ - E₀) / 2))) / β T  := 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 [helmholtzFreeEnergy, twoState_partitionFunction_apply,
+    show (T.val : ℝ) = T.toReal by rfl,hE0, hE1]
+  have hfactor :
+      Real.exp (x + (- C)) + Real.exp (-x + (- C)) = Real.exp (-C) * (2 * Real.cosh x) := by
+    rw [Real.exp_add, Real.exp_add, Real.cosh_eq]
+    ring
+  rw [hfactor, Real.log_mul
+        (Real.exp_pos _).ne'
+        (by positivity : 2 * Real.cosh x ≠ 0)]
+  simp only [Real.log_exp,Temperature.β_toReal,div_eq_mul_inv, one_mul, inv_inv]
+  ring
 
 end CanonicalEnsemble