[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (a b c : FreeAlgebra R X), a * b * c = a * (b * c)
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝³ : FreeAlgebra R X
a✝² : Pre R X
b✝ : FreeAlgebra R X
a✝¹ : Pre R X
c✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝² * Quot.mk (Rel R X) a✝¹ * Quot.mk (Rel R X) a✝ =
    Quot.mk (Rel R X) a✝² * (Quot.mk (Rel R X) a✝¹ * Quot.mk (Rel R X) a✝)
[PROOFSTEP]
exact Quot.sound Rel.mul_assoc
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (a : FreeAlgebra R X), 1 * a = a
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ 1 * Quot.mk (Rel R X) a✝ = Quot.mk (Rel R X) a✝
[PROOFSTEP]
exact Quot.sound Rel.one_mul
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (a : FreeAlgebra R X), a * 1 = a
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝ * 1 = Quot.mk (Rel R X) a✝
[PROOFSTEP]
exact Quot.sound Rel.mul_one
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (a : FreeAlgebra R X), 0 * a = 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ 0 * Quot.mk (Rel R X) a✝ = 0
[PROOFSTEP]
exact Quot.sound Rel.zero_mul
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (a : FreeAlgebra R X), a * 0 = 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝ * 0 = 0
[PROOFSTEP]
exact Quot.sound Rel.mul_zero
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (a b c : FreeAlgebra R X), a * (b + c) = a * b + a * c
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝³ : FreeAlgebra R X
a✝² : Pre R X
b✝ : FreeAlgebra R X
a✝¹ : Pre R X
c✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝² * (Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝) =
    Quot.mk (Rel R X) a✝² * Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝² * Quot.mk (Rel R X) a✝
[PROOFSTEP]
exact Quot.sound Rel.left_distrib
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (a b c : FreeAlgebra R X), (a + b) * c = a * c + b * c
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝³ : FreeAlgebra R X
a✝² : Pre R X
b✝ : FreeAlgebra R X
a✝¹ : Pre R X
c✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ (Quot.mk (Rel R X) a✝² + Quot.mk (Rel R X) a✝¹) * Quot.mk (Rel R X) a✝ =
    Quot.mk (Rel R X) a✝² * Quot.mk (Rel R X) a✝ + Quot.mk (Rel R X) a✝¹ * Quot.mk (Rel R X) a✝
[PROOFSTEP]
exact Quot.sound Rel.right_distrib
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (a b c : FreeAlgebra R X), a + b + c = a + (b + c)
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ ⟨⟩
[GOAL]
case mk.mk.mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝³ : FreeAlgebra R X
a✝² : Pre R X
b✝ : FreeAlgebra R X
a✝¹ : Pre R X
c✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝² + Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝ =
    Quot.mk (Rel R X) a✝² + (Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝)
[PROOFSTEP]
exact Quot.sound Rel.add_assoc
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (a : FreeAlgebra R X), 0 + a = a
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ 0 + Quot.mk (Rel R X) a✝ = Quot.mk (Rel R X) a✝
[PROOFSTEP]
exact Quot.sound Rel.zero_add
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (a : FreeAlgebra R X), a + 0 = a
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝ + 0 = Quot.mk (Rel R X) a✝
[PROOFSTEP]
change Quot.mk _ _ = _
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝¹ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) (a✝ + 0) = Quot.mk (Rel R X) a✝
[PROOFSTEP]
rw [Quot.sound Rel.add_comm, Quot.sound Rel.zero_add]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (x : FreeAlgebra R X), (fun x x_1 => x • x_1) 0 x = 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ (fun x x_1 => x • x_1) 0 (Quot.mk (Rel R X) a✝) = 0
[PROOFSTEP]
change Quot.mk _ (_ * _) = _
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) (Pre.of_scalar (↑(algebraMap ℕ R) 0) * a✝) = 0
[PROOFSTEP]
rw [map_zero]
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) (Pre.of_scalar 0 * a✝) = 0
[PROOFSTEP]
exact Quot.sound Rel.zero_mul
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
n : ℕ
⊢ ∀ (x : FreeAlgebra R X), (fun x x_1 => x • x_1) (n + 1) x = x + (fun x x_1 => x • x_1) n x
[PROOFSTEP]
rintro ⟨a⟩
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ (fun x x_1 => x • x_1) (n + 1) (Quot.mk (Rel R X) a) =
    Quot.mk (Rel R X) a + (fun x x_1 => x • x_1) n (Quot.mk (Rel R X) a)
[PROOFSTEP]
dsimp only [HSMul.hSMul, instSMul, Quot.map]
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.of_scalar (↑(algebraMap ℕ R) (n + 1)) * a) =
    Quot.mk (Rel R X) a + Quot.mk (Rel R X) (Pre.of_scalar (↑(algebraMap ℕ R) n) * a)
[PROOFSTEP]
rw [map_add, map_one, add_comm, mk_mul, mk_mul, ← one_add_mul (_ : FreeAlgebra R X)]
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.of_scalar (1 + ↑(algebraMap ℕ R) n)) * Quot.mk (Rel R X) a =
    (1 + Quot.mk (Rel R X) (Pre.of_scalar (↑(algebraMap ℕ R) n))) * Quot.mk (Rel R X) a
[PROOFSTEP]
congr 1
[GOAL]
case mk.e_a
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
n : ℕ
x✝ : FreeAlgebra R X
a : Pre R X
⊢ Quot.mk (Rel R X) (Pre.of_scalar (1 + ↑(algebraMap ℕ R) n)) =
    1 + Quot.mk (Rel R X) (Pre.of_scalar (↑(algebraMap ℕ R) n))
