awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
h : -a = b + a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Ring.Invertible
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
rw₁ rw₂ :
  -a = b + a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a ↔
    -a = 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

Tactic:
rw [mul_invOf_self, one_mul]

Premises used: mul_invOf_self, one_mul
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
⊢ -a =
      a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
        a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a ↔
    -a =
      a *
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
          @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a)

Tactic:
simp only [mul_add, mul_assoc]

Premises used: mul_assoc, mul_add
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
h :
  -a =
    a *
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a)
⊢ -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a

Tactic:
simpa using congr_arg (⅟a * ·) h

Premises used: HMul.hMul, Invertible.invOf, congr_arg
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
inst_1 : Invertible a
inst_2 : Invertible b
h :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ -a =
    a *
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a)

Tactic:
simp [← h]
-- 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 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 _
⊢ @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)

Tactic:
rw [mul_left_inj_of_invertible]

Premises used: mul_left_inj_of_invertible
-- 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 =
      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)
rw₂ 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)
⊢ 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)

Tactic:
rw [invOf_mul_self, invOf_mul_self, add_comm _ 1]

Premises used: invOf_mul_self, add_comm, OfNat.ofNat
-- 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 =
      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
rw₂ 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
⊢ 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]

Premises used: add_assoc, add_comm, OfNat.ofNat
-- 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 =
      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)
rw₁ 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
⊢ 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)

Tactic:
rw [one_add_one_eq_two, add_right_inj]

Premises used: one_add_one_eq_two, add_right_inj
-- 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 :
  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
rw₁ :
  HAdd.hAdd (α := R) (-2) 1 =
      HAdd.hAdd (α := R) (-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
rw₂ :
  HAdd.hAdd (α := R) (-2) 1 =
      0 + @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
rw₃ rw₄ :
  HAdd.hAdd (α := R) (-2) 1 =
      @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
⊢ 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:
rw [← add_assoc, ← add_assoc, neg_add_cancel, zero_add]

Premises used: add_assoc, zero_add, neg_add_cancel
-- 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 :
  -HAdd.hAdd (α := R) 1 1 + 1 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b ↔
    HAdd.hAdd (α := R) (-1) 0 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
rw₁ :
  HAdd.hAdd (α := R) (-1) (-1) + 1 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b ↔
    HAdd.hAdd (α := R) (-1) 0 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
rw₂ :
  -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) (-1) 0 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
rw₃ rw₄ :
  HAdd.hAdd (α := R) (-1) 0 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b ↔
    HAdd.hAdd (α := R) (-1) 0 =
      @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 ↔
    HAdd.hAdd (α := R) (-1) 0 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b

Tactic:
rw [← one_add_one_eq_two, neg_add, add_assoc, neg_add_cancel]

Premises used: add_assoc, neg_add, one_add_one_eq_two, neg_add_cancel
-- 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 b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b ↔
    -1 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
rw₁ rw₂ :
  -1 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a ↔
    -1 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ HAdd.hAdd (α := R) (-1) 0 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b ↔
    -1 =
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a

Tactic:
rw [add_zero, add_comm]

Premises used: add_comm, add_zero
-- 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)
h :
  @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

Tactic:
have h' := neg_one_eq_invOf_mul_add_invOf_mul_iff.mp h
-- 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)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a

Tactic:
have h_a_binv_a : -(b + a) = a * ⅟b * a := neg_add_eq_mul_invOf_mul_same_iff.mpr h'
-- 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)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b

Tactic:
rw [add_comm] at h'

Premises used: add_comm
-- 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)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h'₁ :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
⊢ -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a

Tactic:
rw [add_comm] at h'

Premises used: add_comm
-- 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)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ -(a + b) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b

Tactic:
neg_add_eq_mul_invOf_mul_same_iff.mpr h'

Premises used: Iff.mpr, neg_add_eq_mul_invOf_mul_same_iff
-- 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)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ -(a + b) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b

Tactic:
exact neg_add_eq_mul_invOf_mul_same_iff.mpr h'

Premises used: Iff.mpr, neg_add_eq_mul_invOf_mul_same_iff
-- 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)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
⊢ -(a + b) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b

Tactic:
have h_b_ainv_b : -(a + b) = b * ⅟a * b := by
    rw [add_comm] at h'
    exact neg_add_eq_mul_invOf_mul_same_iff.mpr h'
-- 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)
h :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne (a + b) _ =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _
h' :
  -1 =
    @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b +
      @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_a_binv_a : -(b + a) = a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a
h_b_ainv_b : -(a + b) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
rw : -(b + a) = b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b
rw₁ : -(b + a) = -(a + b)
rw₂ rw₃ : -(a + b) = -(a + b)
⊢ a * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne b _ * a =
    b * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne a _ * b

Tactic:
rw [← h_a_binv_a, ← h_b_ainv_b, add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
pos : ∀ (ha : IsUnit a), a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
neg : ∀ (ha : ¬IsUnit a), a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
by_cases ha : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ IsUnit b

Tactic:
have hb := h.mp ha
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
pos : ∀ (ia : Invertible a), a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
obtain ⟨ia⟩ := ha.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
pos : ∀ (ib : Invertible b), a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
obtain ⟨ib⟩ := hb.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
pos :
  @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne a _ + @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne b _ =
    @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne a _ * (a + b) *
      @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne b _
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
simp_rw [inverse_invertible, invOf_add_invOf]

Premises used: Ring.inverse_invertible, invOf_add_invOf
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
⊢ ¬IsUnit b

Tactic:
have hb := h.not.mp ha
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Semiring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : ¬IsUnit a
hb : ¬IsUnit b
⊢ a⁻¹ʳ + b⁻¹ʳ = a⁻¹ʳ * (a + b) * b⁻¹ʳ

Tactic:
simp [inverse_non_unit, ha, hb]

Premises used: Ring.inverse_non_unit
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
pos : ∀ (ha : IsUnit a), a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
neg : ∀ (ha : ¬IsUnit a), a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
by_cases ha : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
⊢ IsUnit b

Tactic:
have hb := h.mp ha
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
pos : ∀ (ia : Invertible a), a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
obtain ⟨ia⟩ := ha.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
pos : ∀ (ib : Invertible b), a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
obtain ⟨ib⟩ := hb.nonempty_invertible

Premises used: IsUnit.nonempty_invertible
-- Module: Mathlib.Algebra.Ring.Invertible
Goal:
R : Type u_1
inst : Ring R
a b : R
h : IsUnit a ↔ IsUnit b
ha : IsUnit a
hb : IsUnit b
ia : Invertible a
ib : Invertible b
pos :
  @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne a _ - @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne b _ =
    @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne a _ * (b - a) *
      @Invertible.invOf _ MulZeroClass.toMul MulOne.toOne b _
⊢ a⁻¹ʳ - b⁻¹ʳ = a⁻¹ʳ * (b - a) * b⁻¹ʳ

Tactic:
simp_rw [inverse_invertible, invOf_sub_invOf]

Premises used: Ring.inverse_invertible, invOf_sub_invOf