case h
α : Type u
x : FreeRing α
⊢ ↑x = (fun l => ↑l) <$> x
α : Type u
⊢ castFreeCommRing = Functor.map fun l => ↑l
funext x
case h
α : Type u
x : FreeRing α
⊢ ↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) x = (fun l => ↑l) <$> x
case h
α : Type u
x : FreeRing α
⊢ ↑x = (fun l => ↑l) <$> x
erw [castFreeCommRing, toFreeCommRing, FreeRing.lift, Equiv.coe_trans, Function.comp,
  FreeAbelianGroup.liftMonoid_coe (FreeMonoid.lift FreeCommRing.of)]
case h
α : Type u
x : FreeRing α
⊢ ↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) x =
    ↑(↑FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x
case h
α : Type u
x : FreeRing α
⊢ ↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) x = (fun l => ↑l) <$> x
dsimp [Functor.map]
case h
α : Type u
x : FreeRing α
⊢ ↑↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) x =
    ↑(↑FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x
case h
α : Type u
x : FreeRing α
⊢ ↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) x =
    ↑(↑FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x
rw [← AddMonoidHom.coe_coe]
case h.hg
α : Type u
x : FreeRing α
⊢ ∀ (x : FreeMonoid α),
    ↑↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of x) =
      ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l) x
case h
α : Type u
x : FreeRing α
⊢ ↑↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) x =
    ↑(↑FreeAbelianGroup.lift ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l)) x
apply FreeAbelianGroup.lift.unique
case h.hg
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ ↑↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of L) =
    ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l) L
case h.hg
α : Type u
x : FreeRing α
⊢ ∀ (x : FreeMonoid α),
    ↑↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of x) =
      ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l) x
intro L
case h.hg
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ ↑(↑FreeMonoid.lift FreeCommRing.of) L = FreeAbelianGroup.of ↑L
case h.hg
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ ↑↑(↑FreeAbelianGroup.lift ↑(↑FreeMonoid.lift FreeCommRing.of)) (FreeAbelianGroup.of L) =
    ((fun α_1 => FreeAbelianGroup.of α_1) ∘ fun l => ↑l) L
erw [FreeAbelianGroup.lift.of, Function.comp]
no goals
case h.hg
α : Type u
x : FreeRing α
L : FreeMonoid α
⊢ ↑(↑FreeMonoid.lift FreeCommRing.of) L = FreeAbelianGroup.of ↑L
exact
  FreeMonoid.recOn L rfl fun hd tl ih => by
    rw [(FreeMonoid.lift _).map_mul, FreeMonoid.lift_eval_of, ih]
    conv_lhs => reduce
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : ↑(↑FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
⊢ FreeCommRing.of hd * FreeAbelianGroup.of ↑tl = FreeAbelianGroup.of ↑(FreeMonoid.of hd * tl)
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : ↑(↑FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
⊢ ↑(↑FreeMonoid.lift FreeCommRing.of) (FreeMonoid.of hd * tl) = FreeAbelianGroup.of ↑(FreeMonoid.of hd * tl)
rw [(FreeMonoid.lift _).map_mul, FreeMonoid.lift_eval_of, ih]
no goals
α : Type u
x : FreeRing α
L : FreeMonoid α
hd : α
tl : FreeMonoid α
ih : ↑(↑FreeMonoid.lift FreeCommRing.of) tl = FreeAbelianGroup.of ↑tl
⊢ FreeCommRing.of hd * FreeAbelianGroup.of ↑tl = FreeAbelianGroup.of ↑(FreeMonoid.of hd * tl)
conv_lhs => reduce