case h.a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S✝ S : Subalgebra R A
a✝ : { x // x ∈ S }
⊢ ↑(↑(equivOfEq S S (_ : S = S)) a✝) = ↑(↑AlgEquiv.refl a✝)
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S✝ S : Subalgebra R A
⊢ equivOfEq S S (_ : S = S) = AlgEquiv.refl
ext
no goals
case h.a
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S✝ S : Subalgebra R A
a✝ : { x // x ∈ S }
⊢ ↑(↑(equivOfEq S S (_ : S = S)) a✝) = ↑(↑AlgEquiv.refl a✝)
rfl