awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β α_1 β_1 : Type u
x : FreeAbelianGroup α_1
y : FreeAbelianGroup β_1
zero : Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> 0 <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> 0)
pure :
  ∀ (p : α_1),
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> Pure.pure p <*> y)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p)
neg :
  ∀ (p : α_1)
    (ih :
      Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> Pure.pure p <*> y)
        ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> Pure.pure p)),
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (-Pure.pure p) <*> y)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> -Pure.pure p)
add :
  ∀ (x₁ x₂ : FreeAbelianGroup α_1)
    (ih1 :
      Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₁ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁))
    (ih2 :
      Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x₂ <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₂)),
    Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> (x₁ + x₂) <*> y)
      ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x₁ + x₂)
⊢ Eq (α := FreeAbelianGroup (α_1 × β_1)) (Prod.mk <$> x <*> y) ((fun (b : β_1) (a : α_1) ↦ (a, b)) <$> y <*> x)

Tactic:
induction x using FreeAbelianGroup.induction_on' with
    | zero => rw [FreeAbelianGroup.map_zero, zero_seq, seq_zero]
    | pure p =>
      rw [map_pure, pure_seq]
      induction y using FreeAbelianGroup.induction_on' with
      | zero => rw [FreeAbelianGroup.map_zero, FreeAbelianGroup.map_zero, zero_seq]
      | pure q => rw [map_pure, map_pure, pure_seq, map_pure]
      | neg q ih => rw [FreeAbelianGroup.map_neg, FreeAbelianGroup.map_neg, neg_seq, ih]
      | add y₁ y₂ ih1 ih2 =>
        rw [FreeAbelianGroup.map_add, FreeAbelianGroup.map_add, add_seq, ih1, ih2]
    | neg p ih => rw [FreeAbelianGroup.map_neg, neg_seq, seq_neg, ih]
    | add x₁ x₂ ih1 ih2 => rw [FreeAbelianGroup.map_add, add_seq, seq_add, ih1, ih2]

Premises used: Pure.pure, FreeAbelianGroup.pure_seq, FreeAbelianGroup.seq_zero, FreeAbelianGroup.seq_add, FreeAbelianGroup.map_add, FreeAbelianGroup.seq_neg, FreeAbelianGroup.map_neg, FreeAbelianGroup.neg_seq, FreeAbelianGroup.map_pure, FreeAbelianGroup.map_zero, FreeAbelianGroup.zero_seq, FreeAbelianGroup.add_seq
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup γ
f : α → β
g : β → γ
⊢ Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        0 :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) 0) :
      γ)

Tactic:
simp only [map_zero]

Premises used: map_zero
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup γ
f : α → β
g : β → γ
x : α
⊢ Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        (of x) :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (of x) : FreeAbelianGroup β) :
      γ)

Tactic:
simp only [lift_apply_of, map, Function.comp]

Premises used: Function.comp, FreeAbelianGroup.lift_apply_of, FreeAbelianGroup.map
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup γ
f : α → β
g : β → γ
x : α
h :
  Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        (of x) :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (of x) : FreeAbelianGroup β) :
      γ)
⊢ Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        (-of x) :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (-of x) : FreeAbelianGroup β) :
      γ)

Tactic:
simp only [h, map_neg]

Premises used: map_neg
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup γ
f : α → β
g : β → γ
x y : FreeAbelianGroup α
h₁ :
  Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        x :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x : FreeAbelianGroup β) :
      γ)
h₂ :
  Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        y :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) y : FreeAbelianGroup β) :
      γ)
⊢ Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        (x + y) :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (x + y) : FreeAbelianGroup β) :
      γ)

Tactic:
simp only [h₁, h₂, map_add]

Premises used: map_add
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
⊢ Eq.{u + 1} (α := FreeAbelianGroup α →+ FreeAbelianGroup α) (map id) (AddMonoidHom.id (FreeAbelianGroup α))

Tactic:
Eq.symm <|
    lift_ext _ _ fun _ ↦ lift_unique of (AddMonoidHom.id _) fun _ ↦ AddMonoidHom.id_apply _ _

