awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
x : FreeAbelianGroup α
⊢ (map id : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x
have rw : (AddMonoidHom.id (FreeAbelianGroup α) : (a : FreeAbelianGroup α) → FreeAbelianGroup α) x = x
Tactic: rw [map_id]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
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 γ)
have 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 γ)
Tactic: rw [map_comp]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
inst : Mul α
x y : α
⊢ of x * of y = of (x * y)
have 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)
Tactic: rw [mul_def, lift_apply_of, lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ of x * of y = of (x * y)
have rw₁ : ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * y) :
      (a : FreeAbelianGroup α) → FreeAbelianGroup α)
    (of x) =
  of (x * y)
Tactic: rw [mul_def, lift_apply_of, lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ of x * of y = of (x * y)
have rw₂ : of (x * y) = of (x * y)
Tactic: rw [mul_def, lift_apply_of, lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (hypothesis)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Mul α
a : FreeAbelianGroup α
⊢ 0 * a = 0
have h : 0 * a + 0 * a = 0 * a
Tactic: have h : 0 * a + 0 * a = 0 * a := by simp [← add_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
L3 L2 L1 : α
⊢ of L1 * of L2 * of L3 = of L1 * (of L2 * of L3)
have of : of (L1 * L2) * of L3 = of L1 * (of L2 * of L3)
Tactic: rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₁ : FreeAbelianGroup.of (L1 * L2 * 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]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₂ : FreeAbelianGroup.of (L1 * L2 * L3) = FreeAbelianGroup.of L1 * FreeAbelianGroup.of (L2 * L3)
Tactic: rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₃ : FreeAbelianGroup.of (L1 * L2 * L3) = FreeAbelianGroup.of (L1 * (L2 * L3))
Tactic: rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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))
⊢ FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₄ : FreeAbelianGroup.of (L1 * (L2 * L3)) = FreeAbelianGroup.of (L1 * (L2 * L3))
Tactic: rw [of_mul_of, of_mul_of, of_mul_of, of_mul_of, mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
L3 L2 L1 : α
ih : of L1 * of L2 * of L3 = of L1 * (of L2 * of L3)
⊢ -of L1 * of L2 * of L3 = -of L1 * (of L2 * of L3)
have of : -(of L1 * of L2) * of L3 = -of L1 * (of L2 * of L3)
Tactic: rw [neg_mul, neg_mul, neg_mul, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ -FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    -FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₁ : -(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]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ -FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    -FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₂ : -(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]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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))
⊢ -FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    -FreeAbelianGroup.of L1 * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₃ : -(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]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
L3 L2 : α
x₁ x₂ : FreeAbelianGroup α
ih₁ : x₁ * of L2 * of L3 = x₁ * (of L2 * of L3)
ih₂ : x₂ * of L2 * of L3 = x₂ * (of L2 * of L3)
⊢ (x₁ + x₂) * of L2 * of L3 = (x₁ + x₂) * (of L2 * of L3)
have of : (x₁ * of L2 + x₂ * of L2) * of L3 = (x₁ + x₂) * (of L2 * of L3)
Tactic: rw [add_mul, add_mul, add_mul, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ (x₁ + x₂) * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    (x₁ + x₂) * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₁ : x₁ * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 + 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₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ (x₁ + x₂) * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    (x₁ + x₂) * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have 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 [add_mul, add_mul, add_mul, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ (x₁ + x₂) * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    (x₁ + x₂) * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have 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 [add_mul, add_mul, add_mul, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ (x₁ + x₂) * FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 =
    (x₁ + x₂) * (FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have 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 [add_mul, add_mul, add_mul, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
ih : x * of L2 * of L3 = x * (of L2 * of L3)
⊢ x * -of L2 * of L3 = x * (-of L2 * of L3)
have of : x * -of L2 * of L3 = x * -(of L2 * of L3)
Tactic: rw [neg_mul, mul_neg, mul_neg, neg_mul, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ x * -FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (-FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₁ : -(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]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ x * -FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (-FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₂ : -(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]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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))
⊢ x * -FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (-FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₃ : -(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]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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))
⊢ x * -FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3 = x * (-FreeAbelianGroup.of L2 * FreeAbelianGroup.of L3)
have of₄ : -(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]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * of L3 = x * (y₁ * of L3)
ih₂ : x * y₂ * of L3 = x * (y₂ * of L3)
⊢ x * (y₁ + y₂) * of L3 = x * ((y₁ + y₂) * of L3)
have of : x * (y₁ + y₂) * of L3 = x * (y₁ * of L3 + y₂ * of L3)
Tactic: rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ x * (y₁ + y₂) * FreeAbelianGroup.of L3 = x * ((y₁ + y₂) * FreeAbelianGroup.of L3)
have of₁ : (x * y₁ + x * y₂) * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3 + y₂ * FreeAbelianGroup.of L3)
Tactic: rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ x * (y₁ + y₂) * FreeAbelianGroup.of L3 = x * ((y₁ + y₂) * FreeAbelianGroup.of L3)
have of₂ : (x * y₁ + x * y₂) * FreeAbelianGroup.of L3 = x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3)
Tactic: rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ x * (y₁ + y₂) * FreeAbelianGroup.of L3 = x * ((y₁ + y₂) * FreeAbelianGroup.of L3)
have of₃ : x * y₁ * FreeAbelianGroup.of L3 + x * y₂ * FreeAbelianGroup.of L3 =
  x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3)
Tactic: rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ x * (y₁ + y₂) * FreeAbelianGroup.of L3 = x * ((y₁ + y₂) * FreeAbelianGroup.of L3)
have of₄ : x * (y₁ * FreeAbelianGroup.of L3) + x * y₂ * FreeAbelianGroup.of L3 =
  x * (y₁ * FreeAbelianGroup.of L3) + x * (y₂ * FreeAbelianGroup.of L3)
Tactic: rw [add_mul, mul_add, mul_add, add_mul, ih₁, ih₂]