[PROOFSTEP]
exact Quot.sound Rel.add_scalar
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
⊢ ∀ (a b : FreeAlgebra R X), a + b = b + a
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩
[GOAL]
case mk.mk
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
a✝² : FreeAlgebra R X
a✝¹ : Pre R X
b✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝ = Quot.mk (Rel R X) a✝ + Quot.mk (Rel R X) a✝¹
[PROOFSTEP]
exact Quot.sound Rel.add_comm
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
src✝² : MonoidWithZero (FreeAlgebra R X) := instMonoidWithZero R X
src✝¹ : AddCommMonoid (FreeAlgebra R X) := instAddCommMonoid R X
src✝ : Distrib (FreeAlgebra R X) := instDistrib R X
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
src✝² : MonoidWithZero (FreeAlgebra R X) := instMonoidWithZero R X
src✝¹ : AddCommMonoid (FreeAlgebra R X) := instAddCommMonoid R X
src✝ : Distrib (FreeAlgebra R X) := instDistrib R X
⊢ Quot.mk (Rel R X) (Pre.of_scalar 0) = 0
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
src✝² : MonoidWithZero (FreeAlgebra R X) := instMonoidWithZero R X
src✝¹ : AddCommMonoid (FreeAlgebra R X) := instAddCommMonoid R X
src✝ : Distrib (FreeAlgebra R X) := instDistrib R X
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
src✝² : MonoidWithZero (FreeAlgebra R X) := instMonoidWithZero R X
src✝¹ : AddCommMonoid (FreeAlgebra R X) := instAddCommMonoid R X
src✝ : Distrib (FreeAlgebra R X) := instDistrib R X
n : ℕ
⊢ Quot.mk (Rel R X) (Pre.of_scalar (↑n + 1)) = Quot.mk (Rel R X) (Pre.of_scalar ↑n) + 1
[PROOFSTEP]
exact Quot.sound Rel.add_scalar
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type ?u.69679
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x✝ : R
⊢ ∀ (x : (fun x => FreeAlgebra A X) x✝),
    ↑(RingHom.comp
              {
                toMonoidHom :=
                  {
                    toOneHom :=
                      { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                        map_one' :=
                          (_ :
                            (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                              (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                    map_mul' :=
                      (_ :
                        ∀ (x x_1 : A),
                          Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                            Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                                map_one' :=
                                  (_ :
                                    (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                                      (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x x_1 : A),
                                  Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                                    Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) })
                        0 =
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                                map_one' :=
                                  (_ :
                                    (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                                      (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x x_1 : A),
                                  Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                                    Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) })
                        0),
                map_add' :=
                  (_ :
                    ∀ (x x_1 : A),
                      Quot.mk (Rel A X) (Pre.of_scalar (x + x_1)) =
                        Quot.mk (Rel A X) (Pre.of_scalar x + Pre.of_scalar x_1)) }
              (algebraMap R A))
          x✝ *
        x =
      x *
        ↑(RingHom.comp
              {
                toMonoidHom :=
                  {
                    toOneHom :=
                      { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                        map_one' :=
                          (_ :
                            (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                              (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                    map_mul' :=
                      (_ :
                        ∀ (x x_1 : A),
                          Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                            Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                                map_one' :=
                                  (_ :
                                    (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                                      (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x x_1 : A),
                                  Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                                    Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) })
                        0 =
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                                map_one' :=
                                  (_ :
                                    (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                                      (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x x_1 : A),
                                  Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                                    Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) })
                        0),
                map_add' :=
                  (_ :
                    ∀ (x x_1 : A),
                      Quot.mk (Rel A X) (Pre.of_scalar (x + x_1)) =
                        Quot.mk (Rel A X) (Pre.of_scalar x + Pre.of_scalar x_1)) }
              (algebraMap R A))
          x✝
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case mk
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type ?u.69679
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
x✝¹ : R
x✝ : FreeAlgebra A X
a✝ : Pre A X
⊢ ↑(RingHom.comp
            {
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                      map_one' :=
                        (_ :
                          (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                            (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x x_1 : A),
                        Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                          Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                              map_one' :=
                                (_ :
                                  (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                                    (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x x_1 : A),
                                Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                                  Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) })
                      0 =
                    OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                              map_one' :=
                                (_ :
                                  (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                                    (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x x_1 : A),
                                Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                                  Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) })
                      0),
              map_add' :=
                (_ :
                  ∀ (x x_1 : A),
                    Quot.mk (Rel A X) (Pre.of_scalar (x + x_1)) =
                      Quot.mk (Rel A X) (Pre.of_scalar x + Pre.of_scalar x_1)) }
            (algebraMap R A))
        x✝¹ *
      Quot.mk (Rel A X) a✝ =
    Quot.mk (Rel A X) a✝ *
      ↑(RingHom.comp
            {
              toMonoidHom :=
                {
                  toOneHom :=
                    { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                      map_one' :=
                        (_ :
                          (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                            (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x x_1 : A),
                        Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                          Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                              map_one' :=
                                (_ :
                                  (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                                    (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x x_1 : A),
                                Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                                  Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) })
                      0 =
                    OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun r => Quot.mk (Rel A X) (Pre.of_scalar r),
                              map_one' :=
                                (_ :
                                  (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1 =
                                    (fun r => Quot.mk (Rel A X) (Pre.of_scalar r)) 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x x_1 : A),
                                Quot.mk (Rel A X) (Pre.of_scalar (x * x_1)) =
                                  Quot.mk (Rel A X) (Pre.of_scalar x * Pre.of_scalar x_1)) })
                      0),
              map_add' :=
                (_ :
                  ∀ (x x_1 : A),
                    Quot.mk (Rel A X) (Pre.of_scalar (x + x_1)) =
                      Quot.mk (Rel A X) (Pre.of_scalar x + Pre.of_scalar x_1)) }
            (algebraMap R A))
        x✝¹
[PROOFSTEP]
exact Quot.sound Rel.central_scalar
[GOAL]
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
X : Type u_2
R : Type ?u.71720
S : Type ?u.71723
A : Type ?u.71726
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : SMul R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
⊢ (r • s) • x = r • s • x
[PROOFSTEP]
change algebraMap S A (r • s) • x = algebraMap R A _ • (algebraMap S A _ • x)
[GOAL]
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
X : Type u_2
R : Type ?u.71720
S : Type ?u.71723
A : Type ?u.71726
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : SMul R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
⊢ ↑(algebraMap S A) (r • s) • x = ↑(algebraMap R A) r • ↑(algebraMap S A) s • x
[PROOFSTEP]
rw [← smul_assoc]
[GOAL]
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
X : Type u_2
R : Type ?u.71720
S : Type ?u.71723
A : Type ?u.71726
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : SMul R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
⊢ ↑(algebraMap S A) (r • s) • x = (↑(algebraMap R A) r • ↑(algebraMap S A) s) • x
[PROOFSTEP]
congr
[GOAL]
case e_a
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
X : Type u_2
R : Type ?u.71720
S : Type ?u.71723
A : Type ?u.71726
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : SMul R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
⊢ ↑(algebraMap S A) (r • s) = ↑(algebraMap R A) r • ↑(algebraMap S A) s
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, smul_eq_mul]
[GOAL]
case e_a
R✝ : Type u_1
inst✝⁷ : CommSemiring R✝
X : Type u_2
R : Type ?u.71720
S : Type ?u.71723
A : Type ?u.71726
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : SMul R S
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
r : R
s : S
x : FreeAlgebra A X
⊢ (r • s) • 1 = r • 1 * s • 1
[PROOFSTEP]
rw [smul_assoc, ← smul_one_mul]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
m : X
⊢ Quot.mk (Rel R X) (Pre.of m) = ι R m
[PROOFSTEP]
rw [ι_def]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝ : FreeAlgebra R X
a b : Pre R X
h : Rel R X a b
⊢ liftFun R X f a = liftFun R X f b
[PROOFSTEP]
induction' h
[GOAL]
case add_scalar
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝ : FreeAlgebra R X
a b : Pre R X
r✝ s✝ : R
⊢ liftFun R X f (Pre.of_scalar (r✝ + s✝)) = liftFun R X f (Pre.of_scalar r✝ + Pre.of_scalar s✝)
[PROOFSTEP]
exact (algebraMap R A).map_add _ _
[GOAL]
case mul_scalar
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝ : FreeAlgebra R X
a b : Pre R X
r✝ s✝ : R
⊢ liftFun R X f (Pre.of_scalar (r✝ * s✝)) = liftFun R X f (Pre.of_scalar r✝ * Pre.of_scalar s✝)
[PROOFSTEP]
exact (algebraMap R A).map_mul _ _
[GOAL]
case central_scalar
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b : Pre R X
r✝ : R
a✝ : Pre R X
⊢ liftFun R X f (Pre.of_scalar r✝ * a✝) = liftFun R X f (a✝ * Pre.of_scalar r✝)
[PROOFSTEP]
apply Algebra.commutes
[GOAL]
case add_assoc
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f (a✝ + b✝ + c✝) = liftFun R X f (a✝ + (b✝ + c✝))
[PROOFSTEP]
change _ + _ + _ = _ + (_ + _)
[GOAL]
case add_assoc
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f a✝ + liftFun R X f b✝ + liftFun R X f c✝ = liftFun R X f a✝ + (liftFun R X f b✝ + liftFun R X f c✝)
[PROOFSTEP]
rw [add_assoc]
[GOAL]
case add_comm
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ : Pre R X
⊢ liftFun R X f (a✝ + b✝) = liftFun R X f (b✝ + a✝)
[PROOFSTEP]
change _ + _ = _ + _
[GOAL]
case add_comm
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ : Pre R X
⊢ liftFun R X f a✝ + liftFun R X f b✝ = liftFun R X f b✝ + liftFun R X f a✝
[PROOFSTEP]
rw [add_comm]
[GOAL]
case zero_add
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ liftFun R X f (0 + a✝) = liftFun R X f a✝
[PROOFSTEP]
change algebraMap _ _ _ + liftFun R X f _ = liftFun R X f _
[GOAL]
case zero_add
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ ↑(algebraMap R A) 0 + liftFun R X f a✝ = liftFun R X f a✝
[PROOFSTEP]
simp
[GOAL]
case mul_assoc
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f (a✝ * b✝ * c✝) = liftFun R X f (a✝ * (b✝ * c✝))
[PROOFSTEP]
change _ * _ * _ = _ * (_ * _)
[GOAL]
case mul_assoc
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f a✝ * liftFun R X f b✝ * liftFun R X f c✝ = liftFun R X f a✝ * (liftFun R X f b✝ * liftFun R X f c✝)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case one_mul
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ liftFun R X f (1 * a✝) = liftFun R X f a✝
[PROOFSTEP]
change algebraMap _ _ _ * liftFun R X f _ = liftFun R X f _
[GOAL]
case one_mul
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ ↑(algebraMap R A) 1 * liftFun R X f a✝ = liftFun R X f a✝
[PROOFSTEP]
simp
[GOAL]
case mul_one
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ liftFun R X f (a✝ * 1) = liftFun R X f a✝
[PROOFSTEP]
change liftFun R X f _ * algebraMap _ _ _ = liftFun R X f _
[GOAL]
case mul_one
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ liftFun R X f a✝ * ↑(algebraMap R A) 1 = liftFun R X f a✝
[PROOFSTEP]
simp
[GOAL]
case left_distrib
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f (a✝ * (b✝ + c✝)) = liftFun R X f (a✝ * b✝ + a✝ * c✝)
[PROOFSTEP]
change _ * (_ + _) = _ * _ + _ * _
[GOAL]
case left_distrib
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f a✝ * (liftFun R X f b✝ + liftFun R X f c✝) =
    liftFun R X f a✝ * liftFun R X f b✝ + liftFun R X f a✝ * liftFun R X f c✝
[PROOFSTEP]
rw [left_distrib]
[GOAL]
case right_distrib
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ liftFun R X f ((a✝ + b✝) * c✝) = liftFun R X f (a✝ * c✝ + b✝ * c✝)
[PROOFSTEP]
change (_ + _) * _ = _ * _ + _ * _
[GOAL]
case right_distrib
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ b✝ c✝ : Pre R X
⊢ (liftFun R X f a✝ + liftFun R X f b✝) * liftFun R X f c✝ =
    liftFun R X f a✝ * liftFun R X f c✝ + liftFun R X f b✝ * liftFun R X f c✝
[PROOFSTEP]
rw [right_distrib]
[GOAL]
case zero_mul
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ liftFun R X f (0 * a✝) = liftFun R X f 0
[PROOFSTEP]
change algebraMap _ _ _ * _ = algebraMap _ _ _
[GOAL]
case zero_mul
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ ↑(algebraMap R A) 0 * liftFun R X f a✝ = ↑(algebraMap R A) 0
[PROOFSTEP]
simp
[GOAL]
case mul_zero
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ liftFun R X f (a✝ * 0) = liftFun R X f 0
[PROOFSTEP]
change _ * algebraMap _ _ _ = algebraMap _ _ _
[GOAL]
case mul_zero
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝¹ : FreeAlgebra R X
a b a✝ : Pre R X
⊢ liftFun R X f a✝ * ↑(algebraMap R A) 0 = ↑(algebraMap R A) 0
[PROOFSTEP]
simp
[GOAL]
case add_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ + c✝) = liftFun R X f (b✝ + c✝)
case add_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
repeat
  change liftFun R X f _ + liftFun R X f _ = _
  simp only [*]
  rfl
[GOAL]
case add_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ + c✝) = liftFun R X f (b✝ + c✝)
case add_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
change liftFun R X f _ + liftFun R X f _ = _
[GOAL]
case add_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f a✝¹ + liftFun R X f c✝ = liftFun R X f (b✝ + c✝)
case add_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
simp only [*]
[GOAL]
case add_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f b✝ + liftFun R X f c✝ = liftFun R X f (b✝ + c✝)
case add_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
rfl
[GOAL]
case add_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ + a✝¹) = liftFun R X f (c✝ + b✝)
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
change liftFun R X f _ + liftFun R X f _ = _
[GOAL]
case add_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f c✝ + liftFun R X f a✝¹ = liftFun R X f (c✝ + b✝)
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
simp only [*]
[GOAL]
case add_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f c✝ + liftFun R X f b✝ = liftFun R X f (c✝ + b✝)
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
rfl
[GOAL]
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
change liftFun R X f _ + liftFun R X f _ = _
[GOAL]
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
repeat
  change liftFun R X f _ * liftFun R X f _ = _
  simp only [*]
  rfl
[GOAL]
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (a✝¹ * c✝) = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
change liftFun R X f _ * liftFun R X f _ = _
[GOAL]
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f a✝¹ * liftFun R X f c✝ = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
simp only [*]
[GOAL]
case mul_compat_left
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f b✝ * liftFun R X f c✝ = liftFun R X f (b✝ * c✝)
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
rfl
[GOAL]
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f (c✝ * a✝¹) = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
change liftFun R X f _ * liftFun R X f _ = _
[GOAL]
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f c✝ * liftFun R X f a✝¹ = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
simp only [*]
[GOAL]
case mul_compat_right
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝² : FreeAlgebra R X
a b a✝¹ b✝ c✝ : Pre R X
a✝ : Rel R X a✝¹ b✝
a_ih✝ : liftFun R X f a✝¹ = liftFun R X f b✝
⊢ liftFun R X f c✝ * liftFun R X f b✝ = liftFun R X f (c✝ * b✝)
[PROOFSTEP]
rfl
[GOAL]

[PROOFSTEP]
change liftFun R X f _ * liftFun R X f _ = _
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ (fun a => Quot.liftOn a (liftFun R X f) (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b)) 1 =
    1
[PROOFSTEP]
change algebraMap _ _ _ = _
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ ↑(algebraMap R A) 1 = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ ∀ (x y : FreeAlgebra R X),
    OneHom.toFun
        {
          toFun := fun a =>
            Quot.liftOn a (liftFun R X f) (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
        (x * y) =
      OneHom.toFun
          {
            toFun := fun a =>
              Quot.liftOn a (liftFun R X f) (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
            map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
          x *
        OneHom.toFun
          {
            toFun := fun a =>
              Quot.liftOn a (liftFun R X f) (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
            map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
          y
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩
[GOAL]
case mk.mk
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : FreeAlgebra R X
a✝¹ : Pre R X
y✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ OneHom.toFun
      {
        toFun := fun a =>
          Quot.liftOn a (liftFun R X f) (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
        map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
      (Quot.mk (Rel R X) a✝¹ * Quot.mk (Rel R X) a✝) =
    OneHom.toFun
        {
          toFun := fun a =>
            Quot.liftOn a (liftFun R X f) (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
        (Quot.mk (Rel R X) a✝¹) *
      OneHom.toFun
        {
          toFun := fun a =>
            Quot.liftOn a (liftFun R X f) (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
        (Quot.mk (Rel R X) a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            {
              toFun := fun a =>
                Quot.liftOn a (liftFun R X f) (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
              map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : FreeAlgebra R X),
                OneHom.toFun
                    {
                      toFun := fun a =>
                        Quot.liftOn a (liftFun R X f)
                          (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                      map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      {
                        toFun := fun a =>
                          Quot.liftOn a (liftFun R X f)
                            (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                        map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                      x *
                    OneHom.toFun
                      {
                        toFun := fun a =>
                          Quot.liftOn a (liftFun R X f)
                            (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                        map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                      y) })
      0 =
    0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ Quot.liftOn 0 (liftFun R X f) (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b) = 0
[PROOFSTEP]
change algebraMap _ _ _ = _
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ ↑(algebraMap R A) 0 = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ ∀ (x y : FreeAlgebra R X),
    OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun a =>
                  Quot.liftOn a (liftFun R X f)
                    (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : FreeAlgebra R X),
                  OneHom.toFun
                      {
                        toFun := fun a =>
                          Quot.liftOn a (liftFun R X f)
                            (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                        map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun a =>
                            Quot.liftOn a (liftFun R X f)
                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun a =>
                            Quot.liftOn a (liftFun R X f)
                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                        y) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun a =>
                    Quot.liftOn a (liftFun R X f)
                      (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                  map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : FreeAlgebra R X),
                    OneHom.toFun
                        {
                          toFun := fun a =>
                            Quot.liftOn a (liftFun R X f)
                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun a =>
                              Quot.liftOn a (liftFun R X f)
                                (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                            map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun a =>
                              Quot.liftOn a (liftFun R X f)
                                (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                            map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                {
                  toFun := fun a =>
                    Quot.liftOn a (liftFun R X f)
                      (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                  map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : FreeAlgebra R X),
                    OneHom.toFun
                        {
                          toFun := fun a =>
                            Quot.liftOn a (liftFun R X f)
                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          {
                            toFun := fun a =>
                              Quot.liftOn a (liftFun R X f)
                                (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                            map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                          x *
                        OneHom.toFun
                          {
                            toFun := fun a =>
                              Quot.liftOn a (liftFun R X f)
                                (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                            map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                          y) })
          y
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩
[GOAL]
case mk.mk
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : FreeAlgebra R X
a✝¹ : Pre R X
y✝ : FreeAlgebra R X
a✝ : Pre R X
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            {
              toFun := fun a =>
                Quot.liftOn a (liftFun R X f) (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
              map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : FreeAlgebra R X),
                OneHom.toFun
                    {
                      toFun := fun a =>
                        Quot.liftOn a (liftFun R X f)
                          (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                      map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      {
                        toFun := fun a =>
                          Quot.liftOn a (liftFun R X f)
                            (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                        map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                      x *
                    OneHom.toFun
                      {
                        toFun := fun a =>
                          Quot.liftOn a (liftFun R X f)
                            (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                        map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                      y) })
      (Quot.mk (Rel R X) a✝¹ + Quot.mk (Rel R X) a✝) =
    OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun a =>
                  Quot.liftOn a (liftFun R X f)
                    (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : FreeAlgebra R X),
                  OneHom.toFun
                      {
                        toFun := fun a =>
                          Quot.liftOn a (liftFun R X f)
                            (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                        map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun a =>
                            Quot.liftOn a (liftFun R X f)
                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun a =>
                            Quot.liftOn a (liftFun R X f)
                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                        y) })
        (Quot.mk (Rel R X) a✝¹) +
      OneHom.toFun
        (↑{
            toOneHom :=
              {
                toFun := fun a =>
                  Quot.liftOn a (liftFun R X f)
                    (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : FreeAlgebra R X),
                  OneHom.toFun
                      {
                        toFun := fun a =>
                          Quot.liftOn a (liftFun R X f)
                            (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                        map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        {
                          toFun := fun a =>
                            Quot.liftOn a (liftFun R X f)
                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                        x *
                      OneHom.toFun
                        {
                          toFun := fun a =>
                            Quot.liftOn a (liftFun R X f)
                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                        y) })
        (Quot.mk (Rel R X) a✝)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ ∀ (r : R),
    OneHom.toFun
        (↑↑{
              toMonoidHom :=
                {
                  toOneHom :=
                    {
                      toFun := fun a =>
                        Quot.liftOn a (liftFun R X f)
                          (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                      map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (x y : FreeAlgebra R X),
                        OneHom.toFun
                            {
                              toFun := fun a =>
                                Quot.liftOn a (liftFun R X f)
                                  (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                              map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                            (x * y) =
                          OneHom.toFun
                              {
                                toFun := fun a =>
                                  Quot.liftOn a (liftFun R X f)
                                    (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                              x *
                            OneHom.toFun
                              {
                                toFun := fun a =>
                                  Quot.liftOn a (liftFun R X f)
                                    (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                              y) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            {
                              toFun := fun a =>
                                Quot.liftOn a (liftFun R X f)
                                  (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                              map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : FreeAlgebra R X),
                                OneHom.toFun
                                    {
                                      toFun := fun a =>
                                        Quot.liftOn a (liftFun R X f)
                                          (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                      map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                    (x * y) =
                                  OneHom.toFun
                                      {
                                        toFun := fun a =>
                                          Quot.liftOn a (liftFun R X f)
                                            (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                        map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                      x *
                                    OneHom.toFun
                                      {
                                        toFun := fun a =>
                                          Quot.liftOn a (liftFun R X f)
                                            (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                        map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                      y) })
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : FreeAlgebra R X),
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              {
                                toFun := fun a =>
                                  Quot.liftOn a (liftFun R X f)
                                    (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : FreeAlgebra R X),
                                  OneHom.toFun
                                      {
                                        toFun := fun a =>
                                          Quot.liftOn a (liftFun R X f)
                                            (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                        map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                      (x * y) =
                                    OneHom.toFun
                                        {
                                          toFun := fun a =>
                                            Quot.liftOn a (liftFun R X f)
                                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                        x *
                                      OneHom.toFun
                                        {
                                          toFun := fun a =>
                                            Quot.liftOn a (liftFun R X f)
                                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                        y) })
                        (x + y) =
                      OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun a =>
                                    Quot.liftOn a (liftFun R X f)
                                      (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                  map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : FreeAlgebra R X),
                                    OneHom.toFun
                                        {
                                          toFun := fun a =>
                                            Quot.liftOn a (liftFun R X f)
                                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun a =>
                                              Quot.liftOn a (liftFun R X f)
                                                (_ :
                                                  ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                            map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun a =>
                                              Quot.liftOn a (liftFun R X f)
                                                (_ :
                                                  ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                            map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                          y) })
                          x +
                        OneHom.toFun
                          (↑{
                              toOneHom :=
                                {
                                  toFun := fun a =>
                                    Quot.liftOn a (liftFun R X f)
                                      (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                  map_one' := (_ : ↑(algebraMap R A) 1 = 1) },
                              map_mul' :=
                                (_ :
                                  ∀ (x y : FreeAlgebra R X),
                                    OneHom.toFun
                                        {
                                          toFun := fun a =>
                                            Quot.liftOn a (liftFun R X f)
                                              (_ : ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                          map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                        (x * y) =
                                      OneHom.toFun
                                          {
                                            toFun := fun a =>
                                              Quot.liftOn a (liftFun R X f)
                                                (_ :
                                                  ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                            map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                          x *
                                        OneHom.toFun
                                          {
                                            toFun := fun a =>
                                              Quot.liftOn a (liftFun R X f)
                                                (_ :
                                                  ∀ (a b : Pre R X), Rel R X a b → liftFun R X f a = liftFun R X f b),
                                            map_one' := (_ : ↑(algebraMap R A) 1 = 1) }
                                          y) })
                          y) })
        (↑(algebraMap R (FreeAlgebra R X)) r) =
      ↑(algebraMap R A) r
[PROOFSTEP]
tauto
  -- Porting note: removed #align declaration since it is a private lemma
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ (fun F => ↑F ∘ ι R) (FreeAlgebra.liftAux R f) = f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ (fun F => ↑F ∘ ι R) (FreeAlgebra.liftAux R f) x✝ = f x✝
[PROOFSTEP]
simp only [Function.comp_apply, ι_def]
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ ↑(FreeAlgebra.liftAux R f) (Quot.mk (Rel R X) (Pre.of x✝)) = f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
⊢ FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F) = F
[PROOFSTEP]
ext t
[GOAL]
case H
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) t = ↑F t
[PROOFSTEP]
rcases t with ⟨x⟩
[GOAL]
case H.mk
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : Pre R X
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) x) = ↑F (Quot.mk (Rel R X) x)
[PROOFSTEP]
induction x
[GOAL]
case H.mk.of
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝ : X
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.of a✝)) = ↑F (Quot.mk (Rel R X) (Pre.of a✝))
case H.mk.of_scalar
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝ : R
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.of_scalar a✝)) =
    ↑F (Quot.mk (Rel R X) (Pre.of_scalar a✝))
case H.mk.add
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝¹ a✝ : Pre R X
a_ih✝¹ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝¹) = ↑F (Quot.mk (Rel R X) a✝¹)
a_ih✝ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝) = ↑F (Quot.mk (Rel R X) a✝)
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.add a✝¹ a✝)) =
    ↑F (Quot.mk (Rel R X) (Pre.add a✝¹ a✝))
case H.mk.mul
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝¹ a✝ : Pre R X
a_ih✝¹ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝¹) = ↑F (Quot.mk (Rel R X) a✝¹)
a_ih✝ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝) = ↑F (Quot.mk (Rel R X) a✝)
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.mul a✝¹ a✝)) =
    ↑F (Quot.mk (Rel R X) (Pre.mul a✝¹ a✝))
[PROOFSTEP]
case of =>
  change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _
  simp only [Function.comp_apply, ι_def]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝ : X
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.of a✝)) = ↑F (Quot.mk (Rel R X) (Pre.of a✝))
[PROOFSTEP]
case of =>
  change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _
  simp only [Function.comp_apply, ι_def]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝ : X
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.of a✝)) = ↑F (Quot.mk (Rel R X) (Pre.of a✝))
[PROOFSTEP]
change ((F : FreeAlgebra R X → A) ∘ ι R) _ = _
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝ : X
⊢ (↑F ∘ ι R) a✝ = ↑F (Quot.mk (Rel R X) (Pre.of a✝))
[PROOFSTEP]
simp only [Function.comp_apply, ι_def]
[GOAL]
case H.mk.of_scalar
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝ : R
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.of_scalar a✝)) =
    ↑F (Quot.mk (Rel R X) (Pre.of_scalar a✝))
case H.mk.add
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝¹ a✝ : Pre R X
a_ih✝¹ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝¹) = ↑F (Quot.mk (Rel R X) a✝¹)
a_ih✝ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝) = ↑F (Quot.mk (Rel R X) a✝)
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.add a✝¹ a✝)) =
    ↑F (Quot.mk (Rel R X) (Pre.add a✝¹ a✝))
case H.mk.mul
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝¹ a✝ : Pre R X
a_ih✝¹ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝¹) = ↑F (Quot.mk (Rel R X) a✝¹)
a_ih✝ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝) = ↑F (Quot.mk (Rel R X) a✝)
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.mul a✝¹ a✝)) =
    ↑F (Quot.mk (Rel R X) (Pre.mul a✝¹ a✝))
[PROOFSTEP]
case of_scalar x =>
  change algebraMap _ _ x = F (algebraMap _ _ x)
  rw [AlgHom.commutes F _]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : R
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.of_scalar x)) =
    ↑F (Quot.mk (Rel R X) (Pre.of_scalar x))
[PROOFSTEP]
case of_scalar x =>
  change algebraMap _ _ x = F (algebraMap _ _ x)
  rw [AlgHom.commutes F _]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : R
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.of_scalar x)) =
    ↑F (Quot.mk (Rel R X) (Pre.of_scalar x))
[PROOFSTEP]
change algebraMap _ _ x = F (algebraMap _ _ x)
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
x : R
⊢ ↑(algebraMap R A) x = ↑F (↑(algebraMap R (FreeAlgebra R X)) x)
[PROOFSTEP]
rw [AlgHom.commutes F _]
[GOAL]
case H.mk.add
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝¹ a✝ : Pre R X
a_ih✝¹ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝¹) = ↑F (Quot.mk (Rel R X) a✝¹)
a_ih✝ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝) = ↑F (Quot.mk (Rel R X) a✝)
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.add a✝¹ a✝)) =
    ↑F (Quot.mk (Rel R X) (Pre.add a✝¹ a✝))
case H.mk.mul
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝¹ a✝ : Pre R X
a_ih✝¹ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝¹) = ↑F (Quot.mk (Rel R X) a✝¹)
a_ih✝ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝) = ↑F (Quot.mk (Rel R X) a✝)
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.mul a✝¹ a✝)) =
    ↑F (Quot.mk (Rel R X) (Pre.mul a✝¹ a✝))
[PROOFSTEP]
case add a b ha hb =>
  -- Porting note: it is necessary to declare fa and fb explicitly otherwise Lean refuses
          -- to consider `Quot.mk (Rel R X) ·` as element of FreeAlgebra R X
  let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
  let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
  change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)
  rw [AlgHom.map_add, AlgHom.map_add, ha, hb]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = ↑F (Quot.mk (Rel R X) a)
hb : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = ↑F (Quot.mk (Rel R X) b)
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.add a b)) =
    ↑F (Quot.mk (Rel R X) (Pre.add a b))
[PROOFSTEP]
case add a b ha hb =>
  -- Porting note: it is necessary to declare fa and fb explicitly otherwise Lean refuses
          -- to consider `Quot.mk (Rel R X) ·` as element of FreeAlgebra R X
  let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
  let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
  change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)
  rw [AlgHom.map_add, AlgHom.map_add, ha, hb]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = ↑F (Quot.mk (Rel R X) a)
hb : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = ↑F (Quot.mk (Rel R X) b)
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.add a b)) =
    ↑F (Quot.mk (Rel R X) (Pre.add a b))
[PROOFSTEP]
let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = ↑F (Quot.mk (Rel R X) a)
hb : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = ↑F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.add a b)) =
    ↑F (Quot.mk (Rel R X) (Pre.add a b))
[PROOFSTEP]
let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = ↑F (Quot.mk (Rel R X) a)
hb : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = ↑F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.add a b)) =
    ↑F (Quot.mk (Rel R X) (Pre.add a b))
