-- Mathlib/RingTheory/FreeCommRing.lean
theorem coe_eq : ((↑) : FreeRing α → FreeCommRing α) =
    @Functor.map FreeAbelianGroup _ _ _ fun l : List α => (l : Multiset α)

Proof state:
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : (FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
⊢ Quot.lift
      (fun L =>
        List.foldr
          (fun x1 x2 =>
            Quot.lift
              (fun a₁ =>
                Quot.lift
                  (fun y =>
                    Quot.mk
                      (fun a b => a ∈ MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
                      (Quot.lift (fun L₁ => Quot.lift (fun L₂ => Quot.mk FreeGroup.Red.Step (L₁.append L₂)) ⋯ y) ⋯ a₁))
                  ⋯ x2)
              ⋯ x1)
          (Quot.mk (fun a b => a ∈ MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
            (Quot.mk FreeGroup.Red.Step []))
          (List.map
            (fun x =>
              (fun motive c h_1 h_2 => Bool.rec (h_2 PUnit.unit) (h_1 PUnit.unit) c)
                (fun c => Multiplicative (FreeAbelianGroup (Multiplicative (Multiset α)))) x.2
                (fun _ =>
                  Quot.lift
                    (fun L =>
                      List.foldr
                        (fun x1 x2 =>
                          Quot.lift
                            (fun a₁ =>
                              Quot.lift
                                (fun y =>
                                  Quot.mk
                                    (fun a b =>
                                      a ∈
                                        MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
                                    (Quot.lift
                                      (fun L₁ => Quot.lift (fun L₂ => Quot.mk FreeGroup.Red.Step (L₁.append L₂)) ⋯ y) ⋯
                                      a₁))
                                ⋯ x2)
                            ⋯ x1)
                        (Quot.mk
                          (fun a b =>
                            a ∈ MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
                          (Quot.mk FreeGroup.Red.Step []))
                        (List.map
                          (fun x_1 =>
                            (fun motive c h_1 h_2 => Bool.rec (h_2 PUnit.unit) (h_1 PUnit.unit) c)
                              (fun c => Multiplicative (FreeAbelianGroup (Multiplicative (Multiset α)))) x_1.2
                              (fun _ =>
                                Quot.mk
                                  (fun a b =>
                                    a ∈ MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
                                  (Quot.mk FreeGroup.Red.Step
                                    [(Quot.lift (fun a₁ => Quot.lift (fun l₂ => Quot.mk List.Perm (a₁.append l₂)) ⋯ x.1)
                                          ⋯ x_1.1,
                                        true)]))
                              fun _ =>
                              Quot.mk
                                (fun a b =>
                                  a ∈ MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
                                (Quot.mk FreeGroup.Red.Step
                                  [(Quot.lift (fun a₁ => Quot.lift (fun l₂ => Quot.mk List.Perm (a₁.append l₂)) ⋯ x.1) ⋯
                                        x_1.1,
                                      false)]))
                          L))
                    ⋯ (Quot.mk FreeGroup.Red.Step [(Quot.mk List.Perm [hd], true)]))
                fun _ =>
                Quot.lift
                  (fun x =>
                    Quot.mk
                      (fun a b => a ∈ MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
                      (Quot.lift
                        (fun x =>
                          Quot.mk FreeGroup.Red.Step
                            ((List.map
                                  (fun g =>
                                    (g.1,
                                      (fun motive c h_1 h_2 => Bool.rec (h_2 PUnit.unit) (h_1 PUnit.unit) c)
                                        (fun x => Bool) g.2 (fun _ => false) fun _ => true))
                                  x).reverseAux
                              []))
                        ⋯ x))
                  ⋯
                  (Quot.lift
                    (fun L =>
                      List.foldr
                        (fun x1 x2 =>
                          Quot.lift
                            (fun a₁ =>
                              Quot.lift
                                (fun y =>
                                  Quot.mk
                                    (fun a b =>
                                      a ∈
                                        MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
                                    (Quot.lift
                                      (fun L₁ => Quot.lift (fun L₂ => Quot.mk FreeGroup.Red.Step (L₁.append L₂)) ⋯ y) ⋯
                                      a₁))
                                ⋯ x2)
                            ⋯ x1)
                        (Quot.mk
                          (fun a b =>
                            a ∈ MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
                          (Quot.mk FreeGroup.Red.Step []))
                        (List.map
                          (fun x_1 =>
                            (fun motive c h_1 h_2 => Bool.rec (h_2 PUnit.unit) (h_1 PUnit.unit) c)
                              (fun c => Multiplicative (FreeAbelianGroup (Multiplicative (Multiset α)))) x_1.2
                              (fun _ =>
                                Quot.mk
                                  (fun a b =>
                                    a ∈ MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
                                  (Quot.mk FreeGroup.Red.Step
                                    [(Quot.lift (fun a₁ => Quot.lift (fun l₂ => Quot.mk List.Perm (a₁.append l₂)) ⋯ x.1)
                                          ⋯ x_1.1,
                                        true)]))
                              fun _ =>
                              Quot.mk
                                (fun a b =>
                                  a ∈ MulAction.orbit (↥(commutator (FreeGroup (Multiplicative (Multiset α)))).op) b)
                                (Quot.mk FreeGroup.Red.Step
                                  [(Quot.lift (fun a₁ => Quot.lift (fun l₂ => Quot.mk List.Perm (a₁.append l₂)) ⋯ x.1) ⋯
                                        x_1.1,
                                      false)]))
                          L))
                    ⋯ (Quot.mk FreeGroup.Red.Step [(Quot.mk List.Perm [hd], true)])))
            L))
      ⋯ (Quot.mk FreeGroup.Red.Step [(Quot.mk List.Perm tl, true)]) =
    FreeAbelianGroup.of ↑(FreeMonoid.of hd * tl)

Tactic:
rfl

Result:
no goals

Proof state:
case h
α : Type u
x : FreeRing α
⊢ ↑x = (fun l => ↑l) <$> x

Tactic:
erw [castFreeCommRing, toFreeCommRing, FreeRing.lift, Equiv.coe_trans, Function.comp,
  FreeAbelianGroup.liftMonoid_coe (FreeMonoid.lift FreeCommRing.of)]

Result:
case h
α : Type u
x : FreeRing α
⊢ (FreeAbelianGroup.lift ⇑(FreeMonoid.lift FreeCommRing.of)) x = (fun l => ↑l) <$> x