awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x_1 : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x_1.IsSupported s
x y : FreeCommRing α
ihx :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) =
    x
ihy :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y) =
    y
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (x + y)) =
    x + y
have refine_4 : (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
    (HAdd.hAdd (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x : FreeCommRing (↑s : Type u))
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y : FreeCommRing (↑s : Type u))) =
  x + y
Tactic: rw [map_add, map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x_1 : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x_1.IsSupported s
x y : FreeCommRing α
ihx :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) =
    x
ihy :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y) =
    y
refine_4 :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HAdd.hAdd (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x : FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y : FreeCommRing (↑s : Type u))) =
    x + y
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (x + y)) =
    x + y
have refine_4₁ : HAdd.hAdd (α := FreeCommRing α) (β := FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) :
      FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y) :
      FreeCommRing α) =
  x + y
Tactic: rw [map_add, map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x_1 : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x_1.IsSupported s
x y : FreeCommRing α
ihx :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) =
    x
ihy :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y) =
    y
refine_4 :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HAdd.hAdd (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x : FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y : FreeCommRing (↑s : Type u))) =
    x + y
refine_4₁ :
  HAdd.hAdd (α := FreeCommRing α) (β := FreeCommRing α)
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) :
        FreeCommRing α)
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y) :
        FreeCommRing α) =
    x + y
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (x + y)) =
    x + y
have refine_4₂ : HAdd.hAdd (β := FreeCommRing α) x
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y) :
      FreeCommRing α) =
  x + y
Tactic: rw [map_add, map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x_1 : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x_1.IsSupported s
x y : FreeCommRing α
ihx :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) =
    x
ihy :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y) =
    y
refine_4 :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HAdd.hAdd (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x : FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y : FreeCommRing (↑s : Type u))) =
    x + y
refine_4₁ :
  HAdd.hAdd (α := FreeCommRing α) (β := FreeCommRing α)
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) :
        FreeCommRing α)
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y) :
        FreeCommRing α) =
    x + y
refine_4₂ :
  HAdd.hAdd (β := FreeCommRing α) x
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) y) :
        FreeCommRing α) =
    x + y
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (x + y)) =
    x + y
