awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
of :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (0 * FreeAbelianGroup.of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          0 :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (FreeAbelianGroup.of L2) :
        R)
⊢ (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * FreeAbelianGroup.of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (FreeAbelianGroup.of L2) :
        R)
have of₁ : ∀ (L1 : α),
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (FreeAbelianGroup.of L1) :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (FreeAbelianGroup.of L2) :
        R)
Tactic: induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul, map_zero]
        | of L1 =>
          simp_rw [of_mul_of, lift_apply_of]
          exact f.map_mul _ _
        | neg L1 ih =>
          simp_rw [neg_mul, map_neg, neg_mul]
          exact congr_arg Neg.neg ih
        | add x1 x2 ih1 ih2 => simp only [add_mul, map_add, ih1, ih2]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
ih :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (of L2) :
        R)
⊢ (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * -of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (-of L2) :
        R)
have neg : (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
      (a : FreeAbelianGroup α) → R)
    (-(x * of L2)) =
  HMul.hMul (α := R) (β := R)
    ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        x :
      R)
    ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        (-of L2) :
      R)
Tactic: rw [mul_neg, map_neg, map_neg, mul_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
ih :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (of L2) :
        R)
neg :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (-(x * of L2)) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (-of L2) :
        R)
⊢ (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * -of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (-of L2) :
        R)
have neg₁ : -(((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * of L2) =
  HMul.hMul (α := R) (β := R)
    ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        x :
      R)
    ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        (-of L2) :
      R)
Tactic: rw [mul_neg, map_neg, map_neg, mul_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
x y1 y2 : FreeAbelianGroup α
ih1 :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * y1) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          y1 :
        R)
ih2 :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * y2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          y2 :
        R)
⊢ (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * (y1 + y2)) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (y1 + y2) :
        R)
have add : (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
      (a : FreeAbelianGroup α) → R)
    (x * y1 + x * y2) =
  HMul.hMul (α := R) (β := R)
    ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        x :
      R)
    ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        (y1 + y2) :
      R)
Tactic: rw [mul_add, map_add, map_add, mul_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
x y : FreeAbelianGroup α
⊢ (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * y) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          y :
        R)
have zero : (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
      (a : FreeAbelianGroup α) → R)
    (x * 0) =
  HMul.hMul (α := R) (β := R)
    ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        x :
      R)
    ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        0 :
      R)
Tactic: induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, map_zero]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul, map_zero]
        | of L1 =>
          simp_rw [of_mul_of, lift_apply_of]
          exact f.map_mul _ _
        | neg L1 ih =>
          simp_rw [neg_mul, map_neg, neg_mul]
          exact congr_arg Neg.neg ih
        | add x1 x2 ih1 ih2 => simp only [add_mul, map_add, ih1, ih2]
      | neg L2 ih => rw [mul_neg, map_neg, map_neg, mul_neg, ih]
      | add y1 y2 ih1 ih2 => rw [mul_add, map_add, map_add, mul_add, ih1, ih2]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
x y : FreeAbelianGroup α
zero :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * 0) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          0 :
        R)
⊢ (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * y) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          y :
        R)
have of : ∀ (L2 : α),
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (of L2) :
        R)
