-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
inst_3 : Invertible (a + b)
rw :
  1 =
      (@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)
rw₁ :
  1 =
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _) *
          a +
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _) *
          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)
rw₂ :
  1 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
            @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _) *
          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)
rw₃ rw₄ :
  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 =
      @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)
⊢ @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)

Tactic:
rw [invOf_mul_self, mul_add, add_mul, add_mul]

Premises used: add_mul, invOf_mul_self, mul_add