[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r₁ r₂ : R
⊢ OneHom.toFun { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) } (r₁ * r₂) =
    OneHom.toFun { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) } r₁ *
      OneHom.toFun { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) } r₂
[PROOFSTEP]
simp only [h₁, mul_smul]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r : R
x : (fun x => A) r
⊢ ↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) },
                map_mul' := (_ : ∀ (r₁ r₂ : R), (r₁ * r₂) • 1 = r₁ • 1 * r₂ • 1) },
            map_zero' := (_ : 0 • 1 = 0), map_add' := (_ : ∀ (r₁ r₂ : R), (r₁ + r₂) • 1 = r₁ • 1 + r₂ • 1) }
        r *
      x =
    x *
      ↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) },
                map_mul' := (_ : ∀ (r₁ r₂ : R), (r₁ * r₂) • 1 = r₁ • 1 * r₂ • 1) },
            map_zero' := (_ : 0 • 1 = 0), map_add' := (_ : ∀ (r₁ r₂ : R), (r₁ + r₂) • 1 = r₁ • 1 + r₂ • 1) }
        r
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r : R
x : (fun x => A) r
⊢ r • x =
    ↑{
            toMonoidHom :=
              { toOneHom := { toFun := fun r => r • 1, map_one' := (_ : 1 • 1 = 1) },
                map_mul' := (_ : ∀ (r₁ r₂ : R), (r₁ * r₂) • 1 = r₁ • 1 * r₂ • 1) },
            map_zero' := (_ : 0 • 1 = 0), map_add' := (_ : ∀ (r₁ r₂ : R), (r₁ + r₂) • 1 = r₁ • 1 + r₂ • 1) }
        r *
      x
[PROOFSTEP]
simp [h₁]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • 1 * x = r • x
[PROOFSTEP]
rw [h₁, one_mul]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ x * r • 1 = r • x
[PROOFSTEP]
rw [h₂, mul_one]
[GOAL]
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : ∀ (r : R), ↑(algebraMap R A) r = ↑(algebraMap R A) r
⊢ P = Q
[PROOFSTEP]
replace h : P.toRingHom = Q.toRingHom := FunLike.ext _ _ h
[GOAL]
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : toRingHom = toRingHom
⊢ P = Q
[PROOFSTEP]
have h' :
  (haveI := P;
      (· • ·) :
      R → A → A) =
    (haveI := Q;
      (· • ·) :
      R → A → A) :=
  by
  funext r a
  rw [P.smul_def', Q.smul_def', h]
[GOAL]
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : toRingHom = toRingHom
⊢ (fun x x_1 => x • x_1) = fun x x_1 => x • x_1
[PROOFSTEP]
funext r a
[GOAL]
case h.h
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : toRingHom = toRingHom
r : R
a : A
⊢ r • a = r • a
[PROOFSTEP]
rw [P.smul_def', Q.smul_def', h]
[GOAL]
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : toRingHom = toRingHom
h' : (fun x x_1 => x • x_1) = fun x x_1 => x • x_1
⊢ P = Q
[PROOFSTEP]
rcases P with @⟨⟨P⟩⟩
[GOAL]
case mk.mk
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
Q : Algebra R A
toRingHom✝ : R →+* A
commutes'✝ : ∀ (r : R) (x : (fun x => A) r), ↑toRingHom✝ r * x = x * ↑toRingHom✝ r
P : R → A → A
smul_def'✝ : ∀ (r : R) (x : (fun x => A) r), r • x = ↑toRingHom✝ r * x
h : toRingHom = toRingHom
h' : (fun x x_1 => x • x_1) = fun x x_1 => x • x_1
⊢ mk toRingHom✝ commutes'✝ smul_def'✝ = Q
[PROOFSTEP]
rcases Q with @⟨⟨Q⟩⟩
[GOAL]
case mk.mk.mk.mk
R✝ : Type u
S : Type v
A✝ : Type w
B : Type u_1
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
toRingHom✝¹ : R →+* A
commutes'✝¹ : ∀ (r : R) (x : (fun x => A) r), ↑toRingHom✝¹ r * x = x * ↑toRingHom✝¹ r
P : R → A → A
smul_def'✝¹ : ∀ (r : R) (x : (fun x => A) r), r • x = ↑toRingHom✝¹ r * x
toRingHom✝ : R →+* A
commutes'✝ : ∀ (r : R) (x : (fun x => A) r), ↑toRingHom✝ r * x = x * ↑toRingHom✝ r
Q : R → A → A
smul_def'✝ : ∀ (r : R) (x : (fun x => A) r), r • x = ↑toRingHom✝ r * x
h : toRingHom = toRingHom
h' : (fun x x_1 => x • x_1) = fun x x_1 => x • x_1
⊢ mk toRingHom✝¹ commutes'✝¹ smul_def'✝¹ = mk toRingHom✝ commutes'✝ smul_def'✝
[PROOFSTEP]
congr
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A
⊢ 1 • x✝ = x✝
[PROOFSTEP]
simp [smul_def']
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ∀ (x y : R) (b : A), (x * y) • b = x • y • b
[PROOFSTEP]
simp [smul_def', mul_assoc]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ∀ (a : R), a • 0 = 0
[PROOFSTEP]
simp [smul_def']
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ∀ (a : R) (x y : A), a • (x + y) = a • x + a • y
[PROOFSTEP]
simp [smul_def', mul_add]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ∀ (r s : R) (x : A), (r + s) • x = r • x + s • x
[PROOFSTEP]
simp [smul_def', add_mul]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
⊢ ∀ (x : A), 0 • x = 0
[PROOFSTEP]
simp [smul_def']
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
r : R
y : A
⊢ x * (↑(algebraMap R A) r * y) = ↑(algebraMap R A) r * (x * y)
[PROOFSTEP]
rw [← mul_assoc, ← commutes, mul_assoc]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : A
r : R
y : A
⊢ x * ↑(algebraMap R A) r * y = x * y * ↑(algebraMap R A) r
[PROOFSTEP]
rw [mul_assoc, commutes, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x : R
y z : A
⊢ (x • y) • z = x • y • z
[PROOFSTEP]
rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
s : R
x y : A
⊢ x * s • y = s • (x * y)
[PROOFSTEP]
rw [smul_def, smul_def, left_comm]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
α : Type u_2
inst✝² : Monoid α
inst✝¹ : MulDistribMulAction α A
inst✝ : SMulCommClass α R A
a : α
r : R
⊢ a • ↑(algebraMap R A) r = ↑(algebraMap R A) r
[PROOFSTEP]
rw [algebraMap_eq_smul_one, smul_comm a r (1 : A), smul_one]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
src✝ : R →+* A := algebraMap R A
x y : R
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
      (x • y) =
    ↑(RingHom.id R) x •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        y
[PROOFSTEP]
simp [Algebra.smul_def]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * (x - ↑(algebraMap R A) r) = (x - ↑(algebraMap R A) r) * x
[PROOFSTEP]
rw [mul_sub, ← commutes, sub_mul]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
⊢ x * (x - ↑(algebraMap R A) r) ^ n = (x - ↑(algebraMap R A) r) ^ n * x
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
⊢ x * (x - ↑(algebraMap R A) r) ^ Nat.zero = (x - ↑(algebraMap R A) r) ^ Nat.zero * x
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
x : A
r : R
n : ℕ
ih : x * (x - ↑(algebraMap R A) r) ^ n = (x - ↑(algebraMap R A) r) ^ n * x
⊢ x * (x - ↑(algebraMap R A) r) ^ Nat.succ n = (x - ↑(algebraMap R A) r) ^ Nat.succ n * x
[PROOFSTEP]
rw [pow_succ, ← mul_assoc, mul_sub_algebraMap_commutes, mul_assoc, ih, ← mul_assoc]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝¹ : AddCommGroup A := Module.addCommMonoidToAddCommGroup R
src✝ : Semiring A := inferInstance
z : ℕ
⊢ IntCast.intCast ↑z = ↑z
[PROOFSTEP]
simp only [Int.cast_ofNat, map_natCast]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommRing R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝¹ : AddCommGroup A := Module.addCommMonoidToAddCommGroup R
src✝ : Semiring A := inferInstance
z : ℕ
⊢ IntCast.intCast (Int.negSucc z) = -↑(z + 1)
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h)⁻¹ (x • m') = m'
[PROOFSTEP]
apply_fun ⇑h.unit.val using ((Module.End_isUnit_iff _).mp h).injective
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h) (↑↑(IsUnit.unit h)⁻¹ (x • m')) = ↑↑(IsUnit.unit h) m'
[PROOFSTEP]
erw [End_isUnit_apply_inv_apply_of_isUnit]
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ x • m' = ↑↑(IsUnit.unit h) m'
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ m' = ↑↑(IsUnit.unit h)⁻¹ (x • m')
[PROOFSTEP]
apply_fun (↑h.unit : M → M) using ((Module.End_isUnit_iff _).mp h).injective
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h) m' = ↑↑(IsUnit.unit h) (↑↑(IsUnit.unit h)⁻¹ (x • m'))
[PROOFSTEP]
erw [End_isUnit_apply_inv_apply_of_isUnit]
[GOAL]
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit (↑(algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑↑(IsUnit.unit h) m' = x • m'
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ ↑f (↑(algebraMap R A) r * a) = ↑(algebraMap R B) r * ↑f a
[PROOFSTEP]
rw [← Algebra.smul_def, ← Algebra.smul_def, map_smul]
[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₗ[R] B
a : A
r : R
⊢ ↑f (a * ↑(algebraMap R A) r) = ↑f a * ↑(algebraMap R B) r
[PROOFSTEP]
rw [← Algebra.commutes, ← Algebra.commutes, map_algebraMap_mul]
[GOAL]
R : Type u_1
inst✝ : Semiring R
P Q : Algebra ℕ R
⊢ P = Q
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
P Q : Algebra ℕ R
r✝ : ℕ
⊢ ↑(algebraMap ℕ R) r✝ = ↑(algebraMap ℕ R) r✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Nontrivial A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
⊢ Function.Injective ↑(algebraMap R A)
[PROOFSTEP]
have := @smul_left_injective R A CommRing.toRing Ring.toAddCommGroup Algebra.toModule ‹_› 1 one_ne_zero
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Nontrivial A
inst✝¹ : Algebra R A
inst✝ : NoZeroSMulDivisors R A
this : Function.Injective fun c => c • 1
⊢ Function.Injective ↑(algebraMap R A)
[PROOFSTEP]
simpa only [algebraMap_eq_smul_one'] using this
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module A N
inst✝¹ : Module R N
inst✝ : IsScalarTower R A N
r : R
m : M
⊢ r • m = ↑(algebraMap R A) r • m
[PROOFSTEP]
rw [← one_smul A m, ← smul_assoc, Algebra.smul_def, mul_one, one_smul]
[GOAL]
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
⊢ NoZeroSMulDivisors R M
[PROOFSTEP]
refine' ⟨fun {r m} h => _⟩
[GOAL]
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : r • m = 0
⊢ r = 0 ∨ m = 0
[PROOFSTEP]
rw [algebra_compatible_smul A r m] at h
[GOAL]
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
⊢ r = 0 ∨ m = 0
[PROOFSTEP]
cases' smul_eq_zero.1 h with H H
[GOAL]
case inl
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
H : ↑(algebraMap R A) r = 0
⊢ r = 0 ∨ m = 0
[PROOFSTEP]
have : Function.Injective (algebraMap R A) := NoZeroSMulDivisors.iff_algebraMap_injective.1 inferInstance
[GOAL]
case inl
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
H : ↑(algebraMap R A) r = 0
this : Function.Injective ↑(algebraMap R A)
⊢ r = 0 ∨ m = 0
[PROOFSTEP]
left
[GOAL]
case inl.h
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
H : ↑(algebraMap R A) r = 0
this : Function.Injective ↑(algebraMap R A)
⊢ r = 0
[PROOFSTEP]
exact (injective_iff_map_eq_zero _).1 this _ H
[GOAL]
case inr
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
H : m = 0
⊢ r = 0 ∨ m = 0
[PROOFSTEP]
right
[GOAL]
case inr.h
R✝ : Type u_1
inst✝²⁰ : CommSemiring R✝
A✝ : Type u_2
inst✝¹⁹ : Semiring A✝
inst✝¹⁸ : Algebra R✝ A✝
M✝ : Type u_3
inst✝¹⁷ : AddCommMonoid M✝
inst✝¹⁶ : Module A✝ M✝
inst✝¹⁵ : Module R✝ M✝
inst✝¹⁴ : IsScalarTower R✝ A✝ M✝
N : Type u_4
inst✝¹³ : AddCommMonoid N
inst✝¹² : Module A✝ N
inst✝¹¹ : Module R✝ N
inst✝¹⁰ : IsScalarTower R✝ A✝ N
R : Type u_5
A : Type u_6
M : Type u_7
inst✝⁹ : CommRing R
inst✝⁸ : Ring A
inst✝⁷ : IsDomain A
inst✝⁶ : Algebra R A
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : NoZeroSMulDivisors R A
inst✝ : NoZeroSMulDivisors A M
r : R
m : M
h : ↑(algebraMap R A) r • m = 0
H : m = 0
⊢ m = 0
[PROOFSTEP]
exact H
[GOAL]
R : Type u_1
inst✝¹⁰ : CommSemiring R
A : Type u_2
inst✝⁹ : Semiring A
inst✝⁸ : Algebra R A
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module A N
inst✝¹ : Module R N
inst✝ : IsScalarTower R A N
r : R
a : A
m : M
⊢ r • a • m = a • r • m
[PROOFSTEP]
rw [algebra_compatible_smul A r (a • m), smul_smul, Algebra.commutes, mul_smul, ← algebra_compatible_smul]


[GOAL]
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Semiring B
inst✝² : Algebra R A
inst✝¹ : Algebra R B
F : Type ?u.56163
inst✝ : AlgHomClass F R A B
src✝ : AlgHomClass F R A B := inst✝
f : F
r : R
x : A
⊢ ↑f (r • x) = ↑(RingHom.id R) r • ↑f x
[PROOFSTEP]
simp only [Algebra.smul_def, map_mul, commutes, RingHom.id_apply]
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
f g : A →ₐ[R] B
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
rcases f with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
[GOAL]
case mk.mk.mk.mk
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : A →ₐ[R] B
toFun✝ : A → B
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } x *
        OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } y
map_zero'✝ : OneHom.toFun (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) 0 = 0
map_add'✝ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) y
commutes'✝ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
h :
  (fun f => f.toFun)
      {
        toRingHom :=
          { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
            map_zero' := map_zero'✝, map_add' := map_add'✝ },
        commutes' := commutes'✝ } =
    (fun f => f.toFun) g
⊢ {
      toRingHom :=
        { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
          map_zero' := map_zero'✝, map_add' := map_add'✝ },
      commutes' := commutes'✝ } =
    g
[PROOFSTEP]
rcases g with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
toFun✝¹ : A → B
map_one'✝¹ : toFun✝¹ 1 = 1
map_mul'✝¹ :
  ∀ (x y : A),
    OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } (x * y) =
      OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } x *
        OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } y
map_zero'✝¹ : OneHom.toFun (↑{ toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) y
commutes'✝¹ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
              map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
toFun✝ : A → B
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } x *
        OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } y
map_zero'✝ : OneHom.toFun (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) 0 = 0
map_add'✝ :
  ∀ (x y : A),
    OneHom.toFun (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) y
commutes'✝ :
  ∀ (r : R),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R B) r
h :
  (fun f => f.toFun)
      {
        toRingHom :=
          { toMonoidHom := { toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
            map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
        commutes' := commutes'✝¹ } =
    (fun f => f.toFun)
      {
        toRingHom :=
          { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
            map_zero' := map_zero'✝, map_add' := map_add'✝ },
        commutes' := commutes'✝ }
⊢ {
      toRingHom :=
        { toMonoidHom := { toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
          map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
      commutes' := commutes'✝¹ } =
    {
      toRingHom :=
        { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
          map_zero' := map_zero'✝, map_add' := map_add'✝ },
      commutes' := commutes'✝ }
[PROOFSTEP]
congr
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
f : A →+* B
h : ∀ (c : R) (x : A), ↑f (c • x) = c • ↑f x
c : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := ↑f, map_one' := (_ : OneHom.toFun (↑↑f) 1 = 1) },
                map_mul' :=
                  (_ : ∀ (x y : A), OneHom.toFun (↑↑f) (x * y) = OneHom.toFun (↑↑f) x * OneHom.toFun (↑↑f) y) },
            map_zero' := (_ : OneHom.toFun (↑↑f) 0 = 0),
            map_add' := (_ : ∀ (x y : A), OneHom.toFun (↑↑f) (x + y) = OneHom.toFun (↑↑f) x + OneHom.toFun (↑↑f) y) })
      (↑(algebraMap R A) c) =
    ↑(algebraMap R B) c
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, h, f.map_one]
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
src✝ : A →+* C := RingHom.comp ↑φ₁ ↑φ₂
r : R
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : A), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R A) r) =
    ↑(algebraMap R C) r
[PROOFSTEP]
rw [← φ₁.commutes, ← φ₂.commutes]
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
φ₁ : B →ₐ[R] C
φ₂ : A →ₐ[R] B
src✝ : A →+* C := RingHom.comp ↑φ₁ ↑φ₂
r : R
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : A), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) })
      (↑(algebraMap R A) r) =
    ↑φ₁ (↑φ₂ (↑(algebraMap R A) r))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