[PROOFSTEP]
change liftAux R (F ∘ ι R) (fa + fb) = F (fa + fb)
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = ↑F (Quot.mk (Rel R X) a)
hb : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = ↑F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
⊢ ↑(FreeAlgebra.liftAux R (↑F ∘ ι R)) (fa + fb) = ↑F (fa + fb)
[PROOFSTEP]
rw [AlgHom.map_add, AlgHom.map_add, ha, hb]
[GOAL]
case H.mk.mul
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a✝¹ a✝ : Pre R X
a_ih✝¹ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝¹) = ↑F (Quot.mk (Rel R X) a✝¹)
a_ih✝ : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a✝) = ↑F (Quot.mk (Rel R X) a✝)
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.mul a✝¹ a✝)) =
    ↑F (Quot.mk (Rel R X) (Pre.mul a✝¹ a✝))
[PROOFSTEP]
case mul a b ha hb =>
  let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
  let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
  change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)
  rw [AlgHom.map_mul, AlgHom.map_mul, ha, hb]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = ↑F (Quot.mk (Rel R X) a)
hb : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = ↑F (Quot.mk (Rel R X) b)
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.mul a b)) =
    ↑F (Quot.mk (Rel R X) (Pre.mul a b))
[PROOFSTEP]
case mul a b ha hb =>
  let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
  let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
  change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)
  rw [AlgHom.map_mul, AlgHom.map_mul, ha, hb]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = ↑F (Quot.mk (Rel R X) a)