Premises used: FreeAbelianGroup.lift_ext, AddMonoidHom.id_apply, AddMonoidHom.id, FreeAbelianGroup.lift_unique, FreeAbelianGroup.of, FreeAbelianGroup, Eq.symm
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
x : FreeAbelianGroup α
rw : (AddMonoidHom.id (FreeAbelianGroup α) : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x
⊢ (map id : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x

Tactic:
rw [map_id]

Premises used: FreeAbelianGroup.map_id
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
x : FreeAbelianGroup α
⊢ (AddMonoidHom.id (FreeAbelianGroup α) : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : α
⊢ Eq.{w + 1} (α := FreeAbelianGroup γ)
    (((map g).comp (map f) : (a : FreeAbelianGroup α) → FreeAbelianGroup γ) (of x) : FreeAbelianGroup γ)
    ((map (g ∘ f) : (a : FreeAbelianGroup α) → FreeAbelianGroup γ) (of x) : FreeAbelianGroup γ)

Tactic:
simp [map]

Premises used: FreeAbelianGroup.map
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
rw :
  Eq.{w + 1} (α := FreeAbelianGroup γ)
    (((map g).comp (map f) : (a : FreeAbelianGroup α) → FreeAbelianGroup γ) x : FreeAbelianGroup γ)
    ((map g : (a : FreeAbelianGroup β) → FreeAbelianGroup γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x) :
      FreeAbelianGroup γ)
⊢ Eq.{w + 1} (α := FreeAbelianGroup γ)
    ((map (g ∘ f) : (a : FreeAbelianGroup α) → FreeAbelianGroup γ) x : FreeAbelianGroup γ)
    ((map g : (a : FreeAbelianGroup β) → FreeAbelianGroup γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x) :
      FreeAbelianGroup γ)

Tactic:
rw [map_comp]

Premises used: FreeAbelianGroup.map_comp
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ Eq.{w + 1} (α := FreeAbelianGroup γ)
    (((map g).comp (map f) : (a : FreeAbelianGroup α) → FreeAbelianGroup γ) x : FreeAbelianGroup γ)
    ((map g : (a : FreeAbelianGroup β) → FreeAbelianGroup γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x) :
      FreeAbelianGroup γ)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
β : Type v
f : α → β
a : α
⊢ (map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (of a) = of (f a)

Tactic:
rfl

Premises used: FreeGroup.of, Quotient.liftOn', FreeGroup.Lift.aux, Quotient.map₂, List.append, Con.liftOn, FreeAbelianGroup.of, FreeGroup.mk, List.foldr, rfl, List.prod
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
inst : Mul α
x y : FreeAbelianGroup α
⊢ x * y =
    ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                of (x₁ * x₂) :
              (a : FreeAbelianGroup α) → FreeAbelianGroup α)
            x :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
inst : Mul α
x y : α
rw :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
                of (x₁ * x₂) :
              (a : FreeAbelianGroup α) → FreeAbelianGroup α)
            (of x) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of y) =
    of (x * y)
rw₁ :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * y) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of x) =
    of (x * y)
rw₂ rw₃ : of (x * y) = of (x * y)
⊢ of x * of y = of (x * y)

Tactic:
rw [mul_def, lift_apply_of, lift_apply_of]

Premises used: FreeAbelianGroup.mul_def, FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
inst : Mul α
x y : α
⊢ of (x * y) = of x * of y

Tactic:
Eq.symm <| of_mul_of x y

Premises used: FreeAbelianGroup.of_mul_of, Eq.symm
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Mul α
x y z : FreeAbelianGroup α
⊢ (x + y) * z = x * z + y * z

Tactic:
simp [mul_def, ← Pi.add_def]

Premises used: Pi.add_def, FreeAbelianGroup.mul_def
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Mul α
a : FreeAbelianGroup α
⊢ 0 * a + 0 * a = 0 * a

Tactic:
simp [← add_mul]

Premises used: add_mul
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Mul α
a : FreeAbelianGroup α
⊢ 0 * a + 0 * a = 0 * a