f : A →ₗ[R] B
map_one : ↑f 1 = 1
map_mul : ∀ (x y : A), ↑f (x * y) = ↑f x * ↑f y
src✝ : A →+ B := LinearMap.toAddMonoidHom f
c : R
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := { toOneHom := { toFun := ↑f, map_one' := map_one }, map_mul' := map_mul },
            map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : A), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (↑(algebraMap R A) c) =
    ↑(algebraMap R B) c
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, f.map_smul, map_one]
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
map_one : ↑(toLinearMap φ) 1 = 1
map_mul : ∀ (x y : A), ↑(toLinearMap φ) (x * y) = ↑(toLinearMap φ) x * ↑(toLinearMap φ) y
⊢ ofLinearMap (toLinearMap φ) map_one map_mul = φ
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
map_one : ↑(toLinearMap φ) 1 = 1
map_mul : ∀ (x y : A), ↑(toLinearMap φ) (x * y) = ↑(toLinearMap φ) x * ↑(toLinearMap φ) y
x✝ : A
⊢ ↑(ofLinearMap (toLinearMap φ) map_one map_mul) x✝ = ↑φ x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
f : A →ₗ[R] B
map_one : ↑f 1 = 1
map_mul : ∀ (x y : A), ↑f (x * y) = ↑f x * ↑f y
⊢ toLinearMap (ofLinearMap f map_one map_mul) = f
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
A : Type v
B : Type w
C : Type u₁
D : Type v₁
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Semiring C
inst✝⁴ : Semiring D
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra R C
inst✝ : Algebra R D
φ : A →ₐ[R] B
f : A →ₗ[R] B
map_one : ↑f 1 = 1
map_mul : ∀ (x y : A), ↑f (x * y) = ↑f x * ↑f y
x✝ : A
⊢ ↑(toLinearMap (ofLinearMap f map_one map_mul)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
n : ℕ
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := ↑f, map_one' := (_ : OneHom.toFun (↑↑f) 1 = 1) },
                map_mul' :=
                  (_ : ∀ (x y : R), OneHom.toFun (↑↑f) (x * y) = OneHom.toFun (↑↑f) x * OneHom.toFun (↑↑f) y) },
            map_zero' := (_ : OneHom.toFun (↑↑f) 0 = 0),
            map_add' := (_ : ∀ (x y : R), OneHom.toFun (↑↑f) (x + y) = OneHom.toFun (↑↑f) x + OneHom.toFun (↑↑f) y) })
      (↑(algebraMap ℕ R) n) =
    ↑(algebraMap ℕ S) n
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
inst✝³ : Ring R
inst✝² : Ring S
inst✝¹ : Algebra ℤ R
inst✝ : Algebra ℤ S
f : R →+* S
n : ℤ
⊢ OneHom.toFun
      (↑↑{ toMonoidHom := ↑f, map_zero' := (_ : OneHom.toFun (↑↑f) 0 = 0),
            map_add' := (_ : ∀ (x y : R), OneHom.toFun (↑↑f) (x + y) = OneHom.toFun (↑↑f) x + OneHom.toFun (↑↑f) y) })
      (↑(algebraMap ℤ R) n) =
    ↑(algebraMap ℤ S) n
[PROOFSTEP]
simp


[GOAL]
R : Type u
M : Type v
N : Type w
inst✝³ : SMul R M
inst✝² : SMul M N
inst✝¹ : SMul R N
inst✝ : IsScalarTower R M N
x : R
y : M
z : ULift N
⊢ { down := (x • y) • z.down } = { down := x • y • z.down }
[PROOFSTEP]
rw [smul_assoc]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ c • 0 = 0
[PROOFSTEP]
{ext; simp [smul_zero]
}
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ c • 0 = 0
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ (c • 0).down = 0.down
[PROOFSTEP]
simp [smul_zero]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝¹ : AddZeroClass M
inst✝ : DistribSMul R M
c : R
f g : ULift M
⊢ c • (f + g) = c • f + c • g
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
M : Type v
N : Type w
inst✝¹ : AddZeroClass M
inst✝ : DistribSMul R M
c : R
f g : ULift M
⊢ (c • (f + g)).down = (c • f + c • g).down
[PROOFSTEP]
simp [smul_add]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
src✝ : MulAction R (ULift M) := mulAction'
x✝² : R
x✝¹ x✝ : ULift M
⊢ x✝² • (x✝¹ * x✝) = x✝² • x✝¹ * x✝² • x✝
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
src✝ : MulAction R (ULift M) := mulAction'
x✝² : R
x✝¹ x✝ : ULift M
⊢ (x✝² • (x✝¹ * x✝)).down = (x✝² • x✝¹ * x✝² • x✝).down
[PROOFSTEP]
simp [smul_mul']
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
src✝ : MulAction R (ULift M) := mulAction'
x✝ : R
⊢ x✝ • 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
M : Type v
N : Type w
inst✝² : Monoid R
inst✝¹ : Monoid M
inst✝ : MulDistribMulAction R M
src✝ : MulAction R (ULift M) := mulAction'
x✝ : R
⊢ (x✝ • 1).down = 1.down
[PROOFSTEP]
simp [smul_one]


[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
r₁ r₂ : R
⊢ 0 = r₁ • 0 + r₂ • 0 + 0 * 0
[PROOFSTEP]
simp only [smul_zero, add_zero, mul_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : SMulWithZero R A
a₁ a₂ : A
⊢ a₁ * a₂ = 0 • a₂ + 0 • a₁ + a₁ * a₂
[PROOFSTEP]
simp only [zero_smul, zero_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
r : R
a : A
⊢ r • a + 0 • 0 + 0 * a = r • a
[PROOFSTEP]
rw [smul_zero, add_zero, zero_mul, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
r : R
a : A
⊢ 0 • 0 + r • a + a * 0 = r • a
[PROOFSTEP]
rw [smul_zero, zero_add, mul_zero, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
src✝¹ : One (Unitization R A) := instOne
src✝ : Mul (Unitization R A) := instMul
x : Unitization R A
⊢ 1 • x.snd + x.fst • 0 + 0 * x.snd = x.snd
[PROOFSTEP]
rw [one_smul, smul_zero, add_zero, zero_mul, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Monoid R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : DistribMulAction R A
src✝¹ : One (Unitization R A) := instOne
src✝ : Mul (Unitization R A) := instMul
x : Unitization R A
⊢ x.fst • 0 + 1 • x.snd + x.snd * 0 = x.snd
[PROOFSTEP]
rw [smul_zero, zero_add, one_smul, mul_zero, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ x₁.fst • (x₂.snd + x₃.snd) + (x₂.fst + x₃.fst) • x₁.snd + x₁.snd * (x₂.snd + x₃.snd) =
    x₁.fst • x₂.snd + x₂.fst • x₁.snd + x₁.snd * x₂.snd + (x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd)
[PROOFSTEP]
simp only [smul_add, add_smul, mul_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ x₁.fst • x₂.snd + x₁.fst • x₃.snd + (x₂.fst • x₁.snd + x₃.fst • x₁.snd) + (x₁.snd * x₂.snd + x₁.snd * x₃.snd) =
    x₁.fst • x₂.snd + x₂.fst • x₁.snd + x₁.snd * x₂.snd + (x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ x₁.fst • x₂.snd + x₁.fst • x₃.snd + (x₂.fst • x₁.snd + x₃.fst • x₁.snd) + (x₁.snd * x₂.snd + x₁.snd * x₃.snd) =
    x₁.fst • x₂.snd + x₂.fst • x₁.snd + x₁.snd * x₂.snd + (x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ (x₁.fst + x₂.fst) • x₃.snd + x₃.fst • (x₁.snd + x₂.snd) + (x₁.snd + x₂.snd) * x₃.snd =
    x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd + (x₂.fst • x₃.snd + x₃.fst • x₂.snd + x₂.snd * x₃.snd)
[PROOFSTEP]
simp only [add_smul, smul_add, add_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ x₁.fst • x₃.snd + x₂.fst • x₃.snd + (x₃.fst • x₁.snd + x₃.fst • x₂.snd) + (x₁.snd * x₃.snd + x₂.snd * x₃.snd) =
    x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd + (x₂.fst • x₃.snd + x₃.fst • x₂.snd + x₂.snd * x₃.snd)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x₁ x₂ x₃ : Unitization R A
⊢ x₁.fst • x₃.snd + x₂.fst • x₃.snd + (x₃.fst • x₁.snd + x₃.fst • x₂.snd) + (x₁.snd * x₃.snd + x₂.snd * x₃.snd) =
    x₁.fst • x₃.snd + x₃.fst • x₁.snd + x₁.snd * x₃.snd + (x₂.fst • x₃.snd + x₃.fst • x₂.snd + x₂.snd * x₃.snd)
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x : Unitization R A
⊢ 0 • x.snd + x.fst • 0 + 0 * x.snd = 0
[PROOFSTEP]
rw [zero_smul, zero_add, smul_zero, zero_mul, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : NonUnitalNonAssocSemiring A
inst✝ : Module R A
src✝¹ : MulOneClass (Unitization R A) := instMulOneClass
src✝ : AddCommMonoid (Unitization R A) := instAddCommMonoid
x : Unitization R A
⊢ x.fst • 0 + 0 • x.snd + x.snd * 0 = 0
[PROOFSTEP]
rw [smul_zero, zero_add, zero_smul, mul_zero, add_zero]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : MulOneClass (Unitization R A) := instMulOneClass
x y z : Unitization R A
⊢ (x.fst * y.fst) • z.snd + z.fst • (x.fst • y.snd + y.fst • x.snd + x.snd * y.snd) +
      (x.fst • y.snd + y.fst • x.snd + x.snd * y.snd) * z.snd =
    x.fst • (y.fst • z.snd + z.fst • y.snd + y.snd * z.snd) + (y.fst * z.fst) • x.snd +
      x.snd * (y.fst • z.snd + z.fst • y.snd + y.snd * z.snd)
[PROOFSTEP]
simp only [smul_add, mul_add, add_mul, smul_smul, smul_mul_assoc, mul_smul_comm, mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : MulOneClass (Unitization R A) := instMulOneClass
x y z : Unitization R A
⊢ (x.fst * y.fst) • z.snd + ((z.fst * x.fst) • y.snd + (z.fst * y.fst) • x.snd + z.fst • (x.snd * y.snd)) +
      (x.fst • (y.snd * z.snd) + y.fst • (x.snd * z.snd) + x.snd * (y.snd * z.snd)) =
    (x.fst * y.fst) • z.snd + (x.fst * z.fst) • y.snd + x.fst • (y.snd * z.snd) + (y.fst * z.fst) • x.snd +
      (y.fst • (x.snd * z.snd) + z.fst • (x.snd * y.snd) + x.snd * (y.snd * z.snd))
[PROOFSTEP]
rw [mul_comm z.1 x.1]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : MulOneClass (Unitization R A) := instMulOneClass
x y z : Unitization R A
⊢ (x.fst * y.fst) • z.snd + ((x.fst * z.fst) • y.snd + (z.fst * y.fst) • x.snd + z.fst • (x.snd * y.snd)) +
      (x.fst • (y.snd * z.snd) + y.fst • (x.snd * z.snd) + x.snd * (y.snd * z.snd)) =
    (x.fst * y.fst) • z.snd + (x.fst * z.fst) • y.snd + x.fst • (y.snd * z.snd) + (y.fst * z.fst) • x.snd +
      (y.fst • (x.snd * z.snd) + z.fst • (x.snd * y.snd) + x.snd * (y.snd * z.snd))
[PROOFSTEP]
rw [mul_comm z.1 y.1]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : MulOneClass (Unitization R A) := instMulOneClass
x y z : Unitization R A
⊢ (x.fst * y.fst) • z.snd + ((x.fst * z.fst) • y.snd + (y.fst * z.fst) • x.snd + z.fst • (x.snd * y.snd)) +
      (x.fst • (y.snd * z.snd) + y.fst • (x.snd * z.snd) + x.snd * (y.snd * z.snd)) =
    (x.fst * y.fst) • z.snd + (x.fst * z.fst) • y.snd + x.fst • (y.snd * z.snd) + (y.fst * z.fst) • x.snd +
      (y.fst • (x.snd * z.snd) + z.fst • (x.snd * y.snd) + x.snd * (y.snd * z.snd))
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : MulOneClass (Unitization R A) := instMulOneClass
x y z : Unitization R A
⊢ (x.fst * y.fst) • z.snd + ((x.fst * z.fst) • y.snd + (y.fst * z.fst) • x.snd + z.fst • (x.snd * y.snd)) +
      (x.fst • (y.snd * z.snd) + y.fst • (x.snd * z.snd) + x.snd * (y.snd * z.snd)) =
    (x.fst * y.fst) • z.snd + (x.fst * z.fst) • y.snd + x.fst • (y.snd * z.snd) + (y.fst * z.fst) • x.snd +
      (y.fst • (x.snd * z.snd) + z.fst • (x.snd * y.snd) + x.snd * (y.snd * z.snd))
[PROOFSTEP]
abel
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommMonoid R
inst✝³ : NonUnitalCommSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
src✝ : Monoid (Unitization R A) := instMonoid
x₁ x₂ : Unitization R A
⊢ x₁.fst • x₂.snd + x₂.fst • x₁.snd + x₁.snd * x₂.snd = x₂.fst • x₁.snd + x₁.fst • x₂.snd + x₂.snd * x₁.snd
[PROOFSTEP]
rw [add_comm (x₁.1 • x₂.2), mul_comm]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : Star R
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
r : R
⊢ snd (inl (star r)) = snd (star (inl r))
[PROOFSTEP]
simp only [snd_star, star_zero, snd_inl]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : AddMonoid R
inst✝¹ : StarAddMonoid R
inst✝ : Star A
a : A
⊢ fst ↑(star a) = fst (star ↑a)
[PROOFSTEP]
simp only [fst_star, star_zero, fst_inr]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : Module R A
inst✝ : StarModule R A
r : R
x : Unitization R A
⊢ fst (star (r • x)) = fst (star r • star x)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : AddCommMonoid A
inst✝² : StarAddMonoid A
inst✝¹ : Module R A
inst✝ : StarModule R A
r : R
x : Unitization R A
⊢ snd (star (r • x)) = snd (star r • star x)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
src✝ : StarAddMonoid (Unitization R A) := instStarAddMonoid
x y : Unitization R A
⊢ fst (star (x * y)) = fst (star y * star x)
[PROOFSTEP]
simp [-star_mul']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
src✝ : StarAddMonoid (Unitization R A) := instStarAddMonoid
x y : Unitization R A
⊢ snd (star (x * y)) = snd (star y * star x)
[PROOFSTEP]
simp [-star_mul', add_comm (star x.fst • star y.snd)]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
x : (fun x => Unitization R A) s
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s *
      x =
    x *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s
[PROOFSTEP]
induction' x using Unitization.ind with r a
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
r : R
a : A
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s *
      (inl r + ↑a) =
    (inl r + ↑a) *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s
[PROOFSTEP]
show inl (algebraMap S R s) * _ = _ * inl (algebraMap S R s)
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
r : R
a : A
⊢ inl (↑(algebraMap S R) s) * (inl r + ↑a) = (inl r + ↑a) * inl (↑(algebraMap S R) s)
[PROOFSTEP]
rw [mul_add, add_mul, inl_mul_inl, inl_mul_inl, inl_mul_inr, inr_mul_inl, mul_comm]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
x : (fun x => Unitization R A) s
⊢ s • x =
    ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s *
      x
[PROOFSTEP]
induction' x using Unitization.ind with r a
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
r : R
a : A
⊢ s • (inl r + ↑a) =
    ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : S), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        s *
      (inl r + ↑a)
[PROOFSTEP]
show _ = inl (algebraMap S R s) * _
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝⁸ : CommSemiring S
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalSemiring A
inst✝⁵ : Module R A
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
inst✝² : Algebra S R
inst✝¹ : DistribMulAction S A
inst✝ : IsScalarTower S R A
src✝ : S →+* Unitization R A := RingHom.comp (inlRingHom R A) (algebraMap S R)
s : S
r : R
a : A
⊢ s • (inl r + ↑a) = inl (↑(algebraMap S R) s) * (inl r + ↑a)
[PROOFSTEP]
rw [mul_add, smul_add, Algebra.algebraMap_eq_smul_one, inl_mul_inl, inl_mul_inr, smul_one_mul, inl_smul, inr_smul,
  smul_one_smul]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹³ : CommSemiring S
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
B : Type u_4
inst✝⁷ : Semiring B
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra S R
inst✝⁴ : DistribMulAction S A
inst✝³ : IsScalarTower S R A
C : Type u_5
inst✝² : Semiring C
inst✝¹ : Algebra R C
F : Type u_6
inst✝ : AlgHomClass F S (Unitization R A) B
φ ψ : F
h : ∀ (a : A), ↑φ ↑a = ↑ψ ↑a
h' : ∀ (r : R), ↑φ (↑(algebraMap R (Unitization R A)) r) = ↑ψ (↑(algebraMap R (Unitization R A)) r)
⊢ φ = ψ
[PROOFSTEP]
refine FunLike.ext φ ψ (fun x ↦ ?_)
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹³ : CommSemiring S
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
B : Type u_4
inst✝⁷ : Semiring B
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra S R
inst✝⁴ : DistribMulAction S A
inst✝³ : IsScalarTower S R A
C : Type u_5
inst✝² : Semiring C
inst✝¹ : Algebra R C
F : Type u_6
inst✝ : AlgHomClass F S (Unitization R A) B
φ ψ : F
h : ∀ (a : A), ↑φ ↑a = ↑ψ ↑a
h' : ∀ (r : R), ↑φ (↑(algebraMap R (Unitization R A)) r) = ↑ψ (↑(algebraMap R (Unitization R A)) r)
x : Unitization R A
⊢ ↑φ x = ↑ψ x
[PROOFSTEP]
induction x using Unitization.ind
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹³ : CommSemiring S
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
B : Type u_4
inst✝⁷ : Semiring B
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra S R
inst✝⁴ : DistribMulAction S A
inst✝³ : IsScalarTower S R A
C : Type u_5
inst✝² : Semiring C
inst✝¹ : Algebra R C
F : Type u_6
inst✝ : AlgHomClass F S (Unitization R A) B
φ ψ : F
h : ∀ (a : A), ↑φ ↑a = ↑ψ ↑a
h' : ∀ (r : R), ↑φ (↑(algebraMap R (Unitization R A)) r) = ↑ψ (↑(algebraMap R (Unitization R A)) r)
r✝ : R
a✝ : A
⊢ ↑φ (inl r✝ + ↑a✝) = ↑ψ (inl r✝ + ↑a✝)
[PROOFSTEP]
simp only [map_add, ← algebraMap_eq_inl, h, h']
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹³ : CommSemiring S
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : SMulCommClass R A A
inst✝⁸ : IsScalarTower R A A
B : Type u_4
inst✝⁷ : Semiring B
inst✝⁶ : Algebra S B
inst✝⁵ : Algebra S R
inst✝⁴ : DistribMulAction S A
inst✝³ : IsScalarTower S R A
C : Type u_5
inst✝² : Semiring C
inst✝¹ : Algebra R C
F : Type u_6
inst✝ : AlgHomClass F R (Unitization R A) C
φ ψ : F
h : ∀ (a : A), ↑φ ↑a = ↑ψ ↑a
r : R
⊢ ↑φ (↑(algebraMap R (Unitization R A)) r) = ↑ψ (↑(algebraMap R (Unitization R A)) r)
[PROOFSTEP]
simp only [AlgHomClass.commutes]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
⊢ (fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x)) 1 = 1
[PROOFSTEP]
simp only [fst_one, map_one, snd_one, φ.map_zero, add_zero]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x y : Unitization R A
⊢ OneHom.toFun
      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) } y
[PROOFSTEP]
induction' x using Unitization.ind with x_r x_a
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
y : Unitization R A
x_r : R
x_a : A
⊢ OneHom.toFun
      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
      ((inl x_r + ↑x_a) * y) =
    OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
        (inl x_r + ↑x_a) *
      OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) } y
[PROOFSTEP]
induction' y using Unitization.ind with y_r y_a
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ OneHom.toFun
      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
      ((inl x_r + ↑x_a) * (inl y_r + ↑y_a)) =
    OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
        (inl x_r + ↑x_a) *
      OneHom.toFun
        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x), map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
        (inl y_r + ↑y_a)
[PROOFSTEP]
simp only [fst_mul, fst_add, fst_inl, fst_inr, snd_mul, snd_add, snd_inl, snd_inr, add_zero, map_mul, zero_add, map_add,
  map_smul φ]
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ ↑(algebraMap R C) x_r * ↑(algebraMap R C) y_r + (x_r • ↑φ y_a + y_r • ↑φ x_a + ↑φ x_a * ↑φ y_a) =
    (↑(algebraMap R C) x_r + ↑φ x_a) * (↑(algebraMap R C) y_r + ↑φ y_a)
[PROOFSTEP]
rw [add_mul, mul_add, mul_add]
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ ↑(algebraMap R C) x_r * ↑(algebraMap R C) y_r + (x_r • ↑φ y_a + y_r • ↑φ x_a + ↑φ x_a * ↑φ y_a) =
    ↑(algebraMap R C) x_r * ↑(algebraMap R C) y_r + ↑(algebraMap R C) x_r * ↑φ y_a +
      (↑φ x_a * ↑(algebraMap R C) y_r + ↑φ x_a * ↑φ y_a)
[PROOFSTEP]
rw [← Algebra.commutes _ (φ x_a)]
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ ↑(algebraMap R C) x_r * ↑(algebraMap R C) y_r + (x_r • ↑φ y_a + y_r • ↑φ x_a + ↑φ x_a * ↑φ y_a) =
    ↑(algebraMap R C) x_r * ↑(algebraMap R C) y_r + ↑(algebraMap R C) x_r * ↑φ y_a +
      (↑(algebraMap R ((fun x => C) x_a)) y_r * ↑φ x_a + ↑φ x_a * ↑φ y_a)
[PROOFSTEP]
simp only [Algebra.algebraMap_eq_smul_one, smul_one_mul, add_assoc]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Unitization R A),
                OneHom.toFun
                    { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                      map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      y) })
      0 =
    0
[PROOFSTEP]
simp only [fst_zero, map_zero, snd_zero, φ.map_zero, add_zero]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x y : Unitization R A
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Unitization R A),
                OneHom.toFun
                    { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                      map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      y) })
      (x + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        x +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        y
[PROOFSTEP]
induction' x using Unitization.ind with x_r x_a
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
y : Unitization R A
x_r : R
x_a : A
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Unitization R A),
                OneHom.toFun
                    { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                      map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      y) })
      (inl x_r + ↑x_a + y) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        (inl x_r + ↑x_a) +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        y
[PROOFSTEP]
induction' y using Unitization.ind with y_r y_a
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : Unitization R A),
                OneHom.toFun
                    { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                      map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      y) })
      (inl x_r + ↑x_a + (inl y_r + ↑y_a)) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        (inl x_r + ↑x_a) +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                        y) })
        (inl y_r + ↑y_a)
