R✝ : Type u
S : Type v
A✝ : Type w
B : Type ?u.159950
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
P Q : Algebra R A
h : toRingHom = toRingHom
⊢ P = Q
R✝ : Type u
S : Type v
A✝ : Type w
B : Type ?u.159950
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
P Q : Algebra R A
h : ∀ (r : R), ↑(algebraMap R A) r = ↑(algebraMap R A) r
⊢ P = Q
replace h : P.toRingHom = Q.toRingHom := FunLike.ext _ _ h
case mk.mk
R✝ : Type u
S : Type v
A✝ : Type w
B : Type ?u.159950
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
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
R✝ : Type u
S : Type v
A✝ : Type w
B : Type ?u.159950
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
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
rcases P with @⟨⟨P⟩⟩
case mk.mk.mk.mk
R✝ : Type u
S : Type v
A✝ : Type w
B : Type ?u.159950
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
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'✝
case mk.mk
R✝ : Type u
S : Type v
A✝ : Type w
B : Type ?u.159950
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
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
rcases Q with @⟨⟨Q⟩⟩
no goals
case mk.mk.mk.mk
R✝ : Type u
S : Type v
A✝ : Type w
B : Type ?u.159950
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
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'✝
congr
case h.h
R✝ : Type u
S : Type v
A✝ : Type w
B : Type ?u.159950
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
P Q : Algebra R A
h : toRingHom = toRingHom
r : R
a : A
⊢ r • a = r • a
R✝ : Type u
S : Type v
A✝ : Type w
B : Type ?u.159950
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
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
funext r a
no goals
case h.h
R✝ : Type u
S : Type v
A✝ : Type w
B : Type ?u.159950
inst✝⁷ : CommSemiring R✝
inst✝⁶ : CommSemiring S
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
inst✝³ : Semiring B
inst✝² : Algebra R✝ B
R : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
P Q : Algebra R A
h : toRingHom = toRingHom
r : R
a : A
⊢ r • a = r • a
rw [P.smul_def', Q.smul_def', h]