have refine_4₃ : x + y = x + y
Tactic: rw [map_add, map_add, ihx, ihy]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeRing α
⊢ (↑(-x) : FreeCommRing α) = -(↑x : FreeCommRing α)
have rw : Eq (α := FreeCommRing α) ((toFreeCommRing : (a : FreeRing α) → FreeCommRing α) (-x) : FreeCommRing α)
  (-(toFreeCommRing : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
Tactic: rw [castFreeCommRing, map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeRing α
rw :
  Eq (α := FreeCommRing α) ((toFreeCommRing : (a : FreeRing α) → FreeCommRing α) (-x) : FreeCommRing α)
    (-(toFreeCommRing : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
⊢ (↑(-x) : FreeCommRing α) = -(↑x : FreeCommRing α)
have rw₁ : Eq (α := FreeCommRing α) (-(toFreeCommRing : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
  (-(toFreeCommRing : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
Tactic: rw [castFreeCommRing, map_neg]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x y : FreeRing α
⊢ (↑(x - y) : FreeCommRing α) = (↑x : FreeCommRing α) - (↑y : FreeCommRing α)
have rw : (toFreeCommRing : (a : FreeRing α) → FreeCommRing α) (x - y) =
  HSub.hSub (α := FreeCommRing α) (β := FreeCommRing α)
    ((toFreeCommRing : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
    ((toFreeCommRing : (a : FreeRing α) → FreeCommRing α) y : FreeCommRing α)
Tactic: rw [castFreeCommRing, map_sub]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x y : FreeRing α
rw :
  (toFreeCommRing : (a : FreeRing α) → FreeCommRing α) (x - y) =
    HSub.hSub (α := FreeCommRing α) (β := FreeCommRing α)
      ((toFreeCommRing : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
      ((toFreeCommRing : (a : FreeRing α) → FreeCommRing α) y : FreeCommRing α)
⊢ (↑(x - y) : FreeCommRing α) = (↑x : FreeCommRing α) - (↑y : FreeCommRing α)
have rw₁ : HSub.hSub (α := FreeCommRing α) (β := FreeCommRing α)
    ((toFreeCommRing : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
    ((toFreeCommRing : (a : FreeRing α) → FreeCommRing α) y : FreeCommRing α) =
  HSub.hSub (α := FreeCommRing α) (β := FreeCommRing α)
    ((toFreeCommRing : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
    ((toFreeCommRing : (a : FreeRing α) → FreeCommRing α) y : FreeCommRing α)
Tactic: rw [castFreeCommRing, map_sub]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = -1
have h : Eq.{u + 1} (α := FreeCommRing α) (↑(-1) : FreeCommRing α) (-1)
Tactic: use -1
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x y : FreeCommRing α
hx : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x
hy : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = y
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x + y
have add : ∀ (x : FreeRing α), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) + y
Tactic: rcases hx with ⟨x, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
y : FreeCommRing α
hy : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = y
x : FreeRing α
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) + y
have add : ∀ (y : FreeRing α), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) + (↑y : FreeCommRing α)
Tactic: rcases hy with ⟨y, rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x y : FreeCommRing α
hx : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x
hy : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = y
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x * y
have mul : ∀ (x : FreeRing α), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) * y
Tactic: rcases hx with ⟨x, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
y : FreeCommRing α
hy : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = y
x : FreeRing α
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) * y
have mul : ∀ (y : FreeRing α), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) * (↑y : FreeCommRing α)
Tactic: rcases hy with ⟨y, rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeCommRing α
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x
have neg_one : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = -1
Tactic: induction x with
  | neg_one => use -1; rfl
  | of b => exact ⟨FreeRing.of b, rfl⟩
  | add _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
  | mul _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeCommRing α
neg_one : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = -1
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x
have of : ∀ (b : α), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = FreeCommRing.of b
Tactic: induction x with
  | neg_one => use -1; rfl
  | of b => exact ⟨FreeRing.of b, rfl⟩
  | add _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
  | mul _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeCommRing α
neg_one : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = -1
of : ∀ (b : α), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = FreeCommRing.of b
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x
have add : ∀ (x y : FreeCommRing α) (hx : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x)
  (hy : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = y), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x + y
Tactic: induction x with
  | neg_one => use -1; rfl
  | of b => exact ⟨FreeRing.of b, rfl⟩
  | add _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
  | mul _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeCommRing α
neg_one : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = -1
of : ∀ (b : α), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = FreeCommRing.of b
add :
  ∀ (x y : FreeCommRing α) (hx : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x)
    (hy : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = y), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x + y
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x
have mul : ∀ (x y : FreeCommRing α) (hx : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x)
  (hy : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = y), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x * y
Tactic: induction x with
  | neg_one => use -1; rfl
  | of b => exact ⟨FreeRing.of b, rfl⟩
  | add _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
  | mul _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
⊢ Eq.{u + 1} (α := FreeRing α → FreeCommRing α) castFreeCommRing (Functor.map fun (l : List α) ↦ (↑l : Multiset α))
have h : ∀ (x : FreeRing α), (↑x : FreeCommRing α) = (fun (l : List α) ↦ (↑l : Multiset α)) <$> x
Tactic: funext x
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeRing α
⊢ Eq (α := FreeCommRing α)
    (((↑((FreeAbelianGroup.lift :
                    (a : FreeMonoid α → FreeCommRing α) → FreeAbelianGroup (FreeMonoid α) →+ FreeCommRing α)
                  (⇑((FreeMonoid.lift : (a : α → FreeCommRing α) → FreeMonoid α →* FreeCommRing α) FreeCommRing.of :
                        FreeMonoid α →* FreeCommRing α) :
                    (a : FreeMonoid α) → FreeCommRing α) :
                FreeAbelianGroup (FreeMonoid α) →+ FreeCommRing α) :
            FreeAbelianGroup (FreeMonoid α) →+ FreeCommRing α) :
          (a : FreeAbelianGroup (FreeMonoid α)) → FreeCommRing α)
        x :
      FreeCommRing α)
    ((((FreeAbelianGroup.lift :
                (a : List α → FreeAbelianGroup (Multiset α)) →
                  FreeAbelianGroup (List α) →+ FreeAbelianGroup (Multiset α))
              ((fun (α_1 : Multiset α) ↦ FreeAbelianGroup.of α_1) ∘ fun (l : List α) ↦ (↑l : Multiset α)) :
            FreeAbelianGroup (List α) →+ FreeAbelianGroup (Multiset α)) :
          (a : FreeAbelianGroup (List α)) → FreeAbelianGroup (Multiset α))
        x :
      FreeAbelianGroup (Multiset α))
have h : ∀ (x : FreeMonoid α),
  Eq (α := FreeCommRing α)
    (((↑((FreeAbelianGroup.lift :
                    (a : FreeMonoid α → FreeCommRing α) → FreeAbelianGroup (FreeMonoid α) →+ FreeCommRing α)
                  (⇑((FreeMonoid.lift : (a : α → FreeCommRing α) → FreeMonoid α →* FreeCommRing α) FreeCommRing.of :
                        FreeMonoid α →* FreeCommRing α) :
                    (a : FreeMonoid α) → FreeCommRing α) :
                FreeAbelianGroup (FreeMonoid α) →+ FreeCommRing α) :
            FreeAbelianGroup (FreeMonoid α) →+ FreeCommRing α) :
          (a : FreeAbelianGroup (FreeMonoid α)) → FreeCommRing α)
        (FreeAbelianGroup.of x) :
      FreeCommRing α)
    (((fun (α_1 : Multiset α) ↦ FreeAbelianGroup.of α_1) ∘ fun (l : List α) ↦ (↑l : Multiset α)) x :
      FreeAbelianGroup (Multiset α))
Tactic: apply FreeAbelianGroup.lift_unique
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ Eq (α := FreeCommRing α)
    (((↑((FreeAbelianGroup.lift :
                    (a : FreeMonoid α → FreeCommRing α) → FreeAbelianGroup (FreeMonoid α) →+ FreeCommRing α)
                  (⇑((FreeMonoid.lift : (a : α → FreeCommRing α) → FreeMonoid α →* FreeCommRing α) FreeCommRing.of :
                        FreeMonoid α →* FreeCommRing α) :
                    (a : FreeMonoid α) → FreeCommRing α) :
                FreeAbelianGroup (FreeMonoid α) →+ FreeCommRing α) :
            FreeAbelianGroup (FreeMonoid α) →+ FreeCommRing α) :
          (a : FreeAbelianGroup (FreeMonoid α)) → FreeCommRing α)
        (FreeAbelianGroup.of L) :
      FreeCommRing α)
    (((fun (α_1 : Multiset α) ↦ FreeAbelianGroup.of α_1) ∘ fun (l : List α) ↦ (↑l : Multiset α)) L :
      FreeAbelianGroup (Multiset α))
have h : (((FreeMonoid.lift : (a : α → FreeCommRing α) → FreeMonoid α →* FreeCommRing α) FreeCommRing.of :
        FreeMonoid α →* FreeCommRing α) :
      (a : FreeMonoid α) → FreeCommRing α)
    L =
  FreeAbelianGroup.of (↑L : Multiset α)
Tactic: simp only [AddMonoidHom.coe_coe, comp_apply, FreeAbelianGroup.lift_apply_of]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih :
  (((FreeMonoid.lift : (a : α → FreeCommRing α) → FreeMonoid α →* FreeCommRing α) FreeCommRing.of :
          FreeMonoid α →* FreeCommRing α) :
        (a : FreeMonoid α) → FreeCommRing α)
      tl =
    FreeAbelianGroup.of (↑tl : Multiset α)
⊢ (((FreeMonoid.lift : (a : α → FreeCommRing α) → FreeMonoid α →* FreeCommRing α) FreeCommRing.of :
          FreeMonoid α →* FreeCommRing α) :
        (a : FreeMonoid α) → FreeCommRing α)
      (FreeMonoid.of hd * tl) =
    FreeAbelianGroup.of (↑(FreeMonoid.of hd * tl) : Multiset α)
have rw : FreeCommRing.of hd * FreeAbelianGroup.of (↑tl : Multiset α) =
  FreeAbelianGroup.of (↑(FreeMonoid.of hd * tl) : Multiset α)
Tactic: rw [(FreeMonoid.lift _).map_mul, FreeMonoid.lift_eval_of, ih]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih :
  (((FreeMonoid.lift : (a : α → FreeCommRing α) → FreeMonoid α →* FreeCommRing α) FreeCommRing.of :
          FreeMonoid α →* FreeCommRing α) :
        (a : FreeMonoid α) → FreeCommRing α)
      tl =
    FreeAbelianGroup.of (↑tl : Multiset α)
| FreeCommRing.of hd * FreeAbelianGroup.of (↑tl : Multiset α)
have reduce : Quot.mk
  (fun (a b : FreeGroup (Multiplicative (Multiset α))) ↦
    a ∈ MulAction.orbit (↥(Subgroup.op (commutator (FreeGroup (Multiplicative (Multiset α)))))) b)
  (Quot.mk FreeGroup.Red.Step [(Quot.mk List.Perm (hd :: tl), true)])
Tactic: reduce
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih :
  (((FreeMonoid.lift : (a : α → FreeCommRing α) → FreeMonoid α →* FreeCommRing α) FreeCommRing.of :
          FreeMonoid α →* FreeCommRing α) :
        (a : FreeMonoid α) → FreeCommRing α)
      tl =
    FreeAbelianGroup.of (↑tl : Multiset α)
⊢ FreeCommRing.of hd * FreeAbelianGroup.of (↑tl : Multiset α) =
    FreeAbelianGroup.of (↑(FreeMonoid.of hd * tl) : Multiset α)
have conv_lhs : Quot.mk
    (fun (a b : FreeGroup (Multiplicative (Multiset α))) ↦
      a ∈ MulAction.orbit (↥(Subgroup.op (commutator (FreeGroup (Multiplicative (Multiset α)))))) b)
    (Quot.mk FreeGroup.Red.Step [(Quot.mk List.Perm (hd :: tl), true)]) =
  FreeAbelianGroup.of (↑(FreeMonoid.of hd * tl) : Multiset α)
Tactic: conv_lhs => reduce
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (hypothesis)
Goal:
α : Type u
inst : Subsingleton α
⊢ Bijective (α := FreeRing α) (β := FreeCommRing α) (⇑(coeRingHom α) : (a : FreeRing α) → FreeCommRing α)
have this : Eq (α := (a : FreeRing α) → FreeCommRing α) (⇑(coeRingHom α) : (a : FreeRing α) → FreeCommRing α)
  (⇑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α)) :
    (a : FreeAbelianGroup (List α)) → FreeAbelianGroup (Multiset α))
Tactic: have : (coeRingHom _ : FreeRing α → FreeCommRing α) =
        Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α) :=
      coe_eq α
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
inst : Subsingleton α
this :
  Eq (α := (a : FreeRing α) → FreeCommRing α) (⇑(coeRingHom α) : (a : FreeRing α) → FreeCommRing α)
    (⇑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α)) :
      (a : FreeAbelianGroup (List α)) → FreeAbelianGroup (Multiset α))
⊢ Bijective (α := FreeRing α) (β := FreeCommRing α) (⇑(coeRingHom α) : (a : FreeRing α) → FreeCommRing α)
have rw : Bijective (α := FreeRing α) (β := FreeCommRing α)
  (⇑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α)) :
    (a : FreeAbelianGroup (List α)) → FreeAbelianGroup (Multiset α))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
inst : Subsingleton α
x y : FreeRing α
⊢ x * y = y * x
have rw : x * y =
  ((subsingletonEquivFreeCommRing α).symm : (a : FreeCommRing α) → FreeRing α)
    ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) (y * x))
Tactic: rw [← (subsingletonEquivFreeCommRing α).symm_apply_apply (y * x),
        (subsingletonEquivFreeCommRing α).map_mul, mul_comm,
        ← (subsingletonEquivFreeCommRing α).map_mul,
        (subsingletonEquivFreeCommRing α).symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.FreeCommRing (goal)
Goal:
α : Type u
inst : Subsingleton α
x y : FreeRing α
rw :
  x * y =
    ((subsingletonEquivFreeCommRing α).symm : (a : FreeCommRing α) → FreeRing α)
      ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) (y * x))
⊢ x * y = y * x
have rw₁ : x * y =
  ((subsingletonEquivFreeCommRing α).symm : (a : FreeCommRing α) → FreeRing α)
    (HMul.hMul (α := FreeCommRing α) (β := FreeCommRing α)
      ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) y : FreeCommRing α)
      ((subsingletonEquivFreeCommRing α : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α))
Tactic: rw [← (subsingletonEquivFreeCommRing α).symm_apply_apply (y * x),
        (subsingletonEquivFreeCommRing α).map_mul, mul_comm,
        ← (subsingletonEquivFreeCommRing α).map_mul,
        (subsingletonEquivFreeCommRing α).symm_apply_apply]