awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
x : FreeAbelianGroup α
zero :
  Eq.{u + 1} (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      0)
    0
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
have of : ∀ (L : α),
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦ of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of L) =
    of L
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
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
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          FreeAbelianGroup.of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
have 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
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
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
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₂ : α) ↦
          FreeAbelianGroup.of (1 * x₂) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
have 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
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
x : FreeAbelianGroup α
⊢ x * 1 = x
have rw : ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
      (a : FreeAbelianGroup α) → FreeAbelianGroup α)
    x =
  x
Tactic: rw [mul_def, one_def, lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
L : α
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of L) =
    of L
have of : of (L * 1) = of L
Tactic: rw [lift_apply_of, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
L : α
of : FreeAbelianGroup.of (L * 1) = FreeAbelianGroup.of L
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
          FreeAbelianGroup.of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (FreeAbelianGroup.of L) =
    FreeAbelianGroup.of L
have of₁ : FreeAbelianGroup.of L = FreeAbelianGroup.of L
Tactic: rw [lift_apply_of, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
L : α
ih :
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of L) =
    of L
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (-of L) =
    -of L
have neg : -((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of L) =
  -of L
Tactic: rw [map_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
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
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (-of L) =
    -of L
have neg₁ : -of L = -of L
Tactic: rw [map_neg, ih]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
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
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (x1 + x2) =
    x1 + x2
have 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
Tactic: rw [map_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
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
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (x1 + x2) =
    x1 + x2
have add₁ : HAdd.hAdd (β := FreeAbelianGroup α) x1
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
          (a : FreeAbelianGroup α) → FreeAbelianGroup α)
        x2 :
      FreeAbelianGroup α) =
  x1 + x2
Tactic: rw [map_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
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
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (x1 + x2) =
    x1 + x2
have add₂ : x1 + x2 = x1 + x2
Tactic: rw [map_add, ih1, ih2]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
x : FreeAbelianGroup α
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
have zero : Eq.{u + 1} (α := FreeAbelianGroup α)
  (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
      (a : FreeAbelianGroup α) → FreeAbelianGroup α)
    0)
  0
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
x : FreeAbelianGroup α
zero :
  Eq.{u + 1} (α := FreeAbelianGroup α)
    (((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      0)
    0
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
have of : ∀ (L : α),
  ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦ of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      (of L) =
    of L
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
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
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
          FreeAbelianGroup.of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
have 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
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
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
⊢ ((lift : (a : α → FreeAbelianGroup α) → FreeAbelianGroup α →+ FreeAbelianGroup α) fun (x₁ : α) ↦
          FreeAbelianGroup.of (x₁ * 1) :
        (a : FreeAbelianGroup α) → FreeAbelianGroup α)
      x =
    x
have 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
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]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
L2 L1 : α
⊢ (((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)
have of : (f : (a : α) → R) (L1 * L2) = HMul.hMul (α := R) (β := R) ((f : (a : α) → R) L1 : R) ((f : (a : α) → R) L2 : R)
Tactic: simp_rw [of_mul_of, lift_apply_of]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
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)
have of : -(((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: simp_rw [neg_mul, map_neg, neg_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
⊢ (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (of L2) :
        R)
have of : (((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: induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul, map_zero]
        | of L1 =>
          simp_rw [of_mul_of, lift_apply_of]
          exact f.map_mul _ _
        | neg L1 ih =>
          simp_rw [neg_mul, map_neg, neg_mul]
          exact congr_arg Neg.neg ih
        | add x1 x2 ih1 ih2 => simp only [add_mul, map_add, ih1, ih2]
Cleared hypotheses: x