[PROOFSTEP]
simp only [fst_add, fst_inl, fst_inr, add_zero, map_add, snd_add, snd_inl, snd_inr, zero_add, φ.map_add]
[GOAL]
case h.h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x_r : R
x_a : A
y_r : R
y_a : A
⊢ ↑(algebraMap R C) x_r + ↑(algebraMap R C) y_r + (↑φ x_a + ↑φ y_a) =
    ↑(algebraMap R C) x_r + ↑φ x_a + (↑(algebraMap R C) y_r + ↑φ y_a)
[PROOFSTEP]
rw [add_add_add_comm]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
r : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              {
                toOneHom :=
                  { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                    map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : Unitization R A),
                      OneHom.toFun
                          { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                            map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                            y) },
            map_zero' := (_ : ↑(algebraMap R C) 0 + ↑φ 0 = 0),
            map_add' :=
              (_ :
                ∀ (x y : Unitization R A),
                  OneHom.toFun
                      (↑{
                          toOneHom :=
                            { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                              map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (x y : Unitization R A),
                                OneHom.toFun
                                    { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                      map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                    (x * y) =
                                  OneHom.toFun
                                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                      x *
                                    OneHom.toFun
                                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                      y) })
                      (x + y) =
                    OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : Unitization R A),
                                  OneHom.toFun
                                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                      (x * y) =
                                    OneHom.toFun
                                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                        y) })
                        x +
                      OneHom.toFun
                        (↑{
                            toOneHom :=
                              { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (x y : Unitization R A),
                                  OneHom.toFun
                                      { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                        map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                      (x * y) =
                                    OneHom.toFun
                                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                        x *
                                      OneHom.toFun
                                        { toFun := fun x => ↑(algebraMap R C) (fst x) + ↑φ (snd x),
                                          map_one' := (_ : ↑(algebraMap R C) 1 + ↑φ 0 = 1) }
                                        y) })
                        y) })
      (↑(algebraMap R (Unitization R A)) r) =
    ↑(algebraMap R C) r
