awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
⊢ ∀ (x : α),
    Eq.{u_2 + 1} (α := R)
      (((fun (F : RingHom.{u, u_2} (FreeAbelianGroup α) R) ↦
                (MonoidHom.comp (↑F : FreeAbelianGroup α →* R) ofMulHom : α →* R))
              ((fun (f : α →* R) ↦
                  let __src : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R :=
                    (lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R);
                  ({
                      toFun :=
                        (⇑((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                          (a : FreeAbelianGroup α) → R),
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
                    RingHom.{u, u_2} (FreeAbelianGroup α) R))
                f) :
            (a : α) → R)
          x :
        R)
      ((f : (a : α) → R) x : R)

Tactic:
simp only [RingHom.coe_monoidHom_mk, MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk,
      ofMulHom_coe, Function.comp_apply, lift_apply_of, forall_const]

Premises used: MonoidHom.coe_comp, OneHom.coe_mk, MonoidHom.coe_mk, forall_const, Function.comp_apply, FreeAbelianGroup.ofMulHom_coe, RingHom.coe_monoidHom_mk, FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
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
simp :
  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)
⊢ Eq (α := AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R)
    ((fun (f : RingHom.{u, u_2} (FreeAbelianGroup α) R) ↦
        ((↑f : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R))
      ((fun (f : α →* R) ↦
          let __src : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R :=
            (lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R);
          ({
              toFun :=
                (⇑((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                      AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                  (a : FreeAbelianGroup α) → R),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            RingHom.{u, u_2} (FreeAbelianGroup α) R))
        ((fun (F : RingHom.{u, u_2} (FreeAbelianGroup α) R) ↦
            (MonoidHom.comp (↑F : FreeAbelianGroup α →* R) ofMulHom : α →* R))
          F)))
    ((fun (f : RingHom.{u, u_2} (FreeAbelianGroup α) R) ↦
        ((↑f : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R))
      F)

Tactic:
simp only
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
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
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' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
      FreeAbelianGroup α →+ R)
    ((lift : (a : α → R) → FreeAbelianGroup α →+ R)
      ((Equiv.symm lift : (a : FreeAbelianGroup α →+ R) → α → R) (↑F : 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)

Tactic:
rw [← lift.apply_symm_apply (↑F : FreeAbelianGroup α →+ R)]

Premises used: Equiv.apply_symm_apply, AddMonoidHomClass.toAddMonoidHom, FreeAbelianGroup.lift
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
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)
    ((lift : (a : α → R) → FreeAbelianGroup α →+ R)
      ((Equiv.symm lift : (a : FreeAbelianGroup α →+ R) → α → R) (↑F : FreeAbelianGroup α →+ R)))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
⊢ Eq (α := AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R)
    (↑((liftMonoid : (a : α →* R) → FreeAbelianGroup α →+* R) f : RingHom.{u, u_2} (FreeAbelianGroup α) R) :
      FreeAbelianGroup α →+ R)
    ((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R))

Tactic:
rfl

Premises used: Quotient.liftOn', AddMonoidHomClass.toAddMonoidHom, Additive, Multiplicative, Con.liftOn, FreeAbelianGroup, rfl
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
⊢ Eq (α := (a : FreeAbelianGroup α) → R)
    (⇑((liftMonoid : (a : α →* R) → FreeAbelianGroup α →+* R) f : RingHom.{u, u_2} (FreeAbelianGroup α) R) :
      (a : FreeAbelianGroup α) → R)
    (⇑((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
          AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
      (a : FreeAbelianGroup α) → R)

Tactic:
rfl

Premises used: FreeAbelianGroup, rfl
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : RingHom.{u, u_2} (FreeAbelianGroup α) R
⊢ Eq (α := (a : α) → R) (⇑((Equiv.symm liftMonoid : (a : FreeAbelianGroup α →+* R) → α →* R) f : α →* R) : (a : α) → R)
    ((Equiv.symm lift : (a : FreeAbelianGroup α →+ R) → α → R) (↑f : FreeAbelianGroup α →+ R))

Tactic:
rfl

Premises used: FreeAbelianGroup.of, rfl
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y : FreeAbelianGroup α
⊢ 0 * y = y * 0

Tactic:
zero_mul y

Premises used: Quotient.liftOn', MulZeroClass.zero_mul, FreeGroup.Lift.aux, Con.liftOn, List.foldr, List.prod
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y : FreeAbelianGroup α
⊢ 0 * y = y * 0

Tactic:
exact zero_mul y

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s : α
⊢ of s * 0 = 0 * of s

Tactic:
(zero_mul _).symm

Premises used: Quotient.liftOn', MulZeroClass.zero_mul, FreeGroup.Lift.aux, Con.liftOn, Eq.symm, List.foldr, List.prod
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s : α
⊢ of s * 0 = 0 * of s

Tactic:
exact (zero_mul _).symm

Premises used: MulZeroClass.zero_mul, Eq.symm
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
of :
  Eq (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  FreeAbelianGroup.of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (FreeAbelianGroup.of s) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of t) :
      FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  FreeAbelianGroup.of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (FreeAbelianGroup.of t) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of s) :
      FreeAbelianGroup α)
⊢ FreeAbelianGroup.of s * FreeAbelianGroup.of t = FreeAbelianGroup.of t * FreeAbelianGroup.of s

Tactic:
dsimp only [(· * ·), Mul.mul]

Premises used: HMul.hMul, Mul.mul
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
of :
  Eq (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
            FreeAbelianGroup.of (Mul.mul x₁ t) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of s) :
      FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  FreeAbelianGroup.of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (FreeAbelianGroup.of t) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of s) :
      FreeAbelianGroup α)
⊢ Eq (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  FreeAbelianGroup.of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (FreeAbelianGroup.of s) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of t) :
      FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  FreeAbelianGroup.of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (FreeAbelianGroup.of t) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of s) :
      FreeAbelianGroup α)

Tactic:
rw [lift_apply_of]

Premises used: FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
of :
  FreeAbelianGroup.of (Mul.mul s t) =
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                FreeAbelianGroup.of (Mul.mul x₁ x₂) :
              (a : FreeAbelianGroup α) → FreeAbelianGroup α)
            (FreeAbelianGroup.of t) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (FreeAbelianGroup.of s)
⊢ Eq (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
            FreeAbelianGroup.of (Mul.mul x₁ t) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of s) :
      FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  FreeAbelianGroup.of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (FreeAbelianGroup.of t) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of s) :
      FreeAbelianGroup α)

