[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
