awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @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 _
rw₂ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (a + b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₃ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
Tactic: rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @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 _
rw₂ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₃ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (a + b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₄ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ *
      (b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _)
Tactic: rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @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 _
rw₂ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₃ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₄ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ *
        (b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _)
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (a + b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₅ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * 1
Tactic: rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @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 _
rw₂ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₃ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₄ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ *
        (b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _)
rw₅ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * 1
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (a + b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₆ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _
Tactic: rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Ring.Invertible (goal)
Goal:
R : Type u_1
inst : Semiring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @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 _
rw₂ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₃ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₄ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ *
        (b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _)
rw₅ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * 1
rw₆ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (a + b) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₇ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ =
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ +
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _
Tactic: rw [mul_add, invOf_mul_self, add_mul, one_mul, mul_assoc, mul_invOf_self, mul_one, add_comm]
-- 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
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (b - a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a) *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
Tactic: rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]
-- 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
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b -
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (b - a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b - 1) *
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
Tactic: rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]
-- 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
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b -
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b - 1) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (b - a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₂ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ -
    1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
Tactic: rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]
-- 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
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b -
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b - 1) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₂ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ -
      1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (b - a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₃ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ -
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
Tactic: rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]
-- 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
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b -
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b - 1) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₂ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ -
      1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₃ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (b - a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₄ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ *
      (b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _) -
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
Tactic: rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]
-- 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
rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b -
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₁ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b - 1) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₂ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ -
      1 * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₃ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b *
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
rw₄ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ *
        (b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _) -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * (b - a) *
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
have rw₅ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ -
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ =
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * 1 -
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
Tactic: rw [mul_sub, invOf_mul_self, sub_mul, one_mul, mul_assoc, mul_invOf_self, mul_one]