awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 _
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 _
⊢ @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 _ -
    @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
⊢ -a = b + a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a ↔
    -a =
      a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
        a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
have rw : -a = b + a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a ↔
  -a = 1 * b + a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
Tactic: rw [mul_invOf_self, one_mul]
-- 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 :
  -a = b + a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a ↔
    -a = 1 * b + a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ -a = b + a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a ↔
    -a =
      a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
        a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
have rw₁ : -a = b + a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a ↔
  -a = b + a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
Tactic: rw [mul_invOf_self, one_mul]
-- 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)
⊢ @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)
have rw : @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) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
Tactic: rw [mul_left_inj_of_invertible]
-- 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)
⊢ @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)
have 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)
Tactic: rw [invOf_mul_self, mul_add, add_mul, add_mul]
-- 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)
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)
⊢ @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)
have 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)
Tactic: rw [invOf_mul_self, mul_add, add_mul, add_mul]
-- 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)
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)
⊢ @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)
have 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)
Tactic: rw [invOf_mul_self, mul_add, add_mul, add_mul]
-- 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)
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)
⊢ @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)
have 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)
Tactic: rw [invOf_mul_self, mul_add, add_mul, add_mul]
-- 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)
⊢ 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)
have rw : 1 =
    1 + @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)
Tactic: rw [invOf_mul_self, invOf_mul_self, add_comm _ 1]
-- 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)
rw :
  1 =
      1 + @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)
⊢ 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)
have rw₁ : 1 =
    1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b + 1) ↔
  1 =
    1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b)
Tactic: rw [invOf_mul_self, invOf_mul_self, add_comm _ 1]
-- 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)
rw :
  1 =
      1 + @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)
rw₁ :
  1 =
      1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b + 1) ↔
    1 =
      1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 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) ↔
    1 =
      1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b)
have rw₂ : 1 =
    1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b) ↔
  1 =
    1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b)
Tactic: rw [invOf_mul_self, invOf_mul_self, add_comm _ 1]
-- 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)
⊢ 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
have rw : 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
Tactic: rw [← add_assoc, add_comm _ 1, ← add_assoc]
-- 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)
rw :
  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
⊢ 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
have rw₁ : 1 =
    1 + (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a) +
      @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
Tactic: rw [← add_assoc, add_comm _ 1, ← add_assoc]
-- 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)
rw :
  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
rw₁ :
  1 =
      1 + (1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a) +
        @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
⊢ 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
have rw₂ : 1 =
    HAdd.hAdd (α := R) 1 1 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      @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
Tactic: rw [← add_assoc, add_comm _ 1, ← add_assoc]
-- 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)
⊢ 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)
have rw : 1 =
    2 + @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)
Tactic: rw [one_add_one_eq_two, add_right_inj]
-- 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)
rw :
  1 =
      2 + @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)
⊢ 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)
have rw₁ : 1 =
    2 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b ↔
  1 =
    2 + @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
Tactic: rw [one_add_one_eq_two, add_right_inj]