awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
            HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) c : α)
              (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α)))) :
      αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) b : α)))) :
      αˢʸᵐ)
⊢ (a + b) * c = a * c + b * c

Tactic:
rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]

Premises used: add_mul, SymAlg.unsym_add, SymAlg.sym_add, mul_add, SymAlg.mul_def
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
h :
  HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
      HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) c : α)
        (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α)) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
⊢ Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
            HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) c : α)
              (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α)))) :
      αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) b : α)))) :
      αˢʸᵐ)

Tactic:
congr 2
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
h :
  HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) b : α)) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
⊢ HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
      HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) c : α)
        (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α)) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) b : α))

Tactic:
rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
⊢ HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) b : α)) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) b : α))

Tactic:
abel
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
x : αˢʸᵐ
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) 0 : α) ((unsym : (a : αˢʸᵐ) → α) x : α) +
            HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) ((unsym : (a : αˢʸᵐ) → α) 0 : α))) :
      αˢʸᵐ)
    (0 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) (0 : α) ((unsym : (a : αˢʸᵐ) → α) x : α) +
            HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) (0 : α))) :
      αˢʸᵐ)
    (0 : αˢʸᵐ)
rw₂ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (0 + HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) (0 : α))) :
      αˢʸᵐ)
    (0 : αˢʸᵐ)
rw₃ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 0 0) :
      αˢʸᵐ)
    (0 : αˢʸᵐ)
rw₄ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0) :
      αˢʸᵐ)
    (0 : αˢʸᵐ)
rw₅ : Eq.{u_1 + 1} (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) 0 : αˢʸᵐ) (0 : αˢʸᵐ)
rw₆ rw₇ : Eq.{u_1 + 1} (α := αˢʸᵐ) 0 0
⊢ 0 * x = 0

Tactic:
rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero,
        mul_zero, sym_zero]

Premises used: SymAlg.sym_zero, SymAlg.unsym_zero, MulZeroClass.zero_mul, MulZeroClass.mul_zero, add_zero, SymAlg.mul_def
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
x : αˢʸᵐ
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) ((unsym : (a : αˢʸᵐ) → α) 0 : α) +
            HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) 0 : α) ((unsym : (a : αˢʸᵐ) → α) x : α))) :
      αˢʸᵐ)
    (0 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) (0 : α) +
            HMul.hMul (α := α) (β := α) (0 : α) ((unsym : (a : αˢʸᵐ) → α) x : α))) :
      αˢʸᵐ)
    (0 : αˢʸᵐ)
rw₂ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) (0 : α) + 0)) :
      αˢʸᵐ)
    (0 : αˢʸᵐ)
rw₃ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 0 0) :
      αˢʸᵐ)
    (0 : αˢʸᵐ)
rw₄ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0) :
      αˢʸᵐ)
    (0 : αˢʸᵐ)
rw₅ : Eq.{u_1 + 1} (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) 0 : αˢʸᵐ) (0 : αˢʸᵐ)
rw₆ rw₇ : Eq.{u_1 + 1} (α := αˢʸᵐ) 0 0
⊢ x * 0 = 0

Tactic:
rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero,
        mul_zero, sym_zero]

Premises used: SymAlg.sym_zero, SymAlg.unsym_zero, MulZeroClass.zero_mul, MulZeroClass.mul_zero, add_zero, SymAlg.mul_def
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
x : αˢʸᵐ
rw :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) 1 : α) ((unsym : (a : αˢʸᵐ) → α) x : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) ((unsym : (a : αˢʸᵐ) → α) 1 : α))) =
    x
rw₁ :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) (1 : α) ((unsym : (a : αˢʸᵐ) → α) x : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) (1 : α))) =
    x
rw₂ :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        HAdd.hAdd (β := α) (HMul.hMul (α := α) (β := α) (1 : α) ((unsym : (a : αˢʸᵐ) → α) x : α))
          ((unsym : (a : αˢʸᵐ) → α) x : α)) =
    x
rw₃ :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) ((unsym : (a : αˢʸᵐ) → α) x : α)) =
    x
rw₄ :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        HMul.hMul (α := α) (β := α) (2 : α) ((unsym : (a : αˢʸᵐ) → α) x : α)) =
    x
rw₅ : (sym : (a : α) → αˢʸᵐ) ((unsym : (a : αˢʸᵐ) → α) x : α) = x
rw₆ rw₇ : x = x
⊢ 1 * x = x

Tactic:
rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_cancel_left, sym_unsym]

Premises used: invOf_mul_cancel_left, two_mul, SymAlg.sym_unsym, mul_one, one_mul, SymAlg.unsym_one, SymAlg.mul_def
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
x : αˢʸᵐ
rw :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) ((unsym : (a : αˢʸᵐ) → α) 1 : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) 1 : α) ((unsym : (a : αˢʸᵐ) → α) x : α))) =
    x
rw₁ :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) (1 : α) +
          HMul.hMul (α := α) (β := α) (1 : α) ((unsym : (a : αˢʸᵐ) → α) x : α))) =
    x
rw₂ :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        HAdd.hAdd (α := α) ((unsym : (a : αˢʸᵐ) → α) x : α)
          (HMul.hMul (α := α) (β := α) (1 : α) ((unsym : (a : αˢʸᵐ) → α) x : α))) =
    x
rw₃ :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) ((unsym : (a : αˢʸᵐ) → α) x : α)) =
    x
rw₄ :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        HMul.hMul (α := α) (β := α) (2 : α) ((unsym : (a : αˢʸᵐ) → α) x : α)) =
    x