[PROOFSTEP]
simp only [algebraMap_eq_inl, fst_inl, snd_inl, φ.map_zero, add_zero]
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
⊢ (fun φ => NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)) (NonUnitalAlgHom.toAlgHom φ) = φ
[PROOFSTEP]
ext
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : A →ₙₐ[R] C
x✝ : A
⊢ ↑((fun φ => NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)) (NonUnitalAlgHom.toAlgHom φ)) x✝ = ↑φ x✝
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : Unitization R A →ₐ[R] C
⊢ NonUnitalAlgHom.comp (↑(NonUnitalAlgHom.toAlgHom ((fun φ => NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)) φ)))
      (inrNonUnitalAlgHom R A) =
    NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)
[PROOFSTEP]
ext
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
φ : Unitization R A →ₐ[R] C
x✝ : A
⊢ ↑(NonUnitalAlgHom.comp (↑(NonUnitalAlgHom.toAlgHom ((fun φ => NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)) φ)))
          (inrNonUnitalAlgHom R A))
      x✝ =
    ↑(NonUnitalAlgHom.comp (↑φ) (inrNonUnitalAlgHom R A)) x✝
[PROOFSTEP]
simp
[GOAL]
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
⊢ ↑(NonUnitalAlgHom.toAlgHom 0) = fst
[PROOFSTEP]
ext
[GOAL]
case h
S : Type u_1
R : Type u_2
A : Type u_3
inst✝¹² : CommSemiring S
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : Module R A
inst✝⁸ : SMulCommClass R A A
inst✝⁷ : IsScalarTower R A A
B : Type u_4
inst✝⁶ : Semiring B
inst✝⁵ : Algebra S B
inst✝⁴ : Algebra S R
inst✝³ : DistribMulAction S A
inst✝² : IsScalarTower S R A
C : Type u_5
inst✝¹ : Semiring C
inst✝ : Algebra R C
x✝ : Unitization R A
⊢ ↑(NonUnitalAlgHom.toAlgHom 0) x✝ = fst x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] C
x : Unitization R A
⊢ OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (star x) = star (OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) x)
[PROOFSTEP]
induction x using Unitization.ind
[GOAL]
case h
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] C
r✝ : R
a✝ : A
⊢ OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (star (inl r✝ + ↑a✝)) =
    star (OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (inl r✝ + ↑a✝))