Tactic:
rw [lift_apply_of]

Premises used: FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
of :
  FreeAbelianGroup.of (Mul.mul s t) =
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
          FreeAbelianGroup.of (Mul.mul x₁ s) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (FreeAbelianGroup.of t)
⊢ FreeAbelianGroup.of (Mul.mul s t) =
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                FreeAbelianGroup.of (Mul.mul x₁ x₂) :
              (a : FreeAbelianGroup α) → FreeAbelianGroup α)
            (FreeAbelianGroup.of t) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (FreeAbelianGroup.of s)

Tactic:
rw [lift_apply_of]

Premises used: FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
of : FreeAbelianGroup.of (Mul.mul s t) = FreeAbelianGroup.of (Mul.mul t s)
⊢ FreeAbelianGroup.of (Mul.mul s t) =
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
          FreeAbelianGroup.of (Mul.mul x₁ s) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (FreeAbelianGroup.of t)

Tactic:
rw [lift_apply_of]

Premises used: FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
of : FreeAbelianGroup.of (Mul.mul s t) = FreeAbelianGroup.of (Mul.mul t s)
⊢ Eq (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  FreeAbelianGroup.of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (FreeAbelianGroup.of s) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of t) :
      FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                  FreeAbelianGroup.of (Mul.mul x₁ x₂) :
                (a : FreeAbelianGroup α) → FreeAbelianGroup α)
              (FreeAbelianGroup.of t) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of s) :
      FreeAbelianGroup α)