rw₅ : (sym : (a : α) → αˢʸᵐ) ((unsym : (a : αˢʸᵐ) → α) x : α) = x
rw₆ rw₇ : x = x
⊢ x * 1 = x

Tactic:
rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_cancel_left, sym_unsym]

Premises used: invOf_mul_cancel_left, two_mul, SymAlg.sym_unsym, mul_one, one_mul, SymAlg.unsym_one, SymAlg.mul_def
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a : αˢʸᵐ
rw :
  (unsym : (a : αˢʸᵐ) → α)
      ((sym : (a : α) → αˢʸᵐ)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α))) :
        αˢʸᵐ) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)
rw₁ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)
rw₂ :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
      (2 * HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)
rw₃ rw₄ :
  HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)
⊢ (unsym : (a : αˢʸᵐ) → α) (a * a) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)

Tactic:
rw [mul_def, unsym_sym, ← two_mul, invOf_mul_cancel_left]

Premises used: invOf_mul_cancel_left, two_mul, SymAlg.unsym_sym, SymAlg.mul_def
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a : α
rw :
  Eq (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) (a * a) : αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * (a * a + a * a)) : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) (a * a) : αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * (2 * (a * a))) : αˢʸᵐ)
rw₂ rw₃ : Eq (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) (a * a) : αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) (a * a) : αˢʸᵐ)
⊢ (sym : (a : α) → αˢʸᵐ) (a * a) =
    HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)

Tactic:
rw [sym_mul_sym, ← two_mul, invOf_mul_cancel_left]

Premises used: invOf_mul_cancel_left, two_mul, SymAlg.sym_mul_sym
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddCommSemigroup α
inst_2 : One α
inst_3 : OfNat α 2
inst_4 : Invertible (α := α) 2
a b : αˢʸᵐ
rw :
  (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ inst inst_2 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))) =
    b * a
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst inst_2 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
            HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))) :
      αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst inst_2 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
            HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))) :
      αˢʸᵐ)
rw₂ rw₃ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst inst_2 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
            HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))) :
      αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst inst_2 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
            HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))) :
      αˢʸᵐ)
⊢ a * b = b * a

Tactic:
rw [mul_def, mul_def, add_comm]

Premises used: add_comm, SymAlg.mul_def
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a_1 b : αˢʸᵐ
a : α
⊢ Commute (HAdd.hAdd (α := α) 1 1) a

Tactic:
have := (Commute.one_left a).add_left (Commute.one_left a)
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a_1 b : αˢʸᵐ
a : α
this : Commute (HAdd.hAdd (α := α) 1 1) a
⊢ Commute 2 a

Tactic:
rw [one_add_one_eq_two] at this

Premises used: one_add_one_eq_two
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a_1 b : αˢʸᵐ
a : α
this : Commute 2 a
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _

Tactic:
this.invOf_left.eq

Premises used: Commute.invOf_left, Commute.eq
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a_1 b : αˢʸᵐ
a : α
this : Commute 2 a
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _

Tactic:
exact this.invOf_left.eq

Premises used: Commute.invOf_left, Commute.eq
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a b : αˢʸᵐ
⊢ ∀ (a : α),
    @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _

Tactic:
have commute_half_left := fun a : α => by
      have := (Commute.one_left a).add_left (Commute.one_left a)
      rw [one_add_one_eq_two] at this
      exact this.invOf_left.eq
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a b : αˢʸᵐ
commute_half_left :
  ∀ (a : α),
    @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _
⊢ a * b * (a * a) =
    (sym : (a : α) → αˢʸᵐ)
      (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
        (HMul.hMul (β := α)
                (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
                ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
              HMul.hMul (β := α)
                (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
                ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
            HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
              ((unsym : (a : αˢʸᵐ) → α) b : α) +
          HMul.hMul (β := α)
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
            ((unsym : (a : αˢʸᵐ) → α) a : α)))

Tactic:
?_
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a b : αˢʸᵐ
commute_half_left :
  ∀ (a : α),
    @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _
⊢ Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
            (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
          (HMul.hMul (β := α)
                  (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
                  ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                HMul.hMul (β := α)
                  (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
                  ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
              HMul.hMul (β := α)
                (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
                ((unsym : (a : αˢʸᵐ) → α) b : α) +
            HMul.hMul (β := α)
              (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
              ((unsym : (a : αˢʸᵐ) → α) a : α))) :
      αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
              ((unsym : (a : αˢʸᵐ) → α)
                  ((sym : (a : α) → αˢʸᵐ)
                      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                            ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                            ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                    αˢʸᵐ) :
                α) +
            HMul.hMul (α := α) (β := α)
              ((unsym : (a : αˢʸᵐ) → α)
                  ((sym : (a : α) → αˢʸᵐ)
                      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                            ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                            ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                    αˢʸᵐ) :
                α)
              ((unsym : (a : αˢʸᵐ) → α) a : α))) :
      αˢʸᵐ)

Tactic:
?_
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a b : αˢʸᵐ
commute_half_left :
  ∀ (a : α),
    @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _
⊢ (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
            ((unsym : (a : αˢʸᵐ) → α)
                ((sym : (a : α) → αˢʸᵐ)
                    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                          ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                          ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                  αˢʸᵐ) :
              α) +
          HMul.hMul (α := α) (β := α)
            ((unsym : (a : αˢʸᵐ) → α)
                ((sym : (a : α) → αˢʸᵐ)
                    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
                      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α)
                          ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
                        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)
                          ((unsym : (a : αˢʸᵐ) → α) b : α))) :
                  αˢʸᵐ) :
              α)
            ((unsym : (a : αˢʸᵐ) → α) a : α))) =
    a * (b * (a * a))

Tactic:
?_