case h
F : Type ?u.1020688
R : Type u_1
A : Type u_2
B : Type u_3
C : Type ?u.1020700
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
a✝ : A
⊢ ↑(symm (symm e)) a✝ = ↑e a✝
F : Type ?u.1020688
R : Type u_1
A : Type u_2
B : Type u_3
C : Type ?u.1020700
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
⊢ symm (symm e) = e
ext
no goals
case h
F : Type ?u.1020688
R : Type u_1
A : Type u_2
B : Type u_3
C : Type ?u.1020700
inst✝¹¹ : Add A
inst✝¹⁰ : Add B
inst✝⁹ : Mul A
inst✝⁸ : Mul B
inst✝⁷ : SMul R A
inst✝⁶ : SMul R B
inst✝⁵ : Star A
inst✝⁴ : Star B
inst✝³ : Add C
inst✝² : Mul C
inst✝¹ : SMul R C
inst✝ : Star C
e : A ≃⋆ₐ[R] B
a✝ : A
⊢ ↑(symm (symm e)) a✝ = ↑e a✝
rfl