Tactic:
iterate 4 rw [lift_apply_of]

Premises used: FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
of : Mul.mul s t = Mul.mul t s
⊢ FreeAbelianGroup.of (Mul.mul s t) = FreeAbelianGroup.of (Mul.mul t s)

Tactic:
congr 1
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
⊢ Mul.mul s t = Mul.mul t s

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s t : α
⊢ Mul.mul s t = Mul.mul t s

Tactic:
exact mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
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
of₁ : -(FreeAbelianGroup.of t * FreeAbelianGroup.of s) = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
of₂ of₃ : -FreeAbelianGroup.of t * FreeAbelianGroup.of s = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
⊢ FreeAbelianGroup.of s * -FreeAbelianGroup.of t = -FreeAbelianGroup.of t * FreeAbelianGroup.of s

Tactic:
rw [mul_neg, ih, neg_mul_eq_neg_mul]

Premises used: neg_mul_eq_neg_mul, mul_neg
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
s : α
y1 y2 : FreeAbelianGroup α
ih1 : FreeAbelianGroup.of s * y1 = y1 * FreeAbelianGroup.of s
ih2 : FreeAbelianGroup.of s * y2 = y2 * FreeAbelianGroup.of s
of : FreeAbelianGroup.of s * y1 + FreeAbelianGroup.of s * y2 = (y1 + y2) * FreeAbelianGroup.of s
of₁ : FreeAbelianGroup.of s * y1 + FreeAbelianGroup.of s * y2 = y1 * FreeAbelianGroup.of s + y2 * FreeAbelianGroup.of s
of₂ : y1 * FreeAbelianGroup.of s + FreeAbelianGroup.of s * y2 = y1 * FreeAbelianGroup.of s + y2 * FreeAbelianGroup.of s
of₃ of₄ :
  y1 * FreeAbelianGroup.of s + y2 * FreeAbelianGroup.of s = y1 * FreeAbelianGroup.of s + y2 * FreeAbelianGroup.of s
⊢ FreeAbelianGroup.of s * (y1 + y2) = (y1 + y2) * FreeAbelianGroup.of s

Tactic:
rw [mul_add, add_mul, ih1, ih2]

Premises used: add_mul, mul_add
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y : FreeAbelianGroup α
s : α
of : FreeAbelianGroup.of s * 0 = 0 * FreeAbelianGroup.of s
of₁ : ∀ (t : α), FreeAbelianGroup.of s * FreeAbelianGroup.of t = FreeAbelianGroup.of t * FreeAbelianGroup.of s
of₂ :
  ∀ (t : α) (ih : FreeAbelianGroup.of s * FreeAbelianGroup.of t = FreeAbelianGroup.of t * FreeAbelianGroup.of s),
    FreeAbelianGroup.of s * -FreeAbelianGroup.of t = -FreeAbelianGroup.of t * FreeAbelianGroup.of s
of₃ :
  ∀ (y1 y2 : FreeAbelianGroup α) (ih1 : FreeAbelianGroup.of s * y1 = y1 * FreeAbelianGroup.of s)
    (ih2 : FreeAbelianGroup.of s * y2 = y2 * FreeAbelianGroup.of s),
    FreeAbelianGroup.of s * (y1 + y2) = (y1 + y2) * FreeAbelianGroup.of s
⊢ FreeAbelianGroup.of s * y = y * FreeAbelianGroup.of s

Tactic:
induction y using FreeAbelianGroup.induction_on with
      | zero => exact (zero_mul _).symm
      | of t =>
        dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _
      | neg t ih => rw [mul_neg, ih, neg_mul_eq_neg_mul]
      | add y1 y2 ih1 ih2 => rw [mul_add, add_mul, ih1, ih2]

