awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x.IsSupported s
refine_1 :
  Eq (α := FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) 1))
    1
refine_2 :
  Eq (α := FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (-1)))
    (-1)
refine_3 :
  ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
            ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) =
          n →
        (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
            ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (z * n)) =
          z * n
refine_4 :
  ∀ {x y : FreeCommRing α},
    (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) =
        x →
      (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
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) x) =
    x

Tactic:
refine Subring.InClosure.recOn hxs ?_ ?_ ?_ ?_
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x.IsSupported s
⊢ Eq.{u + 1} (α := FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α) 1) 1

Tactic:
rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x.IsSupported s
⊢ Eq.{u + 1} (α := FreeCommRing α)
    ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α) (-1)) (-1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeCommRing α
s : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
hxs : x.IsSupported s
p : α
hps : p ∈ s
n : FreeCommRing α
ih :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) =
    n
refine_3 :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p) : FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₁ :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (α := FreeCommRing (↑s : Type u)) (β := FreeCommRing (↑s : Type u))
        (if H : p ∈ s then of (Subtype.mk (p := fun (x : α) ↦ x ∈ s) p H) else 0 : FreeCommRing (↑s : Type u))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₂ :
  (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      (HMul.hMul (β := FreeCommRing (↑s : Type u)) (of (Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps))
        ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n : FreeCommRing (↑s : Type u))) =
    of p * n
refine_3₃ :
  HMul.hMul (α := FreeCommRing α) (β := FreeCommRing α)
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          (of (Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps)) :
        FreeCommRing α)
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) :
        FreeCommRing α) =
    of p * n
refine_3₄ :
  HMul.hMul (β := FreeCommRing α) (of (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps) : α))
      ((map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
          ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) n) :
        FreeCommRing α) =
    of p * n
refine_3₅ refine_3₆ : of (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) p hps) : α) * n = of p * n
⊢ (map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) : (a : FreeCommRing (↑s : Type u)) → FreeCommRing α)
      ((restriction s : (a : FreeCommRing α) → FreeCommRing (↑s : Type u)) (of p * n)) =
    of p * n

Tactic:
rw [map_mul, restriction_of, dif_pos hps, map_mul, map_of, ih]

Premises used: dif_pos, map_mul, FreeCommRing.restriction_of, FreeCommRing.map_of
-- Module: Mathlib.RingTheory.FreeCommRing
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
refine_4₃ refine_4₄ : x + y = 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

Tactic:
rw [map_add, map_add, ihx, ihy]

Premises used: map_add
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeCommRing α
⊢ ∃ (s : Set α), s.Finite ∧ x.IsSupported s

Tactic:
FreeCommRing.induction_on x ⟨∅, Set.finite_empty, isSupported_neg isSupported_one⟩
    (fun p => ⟨{p}, Set.finite_singleton p, isSupported_of.2 <| Set.mem_singleton _⟩)
    (fun _ _ ⟨s, hfs, hxs⟩ ⟨t, hft, hxt⟩ =>
      ⟨s ∪ t, hfs.union hft,
        isSupported_add (isSupported_upwards hxs Set.subset_union_left)
          (isSupported_upwards hxt Set.subset_union_right)⟩)
    fun _ _ ⟨s, hfs, hxs⟩ ⟨t, hft, hxt⟩ =>
    ⟨s ∪ t, hfs.union hft,
      isSupported_mul (isSupported_upwards hxs Set.subset_union_left)
        (isSupported_upwards hxt Set.subset_union_right)⟩

Premises used: FreeCommRing.induction_on
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeCommRing α
s : Set α
hfs : s.Finite
hxs rwa rwa₁ rwa₂ rwa₃ : x.IsSupported s
⊢ x.IsSupported (↑(hfs.toFinset (s := s)) : Set α)