Tactic:
have h : 0 * a + 0 * a = 0 * a := by simp [← add_mul]
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Mul α
a : FreeAbelianGroup α
h : 0 * a + 0 * a = 0 * a
⊢ 0 * a = 0

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
inst : One α
⊢ Eq.{u + 1} (α := FreeAbelianGroup α) 1 (of 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
inst : One α
⊢ Eq.{u + 1} (α := FreeAbelianGroup α) (of 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y : FreeAbelianGroup α
⊢ x * y * 0 = x * (y * 0)

Tactic:
simp only [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x : FreeAbelianGroup α
L3 : α
⊢ x * 0 * of L3 = x * (0 * of L3)

Tactic:
simp only [mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
L3 L2 : α
⊢ 0 * of L2 * of L3 = 0 * (of L2 * of L3)

Tactic:
simp only [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
L3 L2 L1 : α
of :
  FreeAbelianGroup.of (L1 * L2) * FreeAbelianGroup.of L3 =
    FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₁ : FreeAbelianGroup.of (L1 * L2 * L3) = FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₂ : FreeAbelianGroup.of (L1 * L2 * L3) = FreeAbelianGroup.of L1 * FreeAbelianGroup.of (L2 * L3)
of₃ : FreeAbelianGroup.of (L1 * L2 * L3) = FreeAbelianGroup.of (L1 * (L2 * L3))
of₄ of₅ : FreeAbelianGroup.of (L1 * (L2 * L3)) = FreeAbelianGroup.of (L1 * (L2 * L3))
⊢ FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)

Tactic:
rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]

Premises used: mul_assoc, FreeAbelianGroup.of_mul_of
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
L3 L2 L1 : α
ih :
  FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of :
  -(FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2) * FreeAbelianGroup.of L3 =
    -FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₁ :
  -(FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3) =
    -FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₂ :
  -(FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3) =
    -(FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3))
of₃ of₄ :
  -(FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)) =
    -(FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3))
⊢ -FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    -FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)

Tactic:
rw [neg_mul, neg_mul, neg_mul, ih]

Premises used: neg_mul
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
L3 L2 : α
x₁ x₂ : FreeAbelianGroup α
ih₁ : x₁ * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x₁ * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
ih₂ : x₂ * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x₂ * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of :
  (x₁ * FreeAbelianGroup.of L2 + x₂ * FreeAbelianGroup.of L2) * FreeAbelianGroup.of L3 =
    (x₁ + x₂) * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₁ :
  x₁ * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 + x₂ * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    (x₁ + x₂) * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₂ :
  x₁ * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 + x₂ * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    x₁ * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3) + x₂ * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₃ :
  x₁ * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3) + x₂ * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    x₁ * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3) + x₂ * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₄ of₅ :
  x₁ * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3) + x₂ * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3) =
    x₁ * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3) + x₂ * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
⊢ (x₁ + x₂) * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    (x₁ + x₂) * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)

Tactic:
rw [add_mul, add_mul, add_mul, ih₁, ih₂]

Premises used: add_mul
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
ih : x * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of : x * -FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * -(FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₁ : -(x * FreeAbelianGroup.of L2) * FreeAbelianGroup.of L3 = x * -(FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₂ : -(x * FreeAbelianGroup.of L2) * FreeAbelianGroup.of L3 = -(x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3))
of₃ : -(x * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3) = -(x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3))
of₄ of₅ :
  -(x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)) = -(x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3))
⊢ x * -FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (-FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)

Tactic:
rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]

Premises used: neg_mul, mul_neg
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3)
ih₂ : x * y₂ * FreeAbelianGroup.of L3 = x * (y₂ * FreeAbelianGroup.of L3)
of : x * (y₁ + y₂) * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3 + y₂ * FreeAbelianGroup.of L3)
of₁ : (x * y₁ + x * y₂) * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3 + y₂ * FreeAbelianGroup.of L3)
of₂ : (x * y₁ + x * y₂) * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3)
of₃ :
  x * y₁ * FreeAbelianGroup.of L3 + x * y₂ * FreeAbelianGroup.of L3 =
    x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3)
of₄ :
  x * (y₁ * FreeAbelianGroup.of L3) + x * y₂ * FreeAbelianGroup.of L3 =
    x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3)
of₅ of₆ :
  x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3) =
    x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3)
⊢ x * (y₁ + y₂) * FreeAbelianGroup.of L3 = x * ((y₁ + y₂) * FreeAbelianGroup.of L3)

Tactic:
rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]

