-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
inst_3 : Invertible (a + b)
calc :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ ↔
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ * (a + b) =
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _) *
        (a + b)
calc₁ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ * (a + b) =
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _) *
        (a + b) ↔
    1 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * b)
calc₂ :
  1 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * b) ↔
    1 =
      1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b)
calc₃ :
  1 =
      1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) ↔
    1 =
      HAdd.hAdd (α := R) 1 1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
calc₄ :
  1 =
      HAdd.hAdd (α := R) 1 1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b ↔
    HAdd.hAdd (α := R) (-2) 1 =
      -2 +
        (2 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b)
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ ↔
    -1 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
have calc₅ : HAdd.hAdd (α := R) (-2) 1 =
    -2 +
      (2 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) ↔
  HAdd.hAdd (α := R) (-2) 1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
Tactic: calc ⅟(a + b) = ⅟a + ⅟b
      ↔ ⅟(a + b) * (a + b) = (⅟a + ⅟b) * (a + b) := by rw [mul_left_inj_of_invertible]
    _ ↔ 1 = ⅟a * a + ⅟b * a + (⅟a * b + ⅟b * b) := by rw [invOf_mul_self, mul_add, add_mul, add_mul]
    _ ↔ 1 = 1 + ⅟b * a + (1 + ⅟a * b) := by rw [invOf_mul_self, invOf_mul_self, add_comm _ 1]
    _ ↔ 1 = 1 + 1 + ⅟b * a + ⅟a * b := by rw [← add_assoc, add_comm _ 1, ← add_assoc]
    _ ↔ -2 + 1 = -2 + (2 + ⅟b * a + ⅟a * b) := by rw [one_add_one_eq_two, add_right_inj]
    _ ↔ -2 + 1 = ⅟b * a + ⅟a * b := by rw [← add_assoc, ← add_assoc, neg_add_cancel, zero_add]
    _ ↔ -1 + 0 = ⅟b * a + ⅟a * b := by rw [← one_add_one_eq_two, neg_add, add_assoc, neg_add_cancel]
    _ ↔ -1 = ⅟a * b + ⅟b * a := by rw [add_zero, add_comm]