Premises used: add_mul, HMul.hMul, MulZeroClass.zero_mul, Mul.mul, FreeAbelianGroup.of, mul_comm, mul_add, neg_mul_eq_neg_mul, FreeAbelianGroup.lift_apply_of, Eq.symm, mul_neg
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y : FreeAbelianGroup α
s : α
ih : of s * y = y * of s
neg : -(of s * y) = y * -of s
neg₁ : -(y * of s) = y * -of s
neg₂ neg₃ : y * -of s = y * -of s
⊢ -of s * y = y * -of s

Tactic:
rw [neg_mul, ih, neg_mul_eq_mul_neg]

Premises used: neg_mul_eq_mul_neg, neg_mul
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
add : x1 * y + x2 * y = y * (x1 + x2)
add₁ : x1 * y + x2 * y = y * x1 + y * x2
add₂ : y * x1 + x2 * y = y * x1 + y * x2
add₃ add₄ : y * x1 + y * x2 = y * x1 + y * x2
⊢ (x1 + x2) * y = y * (x1 + x2)

Tactic:
rw [add_mul, mul_add, ih1, ih2]

Premises used: add_mul, mul_add
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : CommMonoid α
x y : FreeAbelianGroup α
zero : 0 * y = y * 0
of : ∀ (s : α), FreeAbelianGroup.of s * y = y * FreeAbelianGroup.of s
neg :
  ∀ (s : α) (ih : FreeAbelianGroup.of s * y = y * FreeAbelianGroup.of s),
    -FreeAbelianGroup.of s * y = y * -FreeAbelianGroup.of s
add : ∀ (x1 x2 : FreeAbelianGroup α) (ih1 : x1 * y = y * x1) (ih2 : x2 * y = y * x2), (x1 + x2) * y = y * (x1 + x2)
⊢ x * y = y * x

Tactic:
induction x using FreeAbelianGroup.induction_on with
    | zero => exact zero_mul y
    | of s =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => exact (zero_mul _).symm
      | of t =>
        dsimp only [(· * ·), Mul.mul]
        iterate 4 rw [lift_apply_of]
        congr 1
        exact mul_comm _ _
      | neg t ih => rw [mul_neg, ih, neg_mul_eq_neg_mul]
      | add y1 y2 ih1 ih2 => rw [mul_add, add_mul, ih1, ih2]
    | neg s ih => rw [neg_mul, ih, neg_mul_eq_mul_neg]
    | add x1 x2 ih1 ih2 => rw [add_mul, mul_add, ih1, ih2]

Premises used: add_mul, HMul.hMul, MulZeroClass.zero_mul, neg_mul_eq_mul_neg, Mul.mul, FreeAbelianGroup.of, mul_comm, mul_add, neg_mul, neg_mul_eq_neg_mul, FreeAbelianGroup.lift_apply_of, Eq.symm, mul_neg
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
z : FreeAbelianGroup T
⊢ Eq.{u_2 + 1} (α := FreeAbelianGroup T)
    ((fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default))
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
          (a : FreeAbelianGroup T) → ℤ)
        0))
    0

Tactic:
simp only [zero_smul, map_zero]

Premises used: map_zero, zero_smul
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
z : FreeAbelianGroup T
⊢ Eq.{u_2 + 1} (α := FreeAbelianGroup T)
    ((fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default))
      ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
          (a : FreeAbelianGroup T) → ℤ)
        (of default)))
    (of default)

Tactic:
simp only [one_smul, lift_apply_of]

Premises used: one_smul, FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst : Unique T
z : FreeAbelianGroup T
⊢ Eq.{u_2 + 1} (α := FreeAbelianGroup T)
      ((fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default))
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
            (a : FreeAbelianGroup T) → ℤ)
          (of default)))
      (of default) →
    Eq.{u_2 + 1} (α := FreeAbelianGroup T)
      ((fun (n : ℤ) ↦ HSMul.hSMul (β := FreeAbelianGroup T) n (of default))
        ((((lift : (a : T → ℤ) → FreeAbelianGroup T →+ ℤ) fun (x : T) ↦ 1 : FreeAbelianGroup T →+ ℤ) :
            (a : FreeAbelianGroup T) → ℤ)
          (-of default)))
      (-of default)

Tactic:
simp