[PROOFSTEP]
simp [map_star]
[GOAL]
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] C
⊢ (fun φ => NonUnitalStarAlgHom.comp (StarAlgHom.toNonUnitalStarAlgHom φ) (inrNonUnitalStarAlgHom R A))
      ((fun φ =>
          { toAlgHom := ↑lift φ.toNonUnitalAlgHom,
            map_star' :=
              (_ :
                ∀ (x : Unitization R A),
                  OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (star x) =
                    star (OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) x)) })
        φ) =
    φ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
φ : A →⋆ₙₐ[R] C
x✝ : A
⊢ ↑((fun φ => NonUnitalStarAlgHom.comp (StarAlgHom.toNonUnitalStarAlgHom φ) (inrNonUnitalStarAlgHom R A))
          ((fun φ =>
              { toAlgHom := ↑lift φ.toNonUnitalAlgHom,
                map_star' :=
                  (_ :
                    ∀ (x : Unitization R A),
                      OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (star x) =
                        star (OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) x)) })
            φ))
      x✝ =
    ↑φ x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
C : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : SMulCommClass R A A
inst✝⁵ : IsScalarTower R A A
inst✝⁴ : StarModule R A
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : StarRing C
inst✝ : StarModule R C
φ : Unitization R A →⋆ₐ[R] C
⊢ ∀ (a : A),
    ↑((fun φ =>
              { toAlgHom := ↑lift φ.toNonUnitalAlgHom,
                map_star' :=
                  (_ :
                    ∀ (x : Unitization R A),
                      OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) (star x) =
                        star (OneHom.toFun (↑↑↑(↑lift φ.toNonUnitalAlgHom)) x)) })
            ((fun φ => NonUnitalStarAlgHom.comp (StarAlgHom.toNonUnitalStarAlgHom φ) (inrNonUnitalStarAlgHom R A)) φ))
        ↑a =
      ↑φ ↑a
