awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a +
            a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a + 1)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₂ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 1 1) : αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₃ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (HMul.hMul (α := α) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _) 2) : αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₄ : Eq.{u_1 + 1} (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) 1 : αˢʸᵐ) (1 : αˢʸᵐ)
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) =
    1
have rw₅ : Eq.{u_1 + 1} (α := αˢʸᵐ) 1 1
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ) =
    1
have rw : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
        (a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ +
          @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
    αˢʸᵐ)
  (1 : αˢʸᵐ)
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ +
            @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ) =
    1
have rw₁ : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
        (1 + @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
    αˢʸᵐ)
  (1 : αˢʸᵐ)
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ +
            @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (1 + @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ) =
    1
have rw₂ : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 1 1) : αˢʸᵐ)
  (1 : αˢʸᵐ)
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ +
            @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (1 + @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₂ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 1 1) : αˢʸᵐ)
    (1 : αˢʸᵐ)
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ) =
    1
have rw₃ : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ) (HMul.hMul (α := α) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _) 2) : αˢʸᵐ)
  (1 : αˢʸᵐ)
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ +
            @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (1 + @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₂ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 1 1) : αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₃ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (HMul.hMul (α := α) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _) 2) : αˢʸᵐ)
    (1 : αˢʸᵐ)
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ) =
    1
have rw₄ : Eq.{u_1 + 1} (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) 1 : αˢʸᵐ) (1 : αˢʸᵐ)
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ +
            @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (1 + @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₂ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 1 1) : αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₃ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (HMul.hMul (α := α) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _) 2) : αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₄ : Eq.{u_1 + 1} (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) 1 : αˢʸᵐ) (1 : αˢʸᵐ)
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ) =
    1
have rw₅ : Eq.{u_1 + 1} (α := αˢʸᵐ) 1 1
Tactic: rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
⊢ a * (b + c) = a * b + a * c
have rw : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
            (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α)) +
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
            HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)))) :
    αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
            HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
            HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)))) :
    αˢʸᵐ)
Tactic: rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
⊢ Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
              (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α)) +
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)))) :
      αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)))) :
      αˢʸᵐ)
have h : HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
      (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α)) +
    (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
      HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)) =
  HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
      HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
    (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
      HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
⊢ HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
        (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α)) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
have h : HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
      HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
    (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
      HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)) =
  HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
      HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
    (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
      HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
Tactic: rw [mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
⊢ (a + b) * c = a * c + b * c
have 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 : α)))) :
    αˢʸᵐ)
Tactic: rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
⊢ 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 : α)))) :
      αˢʸᵐ)
have 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 : α))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 : α)
        (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 : α))
have 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 : α))
Tactic: rw [mul_add]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
x : αˢʸᵐ
⊢ 0 * x = 0
have 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 : αˢʸᵐ)
Tactic: rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero,
        mul_zero, sym_zero]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 : αˢʸᵐ)
⊢ 0 * x = 0
have rw₁ : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (HMul.hMul (α := α) (β := α) (0 : α) ((unsym : (a : αˢʸᵐ) → α) x : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) (0 : α))) :
    αˢʸᵐ)
  (0 : αˢʸᵐ)
Tactic: rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero,
        mul_zero, sym_zero]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 : αˢʸᵐ)
⊢ 0 * x = 0
have rw₂ : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
        (0 + HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) x : α) (0 : α))) :
    αˢʸᵐ)
  (0 : αˢʸᵐ)
Tactic: rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero,
        mul_zero, sym_zero]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 : αˢʸᵐ)
⊢ 0 * x = 0
have rw₃ : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 0 0) :
    αˢʸᵐ)
  (0 : αˢʸᵐ)
Tactic: rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero,
        mul_zero, sym_zero]
-- Lean 4 proof step from Mathlib.Algebra.Symmetrized (goal)
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 : αˢʸᵐ)
⊢ 0 * x = 0
have rw₄ : Eq (α := αˢʸᵐ)
  ((sym : (a : α) → αˢʸᵐ) (HMul.hMul (α := α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 0) : αˢʸᵐ)
  (0 : αˢʸᵐ)
Tactic: rw [mul_def, unsym_zero, zero_mul, mul_zero, add_zero,
        mul_zero, sym_zero]