∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (toSubalgebra : Subalgebra K L) (inv_mem' : ∀ x ∈ toSubalgebra.carrier, x⁻¹ ∈ toSubalgebra.carrier)
  (toSubalgebra_1 : Subalgebra K L) (inv_mem'_1 : ∀ x ∈ toSubalgebra_1.carrier, x⁻¹ ∈ toSubalgebra_1.carrier),
  ({ toSubalgebra := toSubalgebra, inv_mem' := inv_mem' } =
      { toSubalgebra := toSubalgebra_1, inv_mem' := inv_mem'_1 }) =
    (toSubalgebra = toSubalgebra_1)