[PROOFSTEP]
simp


[GOAL]
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ Projective R P ↔ ∃ s, comp (Finsupp.total P P R id) s = LinearMap.id
[PROOFSTEP]
simp_rw [projective_def, FunLike.ext_iff, Function.LeftInverse, comp_apply, id_apply]
[GOAL]
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
⊢ ∃ h, comp f h = g
[PROOFSTEP]
let φ : (P →₀ R) →ₗ[R] M :=
  Finsupp.total _ _ _ fun p =>
    Function.surjInv hf
      (g p)
        -- By projectivity we have a map `P →ₗ (P →₀ R)`;
[GOAL]
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
⊢ ∃ h, comp f h = g
[PROOFSTEP]
cases' h.out with s hs
[GOAL]
case intro
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
⊢ ∃ h, comp f h = g
[PROOFSTEP]
use φ.comp s
[GOAL]
case h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
⊢ comp f (comp φ s) = g
[PROOFSTEP]
ext p
[GOAL]
case h.h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
p : P
⊢ ↑(comp f (comp φ s)) p = ↑g p
[PROOFSTEP]
conv_rhs => rw [← hs p]
[GOAL]
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
p : P
| ↑g p
[PROOFSTEP]
rw [← hs p]
[GOAL]
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
p : P
| ↑g p
[PROOFSTEP]
rw [← hs p]
[GOAL]
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
p : P
| ↑g p
[PROOFSTEP]
rw [← hs p]
[GOAL]
case h.h
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ↑f
φ : (P →₀ R) →ₗ[R] M := Finsupp.total P M R fun p => Function.surjInv hf (↑g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ↑(Finsupp.total P P R id) ↑s
p : P
⊢ ↑(comp f (comp φ s)) p = ↑g (↑(Finsupp.total P P R id) (↑s p))
[PROOFSTEP]
simp [Finsupp.total_apply, Function.surjInv_eq hf]
[GOAL]
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
⊢ Projective R (P × Q)
[PROOFSTEP]
refine .of_lifting_property'' fun f hf ↦ ?_
[GOAL]
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ↑f
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
rcases projective_lifting_property f (.inl _ _ _) hf with ⟨g₁, hg₁⟩
[GOAL]
case intro
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ↑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : comp f g₁ = inl R P Q
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
rcases projective_lifting_property f (.inr _ _ _) hf with ⟨g₂, hg₂⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ↑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : comp f g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : comp f g₂ = inr R P Q
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
refine ⟨coprod g₁ g₂, ?_⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ↑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : comp f g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : comp f g₂ = inr R P Q
⊢ comp f (coprod g₁ g₂) = LinearMap.id
[PROOFSTEP]
rw [LinearMap.comp_coprod, hg₁, hg₂, LinearMap.coprod_inl_inr]
[GOAL]
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
classical
choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ FunLike.congr_fun (hg i)
refine ⟨DFinsupp.coprodMap g, ?_⟩
ext i x j
simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]
[GOAL]
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
choose g hg using fun i ↦ projective_lifting_property f (DFinsupp.lsingle i) hf
[GOAL]
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι), comp f (g i) = DFinsupp.lsingle i
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
replace hg : ∀ i x, f (g i x) = DFinsupp.single i x := fun i ↦ FunLike.congr_fun (hg i)
[GOAL]
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι) (x : A i), ↑f (↑(g i) x) = DFinsupp.single i x
⊢ ∃ h, comp f h = LinearMap.id
[PROOFSTEP]
refine ⟨DFinsupp.coprodMap g, ?_⟩
[GOAL]
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι) (x : A i), ↑f (↑(g i) x) = DFinsupp.single i x
⊢ comp f (DFinsupp.coprodMap g) = LinearMap.id
[PROOFSTEP]
ext i x j
[GOAL]
case h.h.h
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
ι : Type u_6
A : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : (i : ι) → Module R (A i)
h : ∀ (i : ι), Projective R (A i)
f : ((Π₀ (i : ι), A i) →₀ R) →ₗ[R] Π₀ (i : ι), A i
hf : Function.Surjective ↑f
g : (i : ι) → A i →ₗ[R] (Π₀ (i : ι), A i) →₀ R
hg : ∀ (i : ι) (x : A i), ↑f (↑(g i) x) = DFinsupp.single i x
i : ι
x : A i
j : ι
⊢ ↑(↑(comp (comp f (DFinsupp.coprodMap g)) (DFinsupp.lsingle i)) x) j = ↑(↑(comp LinearMap.id (DFinsupp.lsingle i)) x) j
[PROOFSTEP]
simp only [comp_apply, id_apply, DFinsupp.lsingle_apply, DFinsupp.coprodMap_apply_single, hg]
[GOAL]
R : Type u_1
inst✝² : Ring R
P : Type u_2
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_3
b : Basis ι R P
⊢ Projective R P
[PROOFSTEP]
use b.constr ℕ fun i => Finsupp.single (b i) (1 : R)
[GOAL]
case h
R : Type u_1
inst✝² : Ring R
P : Type u_2
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_3
b : Basis ι R P
⊢ Function.LeftInverse ↑(Finsupp.total P P R id) ↑(↑(Basis.constr b ℕ) fun i => Finsupp.single (↑b i) 1)
[PROOFSTEP]
intro m
[GOAL]
case h
R : Type u_1
inst✝² : Ring R
P : Type u_2
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_3
b : Basis ι R P
m : P
⊢ ↑(Finsupp.total P P R id) (↑(↑(Basis.constr b ℕ) fun i => Finsupp.single (↑b i) 1) m) = m
[PROOFSTEP]
simp only [b.constr_apply, mul_one, id.def, Finsupp.smul_single', Finsupp.total_single, LinearMap.map_finsupp_sum]
[GOAL]
case h
R : Type u_1
inst✝² : Ring R
P : Type u_2
inst✝¹ : AddCommGroup P
inst✝ : Module R P
ι : Type u_3
b : Basis ι R P
m : P
⊢ (sum (↑b.repr m) fun i d => d • ↑b i) = m
[PROOFSTEP]
exact b.total_repr m