Tactic:
rwa [Set.Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
⊢ Eq.{u + 1} (α := FreeCommRing α) (↑0 : FreeCommRing α) 0

Tactic:
rfl

Premises used: Quotient.liftOn', FreeGroup.Lift.aux, Con.liftOn, FreeRing.castFreeCommRing, List.foldr, rfl, List.prod
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
⊢ Eq.{u + 1} (α := FreeCommRing α) (↑1 : FreeCommRing α) 1

Tactic:
rfl

Premises used: FreeGroup.of, Quotient.liftOn', FreeGroup.Lift.aux, Quotient.map₂, List.append, Con.liftOn, FreeAbelianGroup.of, FreeGroup.mk, FreeRing.castFreeCommRing, List.foldr, rfl, List.prod
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
a : α
⊢ (↑(of a) : FreeCommRing α) = FreeCommRing.of a

Tactic:
FreeRing.lift_of _ _

Premises used: FreeRing.lift_of, FreeRing.castFreeCommRing
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeRing α
rw :
  Eq (α := FreeCommRing α) ((toFreeCommRing : (a : FreeRing α) → FreeCommRing α) (-x) : FreeCommRing α)
    (-(toFreeCommRing : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
rw₁ rw₂ :
  Eq (α := FreeCommRing α) (-(toFreeCommRing : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
    (-(toFreeCommRing : (a : FreeRing α) → FreeCommRing α) x : FreeCommRing α)
⊢ (↑(-x) : FreeCommRing α) = -(↑x : FreeCommRing α)

Tactic:
rw [castFreeCommRing, map_neg]

Premises used: map_neg, FreeRing.castFreeCommRing
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x y : FreeRing α
⊢ (↑(x + y) : FreeCommRing α) = (↑x : FreeCommRing α) + (↑y : FreeCommRing α)

Tactic:
(FreeRing.lift _).map_add _ _

Premises used: FreeRing.lift, RingHom.map_add, FreeRing.castFreeCommRing, DFunLike.coe
-- Module: Mathlib.RingTheory.FreeCommRing
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 α)
rw₁ 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 α)
⊢ (↑(x - y) : FreeCommRing α) = (↑x : FreeCommRing α) - (↑y : FreeCommRing α)

Tactic:
rw [castFreeCommRing, map_sub]

Premises used: map_sub, FreeRing.castFreeCommRing
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x y : FreeRing α
⊢ (↑(x * y) : FreeCommRing α) = (↑x : FreeCommRing α) * (↑y : FreeCommRing α)

Tactic:
(FreeRing.lift _).map_mul _ _

Premises used: FreeRing.lift, RingHom.map_mul, FreeRing.castFreeCommRing, DFunLike.coe
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
h : Eq.{u + 1} (α := FreeCommRing α) (↑(-1) : FreeCommRing α) (-1)
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = -1

Tactic:
use -1
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
⊢ Eq.{u + 1} (α := FreeCommRing α) (↑(-1) : FreeCommRing α) (-1)

Tactic:
rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
b : α
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = FreeCommRing.of b

Tactic:
⟨FreeRing.of b, rfl⟩

Premises used: FreeRing.of, Exists.intro, rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
b : α
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = FreeCommRing.of b

Tactic:
exact ⟨FreeRing.of b, rfl⟩
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x y : FreeCommRing α
hx : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x
hy : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = y
add : ∀ (x : FreeRing α), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) + y
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x + y

Tactic:
rcases hx with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
y : FreeCommRing α
hy : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = y
x : FreeRing α
add : ∀ (y : FreeRing α), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) + (↑y : FreeCommRing α)
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) + y

Tactic:
rcases hy with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x y : FreeRing α
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) + (↑y : FreeCommRing α)

Tactic:
⟨x + y, (FreeRing.lift _).map_add _ _⟩

Premises used: FreeRing.lift, HAdd.hAdd, Exists.intro, RingHom.map_add, DFunLike.coe
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x y : FreeRing α
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) + (↑y : FreeCommRing α)

Tactic:
exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x y : FreeCommRing α
hx : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x
hy : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = y
mul : ∀ (x : FreeRing α), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) * y
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = x * y

Tactic:
rcases hx with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
y : FreeCommRing α
hy : ∃ (a : FreeRing α), (↑a : FreeCommRing α) = y
x : FreeRing α
mul : ∀ (y : FreeRing α), ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) * (↑y : FreeCommRing α)
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) * y

Tactic:
rcases hy with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x y : FreeRing α
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) * (↑y : FreeCommRing α)

Tactic:
⟨x * y, (FreeRing.lift _).map_mul _ _⟩