hb : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = ↑F (Quot.mk (Rel R X) b)
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.mul a b)) =
    ↑F (Quot.mk (Rel R X) (Pre.mul a b))
[PROOFSTEP]
let fa : FreeAlgebra R X := Quot.mk (Rel R X) a
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = ↑F (Quot.mk (Rel R X) a)
hb : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = ↑F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.mul a b)) =
    ↑F (Quot.mk (Rel R X) (Pre.mul a b))
[PROOFSTEP]
let fb : FreeAlgebra R X := Quot.mk (Rel R X) b
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = ↑F (Quot.mk (Rel R X) a)
hb : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = ↑F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
⊢ ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) (Pre.mul a b)) =
    ↑F (Quot.mk (Rel R X) (Pre.mul a b))
[PROOFSTEP]
change liftAux R (F ∘ ι R) (fa * fb) = F (fa * fb)
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
t : FreeAlgebra R X
a b : Pre R X
ha : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) a) = ↑F (Quot.mk (Rel R X) a)
hb : ↑(FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F)) (Quot.mk (Rel R X) b) = ↑F (Quot.mk (Rel R X) b)
fa : FreeAlgebra R X := Quot.mk (Rel R X) a
fb : FreeAlgebra R X := Quot.mk (Rel R X) b
⊢ ↑(FreeAlgebra.liftAux R (↑F ∘ ι R)) (fa * fb) = ↑F (fa * fb)
[PROOFSTEP]
rw [AlgHom.map_mul, AlgHom.map_mul, ha, hb]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ FreeAlgebra.liftAux R f = ↑(lift R) f
[PROOFSTEP]
rw [lift]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ FreeAlgebra.liftAux R f =
    ↑{ toFun := FreeAlgebra.liftAux R, invFun := fun F => ↑F ∘ ι R,
          left_inv := (_ : ∀ (f : X → A), (fun F => ↑F ∘ ι R) (FreeAlgebra.liftAux R f) = f),
          right_inv := (_ : ∀ (F : FreeAlgebra R X →ₐ[R] A), FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F) = F) }
      f
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
⊢ ↑(lift R).symm F = ↑F ∘ ι R
[PROOFSTEP]
rw [lift]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
F : FreeAlgebra R X →ₐ[R] A
⊢ ↑{ toFun := FreeAlgebra.liftAux R, invFun := fun F => ↑F ∘ ι R,
            left_inv := (_ : ∀ (f : X → A), (fun F => ↑F ∘ ι R) (FreeAlgebra.liftAux R f) = f),
            right_inv := (_ : ∀ (F : FreeAlgebra R X →ₐ[R] A), FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F) = F) }.symm
      F =
    ↑F ∘ ι R
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ ↑(↑(lift R) f) ∘ ι R = f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ (↑(↑(lift R) f) ∘ ι R) x✝ = f x✝
[PROOFSTEP]
rw [Function.comp_apply, ι_def, lift]
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x✝ : X
⊢ ↑(↑{ toFun := FreeAlgebra.liftAux R, invFun := fun F => ↑F ∘ ι R,
              left_inv := (_ : ∀ (f : X → A), (fun F => ↑F ∘ ι R) (FreeAlgebra.liftAux R f) = f),
              right_inv := (_ : ∀ (F : FreeAlgebra R X →ₐ[R] A), FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F) = F) }
          f)
      (Quot.mk (Rel R X) (Pre.of x✝)) =
    f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x : X