Premises used: add_mul, mul_add
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y : FreeAbelianGroup α
L3 : α
of : x * 0 * FreeAbelianGroup.of L3 = x * (0 * FreeAbelianGroup.of L3)
of₁ :
  ∀ (L2 : α),
    x * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₂ :
  ∀ (L2 : α)
    (ih : x * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)),
    x * -FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (-FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
of₃ :
  ∀ (y₁ y₂ : FreeAbelianGroup α) (ih₁ : x * y₁ * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3))
    (ih₂ : x * y₂ * FreeAbelianGroup.of L3 = x * (y₂ * FreeAbelianGroup.of L3)),
    x * (y₁ + y₂) * FreeAbelianGroup.of L3 = x * ((y₁ + y₂) * FreeAbelianGroup.of L3)
⊢ x * y * FreeAbelianGroup.of L3 = x * (y * FreeAbelianGroup.of L3)

Tactic:
induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]

Premises used: add_mul, MulZeroClass.zero_mul, mul_assoc, FreeAbelianGroup.of_mul_of, MulZeroClass.mul_zero, FreeAbelianGroup.of, mul_add, neg_mul, mul_neg
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
neg : -(x * y * of L3) = x * (y * -of L3)
neg₁ : -(x * y * of L3) = x * -(y * of L3)
neg₂ : -(x * y * of L3) = -(x * (y * of L3))
neg₃ neg₄ : -(x * (y * of L3)) = -(x * (y * of L3))
⊢ x * y * -of L3 = x * (y * -of L3)

Tactic:
rw [mul_neg, mul_neg, mul_neg, ih]

Premises used: mul_neg
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
add : x * y * z₁ + x * y * z₂ = x * (y * (z₁ + z₂))
add₁ : x * y * z₁ + x * y * z₂ = x * (y * z₁ + y * z₂)
add₂ : x * y * z₁ + x * y * z₂ = x * (y * z₁) + x * (y * z₂)
add₃ : x * (y * z₁) + x * y * z₂ = x * (y * z₁) + x * (y * z₂)
add₄ add₅ : x * (y * z₁) + x * (y * z₂) = x * (y * z₁) + x * (y * z₂)
⊢ x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))

Tactic:
rw [mul_add, mul_add, mul_add, ih₁, ih₂]

Premises used: mul_add
-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x y z : FreeAbelianGroup α
zero : x * y * 0 = x * (y * 0)
of : ∀ (L3 : α), x * y * FreeAbelianGroup.of L3 = x * (y * FreeAbelianGroup.of L3)
neg :
  ∀ (L3 : α) (ih : x * y * FreeAbelianGroup.of L3 = x * (y * FreeAbelianGroup.of L3)),
    x * y * -FreeAbelianGroup.of L3 = x * (y * -FreeAbelianGroup.of L3)
add :
  ∀ (z₁ z₂ : FreeAbelianGroup α) (ih₁ : x * y * z₁ = x * (y * z₁)) (ih₂ : x * y * z₂ = x * (y * z₂)),
    x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))
⊢ x * y * z = x * (y * z)

Tactic:
induction z using FreeAbelianGroup.induction_on with
    | zero => simp only [mul_zero]
    | of L3 =>
      induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, zero_mul]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul]
        | of L1 => rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
        | neg L1 ih => rw [neg_mul, neg_mul, neg_mul, ih]
        | add x₁ x₂ ih₁ ih₂ => rw [add_mul, add_mul, add_mul, ih₁, ih₂]
      | neg L2 ih => rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
      | add y₁ y₂ ih₁ ih₂ => rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
    | neg L3 ih => rw [mul_neg, mul_neg, mul_neg, ih]
    | add z₁ z₂ ih₁ ih₂ => rw [mul_add, mul_add, mul_add, ih₁, ih₂]

Premises used: add_mul, MulZeroClass.zero_mul, mul_assoc, FreeAbelianGroup.of_mul_of, MulZeroClass.mul_zero, FreeAbelianGroup.of, mul_add, neg_mul, mul_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
x : FreeAbelianGroup α
simp_rw :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
⊢ 1 * x = x

Tactic:
simp_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 (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      0)
    0

Tactic:
rfl