[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ star (star x) = x
[PROOFSTEP]
unfold Star.star
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ { star := MulOpposite.unop ∘ ↑(↑(lift R) (MulOpposite.op ∘ ι R)) }.1
      ({ star := MulOpposite.unop ∘ ↑(↑(lift R) (MulOpposite.op ∘ ι R)) }.1 x) =
    x
[PROOFSTEP]
simp only [Function.comp_apply]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) x))) = x
[PROOFSTEP]
refine' FreeAlgebra.induction R X _ _ _ _ x
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ ∀ (r : R),
    MulOpposite.unop
        (↑(↑(lift R) (MulOpposite.op ∘ ι R))
          (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (↑(algebraMap R (FreeAlgebra R X)) r)))) =
      ↑(algebraMap R (FreeAlgebra R X)) r
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
r✝ : R
⊢ MulOpposite.unop
      (↑(↑(lift R) (MulOpposite.op ∘ ι R))
        (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (↑(algebraMap R (FreeAlgebra R X)) r✝)))) =
    ↑(algebraMap R (FreeAlgebra R X)) r✝
[PROOFSTEP]
simp only [AlgHom.commutes, MulOpposite.algebraMap_apply, MulOpposite.unop_op]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ ∀ (x : X),
    MulOpposite.unop
        (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (ι R x)))) =
      ι R x
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
x✝ : X
⊢ MulOpposite.unop
      (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (ι R x✝)))) =
    ι R x✝
[PROOFSTEP]
simp only [lift_ι_apply, Function.comp_apply, MulOpposite.unop_op]
[GOAL]
case refine'_3
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ ∀ (a b : FreeAlgebra R X),
    MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) a))) =
        a →
      MulOpposite.unop
            (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) b))) =
          b →
        MulOpposite.unop
            (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (a * b)))) =
          a * b
[PROOFSTEP]
intros
[GOAL]
case refine'_3
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x a✝² b✝ : FreeAlgebra R X
a✝¹ :
  MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) a✝²))) =
    a✝²
a✝ :
  MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) b✝))) =
    b✝
⊢ MulOpposite.unop
      (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (a✝² * b✝)))) =
    a✝² * b✝
[PROOFSTEP]
simp only [*, map_mul, MulOpposite.unop_mul]
[GOAL]
case refine'_4
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
⊢ ∀ (a b : FreeAlgebra R X),
    MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) a))) =
        a →
      MulOpposite.unop
            (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) b))) =
          b →
        MulOpposite.unop
            (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (a + b)))) =
          a + b
[PROOFSTEP]
intros
[GOAL]
case refine'_4
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x a✝² b✝ : FreeAlgebra R X
a✝¹ :
  MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) a✝²))) =
    a✝²
a✝ :
  MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) b✝))) =
    b✝
⊢ MulOpposite.unop
      (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (MulOpposite.unop (↑(↑(lift R) (MulOpposite.op ∘ ι R)) (a✝² + b✝)))) =
    a✝² + b✝
[PROOFSTEP]
simp only [*, map_add, MulOpposite.unop_add]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a b : FreeAlgebra R X
⊢ star (a * b) = star b * star a
[PROOFSTEP]
simp only [Function.comp_apply, map_mul, MulOpposite.unop_mul]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a b : FreeAlgebra R X
⊢ star (a + b) = star a + star b
[PROOFSTEP]
simp only [Function.comp_apply, map_add, MulOpposite.unop_add]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : X
⊢ star (ι R x) = ι R x
[PROOFSTEP]
simp [star, Star.star]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
r : R
⊢ star (↑(algebraMap R (FreeAlgebra R X)) r) = ↑(algebraMap R (FreeAlgebra R X)) r
[PROOFSTEP]
simp [star, Star.star]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
src✝ : FreeAlgebra R X ≃+* (FreeAlgebra R X)ᵐᵒᵖ := starRingEquiv
r : R
⊢ Equiv.toFun src✝.toEquiv (↑(algebraMap R (FreeAlgebra R X)) r) = ↑(algebraMap R (FreeAlgebra R X)ᵐᵒᵖ) r
[PROOFSTEP]
simp [star_algebraMap]
