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
L : α
of : FreeAbelianGroup.of (1 * L) = FreeAbelianGroup.of L
of₁ of₂ : FreeAbelianGroup.of L = FreeAbelianGroup.of L
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          FreeAbelianGroup.of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (FreeAbelianGroup.of L) =
    FreeAbelianGroup.of L

Tactic:
rw [lift_apply_of, one_mul]

Premises used: FreeAbelianGroup.lift_apply_of, one_mul
-- 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
L : α
ih :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of L) =
    of L
neg :
  -((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (of L) =
    -of L
neg₁ neg₂ : -of L = -of L
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (-of L) =
    -of L

Tactic:
rw [map_neg, ih]

Premises used: map_neg
-- 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
x1 x2 : FreeAbelianGroup α
ih1 :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x1 =
    x1
ih2 :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x2 =
    x2
add :
  HAdd.hAdd (α := FreeAbelianGroup α) (β := FreeAbelianGroup α)
      (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x1 :
        FreeAbelianGroup α)
      (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x2 :
        FreeAbelianGroup α) =
    x1 + x2
add₁ :
  HAdd.hAdd (β := FreeAbelianGroup α) x1
      (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x2 :
        FreeAbelianGroup α) =
    x1 + x2
add₂ add₃ : x1 + x2 = x1 + x2
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (x1 + x2) =
    x1 + x2

Tactic:
rw [map_add, ih1, ih2]

Premises used: map_add
-- 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
x : FreeAbelianGroup α
zero :
  Eq.{u + 1} (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          FreeAbelianGroup.of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      0)
    0
of :
  ∀ (L : α),
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            FreeAbelianGroup.of (1 * x₂) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of L) =
      FreeAbelianGroup.of L
neg :
  ∀ (L : α)
    (ih :
      ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
              FreeAbelianGroup.of (1 * x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          (FreeAbelianGroup.of L) =
        FreeAbelianGroup.of L),
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            FreeAbelianGroup.of (1 * x₂) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (-FreeAbelianGroup.of L) =
      -FreeAbelianGroup.of L
add :
  ∀ (x1 x2 : FreeAbelianGroup α)
    (ih1 :
      ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
              FreeAbelianGroup.of (1 * x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x1 =
        x1)
    (ih2 :
      ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
              FreeAbelianGroup.of (1 * x₂) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x2 =
        x2),
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
            FreeAbelianGroup.of (1 * x₂) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (x1 + x2) =
      x1 + x2
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          FreeAbelianGroup.of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x

Tactic:
induction x using FreeAbelianGroup.induction_on with
    | zero => rfl
    | of L => rw [lift_apply_of, one_mul]
    | neg L ih => rw [map_neg, ih]
    | add x1 x2 ih1 ih2 => rw [map_add, ih1, ih2]

Premises used: map_add, map_neg, FreeAbelianGroup.of, FreeAbelianGroup.lift_apply_of, one_mul
-- 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
x : FreeAbelianGroup α
rw :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
⊢ x * 1 = x

Tactic:
rw [mul_def, one_def, lift_apply_of]

Premises used: FreeAbelianGroup.one_def, FreeAbelianGroup.mul_def, 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
⊢ Eq.{u + 1} (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      0)
    0

Tactic:
rfl
-- 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
L : α
of : FreeAbelianGroup.of (L * 1) = FreeAbelianGroup.of L
of₁ of₂ : FreeAbelianGroup.of L = FreeAbelianGroup.of L
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
          FreeAbelianGroup.of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (FreeAbelianGroup.of L) =
    FreeAbelianGroup.of L

Tactic:
rw [lift_apply_of, mul_one]

Premises used: mul_one, 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
L : α
ih :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of L) =
    of L
neg :
  -((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (of L) =
    -of L
neg₁ neg₂ : -of L = -of L
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (-of L) =
    -of L

Tactic:
rw [map_neg, ih]

Premises used: map_neg
-- 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
x1 x2 : FreeAbelianGroup α
ih1 :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x1 =
    x1
ih2 :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x2 =
    x2
add :
  HAdd.hAdd (α := FreeAbelianGroup α) (β := FreeAbelianGroup α)
      (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x1 :
        FreeAbelianGroup α)
      (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x2 :
        FreeAbelianGroup α) =
    x1 + x2
add₁ :
  HAdd.hAdd (β := FreeAbelianGroup α) x1
      (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x2 :
        FreeAbelianGroup α) =
    x1 + x2
add₂ add₃ : x1 + x2 = x1 + x2
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (x1 + x2) =
    x1 + x2

Tactic:
rw [map_add, ih1, ih2]

Premises used: map_add
-- 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
x : FreeAbelianGroup α
zero :
  Eq.{u + 1} (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
          FreeAbelianGroup.of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      0)
    0
of :
  ∀ (L : α),
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
            FreeAbelianGroup.of (x₁ * 1) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (FreeAbelianGroup.of L) =
      FreeAbelianGroup.of L
neg :
  ∀ (L : α)
    (ih :
      ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
              FreeAbelianGroup.of (x₁ * 1) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          (FreeAbelianGroup.of L) =
        FreeAbelianGroup.of L),
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
            FreeAbelianGroup.of (x₁ * 1) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (-FreeAbelianGroup.of L) =
      -FreeAbelianGroup.of L
add :
  ∀ (x1 x2 : FreeAbelianGroup α)
    (ih1 :
      ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
              FreeAbelianGroup.of (x₁ * 1) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x1 =
        x1)
    (ih2 :
      ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
              FreeAbelianGroup.of (x₁ * 1) :
            (a : FreeAbelianGroup α) → FreeAbelianGroup α)
          x2 =
        x2),
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
            FreeAbelianGroup.of (x₁ * 1) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        (x1 + x2) =
      x1 + x2
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
          FreeAbelianGroup.of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x

Tactic:
induction x using FreeAbelianGroup.induction_on with
    | zero => rfl
    | of L => rw [lift_apply_of, mul_one]
    | neg L ih => rw [map_neg, ih]
    | add x1 x2 ih1 ih2 => rw [map_add, ih1, ih2]

Premises used: map_add, map_neg, FreeAbelianGroup.of, mul_one, FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
inst : Monoid α
⊢ Eq.{u + 1} (α := (a : α) → FreeAbelianGroup α) (⇑ofMulHom : (a : α) → FreeAbelianGroup α) of

Tactic:
rfl

Premises used: FreeAbelianGroup.of, rfl
-- 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 : FreeAbelianGroup α
⊢ (((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:
simp only [mul_zero, map_zero]

Premises used: map_zero, MulZeroClass.mul_zero
-- 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
L2 : α
⊢ (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (0 * 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)
          (of L2) :
        R)

Tactic:
simp only [zero_mul, map_zero]

Premises used: MulZeroClass.zero_mul, map_zero
-- 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
L2 L1 : α
of : (f : (a : α) → R) (L1 * L2) = HMul.hMul (α := R) (β := R) ((f : (a : α) → R) L1 : R) ((f : (a : α) → R) L2 : R)
⊢ (((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:
simp_rw [of_mul_of, lift_apply_of]

Premises used: FreeAbelianGroup.of_mul_of, 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 : α →* R
L2 L1 : α
⊢ (f : (a : α) → R) (L1 * L2) = HMul.hMul (α := R) (β := R) ((f : (a : α) → R) L1 : R) ((f : (a : α) → R) L2 : R)

Tactic:
f.map_mul _ _

Premises used: MonoidHom.map_mul
-- 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
L2 L1 : α
⊢ (f : (a : α) → R) (L1 * L2) = HMul.hMul (α := R) (β := R) ((f : (a : α) → R) L1 : R) ((f : (a : α) → R) L2 : R)

Tactic:
exact f.map_mul _ _

Premises used: MonoidHom.map_mul
-- 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
L2 L1 : α
ih :
  (((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)
of :
  -(((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)
⊢ (((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:
simp_rw [neg_mul, map_neg, neg_mul]

Premises used: map_neg, neg_mul
-- 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
L2 L1 : α
ih :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (of L1 * of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (of L1) :
        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)
        (of L1 * of L2) =
    -HMul.hMul (α := R) (β := R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (of L1) :
          R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (of L2) :
          R)

Tactic:
congr_arg Neg.neg ih

Premises used: congr_arg, Neg.neg
-- 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
L2 L1 : α
ih :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (of L1 * of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (of L1) :
        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)
        (of L1 * of L2) =
    -HMul.hMul (α := R) (β := R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (of L1) :
          R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (of L2) :
          R)

Tactic:
exact congr_arg Neg.neg ih

Premises used: congr_arg, Neg.neg
-- 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
L2 : α
x1 x2 : FreeAbelianGroup α
ih1 :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x1 * of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x1 :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (of L2) :
        R)
ih2 :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x2 * of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x2 :
        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)
      ((x1 + x2) * of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (x1 + x2) :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (of L2) :
        R)

Tactic:
simp only [add_mul, map_add, ih1, ih2]

Premises used: add_mul, map_add