awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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
⊢ x * 1 = x
have rw₄ : (sym : (a : α) → αˢʸᵐ)
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
      HMul.hMul (α := α) (β := α) (2 : α) ((unsym : (a : αˢʸᵐ) → α) x : α)) =
  x
Tactic: rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_cancel_left, sym_unsym]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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
⊢ x * 1 = x
have rw₅ : (sym : (a : α) → αˢʸᵐ) ((unsym : (a : αˢʸᵐ) → α) x : α) = x
Tactic: rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_cancel_left, sym_unsym]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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
⊢ x * 1 = x
have rw₆ : x = x
Tactic: rw [mul_def, unsym_one, mul_one, one_mul, ← two_mul, invOf_mul_cancel_left, sym_unsym]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a : αˢʸᵐ
⊢ (unsym : (a : αˢʸᵐ) → α) (a * a) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)
have 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 : α)
Tactic: rw [mul_def, unsym_sym, ← two_mul, invOf_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 : α)
⊢ (unsym : (a : αˢʸᵐ) → α) (a * a) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)
have 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 : α)
Tactic: rw [mul_def, unsym_sym, ← two_mul, invOf_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 : α)
⊢ (unsym : (a : αˢʸᵐ) → α) (a * a) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)
have 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 : α)
Tactic: rw [mul_def, unsym_sym, ← two_mul, invOf_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 : α)
⊢ (unsym : (a : αˢʸᵐ) → α) (a * a) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)
have rw₃ : HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α) =
  HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) a : α)
Tactic: rw [mul_def, unsym_sym, ← two_mul, invOf_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a : α
⊢ (sym : (a : α) → αˢʸᵐ) (a * a) =
    HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)
have rw : Eq (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) (a * a) : αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * (a * a + a * a)) : αˢʸᵐ)
Tactic: rw [sym_mul_sym, ← two_mul, invOf_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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)) : αˢʸᵐ)
⊢ (sym : (a : α) → αˢʸᵐ) (a * a) =
    HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)
have rw₁ : Eq (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) (a * a) : αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * (2 * (a * a))) : αˢʸᵐ)
Tactic: rw [sym_mul_sym, ← two_mul, invOf_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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))) : αˢʸᵐ)
⊢ (sym : (a : α) → αˢʸᵐ) (a * a) =
    HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)
have rw₂ : Eq (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) (a * a) : αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) (a * a) : αˢʸᵐ)
Tactic: rw [sym_mul_sym, ← two_mul, invOf_mul_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddCommSemigroup α
inst_2 : One α
inst_3 : OfNat α 2
inst_4 : Invertible (α := α) 2
a b : αˢʸᵐ
⊢ a * b = b * a
have 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
Tactic: rw [mul_def, mul_def, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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
⊢ a * b = b * a
have 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 : α))) :
    αˢʸᵐ)
Tactic: rw [mul_def, mul_def, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 : α))) :
      αˢʸᵐ)
⊢ a * b = b * a
have 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 : α))) :
    αˢʸᵐ)
Tactic: rw [mul_def, mul_def, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (hypothesis)
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a_1 b : αˢʸᵐ
a : α
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _
have this : Commute (HAdd.hAdd (α := α) 1 1) a
Tactic: have := (Commute.one_left a).add_left (Commute.one_left a)
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (hypothesis)
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a_1 b : αˢʸᵐ
a : α
this : Commute (HAdd.hAdd (α := α) 1 1) a
⊢ @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _ * a = a * @Invertible.invOf _ MulOne.toMul MulOne.toOne 2 _
have this₁ : Commute 2 a
Tactic: rw [one_add_one_eq_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (hypothesis)
Goal:
α : Type u_1
inst : Ring α
inst_1 : Invertible (α := α) 2
a b : αˢʸᵐ
⊢ a * b * (a * a) = a * (b * (a * a))
have commute_half_left : ∀ (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
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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) = a * (b * (a * a))
have calc_1 : 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: calc a * b * (a * a)
      _ = sym (⅟2 * ⅟2 * (unsym a * unsym b * unsym (a * a) +
          unsym b * unsym a * unsym (a * a) +
          unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a)) := ?_
      _ = sym (⅟2 * (unsym a *
          unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) +
          unsym (sym (⅟2 * (unsym b * unsym (a * a) + unsym (a * a) * unsym b))) * unsym a)) := ?_
      _ = a * (b * (a * a)) := ?_
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 : α)))
have calc_1 : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * b) : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) (a * b) : α))) :
    αˢʸᵐ)
  ((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: rw [mul_def, mul_def a b, unsym_sym, ← mul_assoc, ← commute_half_left (unsym (a * a)),
        mul_assoc, mul_assoc, ← mul_add, ← mul_assoc, add_mul, mul_add (unsym (a * a)),
        ← add_assoc, ← mul_assoc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 _
| HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
    (HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α)) +
      HMul.hMul (β := α)
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
        ((unsym : (a : αˢʸᵐ) → α) a : α))
have rw : HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
    (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) *
  (HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α)) +
      HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α)) +
    HMul.hMul (β := α)
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) (a * a) : α) ((unsym : (a : αˢʸᵐ) → α) b : α))
      ((unsym : (a : αˢʸᵐ) → α) a : α))
Tactic: rw [mul_add (unsym a)]