Tactic: induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, map_zero]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul, map_zero]
        | of L1 =>
          simp_rw [of_mul_of, lift_apply_of]
          exact f.map_mul _ _
        | neg L1 ih =>
          simp_rw [neg_mul, map_neg, neg_mul]
          exact congr_arg Neg.neg ih
        | add x1 x2 ih1 ih2 => simp only [add_mul, map_add, ih1, ih2]
      | neg L2 ih => rw [mul_neg, map_neg, map_neg, mul_neg, ih]
      | add y1 y2 ih1 ih2 => rw [mul_add, map_add, map_add, mul_add, ih1, ih2]
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
F : RingHom.{u, u_2} (FreeAbelianGroup α) R
⊢ Eq (α := AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R)
    (↑{
          toFun :=
            (⇑((lift : (a : α → R) → FreeAbelianGroup α →+ R)
                    (⇑(MonoidHom.comp (↑F : FreeAbelianGroup α →* R) ofMulHom) : (a : α) → R) :
                  AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R),
          map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
      FreeAbelianGroup α →+ R)
    (↑F : FreeAbelianGroup α →+ R)
have rw : Eq (α := AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R)
  (↑{
        toFun :=
          (⇑((lift : (a : α → R) → FreeAbelianGroup α →+ R)
                  (⇑(MonoidHom.comp (↑F : FreeAbelianGroup α →* R) ofMulHom) : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R),
        map_one' := sorry, map_mul' := sorry, map_zero' := sorry, map_add' := sorry } :
    FreeAbelianGroup α →+ R)
  ((lift : (a : α → R) → FreeAbelianGroup α →+ R)
    ((Equiv.symm lift : (a : FreeAbelianGroup α →+ R) → α → R) (↑F : FreeAbelianGroup α →+ R)))
Tactic: rw [← lift.apply_symm_apply (↑F : FreeAbelianGroup α →+ R)]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
⊢ of s * of t = of t * of s
have of : Eq (α := FreeAbelianGroup α)
  (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                of (Mul.mul x₁ x₂) :
              (a : FreeAbelianGroup α) → FreeAbelianGroup α)
            (of s) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of t) :
    FreeAbelianGroup α)
  (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                of (Mul.mul x₁ x₂) :
              (a : FreeAbelianGroup α) → FreeAbelianGroup α)
            (of t) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of s) :
    FreeAbelianGroup α)
Tactic: dsimp only [(· * ·), Mul.mul]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
⊢ Eq (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (of s) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (of t) :
      FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (of t) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (of s) :
      FreeAbelianGroup α)
have of : Eq (α := FreeAbelianGroup α)
  (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (Mul.mul x₁ t) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of s) :
    FreeAbelianGroup α)
  (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                of (Mul.mul x₁ x₂) :
              (a : FreeAbelianGroup α) → FreeAbelianGroup α)
            (of t) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of s) :
    FreeAbelianGroup α)
Tactic: rw [lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
⊢ Eq (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
            of (Mul.mul x₁ t) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (of s) :
      FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (of t) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (of s) :
      FreeAbelianGroup α)
have of : of (Mul.mul s t) =
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
        ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
              of (Mul.mul x₁ x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          (of t) :
      (a : FreeAbelianGroup α) → FreeAbelianGroup α)
    (of s)
Tactic: rw [lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
⊢ of (Mul.mul s t) =
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                of (Mul.mul x₁ x₂) :
              (a : FreeAbelianGroup α) → FreeAbelianGroup α)
            (of t) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of s)
have of : of (Mul.mul s t) =
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (Mul.mul x₁ s) :
      (a : FreeAbelianGroup α) → FreeAbelianGroup α)
    (of t)
Tactic: rw [lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
⊢ of (Mul.mul s t) =
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (Mul.mul x₁ s) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of t)
have of : of (Mul.mul s t) = of (Mul.mul t s)
Tactic: rw [lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
⊢ Eq (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (of s) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (of t) :
      FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (of t) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (of s) :
      FreeAbelianGroup α)
have of : of (Mul.mul s t) = of (Mul.mul t s)
Tactic: iterate 4 rw [lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
⊢ of (Mul.mul s t) = of (Mul.mul t s)
have of : Mul.mul s t = Mul.mul t s
Tactic: congr 1
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
ih : of s * of t = of t * of s
⊢ of s * -of t = -of t * of s
have of : -(of s * of t) = -of t * of s
Tactic: rw [mul_neg, ih, neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
ih : FreeAbelianGroup.of s * FreeAbelianGroup.of t = FreeAbelianGroup.of t * FreeAbelianGroup.of s
of : -(FreeAbelianGroup.of s * FreeAbelianGroup.of t) = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
⊢ FreeAbelianGroup.of s * -FreeAbelianGroup.of t = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
have of₁ : -(FreeAbelianGroup.of t * FreeAbelianGroup.of s) = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
Tactic: rw [mul_neg, ih, neg_mul_eq_neg_mul]