Premises used: HMul.hMul, FreeRing.lift, Exists.intro, RingHom.map_mul, DFunLike.coe
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x y : FreeRing α
⊢ ∃ (a : FreeRing α), (↑a : FreeCommRing α) = (↑x : FreeCommRing α) * (↑y : FreeCommRing α)

Tactic:
exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩
-- Module: Mathlib.RingTheory.FreeCommRing
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
mul :
  ∀ (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

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 _ _⟩

Premises used: FreeRing.of, rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
h : ∀ (x : FreeRing α), (↑x : FreeCommRing α) = (fun (l : List α) ↦ (↑l : Multiset α)) <$> x
⊢ Eq.{u + 1} (α := FreeRing α → FreeCommRing α) castFreeCommRing (Functor.map fun (l : List α) ↦ (↑l : Multiset α))

Tactic:
funext x
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeRing α
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 α))
⊢ 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 α))

Tactic:
apply FreeAbelianGroup.lift_unique

Premises used: FreeAbelianGroup.lift_unique
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeRing α
L : FreeMonoid α
h :
  (((FreeMonoid.lift : (a : α → FreeCommRing α) → FreeMonoid α →* FreeCommRing α) FreeCommRing.of :
          FreeMonoid α →* FreeCommRing α) :
        (a : FreeMonoid α) → FreeCommRing α)
      L =
    FreeAbelianGroup.of (↑L : Multiset α)
⊢ 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 α))

Tactic:
simp only [AddMonoidHom.coe_coe, comp_apply, FreeAbelianGroup.lift_apply_of]

Premises used: AddMonoidHom.coe_coe, Function.comp_apply, FreeAbelianGroup.lift_apply_of
-- Module: Mathlib.RingTheory.FreeCommRing
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 α)
rw :
  FreeCommRing.of hd * FreeAbelianGroup.of (↑tl : Multiset α) =
    FreeAbelianGroup.of (↑(FreeMonoid.of hd * 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 α)

Tactic:
rw [(FreeMonoid.lift _).map_mul, FreeMonoid.lift_eval_of, ih]

Premises used: FreeMonoid.lift, FreeMonoid.lift_eval_of, DFunLike.coe, MonoidHom.map_mul
-- Module: Mathlib.RingTheory.FreeCommRing
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 α)
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)])
| FreeCommRing.of hd * FreeAbelianGroup.of (↑tl : Multiset α)

Tactic:
reduce
-- Module: Mathlib.RingTheory.FreeCommRing
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 α)
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 α)
⊢ FreeCommRing.of hd * FreeAbelianGroup.of (↑tl : Multiset α) =
    FreeAbelianGroup.of (↑(FreeMonoid.of hd * tl) : Multiset α)

Tactic:
conv_lhs => reduce
-- Module: Mathlib.RingTheory.FreeCommRing
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 α)
⊢ 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:
rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ (((FreeMonoid.lift : (a : α → FreeCommRing α) → FreeMonoid α →* FreeCommRing α) FreeCommRing.of :
          FreeMonoid α →* FreeCommRing α) :
        (a : FreeMonoid α) → FreeCommRing α)
      L =
    FreeAbelianGroup.of (↑L : Multiset α)

Tactic:
exact
    FreeMonoid.recOn L rfl fun hd tl ih => by
      rw [(FreeMonoid.lift _).map_mul, FreeMonoid.lift_eval_of, ih]
      conv_lhs => reduce
      rfl
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
inst : Subsingleton α
⊢ 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 α
-- Module: Mathlib.RingTheory.FreeCommRing
Goal:
α : Type u
inst : Subsingleton α
this :
  Eq (α := (a : FreeRing α) → FreeCommRing α) (⇑(coeRingHom α) : (a : FreeRing α) → FreeCommRing α)
    (⇑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α)) :
      (a : FreeAbelianGroup (List α)) → FreeAbelianGroup (Multiset α))
rw :
  Bijective (α := FreeRing α) (β := FreeCommRing α)
    (⇑(Functor.mapEquiv FreeAbelianGroup (Multiset.subsingletonEquiv α)) :
      (a : FreeAbelianGroup (List α)) → FreeAbelianGroup (Multiset α))
⊢ Bijective (α := FreeRing α) (β := FreeCommRing α) (⇑(coeRingHom α) : (a : FreeRing α) → FreeCommRing α)

Tactic:
rw [this]