no goals
l : Type ?u.960961
m : Type ?u.960964
n : Type u_1
o : Type ?u.960970
m' : o → Type ?u.960975
n' : o → Type ?u.960980
R : Type ?u.960983
S : Type ?u.960986
α : Type v
β : Type w
γ : Type ?u.960993
inst✝² : DecidableEq n
inst✝¹ : Semiring α
inst✝ : StarRing α
⊢ 1ᴴ = 1
simp [conjTranspose]