⊢ ↑(↑(lift R) f) (ι R x) = f x
[PROOFSTEP]
rw [ι_def, lift]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
x : X
⊢ ↑(↑{ toFun := FreeAlgebra.liftAux R, invFun := fun F => ↑F ∘ ι R,
              left_inv := (_ : ∀ (f : X → A), (fun F => ↑F ∘ ι R) (FreeAlgebra.liftAux R f) = f),
              right_inv := (_ : ∀ (F : FreeAlgebra R X →ₐ[R] A), FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F) = F) }
          f)
      (Quot.mk (Rel R X) (Pre.of x)) =
    f x
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
g : FreeAlgebra R X →ₐ[R] A
⊢ ↑g ∘ ι R = f ↔ g = ↑(lift R) f
[PROOFSTEP]
rw [← (lift R).symm_apply_eq, lift]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
g : FreeAlgebra R X →ₐ[R] A
⊢ ↑g ∘ ι R = f ↔
    ↑{ toFun := FreeAlgebra.liftAux R, invFun := fun F => ↑F ∘ ι R,
              left_inv := (_ : ∀ (f : X → A), (fun F => ↑F ∘ ι R) (FreeAlgebra.liftAux R f) = f),
              right_inv :=
                (_ : ∀ (F : FreeAlgebra R X →ₐ[R] A), FreeAlgebra.liftAux R ((fun F => ↑F ∘ ι R) F) = F) }.symm
        g =
      f
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : FreeAlgebra R X →ₐ[R] A
⊢ ↑(lift R) (↑g ∘ ι R) = g
[PROOFSTEP]
rw [← lift_symm_apply]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : FreeAlgebra R X →ₐ[R] A
⊢ ↑(lift R) (↑(lift R).symm g) = g
[PROOFSTEP]
exact (lift R).apply_symm_apply g
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : FreeAlgebra R X →ₐ[R] A
w : ↑f ∘ ι R = ↑g ∘ ι R
⊢ f = g
[PROOFSTEP]
rw [← lift_symm_apply, ← lift_symm_apply] at w
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : FreeAlgebra R X →ₐ[R] A
w : ↑(lift R).symm f = ↑(lift R).symm g
⊢ f = g
[PROOFSTEP]
exact (lift R).symm.injective w
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ AlgHom.comp (↑(lift R) fun x => ↑(MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))
      (↑(MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (↑FreeMonoid.lift (ι R))) =
    AlgHom.id R (MonoidAlgebra R (FreeMonoid X))
[PROOFSTEP]
apply MonoidAlgebra.algHom_ext
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (x : FreeMonoid X),
    ↑(AlgHom.comp (↑(lift R) fun x => ↑(MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))
            (↑(MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (↑FreeMonoid.lift (ι R))))
        (MonoidAlgebra.single x 1) =
      ↑(AlgHom.id R (MonoidAlgebra R (FreeMonoid X))) (MonoidAlgebra.single x 1)
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : FreeMonoid X
⊢ ↑(AlgHom.comp (↑(lift R) fun x => ↑(MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))
          (↑(MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (↑FreeMonoid.lift (ι R))))
      (MonoidAlgebra.single x 1) =
    ↑(AlgHom.id R (MonoidAlgebra R (FreeMonoid X))) (MonoidAlgebra.single x 1)
[PROOFSTEP]
refine FreeMonoid.recOn x ?_ ?_
[GOAL]
case h.refine_1
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : FreeMonoid X
⊢ ↑(AlgHom.comp (↑(lift R) fun x => ↑(MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))
          (↑(MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (↑FreeMonoid.lift (ι R))))
      (MonoidAlgebra.single 1 1) =
    ↑(AlgHom.id R (MonoidAlgebra R (FreeMonoid X))) (MonoidAlgebra.single 1 1)
[PROOFSTEP]
simp
[GOAL]
case h.refine_1
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : FreeMonoid X
⊢ 1 = MonoidAlgebra.single 1 1
[PROOFSTEP]
rfl
[GOAL]
case h.refine_2
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : FreeMonoid X
⊢ ∀ (x : X) (xs : FreeMonoid X),
    ↑(AlgHom.comp (↑(lift R) fun x => ↑(MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))
              (↑(MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (↑FreeMonoid.lift (ι R))))
          (MonoidAlgebra.single xs 1) =
        ↑(AlgHom.id R (MonoidAlgebra R (FreeMonoid X))) (MonoidAlgebra.single xs 1) →
      ↑(AlgHom.comp (↑(lift R) fun x => ↑(MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))
              (↑(MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (↑FreeMonoid.lift (ι R))))
          (MonoidAlgebra.single (FreeMonoid.of x * xs) 1) =
        ↑(AlgHom.id R (MonoidAlgebra R (FreeMonoid X))) (MonoidAlgebra.single (FreeMonoid.of x * xs) 1)
[PROOFSTEP]
intro x y ih
[GOAL]
case h.refine_2
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : FreeMonoid X
x : X
y : FreeMonoid X
ih :
  ↑(AlgHom.comp (↑(lift R) fun x => ↑(MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))
          (↑(MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (↑FreeMonoid.lift (ι R))))
      (MonoidAlgebra.single y 1) =
    ↑(AlgHom.id R (MonoidAlgebra R (FreeMonoid X))) (MonoidAlgebra.single y 1)
⊢ ↑(AlgHom.comp (↑(lift R) fun x => ↑(MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))
          (↑(MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (↑FreeMonoid.lift (ι R))))
      (MonoidAlgebra.single (FreeMonoid.of x * y) 1) =
    ↑(AlgHom.id R (MonoidAlgebra R (FreeMonoid X))) (MonoidAlgebra.single (FreeMonoid.of x * y) 1)
[PROOFSTEP]
simp at ih
[GOAL]
case h.refine_2
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : FreeMonoid X
x : X
y : FreeMonoid X
ih :
  ↑(↑(lift R) fun x => MonoidAlgebra.single (FreeMonoid.of x) 1) (↑(↑FreeMonoid.lift (ι R)) y) =
    MonoidAlgebra.single y 1
⊢ ↑(AlgHom.comp (↑(lift R) fun x => ↑(MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))
          (↑(MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (↑FreeMonoid.lift (ι R))))
      (MonoidAlgebra.single (FreeMonoid.of x * y) 1) =
    ↑(AlgHom.id R (MonoidAlgebra R (FreeMonoid X))) (MonoidAlgebra.single (FreeMonoid.of x * y) 1)
[PROOFSTEP]
simp [ih]
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ AlgHom.comp (↑(MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (↑FreeMonoid.lift (ι R)))
      (↑(lift R) fun x => ↑(MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x)) =
    AlgHom.id R (FreeAlgebra R X)
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : X
⊢ (↑(AlgHom.comp (↑(MonoidAlgebra.lift R (FreeMonoid X) (FreeAlgebra R X)) (↑FreeMonoid.lift (ι R)))
            (↑(lift R) fun x => ↑(MonoidAlgebra.of R (FreeMonoid X)) (FreeMonoid.of x))) ∘
        ι R)
      x✝ =
    (↑(AlgHom.id R (FreeAlgebra R X)) ∘ ι R) x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : R
⊢ ↑algebraMapInv (↑(algebraMap R (FreeAlgebra R X)) x) = x
[PROOFSTEP]
simp [algebraMapInv]
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x y : X
hoxy : ι R x = ι R y
⊢ ¬x = y → False
[PROOFSTEP]
classical exact fun hxy : x ≠ y ↦
  let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
  have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
  have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
  have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
  one_ne_zero <| hfy1.symm.trans hfy0
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x y : X
hoxy : ι R x = ι R y
⊢ ¬x = y → False
[PROOFSTEP]
exact fun hxy : x ≠ y ↦
  let f : FreeAlgebra R X →ₐ[R] R := lift R fun z ↦ if x = z then (1 : R) else 0
  have hfx1 : f (ι R x) = 1 := (lift_ι_apply _ _).trans <| if_pos rfl
  have hfy1 : f (ι R y) = 1 := hoxy ▸ hfx1
  have hfy0 : f (ι R y) = 0 := (lift_ι_apply _ _).trans <| if_neg hxy
  one_ne_zero <| hfy1.symm.trans hfy0
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
⊢ False
[PROOFSTEP]
let f0 : FreeAlgebra R X →ₐ[R] R := lift R 0
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
⊢ False
[PROOFSTEP]
let f1 : FreeAlgebra R X →ₐ[R] R := lift R 1
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
⊢ False
[PROOFSTEP]
have hf0 : f0 (ι R x) = 0 := lift_ι_apply _ _
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : ↑f0 (ι R x) = 0
⊢ False
[PROOFSTEP]
have hf1 : f1 (ι R x) = 1 := lift_ι_apply _ _
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : ↑f0 (ι R x) = 0
hf1 : ↑f1 (ι R x) = 1
⊢ False
[PROOFSTEP]
rw [h, f0.commutes, Algebra.id.map_eq_self] at hf0
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : r = 0
hf1 : ↑f1 (ι R x) = 1
⊢ False
[PROOFSTEP]
rw [h, f1.commutes, Algebra.id.map_eq_self] at hf1
[GOAL]
R : Type u_1
inst✝³ : CommSemiring R
X : Type u_2
A : Type u_3
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = ↑(algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := ↑(lift R) 1
hf0 : r = 0
hf1 : r = 1
⊢ False
[PROOFSTEP]
exact zero_ne_one (hf0.symm.trans hf1)
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
⊢ C a
[PROOFSTEP]
let s : Subalgebra R (FreeAlgebra R X) :=
  { carrier := C
    mul_mem' := h_mul _ _
    add_mem' := h_add _ _
    algebraMap_mem' := h_grade0 }
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
⊢ C a
[PROOFSTEP]
let of : X → s := Subtype.coind (ι R) h_grade1
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
⊢ C a
[PROOFSTEP]
have of_id : AlgHom.id R (FreeAlgebra R X) = s.val.comp (lift R of) :=
  by
  ext
  simp [Subtype.coind]
    -- finding a proof is finding an element of the subalgebra
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
⊢ AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
x✝ : X
⊢ (↑(AlgHom.id R (FreeAlgebra R X)) ∘ ι R) x✝ = (↑(AlgHom.comp (Subalgebra.val s) (↑(lift R) of)) ∘ ι R) x✝
[PROOFSTEP]
simp [Subtype.coind]
  -- finding a proof is finding an element of the subalgebra
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
⊢ C a
[PROOFSTEP]
suffices : a = lift R of a
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
this : a = ↑(↑(↑(lift R) of) a)
⊢ C a
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
this : a = ↑(↑(↑(lift R) of) a)
⊢ C ↑(↑(↑(lift R) of) a)
[PROOFSTEP]
exact Subtype.prop (lift R of a)
[GOAL]
case this
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : AlgHom.id R (FreeAlgebra R X) = AlgHom.comp (Subalgebra.val s) (↑(lift R) of)
⊢ a = ↑(↑(↑(lift R) of) a)
[PROOFSTEP]
simp [AlgHom.ext_iff] at of_id
[GOAL]
case this
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
C : FreeAlgebra R X → Prop
h_grade0 : ∀ (r : R), C (↑(algebraMap R (FreeAlgebra R X)) r)
h_grade1 : ∀ (x : X), C (ι R x)
h_mul : ∀ (a b : FreeAlgebra R X), C a → C b → C (a * b)
h_add : ∀ (a b : FreeAlgebra R X), C a → C b → C (a + b)
a : FreeAlgebra R X
s : Subalgebra R (FreeAlgebra R X) :=
  {
    toSubsemiring :=
      {
        toSubmonoid :=
          { toSubsemigroup := { carrier := C, mul_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a * b)) },
            one_mem' := (_ : 1 ∈ C) },
        add_mem' := (_ : ∀ {a b : FreeAlgebra R X}, C a → C b → C (a + b)), zero_mem' := (_ : 0 ∈ C) },
    algebraMap_mem' := h_grade0 }
of : X → { x // x ∈ s } := Subtype.coind (ι R) h_grade1
of_id : ∀ (x : FreeAlgebra R X), x = ↑(↑(↑(lift R) (Subtype.coind (ι R) h_grade1)) x)
⊢ a = ↑(↑(↑(lift R) of) a)
[PROOFSTEP]
exact of_id a